Refine assumptions in testUnlockStEth

runtimeverification · Jul 27, 2024 · f4e2678 · f4e2678
1 parent b6c977d
commit f4e2678
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/test/kontrol/EscrowLockUnlock.t.sol b/test/kontrol/EscrowLockUnlock.t.sol
@@ -162,8 +162,9 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp {
         );
 
         AccountingRecord memory pre = this.saveAccountingRecord(sender, signallingEscrow);
+        vm.assume(0 < pre.userSharesLocked);
         vm.assume(pre.userSharesLocked <= pre.totalSharesLocked);
-        vm.assume(Timestamps.now() >= addTo(config.SIGNALLING_ESCROW_MIN_LOCK_TIME(), pre.userLastLockedTime));
+        vm.assume(Timestamps.now() > addTo(config.SIGNALLING_ESCROW_MIN_LOCK_TIME(), pre.userLastLockedTime));
 
         this.escrowInvariants(Mode.Assume, signallingEscrow);
         this.signallingEscrowInvariants(Mode.Assume, signallingEscrow);