diff --git a/tests/obligations/verification/chalice2silver/christian/lt_call.py b/tests/obligations/verification/chalice2silver/christian/lt_call.py index 91600fb59..f7dfaf482 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: