Adapting test annotation

marcoeilers · Feb 7, 2024 · 348dca1 · 348dca1
1 parent 8ff203a
commit 348dca1
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/tests/obligations/verification/chalice2silver/christian/lt_call.py b/tests/obligations/verification/chalice2silver/christian/lt_call.py
@@ -97,7 +97,7 @@ def timed_release_bounded_nodec(self, other: 'A') -> None:
         Requires(Acc(other.b))
         Requires(MustRelease(other.a, other.b))
 
-        #:: ExpectedOutput(silicon)(call.precondition:assertion.false)|ExpectedOutput(carbon)(call.precondition:insufficient.permission)
+        #:: ExpectedOutput(call.precondition:insufficient.permission)
         self.quick_release(other)
 
     def timed_release_bounded_statdec(self, other: 'A') -> None: