From 48e0ac8c64a8c13581c9d9652d3b23853e7701ff Mon Sep 17 00:00:00 2001
From: Marco Eilers <marcoeilers@users.noreply.github.com>
Date: Sun, 5 May 2024 13:43:41 +0200
Subject: [PATCH] Update test annotations (#791)

---
 .../resources/all/issues/silicon/0832.vpr     | 52 +++++++++++++++++++
 .../resources/wands/new_syntax/QPWands.vpr    |  2 +-
 2 files changed, 53 insertions(+), 1 deletion(-)
 create mode 100644 src/test/resources/all/issues/silicon/0832.vpr

diff --git a/src/test/resources/all/issues/silicon/0832.vpr b/src/test/resources/all/issues/silicon/0832.vpr
new file mode 100644
index 000000000..adb55d01d
--- /dev/null
+++ b/src/test/resources/all/issues/silicon/0832.vpr
@@ -0,0 +1,52 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+method test(x0: Array, x1:Array)
+  requires (forall j: Int :: {arrR(j, x0, 10)} 0 <= j && j < 10 ==> arrR(j, x0, 10))
+  requires arr(x1, 10)
+  requires (forall j: Int :: { aloc(x1, j) }
+    0 <= j && j < 10 ==> (unfolding acc(arr(x1, 10), write/2) in aloc(x1, j).int) == j)
+  requires (forall j: Int :: { aloc(x0, j) }
+    0 <= j && j < 10 ==> (unfolding arrR(j, x0, 10) in aloc(x0, j).int == 3 * j))
+{
+  assert (unfolding arrR(0, x0, 10) in
+            aloc(x0, 0).int == 3 * 0)
+}
+
+predicate arrR(x: Int, a: Array, n: Int) {
+  alen(a) == n && 0 <= x && x < n && acc(aloc(a, x).int, write)
+}
+
+predicate arr(a: Array, n: Int) {
+  alen(a) == n && (forall i: Int :: { aloc(a, i) } 0 <= i && i < alen(a) ==> acc(aloc(a, i).int, write))
+}
+
+field int: Int
+domain Array  {
+
+  function array_loc(a: Array, i: Int): Ref
+  function alen(a: Array): Int
+  function loc_inv_1(loc: Ref): Array
+  function loc_inv_2(loc: Ref): Int
+
+  axiom {
+    (forall a: Array, i: Int ::
+      { array_loc(a, i) }
+      loc_inv_1(array_loc(a, i)) == a && loc_inv_2(array_loc(a, i)) == i)
+  }
+
+  axiom {
+    (forall a: Array :: { alen(a) } alen(a) >= 0)
+  }
+}
+
+function aloc(a: Array, i: Int): Ref
+  requires 0 <= i
+  requires i < alen(a)
+  decreases
+  ensures loc_inv_1(result) == a
+  ensures loc_inv_2(result) == i
+{
+  array_loc(a, i)
+}
\ No newline at end of file
diff --git a/src/test/resources/wands/new_syntax/QPWands.vpr b/src/test/resources/wands/new_syntax/QPWands.vpr
index 1497ac30d..a48a4660d 100644
--- a/src/test/resources/wands/new_syntax/QPWands.vpr
+++ b/src/test/resources/wands/new_syntax/QPWands.vpr
@@ -23,7 +23,7 @@ requires acc(y.f) {
     invariant xs == completed ++ toGo
     invariant forall x: Ref :: x in toGo ==> x.f == old[setupComplete](x.f)
     invariant acc(y.f) && y.f == 1
-    //:: UnexpectedOutput(invariant.not.preserved:assertion.false, /silicon/issue/311/)
+
     invariant forall x: Ref :: x in completed ==>
       applying (acc(y.f) --* acc(x.f) && acc(y.f) && y.f == old[lhs](y.f)) in
       x.f == old[setupComplete](x.f) {