From 0ed3647d0edc738b9716ec79560822088cbd8c51 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Sun, 13 Oct 2024 21:58:46 +0200
Subject: [PATCH] Update test annotation

---
 silver                                         | 2 +-
 src/test/resources/moreCompleteExhale/0523.vpr | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/silver b/silver
index d6d6e65fc..89dce6fde 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit d6d6e65fceb454ee6c6e16c8dcbc50d70b7fd481
+Subproject commit 89dce6fde51d0a9bebf6db83c8968a5778be5a1f
diff --git a/src/test/resources/moreCompleteExhale/0523.vpr b/src/test/resources/moreCompleteExhale/0523.vpr
index 7b0414fb7..13d6e9241 100644
--- 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
 }