From 348dca1d202527ccaea52d4b6baa7670ae25bb32 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 7 Feb 2024 21:46:34 +0100 Subject: [PATCH] Adapting test annotation --- .../verification/chalice2silver/christian/lt_call.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/obligations/verification/chalice2silver/christian/lt_call.py b/tests/obligations/verification/chalice2silver/christian/lt_call.py index 91600fb5..f7dfaf48 100644 --- 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: