Merge branch 'master' into inline

marcoeilers · Dec 1, 2024 · 540c1ee · 540c1ee
2 parents 2140268 + 17047a7
commit 540c1ee
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/tests/io/verification/test_forall_exists.py b/tests/io/verification/test_forall_exists.py
@@ -5,7 +5,8 @@
     Ensures,
     Requires,
     Result,
-    Implies
+    Implies,
+    Assume
 )
 from nagini_contracts.io_contracts import *
 from nagini_contracts.obligations import MustTerminate
@@ -133,7 +134,6 @@ def write_four_ints_4(t1: Place) -> Place:
             write_two_ints_io(t2, t3)
         ),
         Ensures(
-            #:: ExpectedOutput(carbon)(postcondition.violated:insufficient.permission)
             token(t3) and
             t3 == Result()
         ),
@@ -151,6 +151,8 @@ def write_four_ints_4(t1: Place) -> Place:
     #:: ExpectedOutput(call.precondition:insufficient.permission)
     t5 = write_int(t4, 3)
 
+    Assume(False)
+
     return t5