Update test annotation

viperproject · Oct 13, 2024 · 0ed3647 · 0ed3647
1 parent f49fee0
commit 0ed3647
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/silver b/silver
diff --git a/src/test/resources/moreCompleteExhale/0523.vpr b/src/test/resources/moreCompleteExhale/0523.vpr
@@ -9,9 +9,9 @@ function req(x: Ref): Bool
 
 method test(x: Ref) {
   inhale acc(x.f)
-  //:: ExpectedOutput(application.precondition:insufficient.permission)
-  assert req(x) // Fails only without --enableMoreCompleteExhale (and should fail)
-  assert false  // Fails even with --enableMoreCompleteExhale (and should fail)
+  assert req(x)
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert false
 }