From e951a1f778f1254a9ce3920469ddae2a3ce35bb5 Mon Sep 17 00:00:00 2001
From: Manuel Dublanc <19774382+manud99@users.noreply.github.com>
Date: Thu, 2 May 2024 18:04:32 +0200
Subject: [PATCH 01/16] Remove MissingOutput flag from test case
 conditionals2.vpr

---
 src/test/resources/wands/regression/conditionals2.vpr | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/test/resources/wands/regression/conditionals2.vpr b/src/test/resources/wands/regression/conditionals2.vpr
index 9ddd639f5..ddafd4b4b 100644
--- a/src/test/resources/wands/regression/conditionals2.vpr
+++ b/src/test/resources/wands/regression/conditionals2.vpr
@@ -19,7 +19,6 @@ method test5a(x: Ref)
     //                       x.g |-> tg' # tf'' ? w : n
 
   //:: ExpectedOutput(assert.failed:insufficient.permission)
-  //:: MissingOutput(assert.failed:insufficient.permission, /silicon/issue/307/)
   assert acc(x.g, 1/1000)
 }
 

From 2f700d3d5eb143ba15811e1d37afa7c49ff49f25 Mon Sep 17 00:00:00 2001
From: Manuel Dublanc <19774382+manud99@users.noreply.github.com>
Date: Mon, 13 May 2024 11:53:59 +0200
Subject: [PATCH 02/16] Add test suite that I used while developing magic wand
 snap functions.

---
 .../resources/wands/snap_functions/README.md  | 27 ++++++
 .../resources/wands/snap_functions/test01.vpr | 47 ++++++++++
 .../resources/wands/snap_functions/test02.vpr | 47 ++++++++++
 .../resources/wands/snap_functions/test03.vpr | 47 ++++++++++
 .../resources/wands/snap_functions/test04.vpr | 47 ++++++++++
 .../resources/wands/snap_functions/test05.vpr | 47 ++++++++++
 .../resources/wands/snap_functions/test06.vpr | 16 ++++
 .../resources/wands/snap_functions/test07.vpr | 16 ++++
 .../resources/wands/snap_functions/test08.vpr | 29 +++++++
 .../resources/wands/snap_functions/test09.vpr | 26 ++++++
 .../resources/wands/snap_functions/test10.vpr | 30 +++++++
 .../resources/wands/snap_functions/test11.vpr | 87 +++++++++++++++++++
 12 files changed, 466 insertions(+)
 create mode 100644 src/test/resources/wands/snap_functions/README.md
 create mode 100644 src/test/resources/wands/snap_functions/test01.vpr
 create mode 100644 src/test/resources/wands/snap_functions/test02.vpr
 create mode 100644 src/test/resources/wands/snap_functions/test03.vpr
 create mode 100644 src/test/resources/wands/snap_functions/test04.vpr
 create mode 100644 src/test/resources/wands/snap_functions/test05.vpr
 create mode 100644 src/test/resources/wands/snap_functions/test06.vpr
 create mode 100644 src/test/resources/wands/snap_functions/test07.vpr
 create mode 100644 src/test/resources/wands/snap_functions/test08.vpr
 create mode 100644 src/test/resources/wands/snap_functions/test09.vpr
 create mode 100644 src/test/resources/wands/snap_functions/test10.vpr
 create mode 100644 src/test/resources/wands/snap_functions/test11.vpr

diff --git a/src/test/resources/wands/snap_functions/README.md b/src/test/resources/wands/snap_functions/README.md
new file mode 100644
index 000000000..a3305229c
--- /dev/null
+++ b/src/test/resources/wands/snap_functions/README.md
@@ -0,0 +1,27 @@
+# Test Suite for Magic Wand Snap Functions
+
+This folder contains Viper test files that I used when working on MagicWandSnapFunctions for the Silicon project.
+
+## Overview
+
+| Name                       | Description                                                                                     | Expected Result |
+|----------------------------|-------------------------------------------------------------------------------------------------|-----------------|
+| [test01.vpr](./test01.vpr) | Boolean Magic Wand with trivial LHS                                                             | ✓               |
+| [test02.vpr](./test02.vpr) | Integer Magic Wand with trivial LHS                                                             | ✓               |
+| [test03.vpr](./test03.vpr) | Integer Magic Wand with LHS = RHS                                                               | ✓               |
+| [test04.vpr](./test04.vpr) | Integer Magic Wand with LHS < RHS                                                               | ✓               |
+| [test05.vpr](./test05.vpr) | Integer Magic Wand with LHS > RHS                                                               | ✓               |
+| [test06.vpr](./test06.vpr) | Applying the magic wand multiple times. Original version leaks information into the outer state | ×               |
+| [test07.vpr](./test07.vpr) | Assigning result of applying expression to the same field using booleans                        | ×               |
+| [test08.vpr](./test08.vpr) | Assigning result of applying expression to the same field using integers                        | ×               |
+| [test09.vpr](./test09.vpr) | Inhaling a magic wand                                                                           | ✓               |
+| [test10.vpr](./test10.vpr) | Magic wand with predicates                                                                      | ✓               |
+| [test11.vpr](./test11.vpr) | Iterate over a List                                                                             | ✓               |
+
+Other interesting test cases in the [Silver repository](https://github.com/viperproject/silver/tree/master/src/test/resources) during the development of `MagicWandSnapFunctions` were:
+* [wands/examples_paper/conditionals.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/examples_paper/conditionals.vpr)
+* [wands/new_syntax/QPFields.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/new_syntax/QPFields.vpr)
+* [wands/new_syntax/SnapshotsNestedMagicWands.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/new_syntax/SnapshotsNestedMagicWands.vpr)
+* [wands/regression/conditionals2.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/regression/conditionals2.vpr)
+* [wands/regression/issue024.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/regression/issue024.vpr)
+* [wands/regression/issue029.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/regression/issue029.vpr)
diff --git a/src/test/resources/wands/snap_functions/test01.vpr b/src/test/resources/wands/snap_functions/test01.vpr
new file mode 100644
index 000000000..5aba1313c
--- /dev/null
+++ b/src/test/resources/wands/snap_functions/test01.vpr
@@ -0,0 +1,47 @@
+field b: Bool
+
+method test01a(x: Ref)
+{
+    inhale acc(x.b) && x.b
+
+    package true --* acc(x.b)
+
+    assert applying (true --* acc(x.b)) in x.b
+}
+
+method test01b(x: Ref)
+{
+    inhale acc(x.b) && x.b
+
+    package true --* acc(x.b)
+
+    apply true --* acc(x.b)
+
+    assert x.b
+}
+
+method test01c(x: Ref)
+{
+    inhale acc(x.b) && x.b
+
+    package true --* acc(x.b)
+
+    assert applying (true --* acc(x.b)) in x.b
+
+    apply true --* acc(x.b)
+
+    assert x.b
+}
+
+method test01d(x: Ref, a: Bool)
+{
+    inhale acc(x.b) && x.b == a
+
+    package true --* acc(x.b)
+
+    assert applying (true --* acc(x.b)) in x.b == a
+
+    apply true --* acc(x.b)
+
+    assert x.b == a
+}
\ No newline at end of file
diff --git a/src/test/resources/wands/snap_functions/test02.vpr b/src/test/resources/wands/snap_functions/test02.vpr
new file mode 100644
index 000000000..7c9e6d792
--- /dev/null
+++ b/src/test/resources/wands/snap_functions/test02.vpr
@@ -0,0 +1,47 @@
+field f: Int
+
+method test02a(x: Ref)
+{
+    inhale acc(x.f) && x.f == 42
+
+    package true --* acc(x.f)
+
+    assert applying (true --* acc(x.f)) in x.f == 42
+}
+
+method test02b(x: Ref)
+{
+    inhale acc(x.f) && x.f == 42
+
+    package true --* acc(x.f)
+
+    apply true --* acc(x.f)
+
+    assert x.f == 42
+}
+
+method test02c(x: Ref)
+{
+    inhale acc(x.f) && x.f == 42
+
+    package true --* acc(x.f)
+
+    assert applying (true --* acc(x.f)) in x.f == 42
+
+    apply true --* acc(x.f)
+
+    assert x.f == 42
+}
+
+method test02d(x: Ref, a: Int)
+{
+    inhale acc(x.f) && x.f == a
+
+    package true --* acc(x.f)
+
+    assert applying (true --* acc(x.f)) in x.f == a
+
+    apply true --* acc(x.f)
+
+    assert x.f == a
+}
\ No newline at end of file
diff --git a/src/test/resources/wands/snap_functions/test03.vpr b/src/test/resources/wands/snap_functions/test03.vpr
new file mode 100644
index 000000000..e673a5984
--- /dev/null
+++ b/src/test/resources/wands/snap_functions/test03.vpr
@@ -0,0 +1,47 @@
+field f: Int
+
+method test03a(x: Ref)
+{
+    inhale acc(x.f) && x.f == 42
+
+    package acc(x.f) --* acc(x.f)
+
+    assert applying (acc(x.f) --* acc(x.f)) in x.f == 42
+}
+
+method test03b(x: Ref)
+{
+    inhale acc(x.f) && x.f == 42
+
+    package acc(x.f) --* acc(x.f)
+
+    apply acc(x.f) --* acc(x.f)
+
+    assert x.f == 42
+}
+
+method test03c(x: Ref)
+{
+    inhale acc(x.f) && x.f == 42
+
+    package acc(x.f) --* acc(x.f)
+
+    assert applying (acc(x.f) --* acc(x.f)) in x.f == 42
+
+    apply acc(x.f) --* acc(x.f)
+
+    assert x.f == 42
+}
+
+method test03d(x: Ref, a: Int)
+{
+    inhale acc(x.f) && x.f == a
+
+    package acc(x.f) --* acc(x.f)
+
+    assert applying (acc(x.f) --* acc(x.f)) in x.f == a
+
+    apply acc(x.f) --* acc(x.f)
+
+    assert x.f == a
+}
\ No newline at end of file
diff --git a/src/test/resources/wands/snap_functions/test04.vpr b/src/test/resources/wands/snap_functions/test04.vpr
new file mode 100644
index 000000000..91cc63212
--- /dev/null
+++ b/src/test/resources/wands/snap_functions/test04.vpr
@@ -0,0 +1,47 @@
+field f: Int
+
+method test04a(x: Ref, y: Ref)
+{
+    inhale acc(x.f) && x.f == 42 && acc(y.f) && y.f == 37
+
+    package acc(x.f) --* acc(x.f) && acc(y.f)
+
+    assert applying (acc(x.f) --* acc(x.f) && acc(y.f)) in x.f == 42 && y.f == 37
+}
+
+method test04b(x: Ref, y: Ref)
+{
+    inhale acc(x.f) && x.f == 42 && acc(y.f) && y.f == 37
+
+    package acc(x.f) --* acc(x.f) && acc(y.f)
+
+    apply acc(x.f) --* acc(x.f) && acc(y.f)
+
+    assert x.f == 42 && y.f == 37
+}
+
+method test04c(x: Ref, y: Ref)
+{
+    inhale acc(x.f) && x.f == 42 && acc(y.f) && y.f == 37
+
+    package acc(x.f) --* acc(x.f) && acc(y.f)
+
+    assert applying (acc(x.f) --* acc(x.f) && acc(y.f)) in x.f == 42 && y.f == 37
+
+    apply acc(x.f) --* acc(x.f) && acc(y.f)
+
+    assert x.f == 42 && y.f == 37
+}
+
+method test04d(x: Ref, y: Ref, a: Int, b: Int)
+{
+    inhale acc(x.f) && x.f == a && acc(y.f) && y.f == b
+
+    package acc(x.f) --* acc(x.f) && acc(y.f)
+
+    assert applying (acc(x.f) --* acc(x.f) && acc(y.f)) in x.f == a && y.f == b
+
+    apply acc(x.f) --* acc(x.f) && acc(y.f)
+
+    assert x.f == a && y.f == b
+}
\ No newline at end of file
diff --git a/src/test/resources/wands/snap_functions/test05.vpr b/src/test/resources/wands/snap_functions/test05.vpr
new file mode 100644
index 000000000..3ce73962d
--- /dev/null
+++ b/src/test/resources/wands/snap_functions/test05.vpr
@@ -0,0 +1,47 @@
+field f: Int
+
+method test05a(x: Ref, y: Ref)
+{
+    inhale acc(x.f) && x.f == 42 && acc(y.f) && y.f == 37
+
+    package acc(x.f) && acc(y.f) --* acc(x.f)
+
+    assert (applying (acc(x.f) && acc(y.f) --* acc(x.f)) in x.f == 42) && y.f == 37
+}
+
+method test05b(x: Ref, y: Ref)
+{
+    inhale acc(x.f) && x.f == 42 && acc(y.f) && y.f == 37
+
+    package acc(x.f) && acc(y.f) --* acc(x.f)
+
+    apply acc(x.f) && acc(y.f) --* acc(x.f)
+
+    assert x.f == 42 && acc(y.f, none)
+}
+
+method test05c(x: Ref, y: Ref)
+{
+    inhale acc(x.f) && x.f == 42 && acc(y.f) && y.f == 37
+
+    package acc(x.f) && acc(y.f) --* acc(x.f)
+
+    assert (applying (acc(x.f) && acc(y.f) --* acc(x.f)) in x.f == 42) && y.f == 37
+
+    apply acc(x.f) && acc(y.f) --* acc(x.f)
+
+    assert x.f == 42 && acc(y.f, none)
+}
+
+method test05d(x: Ref, y: Ref, a: Int, b: Int)
+{
+    inhale acc(x.f) && x.f == a && acc(y.f) && y.f == b
+
+    package acc(x.f) && acc(y.f) --* acc(x.f)
+
+    assert (applying (acc(x.f) && acc(y.f) --* acc(x.f)) in x.f == a) && y.f == b
+
+    apply acc(x.f) && acc(y.f) --* acc(x.f)
+
+    assert x.f == a && acc(y.f, none)
+}
\ No newline at end of file
diff --git a/src/test/resources/wands/snap_functions/test06.vpr b/src/test/resources/wands/snap_functions/test06.vpr
new file mode 100644
index 000000000..2b666f1d6
--- /dev/null
+++ b/src/test/resources/wands/snap_functions/test06.vpr
@@ -0,0 +1,16 @@
+field b: Bool
+
+method test06(x: Ref) {
+    inhale acc(x.b)
+
+    package acc(x.b) --* true
+
+    x.b := true
+    assert applying (acc(x.b) --* true) in true
+
+    x.b := false
+    assert applying (acc(x.b) --* true) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
diff --git a/src/test/resources/wands/snap_functions/test07.vpr b/src/test/resources/wands/snap_functions/test07.vpr
new file mode 100644
index 000000000..f5c07ae7d
--- /dev/null
+++ b/src/test/resources/wands/snap_functions/test07.vpr
@@ -0,0 +1,16 @@
+field b: Bool
+
+method test07a(x: Ref)
+    requires acc(x.b)
+{
+    package acc(x.b) --* acc(x.b)
+
+    x.b := applying (acc(x.b) --* acc(x.b)) in !x.b
+
+    apply acc(x.b) --* acc(x.b)
+
+    assert acc(x.b) && x.b != old(x.b)
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
diff --git a/src/test/resources/wands/snap_functions/test08.vpr b/src/test/resources/wands/snap_functions/test08.vpr
new file mode 100644
index 000000000..7a9185b0f
--- /dev/null
+++ b/src/test/resources/wands/snap_functions/test08.vpr
@@ -0,0 +1,29 @@
+field f: Int
+
+method test08a(x: Ref)
+    requires acc(x.f)
+{
+    package acc(x.f) --* acc(x.f)
+
+    x.f := applying (acc(x.f) --* acc(x.f)) in x.f + 1
+
+    apply acc(x.f) --* acc(x.f)
+
+    assert acc(x.f) && x.f == old(x.f) + 1
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
+
+method test08b(x: Ref)
+    requires acc(x.f) && x.f == 42
+{
+    package acc(x.f) --* acc(x.f)
+
+    x.f := applying (acc(x.f) --* acc(x.f)) in x.f + 1
+
+    apply acc(x.f) --* acc(x.f)
+
+    assert acc(x.f) && x.f == 43
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
diff --git a/src/test/resources/wands/snap_functions/test09.vpr b/src/test/resources/wands/snap_functions/test09.vpr
new file mode 100644
index 000000000..04698b8a4
--- /dev/null
+++ b/src/test/resources/wands/snap_functions/test09.vpr
@@ -0,0 +1,26 @@
+field f: Int
+
+method test09a(x: Ref, y: Ref)
+    requires acc(x.f) && x.f == 42
+    requires acc(x.f) --* acc(x.f) && acc(y.f) && y.f == 37
+{
+    assert applying (acc(x.f) --* acc(x.f) && acc(y.f) && y.f == 37) in y.f == 37
+}
+
+method test09b(x: Ref, y: Ref)
+    requires acc(x.f) && x.f == 42
+    requires acc(x.f) --* acc(x.f) && acc(y.f) && y.f == 37
+{
+    apply acc(x.f) --* acc(x.f) && acc(y.f) && y.f == 37
+
+    assert y.f == 37
+}
+
+method test09c(x: Ref, y: Ref, z: Ref)
+    requires acc(x.f) && x.f == 42
+    requires acc(x.f) --* acc(x.f) && acc(y.f) && acc(z.f) && y.f == 37
+{
+    apply acc(x.f) --* acc(x.f) && acc(y.f) && acc(z.f) && y.f == 37
+
+    assert y.f == 37
+}
diff --git a/src/test/resources/wands/snap_functions/test10.vpr b/src/test/resources/wands/snap_functions/test10.vpr
new file mode 100644
index 000000000..843193945
--- /dev/null
+++ b/src/test/resources/wands/snap_functions/test10.vpr
@@ -0,0 +1,30 @@
+field f: Int
+field g: Int
+
+predicate foo(x: Ref) {
+    acc(x.f)
+}
+
+method test10a(x: Ref)
+{
+    inhale foo(x) && unfolding foo(x) in x.f == 42
+
+    package foo(x) --* foo(x)
+
+    apply foo(x) --* foo(x)
+
+    assert foo(x) && unfolding foo(x) in x.f == 42
+}
+
+method test10b(x: Ref)
+{
+    inhale acc(x.f) && x.f == 42
+
+    package acc(x.f) --* foo(x) {
+        fold foo(x)
+    }
+
+    apply acc(x.f) --* foo(x)
+
+    assert foo(x) && unfolding foo(x) in x.f == 42
+}
diff --git a/src/test/resources/wands/snap_functions/test11.vpr b/src/test/resources/wands/snap_functions/test11.vpr
new file mode 100644
index 000000000..8fa3f95e2
--- /dev/null
+++ b/src/test/resources/wands/snap_functions/test11.vpr
@@ -0,0 +1,87 @@
+field next : Ref
+field val : Int
+
+predicate List(start : Ref)
+{
+  acc(start.val) && acc(start.next) && (start.next != null ==> List(start.next))
+}
+
+function elems(start: Ref) : Seq[Int]
+  requires List(start)
+{
+  unfolding List(start) in (
+    (start.next == null ? Seq(start.val) : Seq(start.val) ++ elems(start.next) )
+  )
+}
+
+function sorted(start: Ref) : Bool
+  requires List(start)
+{
+  unfolding List(start) in
+    start.next == null
+      ? true
+      : (unfolding List(start.next) in start.val <= start.next.val)
+          && sorted(start.next)
+}
+
+method append_it(l1 : Ref, l2: Ref)
+  requires List(l1) && List(l2) && l2 != null
+  ensures List(l1) && elems(l1) == old(elems(l1) ++ elems(l2))
+{
+  unfold List(l1)
+
+  if (l1.next == null) {
+    l1.next := l2
+    fold List(l1)
+
+  } else {
+    var tmp : Ref := l1.next
+    var index : Int := 1
+
+    package List(tmp) --* List(l1) && elems(l1) == old(elems(l1)[..index]) ++ old[lhs](elems(tmp))
+    {
+      fold List(l1)
+    }
+
+    while (unfolding List(tmp) in tmp.next != null)
+      invariant index >= 0
+      invariant List(tmp) && elems(tmp) == old(elems(l1))[index..]
+
+      invariant List(tmp) --* List(l1) && elems(l1) == old(elems(l1)[..index]) ++ old[lhs](elems(tmp))
+    {
+      unfold List(tmp)
+      var prev : Ref := tmp
+      tmp := tmp.next
+      index := index + 1
+
+      package List(tmp) --* List(l1) && elems(l1) == old(elems(l1)[..index]) ++ old[lhs](elems(tmp))
+      {
+        fold List(prev)
+
+        apply List(prev) --* List(l1) && elems(l1) == old(elems(l1)[..index-1]) ++ old[lhs](elems(prev))
+      }
+    }
+
+    unfold List(tmp)
+    tmp.next := l2
+    fold List(tmp)
+
+    apply List(tmp) --* List(l1) && elems(l1) == old(elems(l1)[..index]) ++ old[lhs](elems(tmp))
+  }
+}
+
+method traverse_sorted(l: Ref)
+  requires List(l) && sorted(l)
+  ensures List(l) && sorted(l) && (unfolding List(l) in l.val) == old(unfolding List(l) in l.val)
+{
+  unfold List(l)
+
+  if (l == null) {
+    fold List(l)
+  } elseif (l.next == null) {
+    fold List(l)
+  } else {
+    traverse_sorted(l.next)
+    fold List(l)
+  }
+}

From 637470913ed4c98e4e35e60739f42905e057b2bd Mon Sep 17 00:00:00 2001
From: Manuel Dublanc <19774382+manud99@users.noreply.github.com>
Date: Mon, 13 May 2024 14:00:32 +0200
Subject: [PATCH 03/16] Add UnexpectedOutput annotations for Carbon.

---
 src/test/resources/wands/snap_functions/test01.vpr | 3 +++
 src/test/resources/wands/snap_functions/test02.vpr | 3 +++
 src/test/resources/wands/snap_functions/test04.vpr | 3 +++
 src/test/resources/wands/snap_functions/test09.vpr | 1 +
 src/test/resources/wands/snap_functions/test10.vpr | 1 +
 src/test/resources/wands/snap_functions/test11.vpr | 2 ++
 6 files changed, 13 insertions(+)

diff --git a/src/test/resources/wands/snap_functions/test01.vpr b/src/test/resources/wands/snap_functions/test01.vpr
index 5aba1313c..5ede73fad 100644
--- a/src/test/resources/wands/snap_functions/test01.vpr
+++ b/src/test/resources/wands/snap_functions/test01.vpr
@@ -6,6 +6,7 @@ method test01a(x: Ref)
 
     package true --* acc(x.b)
 
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
     assert applying (true --* acc(x.b)) in x.b
 }
 
@@ -26,6 +27,7 @@ method test01c(x: Ref)
 
     package true --* acc(x.b)
 
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
     assert applying (true --* acc(x.b)) in x.b
 
     apply true --* acc(x.b)
@@ -39,6 +41,7 @@ method test01d(x: Ref, a: Bool)
 
     package true --* acc(x.b)
 
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
     assert applying (true --* acc(x.b)) in x.b == a
 
     apply true --* acc(x.b)
diff --git a/src/test/resources/wands/snap_functions/test02.vpr b/src/test/resources/wands/snap_functions/test02.vpr
index 7c9e6d792..789669d7a 100644
--- a/src/test/resources/wands/snap_functions/test02.vpr
+++ b/src/test/resources/wands/snap_functions/test02.vpr
@@ -6,6 +6,7 @@ method test02a(x: Ref)
 
     package true --* acc(x.f)
 
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
     assert applying (true --* acc(x.f)) in x.f == 42
 }
 
@@ -26,6 +27,7 @@ method test02c(x: Ref)
 
     package true --* acc(x.f)
 
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
     assert applying (true --* acc(x.f)) in x.f == 42
 
     apply true --* acc(x.f)
@@ -39,6 +41,7 @@ method test02d(x: Ref, a: Int)
 
     package true --* acc(x.f)
 
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
     assert applying (true --* acc(x.f)) in x.f == a
 
     apply true --* acc(x.f)
diff --git a/src/test/resources/wands/snap_functions/test04.vpr b/src/test/resources/wands/snap_functions/test04.vpr
index 91cc63212..7c80ab883 100644
--- a/src/test/resources/wands/snap_functions/test04.vpr
+++ b/src/test/resources/wands/snap_functions/test04.vpr
@@ -6,6 +6,7 @@ method test04a(x: Ref, y: Ref)
 
     package acc(x.f) --* acc(x.f) && acc(y.f)
 
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
     assert applying (acc(x.f) --* acc(x.f) && acc(y.f)) in x.f == 42 && y.f == 37
 }
 
@@ -26,6 +27,7 @@ method test04c(x: Ref, y: Ref)
 
     package acc(x.f) --* acc(x.f) && acc(y.f)
 
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
     assert applying (acc(x.f) --* acc(x.f) && acc(y.f)) in x.f == 42 && y.f == 37
 
     apply acc(x.f) --* acc(x.f) && acc(y.f)
@@ -39,6 +41,7 @@ method test04d(x: Ref, y: Ref, a: Int, b: Int)
 
     package acc(x.f) --* acc(x.f) && acc(y.f)
 
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
     assert applying (acc(x.f) --* acc(x.f) && acc(y.f)) in x.f == a && y.f == b
 
     apply acc(x.f) --* acc(x.f) && acc(y.f)
diff --git a/src/test/resources/wands/snap_functions/test09.vpr b/src/test/resources/wands/snap_functions/test09.vpr
index 04698b8a4..081fbdbdd 100644
--- a/src/test/resources/wands/snap_functions/test09.vpr
+++ b/src/test/resources/wands/snap_functions/test09.vpr
@@ -4,6 +4,7 @@ method test09a(x: Ref, y: Ref)
     requires acc(x.f) && x.f == 42
     requires acc(x.f) --* acc(x.f) && acc(y.f) && y.f == 37
 {
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
     assert applying (acc(x.f) --* acc(x.f) && acc(y.f) && y.f == 37) in y.f == 37
 }
 
diff --git a/src/test/resources/wands/snap_functions/test10.vpr b/src/test/resources/wands/snap_functions/test10.vpr
index 843193945..7e01925a1 100644
--- a/src/test/resources/wands/snap_functions/test10.vpr
+++ b/src/test/resources/wands/snap_functions/test10.vpr
@@ -26,5 +26,6 @@ method test10b(x: Ref)
 
     apply acc(x.f) --* foo(x)
 
+    //:: UnexpectedOutput(assert.failed:assertion.false, /Carbon/issue/216/)
     assert foo(x) && unfolding foo(x) in x.f == 42
 }
diff --git a/src/test/resources/wands/snap_functions/test11.vpr b/src/test/resources/wands/snap_functions/test11.vpr
index 8fa3f95e2..3e5751e7e 100644
--- a/src/test/resources/wands/snap_functions/test11.vpr
+++ b/src/test/resources/wands/snap_functions/test11.vpr
@@ -26,6 +26,7 @@ function sorted(start: Ref) : Bool
 
 method append_it(l1 : Ref, l2: Ref)
   requires List(l1) && List(l2) && l2 != null
+  //:: UnexpectedOutput(assert.failed:assertion.false, /Carbon/issue/000/)
   ensures List(l1) && elems(l1) == old(elems(l1) ++ elems(l2))
 {
   unfold List(l1)
@@ -54,6 +55,7 @@ method append_it(l1 : Ref, l2: Ref)
       tmp := tmp.next
       index := index + 1
 
+      //:: UnexpectedOutput(assert.failed:assertion.false, /Carbon/issue/000/)
       package List(tmp) --* List(l1) && elems(l1) == old(elems(l1)[..index]) ++ old[lhs](elems(tmp))
       {
         fold List(prev)

From e0c11acdefdbbd9dd4abac445dfe041f2033d7c4 Mon Sep 17 00:00:00 2001
From: Manuel Dublanc <19774382+manud99@users.noreply.github.com>
Date: Mon, 13 May 2024 14:54:55 +0200
Subject: [PATCH 04/16] Add unsound example illustrating issue
 viperproject/silicon#307.

---
 .../resources/wands/snap_functions/README.md  |  1 +
 .../resources/wands/snap_functions/test12.vpr | 70 +++++++++++++++++++
 2 files changed, 71 insertions(+)
 create mode 100644 src/test/resources/wands/snap_functions/test12.vpr

diff --git a/src/test/resources/wands/snap_functions/README.md b/src/test/resources/wands/snap_functions/README.md
index a3305229c..d9ac96798 100644
--- a/src/test/resources/wands/snap_functions/README.md
+++ b/src/test/resources/wands/snap_functions/README.md
@@ -17,6 +17,7 @@ This folder contains Viper test files that I used when working on MagicWandSnapF
 | [test09.vpr](./test09.vpr) | Inhaling a magic wand                                                                           | ✓               |
 | [test10.vpr](./test10.vpr) | Magic wand with predicates                                                                      | ✓               |
 | [test11.vpr](./test11.vpr) | Iterate over a List                                                                             | ✓               |
+| [test12.vpr](./test12.vpr) | Applying a quantified magic wand multiple times. Original version verifies this unsoundly       | ✓               |
 
 Other interesting test cases in the [Silver repository](https://github.com/viperproject/silver/tree/master/src/test/resources) during the development of `MagicWandSnapFunctions` were:
 * [wands/examples_paper/conditionals.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/examples_paper/conditionals.vpr)
diff --git a/src/test/resources/wands/snap_functions/test12.vpr b/src/test/resources/wands/snap_functions/test12.vpr
new file mode 100644
index 000000000..01add1335
--- /dev/null
+++ b/src/test/resources/wands/snap_functions/test12.vpr
@@ -0,0 +1,70 @@
+// Test cases showing unsound behaviour of current Viper
+// Related to wands/new_syntax/QPWands.vpr
+
+field f: Int
+
+method test12a(xs: Seq[Ref], y: Ref)
+    requires forall x: Ref :: x in xs ==> acc(x.f)
+    requires |xs| >= 1
+    requires acc(y.f)
+{
+    xs[0].f := 0
+    var some: Ref := xs[0]
+
+    package acc(some.f) --* true
+
+    var completed: Seq[Ref] := Seq(some)
+    assert forall x: Ref :: x in completed ==> acc(x.f) --* true
+
+    some.f := 1
+    assert applying (acc(some.f) --* true) in true
+
+    some.f := 2
+    assert applying (acc(some.f) --* true) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    //:: MissingOutput(assert.failed:assertion.false, /Silicon/issue/307/)
+    assert false
+}
+
+method test12b(xs: Seq[Ref], y: Ref)
+    requires forall x: Ref :: x in xs ==> acc(x.f)
+    requires |xs| >= 1
+    requires acc(y.f)
+{
+    xs[0].f := 0
+    var some: Ref := xs[0]
+
+    package acc(some.f) --* acc(some.f)
+
+    var completed: Seq[Ref] := Seq(some)
+    assert forall x: Ref :: x in completed ==> acc(x.f) --* acc(x.f)
+
+    some.f := applying (acc(some.f) --* acc(some.f)) in some.f + 1
+    apply acc(some.f) --* acc(some.f)
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    //:: MissingOutput(assert.failed:assertion.false, /Silicon/issue/307/)
+    assert false
+}
+
+method test12c(xs: Seq[Ref], y: Ref)
+    requires forall x: Ref :: x in xs ==> acc(x.f)
+    requires |xs| >= 1
+    requires acc(y.f)
+{
+    xs[0].f := 0
+    var some: Ref := xs[0]
+
+    package acc(some.f) --* acc(some.f)
+
+    var completed: Seq[Ref] := Seq(some)
+    assert forall x: Ref :: x in completed ==> acc(x.f) --* acc(x.f)
+
+    some.f := applying (acc(some.f) --* acc(some.f)) in some.f + 1
+    some.f := applying (acc(some.f) --* acc(some.f)) in some.f + 1
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    //:: MissingOutput(assert.failed:assertion.false, /Silicon/issue/307/)
+    assert false
+}

From fe2e291bd1e738c76623f1917a74e976cb7284aa Mon Sep 17 00:00:00 2001
From: Manuel Dublanc <19774382+manud99@users.noreply.github.com>
Date: Sun, 19 May 2024 12:36:16 +0200
Subject: [PATCH 05/16] [WIP] Use MWSF for quantified magic wands.

---
 src/test/resources/wands/snap_functions/test12.vpr | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/test/resources/wands/snap_functions/test12.vpr b/src/test/resources/wands/snap_functions/test12.vpr
index 01add1335..1d90c212c 100644
--- a/src/test/resources/wands/snap_functions/test12.vpr
+++ b/src/test/resources/wands/snap_functions/test12.vpr
@@ -23,7 +23,6 @@ method test12a(xs: Seq[Ref], y: Ref)
     assert applying (acc(some.f) --* true) in true
 
     //:: ExpectedOutput(assert.failed:assertion.false)
-    //:: MissingOutput(assert.failed:assertion.false, /Silicon/issue/307/)
     assert false
 }
 
@@ -44,7 +43,6 @@ method test12b(xs: Seq[Ref], y: Ref)
     apply acc(some.f) --* acc(some.f)
 
     //:: ExpectedOutput(assert.failed:assertion.false)
-    //:: MissingOutput(assert.failed:assertion.false, /Silicon/issue/307/)
     assert false
 }
 
@@ -65,6 +63,5 @@ method test12c(xs: Seq[Ref], y: Ref)
     some.f := applying (acc(some.f) --* acc(some.f)) in some.f + 1
 
     //:: ExpectedOutput(assert.failed:assertion.false)
-    //:: MissingOutput(assert.failed:assertion.false, /Silicon/issue/307/)
     assert false
 }

From e040eb86d810921ab56ba9355eaec1a32fd70dfd Mon Sep 17 00:00:00 2001
From: Manuel Dublanc <19774382+manud99@users.noreply.github.com>
Date: Sun, 2 Jun 2024 15:18:24 +0200
Subject: [PATCH 06/16] Find even more unsound test cases.

---
 .../resources/wands/snap_functions/README.md  | 29 ++++---
 .../resources/wands/snap_functions/test13.vpr | 87 +++++++++++++++++++
 2 files changed, 102 insertions(+), 14 deletions(-)
 create mode 100644 src/test/resources/wands/snap_functions/test13.vpr

diff --git a/src/test/resources/wands/snap_functions/README.md b/src/test/resources/wands/snap_functions/README.md
index d9ac96798..99fa72349 100644
--- a/src/test/resources/wands/snap_functions/README.md
+++ b/src/test/resources/wands/snap_functions/README.md
@@ -4,20 +4,21 @@ This folder contains Viper test files that I used when working on MagicWandSnapF
 
 ## Overview
 
-| Name                       | Description                                                                                     | Expected Result |
-|----------------------------|-------------------------------------------------------------------------------------------------|-----------------|
-| [test01.vpr](./test01.vpr) | Boolean Magic Wand with trivial LHS                                                             | ✓               |
-| [test02.vpr](./test02.vpr) | Integer Magic Wand with trivial LHS                                                             | ✓               |
-| [test03.vpr](./test03.vpr) | Integer Magic Wand with LHS = RHS                                                               | ✓               |
-| [test04.vpr](./test04.vpr) | Integer Magic Wand with LHS < RHS                                                               | ✓               |
-| [test05.vpr](./test05.vpr) | Integer Magic Wand with LHS > RHS                                                               | ✓               |
-| [test06.vpr](./test06.vpr) | Applying the magic wand multiple times. Original version leaks information into the outer state | ×               |
-| [test07.vpr](./test07.vpr) | Assigning result of applying expression to the same field using booleans                        | ×               |
-| [test08.vpr](./test08.vpr) | Assigning result of applying expression to the same field using integers                        | ×               |
-| [test09.vpr](./test09.vpr) | Inhaling a magic wand                                                                           | ✓               |
-| [test10.vpr](./test10.vpr) | Magic wand with predicates                                                                      | ✓               |
-| [test11.vpr](./test11.vpr) | Iterate over a List                                                                             | ✓               |
-| [test12.vpr](./test12.vpr) | Applying a quantified magic wand multiple times. Original version verifies this unsoundly       | ✓               |
+| Name                       | Description                                                                                     | Expected Result  |
+|----------------------------|-------------------------------------------------------------------------------------------------|------------------|
+| [test01.vpr](./test01.vpr) | Boolean Magic Wand with trivial LHS                                                             | ✓                |
+| [test02.vpr](./test02.vpr) | Integer Magic Wand with trivial LHS                                                             | ✓                |
+| [test03.vpr](./test03.vpr) | Integer Magic Wand with LHS = RHS                                                               | ✓                |
+| [test04.vpr](./test04.vpr) | Integer Magic Wand with LHS < RHS                                                               | ✓                |
+| [test05.vpr](./test05.vpr) | Integer Magic Wand with LHS > RHS                                                               | ✓                |
+| [test06.vpr](./test06.vpr) | Applying the magic wand multiple times. Original version leaks information into the outer state | ×                |
+| [test07.vpr](./test07.vpr) | Assigning result of applying expression to the same field using booleans                        | ×                |
+| [test08.vpr](./test08.vpr) | Assigning result of applying expression to the same field using integers                        | ×                |
+| [test09.vpr](./test09.vpr) | Inhaling a magic wand                                                                           | ✓                |
+| [test10.vpr](./test10.vpr) | Magic wand with predicates                                                                      | ✓                |
+| [test11.vpr](./test11.vpr) | Iterate over a List                                                                             | ✓                |
+| [test12.vpr](./test12.vpr) | Applying a quantified magic wand multiple times.                                                | ✓                |
+| [test13.vpr](./test13.vpr) | Applying a magic wand multiple times with a quantified expression on the LHS.                   | ✓                |
 
 Other interesting test cases in the [Silver repository](https://github.com/viperproject/silver/tree/master/src/test/resources) during the development of `MagicWandSnapFunctions` were:
 * [wands/examples_paper/conditionals.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/examples_paper/conditionals.vpr)
diff --git a/src/test/resources/wands/snap_functions/test13.vpr b/src/test/resources/wands/snap_functions/test13.vpr
new file mode 100644
index 000000000..d4282939e
--- /dev/null
+++ b/src/test/resources/wands/snap_functions/test13.vpr
@@ -0,0 +1,87 @@
+field f: Int
+
+method test13a(xs: Seq[Ref], y: Ref)
+    requires forall x: Ref :: x in xs ==> acc(x.f)
+    requires |xs| >= 1
+    requires acc(y.f)
+{
+    xs[0].f := 0
+    var some: Ref := xs[0]
+
+    package (forall x: Ref :: x in xs ==> acc(x.f)) --* acc(some.f)
+
+    some.f := 1
+    assert applying ((forall x: Ref :: x in xs ==> acc(x.f)) --* acc(some.f)) in true
+
+    some.f := 2
+    assert applying ((forall x: Ref :: x in xs ==> acc(x.f)) --* acc(some.f)) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
+
+method test13b(xs: Seq[Ref], y: Ref)
+    requires forall x: Ref :: x in xs ==> acc(x.f)
+    requires |xs| >= 1
+    requires acc(y.f)
+{
+    xs[0].f := 0
+    var some: Ref := xs[0]
+
+    package (forall x: Ref :: x in xs ==> acc(x.f)) --* acc(some.f)
+
+    some.f := 1
+    assert applying ((forall x: Ref :: x in xs ==> acc(x.f)) --* acc(some.f)) in true
+
+    some.f := 2
+    assert applying ((forall x: Ref :: x in xs ==> acc(x.f)) --* acc(some.f)) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+
+    var completed: Seq[Ref] := Seq(some)
+    assert forall z: Ref :: z in completed ==> (forall x: Ref :: x in xs ==> acc(x.f)) --* acc(z.f)
+}
+
+method test13c(xs: Seq[Ref], y: Ref)
+    requires forall x: Ref :: x in xs ==> acc(x.f)
+    requires |xs| >= 1
+    requires acc(y.f)
+{
+    xs[0].f := 0
+    var some: Ref := xs[0]
+
+    package (forall x: Ref :: x in xs ==> acc(x.f)) && acc(y.f) --* acc(some.f) && acc(y.f)
+
+    some.f := 1
+    assert applying ((forall x: Ref :: x in xs ==> acc(x.f)) && acc(y.f) --* acc(some.f) && acc(y.f)) in true
+
+    some.f := 2
+    assert applying ((forall x: Ref :: x in xs ==> acc(x.f)) && acc(y.f) --* acc(some.f) && acc(y.f)) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
+
+method test13d(xs: Seq[Ref], y: Ref)
+    requires forall x: Ref :: x in xs ==> acc(x.f)
+    requires |xs| >= 1
+    requires acc(y.f)
+{
+    xs[0].f := 0
+    var some: Ref := xs[0]
+
+    package (forall x: Ref :: x in xs ==> acc(x.f)) && acc(y.f) --* acc(some.f) && acc(y.f)
+
+    some.f := 1
+    assert applying ((forall x: Ref :: x in xs ==> acc(x.f)) && acc(y.f) --* acc(some.f) && acc(y.f)) in true
+
+    some.f := 2
+    assert applying ((forall x: Ref :: x in xs ==> acc(x.f)) && acc(y.f) --* acc(some.f) && acc(y.f)) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+
+    var completed: Seq[Ref] := Seq(some)
+    assert forall z: Ref :: z in completed ==> (forall x: Ref :: x in xs ==> acc(x.f)) && acc(y.f) --* acc(z.f) && acc(y.f)
+}

From 129284b4e8df75ac525c27abde06c7294421febe Mon Sep 17 00:00:00 2001
From: Manuel Dublanc <19774382+manud99@users.noreply.github.com>
Date: Sun, 9 Jun 2024 17:21:11 +0200
Subject: [PATCH 07/16] Record which snapshot maps were created during
 packaging.

---
 .../resources/wands/snap_functions/test14.vpr    | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 src/test/resources/wands/snap_functions/test14.vpr

diff --git a/src/test/resources/wands/snap_functions/test14.vpr b/src/test/resources/wands/snap_functions/test14.vpr
new file mode 100644
index 000000000..3ceef90e9
--- /dev/null
+++ b/src/test/resources/wands/snap_functions/test14.vpr
@@ -0,0 +1,16 @@
+field f: Int
+
+method test14(x: Ref)
+    requires forall y: Ref :: true ==> acc(y.f)
+    // requires x.f == 0
+{
+    package (forall y: Ref :: true ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))
+
+    x.f := 0
+    assert applying ((forall y: Ref :: true ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))) in true
+    x.f := 1
+    assert applying ((forall y: Ref :: true ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
\ No newline at end of file

From 3d6fc1abb2a3b188ea2caa932504d9665c78692b Mon Sep 17 00:00:00 2001
From: Manuel Dublanc <19774382+manud99@users.noreply.github.com>
Date: Tue, 11 Jun 2024 11:46:04 +0200
Subject: [PATCH 08/16] Simplify assume10QPwand.vpr test case.

---
 .../impure_assume/assume10QPwand-light.vpr    | 25 +++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 src/test/resources/all/impure_assume/assume10QPwand-light.vpr

diff --git a/src/test/resources/all/impure_assume/assume10QPwand-light.vpr b/src/test/resources/all/impure_assume/assume10QPwand-light.vpr
new file mode 100644
index 000000000..3250a465e
--- /dev/null
+++ b/src/test/resources/all/impure_assume/assume10QPwand-light.vpr
@@ -0,0 +1,25 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+field f: Int
+
+predicate p(x: Ref)
+
+method m(xs: Set[Ref], q: Perm, xs1: Set[Ref]) {
+
+  inhale none < q
+  inhale forall x: Ref :: (x in xs) ==> acc(x.f) --* acc(p(x))
+
+  assume (forall x1: Ref :: {acc(x1.f, q) --* acc(p(x1), q)} (x1 in xs1) ==> acc(x1.f, q) --* acc(p(x1), q))
+
+  var a: Ref
+
+  assume a in xs1
+
+  //:: UnexpectedOutput(assert.failed:wand.not.found, /carbon/issue/257/)
+  assert acc(a.f, q) --* acc(p(a), q)
+
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert q == write ==> false // MS: Can we expect this to hold?
+}
\ No newline at end of file

From 9dba1b40e7fa6d0f2fd30bb7f3b812048aab8f69 Mon Sep 17 00:00:00 2001
From: Manuel Dublanc <19774382+manud99@users.noreply.github.com>
Date: Tue, 11 Jun 2024 12:39:28 +0200
Subject: [PATCH 09/16] triggerFoldPackage.vpr still fails when using z3
 version 4.13.0

---
 .../all/heap-dependent_triggers/triggerFoldPackage.vpr          | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/test/resources/all/heap-dependent_triggers/triggerFoldPackage.vpr b/src/test/resources/all/heap-dependent_triggers/triggerFoldPackage.vpr
index eedba5049..b191dd60c 100644
--- a/src/test/resources/all/heap-dependent_triggers/triggerFoldPackage.vpr
+++ b/src/test/resources/all/heap-dependent_triggers/triggerFoldPackage.vpr
@@ -12,7 +12,7 @@ method m1(xs: Set[Ref], y: Ref, zs: Seq[Ref]) {
     assume z in zs
     assume !(z in xs)
     package acc(z.f) --* acc(y.f)
-
+    //:: MissingOutput(assert.failed:assertion.false, /Silicon/issue/000/)
     //:: ExpectedOutput(assert.failed:assertion.false)
     assert z != y
 }

From a7d509fd05eed59d195c7478d6bd0ac1cb1474c6 Mon Sep 17 00:00:00 2001
From: Manuel Dublanc <19774382+manud99@users.noreply.github.com>
Date: Wed, 12 Jun 2024 09:56:06 +0200
Subject: [PATCH 10/16] Add tests to prevent unsoundness in QPPredicates.

---
 .../resources/wands/snap_functions/test14.vpr | 111 +++++++++++++++++-
 1 file changed, 108 insertions(+), 3 deletions(-)

diff --git a/src/test/resources/wands/snap_functions/test14.vpr b/src/test/resources/wands/snap_functions/test14.vpr
index 3ceef90e9..ef81e076c 100644
--- a/src/test/resources/wands/snap_functions/test14.vpr
+++ b/src/test/resources/wands/snap_functions/test14.vpr
@@ -1,8 +1,18 @@
 field f: Int
 
-method test14(x: Ref)
+predicate Cell(x: Ref) {
+    acc(x.f)
+}
+
+function get(x: Ref): Int
+    requires acc(Cell(x), 1/2)
+{
+    unfolding acc(Cell(x), 1/2) in x.f
+}
+
+// based on test7 in QPFields.vpr
+method test14a(x: Ref)
     requires forall y: Ref :: true ==> acc(y.f)
-    // requires x.f == 0
 {
     package (forall y: Ref :: true ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))
 
@@ -13,4 +23,99 @@ method test14(x: Ref)
 
     //:: ExpectedOutput(assert.failed:assertion.false)
     assert false
-}
\ No newline at end of file
+}
+
+// based on test9 in QPFields.vpr
+method test14b(x: Ref)
+    requires forall y: Ref :: true ==> acc(y.f)
+{
+    package (forall y: Ref :: true ==> acc(y.f)) --* acc(x.f)
+
+    x.f := 0
+    assert applying ((forall y: Ref :: true ==> acc(y.f)) --* acc(x.f)) in true
+    x.f := 1
+    assert applying ((forall y: Ref :: true ==> acc(y.f)) --* acc(x.f)) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
+
+// based on test11 in QPFields.vpr
+method test14c(x: Ref, z: Ref)
+    requires acc(x.f) && z != x
+{
+    package (forall y: Ref :: y != x ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))
+    inhale forall y: Ref :: y != x ==> acc(y.f)
+
+    assert acc(z.f)
+
+    z.f := 0
+    assert applying ((forall y: Ref :: y != x ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))) in true
+    z.f := 1
+    assert applying ((forall y: Ref :: y != x ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
+
+// based on test7 in QPPredicates.vpr
+method test14d(x: Ref)
+    requires forall y: Ref :: true ==> Cell(y)
+{
+    package (forall y: Ref :: true ==> Cell(y)) --* (forall y: Ref :: true ==> Cell(y))
+
+    unfold Cell(x)
+    x.f := 0
+    fold Cell(x)
+    assert applying ((forall y: Ref :: true ==> Cell(y)) --* (forall y: Ref :: true ==> Cell(y))) in true
+
+    unfold Cell(x)
+    x.f := 1
+    fold Cell(x)
+    assert applying ((forall y: Ref :: true ==> Cell(y)) --* (forall y: Ref :: true ==> Cell(y))) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
+
+// based on test9 in QPPredicates.vpr
+method test14e(x: Ref)
+    requires forall y: Ref :: true ==> Cell(y)
+{
+    package (forall y: Ref :: true ==> Cell(y)) --* Cell(x)
+
+    unfold Cell(x)
+    x.f := 0
+    fold Cell(x)
+    assert applying ((forall y: Ref :: true ==> Cell(y)) --* Cell(x)) in true
+
+    unfold Cell(x)
+    x.f := 1
+    fold Cell(x)
+    assert applying ((forall y: Ref :: true ==> Cell(y)) --* Cell(x)) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
+
+// based on test11 in QPPredicates.vpr
+method test14f(x: Ref, z: Ref)
+    requires Cell(x)
+    requires x != z
+{
+    package (forall y: Ref :: y != x ==> Cell(y)) --* (forall y: Ref :: true ==> Cell(y))
+    inhale forall y: Ref :: y != x ==> Cell(y)
+
+    unfold Cell(z)
+    z.f := 0
+    fold Cell(z)
+    assert applying ((forall y: Ref :: y != x ==> Cell(y)) --* (forall y: Ref :: true ==> Cell(y))) in true
+
+    unfold Cell(z)
+    z.f := 1
+    fold Cell(z)
+    assert applying ((forall y: Ref :: y != x ==> Cell(y)) --* (forall y: Ref :: true ==> Cell(y))) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}

From 710d56ef7f63e38d120bb17c4ee538cf50a9fdd4 Mon Sep 17 00:00:00 2001
From: Manuel Dublanc <19774382+manud99@users.noreply.github.com>
Date: Wed, 12 Jun 2024 17:52:28 +0200
Subject: [PATCH 11/16] Add simplified versions of the QPWands.vpr test file.

---
 .../resources/wands/snap_functions/README.md  |  2 +
 .../resources/wands/snap_functions/test15.vpr | 53 +++++++++++++++++++
 2 files changed, 55 insertions(+)
 create mode 100644 src/test/resources/wands/snap_functions/test15.vpr

diff --git a/src/test/resources/wands/snap_functions/README.md b/src/test/resources/wands/snap_functions/README.md
index 99fa72349..7492d9aa4 100644
--- a/src/test/resources/wands/snap_functions/README.md
+++ b/src/test/resources/wands/snap_functions/README.md
@@ -19,6 +19,8 @@ This folder contains Viper test files that I used when working on MagicWandSnapF
 | [test11.vpr](./test11.vpr) | Iterate over a List                                                                             | ✓                |
 | [test12.vpr](./test12.vpr) | Applying a quantified magic wand multiple times.                                                | ✓                |
 | [test13.vpr](./test13.vpr) | Applying a magic wand multiple times with a quantified expression on the LHS.                   | ✓                |
+| [test14.vpr](./test14.vpr) | Test from QPFields.vpr and QPPredicates.vpr adapted to show some unsound behavior.              | ✓                |
+| [test15.vpr](./test15.vpr) | Test from QPWands.vpr but in a simplified form.                                                 | ✓                |
 
 Other interesting test cases in the [Silver repository](https://github.com/viperproject/silver/tree/master/src/test/resources) during the development of `MagicWandSnapFunctions` were:
 * [wands/examples_paper/conditionals.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/examples_paper/conditionals.vpr)
diff --git a/src/test/resources/wands/snap_functions/test15.vpr b/src/test/resources/wands/snap_functions/test15.vpr
new file mode 100644
index 000000000..3157c2833
--- /dev/null
+++ b/src/test/resources/wands/snap_functions/test15.vpr
@@ -0,0 +1,53 @@
+field f: Int
+
+method test0b(xs: Seq[Ref], y: Ref)
+  requires forall x: Ref :: x in xs ==> acc(x.f)
+  requires forall i: Int, j: Int :: 0 <= i && 0 <= j && i < |xs| && j < |xs| && i != j ==> xs[i] != xs[j]
+  requires |xs| >= 1
+  requires acc(y.f)
+{
+  xs[0].f := 0
+  y.f := 1
+
+  label setupComplete
+  var toGo: Seq[Ref] := xs
+  var completed: Seq[Ref] := Seq()
+
+  var localX: Ref := toGo[0]
+  package acc(y.f) --* acc(localX.f) && acc(y.f) && y.f == old[lhs](y.f)
+  completed := completed ++ Seq(localX)
+  toGo := toGo[1..]
+
+  assert 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)
+}
+
+method test0c(xs: Seq[Ref], y: Ref)
+  requires forall x: Ref :: x in xs ==> acc(x.f)
+  requires |xs| >= 1
+  requires acc(y.f)
+{
+  var localX: Ref := xs[0]
+
+  var toGo: Seq[Ref] := xs[1..]
+  var completed: Seq[Ref] := Seq(localX)
+
+  package acc(y.f) --* acc(localX.f) && acc(y.f) && y.f == old[lhs](y.f)
+
+  assert 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(x.f)
+}
+
+method test0d(xs: Seq[Ref], y: Ref)
+  requires forall x: Ref :: x in xs ==> acc(x.f)
+  requires |xs| >= 1
+  requires acc(y.f)
+{
+  xs[0].f := 0
+  y.f := 1
+  label setupComplete
+
+  var completed: Seq[Ref] := Seq(xs[0])
+
+  package acc(y.f) --* acc(xs[0].f) && acc(y.f) && y.f == old[lhs](y.f)
+
+  assert 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)
+}

From 482e7f2e2b968f9ec003ad2606ac087c5a1b4401 Mon Sep 17 00:00:00 2001
From: Manuel Dublanc <19774382+manud99@users.noreply.github.com>
Date: Sat, 15 Jun 2024 11:31:53 +0200
Subject: [PATCH 12/16] Add annotations for the failing QPWands tests.

---
 .../resources/wands/new_syntax/QPWands.vpr    | 37 ++++++++++++++++++-
 .../resources/wands/snap_functions/test15.vpr |  3 ++
 2 files changed, 39 insertions(+), 1 deletion(-)

diff --git a/src/test/resources/wands/new_syntax/QPWands.vpr b/src/test/resources/wands/new_syntax/QPWands.vpr
index a48a4660d..13a12211f 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/000/)
     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) {
@@ -89,7 +89,42 @@ requires acc(y.f) {
     package acc(y.f) --* acc(some.f) && acc(y.f)
     var completed: Seq[Ref] := Seq(some)
     assert forall x: Ref :: x in completed ==> acc(y.f) --* acc(x.f) && acc(y.f)
+    //:: UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/000/)
+    assert applying (acc(y.f) --* acc(some.f) && acc(y.f)) in some.f == 0
+    assert applying (acc(y.f) --* acc(some.f) && acc(y.f)) in y.f == 1
+    assert forall x: Ref :: x in xs[1..] ==> acc(x.f)
+
+    //:: MissingOutput(assert.failed:insufficient.permission, /silicon/issue/000/)
+    assert forall x: Ref :: x in xs ==> acc(x.f)
+}
+
+method test5b(xs: Seq[Ref], y: Ref)
+requires forall x: Ref :: x in xs ==> acc(x.f)
+requires injectiveSeq(xs)
+requires |xs| >= 1
+requires acc(y.f) {
+    xs[0].f := 0
+    var some: Ref := xs[0]
+    package acc(y.f) --* acc(some.f) && acc(y.f)
+    var completed: Seq[Ref] := Seq(some)
+    assert forall x: Ref :: x in completed ==> acc(y.f) --* acc(x.f) && acc(y.f)
     assert applying (acc(y.f) --* acc(some.f) && acc(y.f)) in some.f == 0
+    assert forall x: Ref :: x in xs[1..] ==> acc(x.f)
+
+    //:: ExpectedOutput(assert.failed:insufficient.permission)
+    assert forall x: Ref :: x in xs ==> acc(x.f)
+}
+
+method test5c(xs: Seq[Ref], y: Ref)
+requires forall x: Ref :: x in xs ==> acc(x.f)
+requires injectiveSeq(xs)
+requires |xs| >= 1
+requires acc(y.f) {
+    y.f := 1
+    var some: Ref := xs[0]
+    package acc(y.f) --* acc(some.f) && acc(y.f)
+    var completed: Seq[Ref] := Seq(some)
+    assert forall x: Ref :: x in completed ==> acc(y.f) --* acc(x.f) && acc(y.f)
     assert applying (acc(y.f) --* acc(some.f) && acc(y.f)) in y.f == 1
     assert forall x: Ref :: x in xs[1..] ==> acc(x.f)
 
diff --git a/src/test/resources/wands/snap_functions/test15.vpr b/src/test/resources/wands/snap_functions/test15.vpr
index 3157c2833..171dda2aa 100644
--- a/src/test/resources/wands/snap_functions/test15.vpr
+++ b/src/test/resources/wands/snap_functions/test15.vpr
@@ -1,3 +1,4 @@
+
 field f: Int
 
 method test0b(xs: Seq[Ref], y: Ref)
@@ -18,6 +19,7 @@ method test0b(xs: Seq[Ref], y: Ref)
   completed := completed ++ Seq(localX)
   toGo := toGo[1..]
 
+  //:: UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/000/)
   assert 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)
 }
 
@@ -49,5 +51,6 @@ method test0d(xs: Seq[Ref], y: Ref)
 
   package acc(y.f) --* acc(xs[0].f) && acc(y.f) && y.f == old[lhs](y.f)
 
+  //:: UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/000/)
   assert 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)
 }

From c295837930686bea707174164bcb2cd0a8689a67 Mon Sep 17 00:00:00 2001
From: Manuel Dublanc <19774382+manud99@users.noreply.github.com>
Date: Tue, 25 Jun 2024 15:22:19 +0200
Subject: [PATCH 13/16] Update test 13 and 15.

---
 src/test/resources/wands/snap_functions/test13.vpr | 6 ++----
 src/test/resources/wands/snap_functions/test15.vpr | 2 --
 2 files changed, 2 insertions(+), 6 deletions(-)

diff --git a/src/test/resources/wands/snap_functions/test13.vpr b/src/test/resources/wands/snap_functions/test13.vpr
index d4282939e..c229473f5 100644
--- a/src/test/resources/wands/snap_functions/test13.vpr
+++ b/src/test/resources/wands/snap_functions/test13.vpr
@@ -1,9 +1,8 @@
 field f: Int
 
-method test13a(xs: Seq[Ref], y: Ref)
+method test13a(xs: Seq[Ref])
     requires forall x: Ref :: x in xs ==> acc(x.f)
     requires |xs| >= 1
-    requires acc(y.f)
 {
     xs[0].f := 0
     var some: Ref := xs[0]
@@ -20,10 +19,9 @@ method test13a(xs: Seq[Ref], y: Ref)
     assert false
 }
 
-method test13b(xs: Seq[Ref], y: Ref)
+method test13b(xs: Seq[Ref])
     requires forall x: Ref :: x in xs ==> acc(x.f)
     requires |xs| >= 1
-    requires acc(y.f)
 {
     xs[0].f := 0
     var some: Ref := xs[0]
diff --git a/src/test/resources/wands/snap_functions/test15.vpr b/src/test/resources/wands/snap_functions/test15.vpr
index 171dda2aa..122fd8884 100644
--- a/src/test/resources/wands/snap_functions/test15.vpr
+++ b/src/test/resources/wands/snap_functions/test15.vpr
@@ -19,7 +19,6 @@ method test0b(xs: Seq[Ref], y: Ref)
   completed := completed ++ Seq(localX)
   toGo := toGo[1..]
 
-  //:: UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/000/)
   assert 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)
 }
 
@@ -51,6 +50,5 @@ method test0d(xs: Seq[Ref], y: Ref)
 
   package acc(y.f) --* acc(xs[0].f) && acc(y.f) && y.f == old[lhs](y.f)
 
-  //:: UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/000/)
   assert 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)
 }

From 7eaf86ac3e8e4b778c01fde55e571c820860f8ef Mon Sep 17 00:00:00 2001
From: Manuel Dublanc <19774382+manud99@users.noreply.github.com>
Date: Thu, 27 Jun 2024 15:25:46 +0200
Subject: [PATCH 14/16] Add test case 16.

---
 .../resources/wands/snap_functions/README.md  |  3 ++
 .../resources/wands/snap_functions/test16.vpr | 30 +++++++++++++++++++
 2 files changed, 33 insertions(+)
 create mode 100644 src/test/resources/wands/snap_functions/test16.vpr

diff --git a/src/test/resources/wands/snap_functions/README.md b/src/test/resources/wands/snap_functions/README.md
index 7492d9aa4..a7ba7d70d 100644
--- a/src/test/resources/wands/snap_functions/README.md
+++ b/src/test/resources/wands/snap_functions/README.md
@@ -21,10 +21,13 @@ This folder contains Viper test files that I used when working on MagicWandSnapF
 | [test13.vpr](./test13.vpr) | Applying a magic wand multiple times with a quantified expression on the LHS.                   | ✓                |
 | [test14.vpr](./test14.vpr) | Test from QPFields.vpr and QPPredicates.vpr adapted to show some unsound behavior.              | ✓                |
 | [test15.vpr](./test15.vpr) | Test from QPWands.vpr but in a simplified form.                                                 | ✓                |
+| [test16.vpr](./test16.vpr) | Extension of some tests in QPFields.vpr and QPWands.vpr.                                        | ✓                |
 
 Other interesting test cases in the [Silver repository](https://github.com/viperproject/silver/tree/master/src/test/resources) during the development of `MagicWandSnapFunctions` were:
 * [wands/examples_paper/conditionals.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/examples_paper/conditionals.vpr)
 * [wands/new_syntax/QPFields.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/new_syntax/QPFields.vpr)
+* [wands/new_syntax/QPPredicates.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/new_syntax/QPPredicates.vpr)
+* [wands/new_syntax/QPWands.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/new_syntax/QPWands.vpr)
 * [wands/new_syntax/SnapshotsNestedMagicWands.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/new_syntax/SnapshotsNestedMagicWands.vpr)
 * [wands/regression/conditionals2.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/regression/conditionals2.vpr)
 * [wands/regression/issue024.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/regression/issue024.vpr)
diff --git a/src/test/resources/wands/snap_functions/test16.vpr b/src/test/resources/wands/snap_functions/test16.vpr
new file mode 100644
index 000000000..61a8673b9
--- /dev/null
+++ b/src/test/resources/wands/snap_functions/test16.vpr
@@ -0,0 +1,30 @@
+field f: Int
+field g: Int
+
+method test16a(xs: Seq[Ref], some: Ref, y: Ref)
+    requires forall x: Ref :: x in xs ==> acc(x.f)
+    requires some in xs && some.f == 0
+    requires acc(y.f)
+{
+    package acc(y.f) --* acc(some.f)
+
+    var completed: Seq[Ref] := Seq(some)
+    assert forall z: Ref :: z in completed ==> acc(y.f) --* acc(z.f)
+
+    apply acc(y.f) --* acc(some.f)
+    assert some.f == 0
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
+
+method test16b(y: Ref)
+    requires forall x: Ref :: acc(x.f) && acc(x.g)
+    requires y.f == 42
+    requires y.g > 0
+{
+    package (forall x: Ref :: acc(x.f) && acc(x.g)) --* acc(y.f) && acc(y.g)
+    apply (forall x: Ref :: acc(x.f) && acc(x.g)) --* acc(y.f) && acc(y.g)
+
+    assert y.f == 42
+    assert y.g > 0
+}

From 547cbdd1eee86eca410a2e7a1492c4b02aa82c7a Mon Sep 17 00:00:00 2001
From: Manuel Dublanc <19774382+manud99@users.noreply.github.com>
Date: Fri, 28 Jun 2024 16:03:29 +0200
Subject: [PATCH 15/16] Rename test files.

---
 src/test/resources/wands/mwsf/README.md       | 35 +++++++++++++
 .../applying-twice-bool.vpr}                  |  0
 .../wands/mwsf/applying-twice-qp-fields.vpr   | 49 +++++++++++++++++++
 .../applying-twice-qp-predicates.vpr}         | 48 ------------------
 .../applying-twice-quantified-lhs.vpr}        |  0
 .../applying-twice-quantified-wand.vpr}       |  0
 .../assign-applying-bool.vpr}                 |  0
 .../assign-applying-int.vpr}                  |  0
 .../test01.vpr => mwsf/basic-bool.vpr}        |  0
 .../test02.vpr => mwsf/basic-int.vpr}         |  0
 .../test03.vpr => mwsf/basic-lhs-eq-rhs.vpr}  |  0
 .../test05.vpr => mwsf/basic-lhs-gt-rhs.vpr}  |  0
 .../test04.vpr => mwsf/basic-lhs-lt-rhs.vpr}  |  0
 .../test11.vpr => mwsf/example-list.vpr}      |  0
 .../inhaling-magic-wand.vpr}                  |  0
 .../predicates-in-magic-wands.vpr}            |  0
 .../quantified-magic-wands.vpr}               | 18 ++++++-
 src/test/resources/wands/mwsf/two-fields.vpr  | 14 ++++++
 .../resources/wands/snap_functions/README.md  | 34 -------------
 .../resources/wands/snap_functions/test16.vpr | 30 ------------
 20 files changed, 115 insertions(+), 113 deletions(-)
 create mode 100644 src/test/resources/wands/mwsf/README.md
 rename src/test/resources/wands/{snap_functions/test06.vpr => mwsf/applying-twice-bool.vpr} (100%)
 create mode 100644 src/test/resources/wands/mwsf/applying-twice-qp-fields.vpr
 rename src/test/resources/wands/{snap_functions/test14.vpr => mwsf/applying-twice-qp-predicates.vpr} (55%)
 rename src/test/resources/wands/{snap_functions/test13.vpr => mwsf/applying-twice-quantified-lhs.vpr} (100%)
 rename src/test/resources/wands/{snap_functions/test12.vpr => mwsf/applying-twice-quantified-wand.vpr} (100%)
 rename src/test/resources/wands/{snap_functions/test07.vpr => mwsf/assign-applying-bool.vpr} (100%)
 rename src/test/resources/wands/{snap_functions/test08.vpr => mwsf/assign-applying-int.vpr} (100%)
 rename src/test/resources/wands/{snap_functions/test01.vpr => mwsf/basic-bool.vpr} (100%)
 rename src/test/resources/wands/{snap_functions/test02.vpr => mwsf/basic-int.vpr} (100%)
 rename src/test/resources/wands/{snap_functions/test03.vpr => mwsf/basic-lhs-eq-rhs.vpr} (100%)
 rename src/test/resources/wands/{snap_functions/test05.vpr => mwsf/basic-lhs-gt-rhs.vpr} (100%)
 rename src/test/resources/wands/{snap_functions/test04.vpr => mwsf/basic-lhs-lt-rhs.vpr} (100%)
 rename src/test/resources/wands/{snap_functions/test11.vpr => mwsf/example-list.vpr} (100%)
 rename src/test/resources/wands/{snap_functions/test09.vpr => mwsf/inhaling-magic-wand.vpr} (100%)
 rename src/test/resources/wands/{snap_functions/test10.vpr => mwsf/predicates-in-magic-wands.vpr} (100%)
 rename src/test/resources/wands/{snap_functions/test15.vpr => mwsf/quantified-magic-wands.vpr} (76%)
 create mode 100644 src/test/resources/wands/mwsf/two-fields.vpr
 delete mode 100644 src/test/resources/wands/snap_functions/README.md
 delete mode 100644 src/test/resources/wands/snap_functions/test16.vpr

diff --git a/src/test/resources/wands/mwsf/README.md b/src/test/resources/wands/mwsf/README.md
new file mode 100644
index 000000000..c8c2e1634
--- /dev/null
+++ b/src/test/resources/wands/mwsf/README.md
@@ -0,0 +1,35 @@
+# Test Suite for Magic Wand Snap Functions
+
+This folder contains Viper test files that I used when working on MagicWandSnapFunctions for the Silicon project.
+
+## Overview
+
+| Name                                                                       | Description                                                                                     | Expected Result |
+|----------------------------------------------------------------------------|-------------------------------------------------------------------------------------------------|-----------------|
+| [basic-bool.vpr](./basic-bool.vpr)                                         | Boolean Magic Wand with trivial LHS                                                             | ✓               |
+| [basic-int.vpr](./basic-int.vpr)                                           | Integer Magic Wand with trivial LHS                                                             | ✓               |
+| [basic-lhs-eq-rhs.vpr](./basic-lhs-eq-rhs.vpr)                             | Integer Magic Wand with LHS = RHS                                                               | ✓               |
+| [basic-lhs-lt-rhs.vpr](./basic-lhs-lt-rhs.vpr)                             | Integer Magic Wand with LHS < RHS                                                               | ✓               |
+| [basic-lhs-gt-rhs.vpr](./basic-lhs-gt-rhs.vpr)                             | Integer Magic Wand with LHS > RHS                                                               | ✓               |
+| [applying-twice-bool.vpr](./applying-twice-bool.vpr)                       | Applying the magic wand multiple times. Original version leaks information into the outer state | ×               |
+| [assign-applying-bool.vpr](./assign-applying-bool.vpr)                     | Assigning result of applying expression to the same field using booleans                        | ×               |
+| [assign-applying-int.vpr](./assign-applying-int.vpr)                       | Assigning result of applying expression to the same field using integers                        | ×               |
+| [inhaling-magic-wand.vpr](./inhaling-magic-wand.vpr)                       | Inhaling a magic wand                                                                           | ✓               |
+| [predicates-in-magic-wands.vpr](./predicates-in-magic-wands.vpr)           | Magic wand with predicates                                                                      | ✓               |
+| [example-list.vpr](./example-list.vpr)                                     | Iterate over a List                                                                             | ✓               |
+| [applying-twice-quantified-wand.vpr](./applying-twice-quantified-wand.vpr) | Applying a quantified magic wand multiple times.                                                | ✓               |
+| [applying-twice-quantified-lhs.vpr](./applying-twice-quantified-lhs.vpr)   | Applying a magic wand multiple times with a quantified expression on the LHS.                   | ✓               |
+| [applying-twice-qp-fields.vpr](./applying-twice-qp-fields.vpr)             | Test from QPFields.vpr adapted to test some unsound behavior.                                   | ✓               |
+| [applying-twice-qp-predicates.vpr](./applying-twice-qp-predicates.vpr)     | Test from QPPredicates.vpr adapted to test some unsound behavior.                               | ✓               |
+| [quantified-magic-wands.vpr](./quantified-magic-wands.vpr)                 | Tests with quantified magic wands.                                                              | ✓               |
+| [two-fields.vpr](./two-fields.vpr)                                         | Magic wand with quantifier over two fields.                                                     | ✓               |
+
+Other interesting test cases in the [Silver repository](https://github.com/viperproject/silver/tree/master/src/test/resources) during the development of `MagicWandSnapFunctions` were:
+* [wands/examples_paper/conditionals.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/examples_paper/conditionals.vpr)
+* [wands/new_syntax/QPFields.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/new_syntax/QPFields.vpr)
+* [wands/new_syntax/QPPredicates.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/new_syntax/QPPredicates.vpr)
+* [wands/new_syntax/QPWands.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/new_syntax/QPWands.vpr)
+* [wands/new_syntax/SnapshotsNestedMagicWands.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/new_syntax/SnapshotsNestedMagicWands.vpr)
+* [wands/regression/conditionals2.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/regression/conditionals2.vpr)
+* [wands/regression/issue024.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/regression/issue024.vpr)
+* [wands/regression/issue029.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/regression/issue029.vpr)
diff --git a/src/test/resources/wands/snap_functions/test06.vpr b/src/test/resources/wands/mwsf/applying-twice-bool.vpr
similarity index 100%
rename from src/test/resources/wands/snap_functions/test06.vpr
rename to src/test/resources/wands/mwsf/applying-twice-bool.vpr
diff --git a/src/test/resources/wands/mwsf/applying-twice-qp-fields.vpr b/src/test/resources/wands/mwsf/applying-twice-qp-fields.vpr
new file mode 100644
index 000000000..b184b1a91
--- /dev/null
+++ b/src/test/resources/wands/mwsf/applying-twice-qp-fields.vpr
@@ -0,0 +1,49 @@
+field f: Int
+
+// based on test7 in QPFields.vpr
+method test14a(x: Ref)
+    requires forall y: Ref :: true ==> acc(y.f)
+{
+    package (forall y: Ref :: true ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))
+
+    x.f := 0
+    assert applying ((forall y: Ref :: true ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))) in true
+    x.f := 1
+    assert applying ((forall y: Ref :: true ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
+
+// based on test9 in QPFields.vpr
+method test14b(x: Ref)
+    requires forall y: Ref :: true ==> acc(y.f)
+{
+    package (forall y: Ref :: true ==> acc(y.f)) --* acc(x.f)
+
+    x.f := 0
+    assert applying ((forall y: Ref :: true ==> acc(y.f)) --* acc(x.f)) in true
+    x.f := 1
+    assert applying ((forall y: Ref :: true ==> acc(y.f)) --* acc(x.f)) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
+
+// based on test11 in QPFields.vpr
+method test14c(x: Ref, z: Ref)
+    requires acc(x.f) && z != x
+{
+    package (forall y: Ref :: y != x ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))
+    inhale forall y: Ref :: y != x ==> acc(y.f)
+
+    assert acc(z.f)
+
+    z.f := 0
+    assert applying ((forall y: Ref :: y != x ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))) in true
+    z.f := 1
+    assert applying ((forall y: Ref :: y != x ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
diff --git a/src/test/resources/wands/snap_functions/test14.vpr b/src/test/resources/wands/mwsf/applying-twice-qp-predicates.vpr
similarity index 55%
rename from src/test/resources/wands/snap_functions/test14.vpr
rename to src/test/resources/wands/mwsf/applying-twice-qp-predicates.vpr
index ef81e076c..db04268ae 100644
--- a/src/test/resources/wands/snap_functions/test14.vpr
+++ b/src/test/resources/wands/mwsf/applying-twice-qp-predicates.vpr
@@ -10,54 +10,6 @@ function get(x: Ref): Int
     unfolding acc(Cell(x), 1/2) in x.f
 }
 
-// based on test7 in QPFields.vpr
-method test14a(x: Ref)
-    requires forall y: Ref :: true ==> acc(y.f)
-{
-    package (forall y: Ref :: true ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))
-
-    x.f := 0
-    assert applying ((forall y: Ref :: true ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))) in true
-    x.f := 1
-    assert applying ((forall y: Ref :: true ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))) in true
-
-    //:: ExpectedOutput(assert.failed:assertion.false)
-    assert false
-}
-
-// based on test9 in QPFields.vpr
-method test14b(x: Ref)
-    requires forall y: Ref :: true ==> acc(y.f)
-{
-    package (forall y: Ref :: true ==> acc(y.f)) --* acc(x.f)
-
-    x.f := 0
-    assert applying ((forall y: Ref :: true ==> acc(y.f)) --* acc(x.f)) in true
-    x.f := 1
-    assert applying ((forall y: Ref :: true ==> acc(y.f)) --* acc(x.f)) in true
-
-    //:: ExpectedOutput(assert.failed:assertion.false)
-    assert false
-}
-
-// based on test11 in QPFields.vpr
-method test14c(x: Ref, z: Ref)
-    requires acc(x.f) && z != x
-{
-    package (forall y: Ref :: y != x ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))
-    inhale forall y: Ref :: y != x ==> acc(y.f)
-
-    assert acc(z.f)
-
-    z.f := 0
-    assert applying ((forall y: Ref :: y != x ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))) in true
-    z.f := 1
-    assert applying ((forall y: Ref :: y != x ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))) in true
-
-    //:: ExpectedOutput(assert.failed:assertion.false)
-    assert false
-}
-
 // based on test7 in QPPredicates.vpr
 method test14d(x: Ref)
     requires forall y: Ref :: true ==> Cell(y)
diff --git a/src/test/resources/wands/snap_functions/test13.vpr b/src/test/resources/wands/mwsf/applying-twice-quantified-lhs.vpr
similarity index 100%
rename from src/test/resources/wands/snap_functions/test13.vpr
rename to src/test/resources/wands/mwsf/applying-twice-quantified-lhs.vpr
diff --git a/src/test/resources/wands/snap_functions/test12.vpr b/src/test/resources/wands/mwsf/applying-twice-quantified-wand.vpr
similarity index 100%
rename from src/test/resources/wands/snap_functions/test12.vpr
rename to src/test/resources/wands/mwsf/applying-twice-quantified-wand.vpr
diff --git a/src/test/resources/wands/snap_functions/test07.vpr b/src/test/resources/wands/mwsf/assign-applying-bool.vpr
similarity index 100%
rename from src/test/resources/wands/snap_functions/test07.vpr
rename to src/test/resources/wands/mwsf/assign-applying-bool.vpr
diff --git a/src/test/resources/wands/snap_functions/test08.vpr b/src/test/resources/wands/mwsf/assign-applying-int.vpr
similarity index 100%
rename from src/test/resources/wands/snap_functions/test08.vpr
rename to src/test/resources/wands/mwsf/assign-applying-int.vpr
diff --git a/src/test/resources/wands/snap_functions/test01.vpr b/src/test/resources/wands/mwsf/basic-bool.vpr
similarity index 100%
rename from src/test/resources/wands/snap_functions/test01.vpr
rename to src/test/resources/wands/mwsf/basic-bool.vpr
diff --git a/src/test/resources/wands/snap_functions/test02.vpr b/src/test/resources/wands/mwsf/basic-int.vpr
similarity index 100%
rename from src/test/resources/wands/snap_functions/test02.vpr
rename to src/test/resources/wands/mwsf/basic-int.vpr
diff --git a/src/test/resources/wands/snap_functions/test03.vpr b/src/test/resources/wands/mwsf/basic-lhs-eq-rhs.vpr
similarity index 100%
rename from src/test/resources/wands/snap_functions/test03.vpr
rename to src/test/resources/wands/mwsf/basic-lhs-eq-rhs.vpr
diff --git a/src/test/resources/wands/snap_functions/test05.vpr b/src/test/resources/wands/mwsf/basic-lhs-gt-rhs.vpr
similarity index 100%
rename from src/test/resources/wands/snap_functions/test05.vpr
rename to src/test/resources/wands/mwsf/basic-lhs-gt-rhs.vpr
diff --git a/src/test/resources/wands/snap_functions/test04.vpr b/src/test/resources/wands/mwsf/basic-lhs-lt-rhs.vpr
similarity index 100%
rename from src/test/resources/wands/snap_functions/test04.vpr
rename to src/test/resources/wands/mwsf/basic-lhs-lt-rhs.vpr
diff --git a/src/test/resources/wands/snap_functions/test11.vpr b/src/test/resources/wands/mwsf/example-list.vpr
similarity index 100%
rename from src/test/resources/wands/snap_functions/test11.vpr
rename to src/test/resources/wands/mwsf/example-list.vpr
diff --git a/src/test/resources/wands/snap_functions/test09.vpr b/src/test/resources/wands/mwsf/inhaling-magic-wand.vpr
similarity index 100%
rename from src/test/resources/wands/snap_functions/test09.vpr
rename to src/test/resources/wands/mwsf/inhaling-magic-wand.vpr
diff --git a/src/test/resources/wands/snap_functions/test10.vpr b/src/test/resources/wands/mwsf/predicates-in-magic-wands.vpr
similarity index 100%
rename from src/test/resources/wands/snap_functions/test10.vpr
rename to src/test/resources/wands/mwsf/predicates-in-magic-wands.vpr
diff --git a/src/test/resources/wands/snap_functions/test15.vpr b/src/test/resources/wands/mwsf/quantified-magic-wands.vpr
similarity index 76%
rename from src/test/resources/wands/snap_functions/test15.vpr
rename to src/test/resources/wands/mwsf/quantified-magic-wands.vpr
index 122fd8884..8c6f30fc2 100644
--- a/src/test/resources/wands/snap_functions/test15.vpr
+++ b/src/test/resources/wands/mwsf/quantified-magic-wands.vpr
@@ -1,6 +1,6 @@
-
 field f: Int
 
+// Test adapted from QPWands.vpr test0
 method test0b(xs: Seq[Ref], y: Ref)
   requires forall x: Ref :: x in xs ==> acc(x.f)
   requires forall i: Int, j: Int :: 0 <= i && 0 <= j && i < |xs| && j < |xs| && i != j ==> xs[i] != xs[j]
@@ -52,3 +52,19 @@ method test0d(xs: Seq[Ref], y: Ref)
 
   assert 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)
 }
+
+method test16a(xs: Seq[Ref], some: Ref, y: Ref)
+    requires forall x: Ref :: x in xs ==> acc(x.f)
+    requires some in xs && some.f == 0
+    requires acc(y.f)
+{
+    package acc(y.f) --* acc(some.f)
+
+    var completed: Seq[Ref] := Seq(some)
+    assert forall z: Ref :: z in completed ==> acc(y.f) --* acc(z.f)
+
+    apply acc(y.f) --* acc(some.f)
+    assert some.f == 0
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
diff --git a/src/test/resources/wands/mwsf/two-fields.vpr b/src/test/resources/wands/mwsf/two-fields.vpr
new file mode 100644
index 000000000..e2e9cea08
--- /dev/null
+++ b/src/test/resources/wands/mwsf/two-fields.vpr
@@ -0,0 +1,14 @@
+field f: Int
+field g: Int
+
+method test16b(y: Ref)
+    requires forall x: Ref :: acc(x.f) && acc(x.g)
+    requires y.f == 42
+    requires y.g > 0
+{
+    package (forall x: Ref :: acc(x.f) && acc(x.g)) --* acc(y.f) && acc(y.g)
+    apply (forall x: Ref :: acc(x.f) && acc(x.g)) --* acc(y.f) && acc(y.g)
+
+    assert y.f == 42
+    assert y.g > 0
+}
diff --git a/src/test/resources/wands/snap_functions/README.md b/src/test/resources/wands/snap_functions/README.md
deleted file mode 100644
index a7ba7d70d..000000000
--- a/src/test/resources/wands/snap_functions/README.md
+++ /dev/null
@@ -1,34 +0,0 @@
-# Test Suite for Magic Wand Snap Functions
-
-This folder contains Viper test files that I used when working on MagicWandSnapFunctions for the Silicon project.
-
-## Overview
-
-| Name                       | Description                                                                                     | Expected Result  |
-|----------------------------|-------------------------------------------------------------------------------------------------|------------------|
-| [test01.vpr](./test01.vpr) | Boolean Magic Wand with trivial LHS                                                             | ✓                |
-| [test02.vpr](./test02.vpr) | Integer Magic Wand with trivial LHS                                                             | ✓                |
-| [test03.vpr](./test03.vpr) | Integer Magic Wand with LHS = RHS                                                               | ✓                |
-| [test04.vpr](./test04.vpr) | Integer Magic Wand with LHS < RHS                                                               | ✓                |
-| [test05.vpr](./test05.vpr) | Integer Magic Wand with LHS > RHS                                                               | ✓                |
-| [test06.vpr](./test06.vpr) | Applying the magic wand multiple times. Original version leaks information into the outer state | ×                |
-| [test07.vpr](./test07.vpr) | Assigning result of applying expression to the same field using booleans                        | ×                |
-| [test08.vpr](./test08.vpr) | Assigning result of applying expression to the same field using integers                        | ×                |
-| [test09.vpr](./test09.vpr) | Inhaling a magic wand                                                                           | ✓                |
-| [test10.vpr](./test10.vpr) | Magic wand with predicates                                                                      | ✓                |
-| [test11.vpr](./test11.vpr) | Iterate over a List                                                                             | ✓                |
-| [test12.vpr](./test12.vpr) | Applying a quantified magic wand multiple times.                                                | ✓                |
-| [test13.vpr](./test13.vpr) | Applying a magic wand multiple times with a quantified expression on the LHS.                   | ✓                |
-| [test14.vpr](./test14.vpr) | Test from QPFields.vpr and QPPredicates.vpr adapted to show some unsound behavior.              | ✓                |
-| [test15.vpr](./test15.vpr) | Test from QPWands.vpr but in a simplified form.                                                 | ✓                |
-| [test16.vpr](./test16.vpr) | Extension of some tests in QPFields.vpr and QPWands.vpr.                                        | ✓                |
-
-Other interesting test cases in the [Silver repository](https://github.com/viperproject/silver/tree/master/src/test/resources) during the development of `MagicWandSnapFunctions` were:
-* [wands/examples_paper/conditionals.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/examples_paper/conditionals.vpr)
-* [wands/new_syntax/QPFields.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/new_syntax/QPFields.vpr)
-* [wands/new_syntax/QPPredicates.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/new_syntax/QPPredicates.vpr)
-* [wands/new_syntax/QPWands.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/new_syntax/QPWands.vpr)
-* [wands/new_syntax/SnapshotsNestedMagicWands.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/new_syntax/SnapshotsNestedMagicWands.vpr)
-* [wands/regression/conditionals2.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/regression/conditionals2.vpr)
-* [wands/regression/issue024.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/regression/issue024.vpr)
-* [wands/regression/issue029.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/regression/issue029.vpr)
diff --git a/src/test/resources/wands/snap_functions/test16.vpr b/src/test/resources/wands/snap_functions/test16.vpr
deleted file mode 100644
index 61a8673b9..000000000
--- a/src/test/resources/wands/snap_functions/test16.vpr
+++ /dev/null
@@ -1,30 +0,0 @@
-field f: Int
-field g: Int
-
-method test16a(xs: Seq[Ref], some: Ref, y: Ref)
-    requires forall x: Ref :: x in xs ==> acc(x.f)
-    requires some in xs && some.f == 0
-    requires acc(y.f)
-{
-    package acc(y.f) --* acc(some.f)
-
-    var completed: Seq[Ref] := Seq(some)
-    assert forall z: Ref :: z in completed ==> acc(y.f) --* acc(z.f)
-
-    apply acc(y.f) --* acc(some.f)
-    assert some.f == 0
-    //:: ExpectedOutput(assert.failed:assertion.false)
-    assert false
-}
-
-method test16b(y: Ref)
-    requires forall x: Ref :: acc(x.f) && acc(x.g)
-    requires y.f == 42
-    requires y.g > 0
-{
-    package (forall x: Ref :: acc(x.f) && acc(x.g)) --* acc(y.f) && acc(y.g)
-    apply (forall x: Ref :: acc(x.f) && acc(x.g)) --* acc(y.f) && acc(y.g)
-
-    assert y.f == 42
-    assert y.g > 0
-}

From 2f8d64b4e2e0d51b135f0d5a82a116be1bfb2095 Mon Sep 17 00:00:00 2001
From: Manuel Dublanc <19774382+manud99@users.noreply.github.com>
Date: Sun, 30 Jun 2024 10:25:43 +0200
Subject: [PATCH 16/16] Update annotations on quantified magic wand tests.

---
 src/test/resources/wands/mwsf/README.md       |  6 +-
 .../mwsf/applying-twice-quantified-wand.vpr   | 36 ++++++++
 ...-eq-rhs.vpr => basic-lhs-equal-to-rhs.vpr} |  0
 ...-rhs.vpr => basic-lhs-larger-than-rhs.vpr} |  0
 ...rhs.vpr => basic-lhs-smaller-than-rhs.vpr} |  0
 .../wands/mwsf/quantified-magic-wands.vpr     | 92 +++++++++++++++++++
 .../resources/wands/new_syntax/QPWands.vpr    |  4 +-
 7 files changed, 132 insertions(+), 6 deletions(-)
 rename src/test/resources/wands/mwsf/{basic-lhs-eq-rhs.vpr => basic-lhs-equal-to-rhs.vpr} (100%)
 rename src/test/resources/wands/mwsf/{basic-lhs-gt-rhs.vpr => basic-lhs-larger-than-rhs.vpr} (100%)
 rename src/test/resources/wands/mwsf/{basic-lhs-lt-rhs.vpr => basic-lhs-smaller-than-rhs.vpr} (100%)

diff --git a/src/test/resources/wands/mwsf/README.md b/src/test/resources/wands/mwsf/README.md
index c8c2e1634..53788dd77 100644
--- a/src/test/resources/wands/mwsf/README.md
+++ b/src/test/resources/wands/mwsf/README.md
@@ -8,9 +8,9 @@ This folder contains Viper test files that I used when working on MagicWandSnapF
 |----------------------------------------------------------------------------|-------------------------------------------------------------------------------------------------|-----------------|
 | [basic-bool.vpr](./basic-bool.vpr)                                         | Boolean Magic Wand with trivial LHS                                                             | ✓               |
 | [basic-int.vpr](./basic-int.vpr)                                           | Integer Magic Wand with trivial LHS                                                             | ✓               |
-| [basic-lhs-eq-rhs.vpr](./basic-lhs-eq-rhs.vpr)                             | Integer Magic Wand with LHS = RHS                                                               | ✓               |
-| [basic-lhs-lt-rhs.vpr](./basic-lhs-lt-rhs.vpr)                             | Integer Magic Wand with LHS < RHS                                                               | ✓               |
-| [basic-lhs-gt-rhs.vpr](./basic-lhs-gt-rhs.vpr)                             | Integer Magic Wand with LHS > RHS                                                               | ✓               |
+| [basic-lhs-eq-rhs.vpr](./basic-lhs-equal-to-rhs.vpr)                             | Integer Magic Wand with LHS = RHS                                                               | ✓               |
+| [basic-lhs-lt-rhs.vpr](./basic-lhs-smaller-than-rhs.vpr)                             | Integer Magic Wand with LHS < RHS                                                               | ✓               |
+| [basic-lhs-gt-rhs.vpr](./basic-lhs-larger-than-rhs.vpr)                             | Integer Magic Wand with LHS > RHS                                                               | ✓               |
 | [applying-twice-bool.vpr](./applying-twice-bool.vpr)                       | Applying the magic wand multiple times. Original version leaks information into the outer state | ×               |
 | [assign-applying-bool.vpr](./assign-applying-bool.vpr)                     | Assigning result of applying expression to the same field using booleans                        | ×               |
 | [assign-applying-int.vpr](./assign-applying-int.vpr)                       | Assigning result of applying expression to the same field using integers                        | ×               |
diff --git a/src/test/resources/wands/mwsf/applying-twice-quantified-wand.vpr b/src/test/resources/wands/mwsf/applying-twice-quantified-wand.vpr
index 1d90c212c..0c4aafed6 100644
--- a/src/test/resources/wands/mwsf/applying-twice-quantified-wand.vpr
+++ b/src/test/resources/wands/mwsf/applying-twice-quantified-wand.vpr
@@ -3,6 +3,16 @@
 
 field f: Int
 
+predicate Cell(x: Ref) {
+    acc(x.f)
+}
+
+function get(x: Ref): Int
+    requires acc(Cell(x), 1/2)
+{
+    unfolding acc(Cell(x), 1/2) in x.f
+}
+
 method test12a(xs: Seq[Ref], y: Ref)
     requires forall x: Ref :: x in xs ==> acc(x.f)
     requires |xs| >= 1
@@ -65,3 +75,29 @@ method test12c(xs: Seq[Ref], y: Ref)
     //:: ExpectedOutput(assert.failed:assertion.false)
     assert false
 }
+
+method test13a(xs: Seq[Ref], y: Ref)
+    requires forall x: Ref :: x in xs ==> Cell(x)
+    requires |xs| >= 1
+    requires Cell(y)
+{
+    var some: Ref := xs[0]
+
+    package Cell(some) --* true
+
+    var completed: Seq[Ref] := Seq(some)
+    assert forall x: Ref :: x in completed ==> Cell(x) --* true
+
+    unfold Cell(some)
+    some.f := 1
+    fold Cell(some)
+    assert applying (Cell(some) --* true) in true
+
+    unfold Cell(some)
+    some.f := 2
+    fold Cell(some)
+    assert applying (Cell(some) --* true) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
diff --git a/src/test/resources/wands/mwsf/basic-lhs-eq-rhs.vpr b/src/test/resources/wands/mwsf/basic-lhs-equal-to-rhs.vpr
similarity index 100%
rename from src/test/resources/wands/mwsf/basic-lhs-eq-rhs.vpr
rename to src/test/resources/wands/mwsf/basic-lhs-equal-to-rhs.vpr
diff --git a/src/test/resources/wands/mwsf/basic-lhs-gt-rhs.vpr b/src/test/resources/wands/mwsf/basic-lhs-larger-than-rhs.vpr
similarity index 100%
rename from src/test/resources/wands/mwsf/basic-lhs-gt-rhs.vpr
rename to src/test/resources/wands/mwsf/basic-lhs-larger-than-rhs.vpr
diff --git a/src/test/resources/wands/mwsf/basic-lhs-lt-rhs.vpr b/src/test/resources/wands/mwsf/basic-lhs-smaller-than-rhs.vpr
similarity index 100%
rename from src/test/resources/wands/mwsf/basic-lhs-lt-rhs.vpr
rename to src/test/resources/wands/mwsf/basic-lhs-smaller-than-rhs.vpr
diff --git a/src/test/resources/wands/mwsf/quantified-magic-wands.vpr b/src/test/resources/wands/mwsf/quantified-magic-wands.vpr
index 8c6f30fc2..a0445e71b 100644
--- a/src/test/resources/wands/mwsf/quantified-magic-wands.vpr
+++ b/src/test/resources/wands/mwsf/quantified-magic-wands.vpr
@@ -1,5 +1,15 @@
 field f: Int
 
+predicate Cell(x: Ref) {
+    acc(x.f)
+}
+
+function get(x: Ref): Int
+    requires acc(Cell(x), 1/2)
+{
+    unfolding acc(Cell(x), 1/2) in x.f
+}
+
 // Test adapted from QPWands.vpr test0
 method test0b(xs: Seq[Ref], y: Ref)
   requires forall x: Ref :: x in xs ==> acc(x.f)
@@ -68,3 +78,85 @@ method test16a(xs: Seq[Ref], some: Ref, y: Ref)
     //:: ExpectedOutput(assert.failed:assertion.false)
     assert false
 }
+
+method test16b(xs: Seq[Ref], some: Ref, y: Ref)
+    requires forall x: Ref :: x in xs ==> acc(x.f)
+    requires some in xs
+    requires acc(y.f) && y.f == 42
+{
+    package acc(y.f) --* acc(some.f) && acc(y.f)
+
+    var completed: Seq[Ref] := Seq(some)
+    assert forall z: Ref :: z in completed ==> acc(y.f) --* acc(z.f) && acc(y.f)
+
+    apply acc(y.f) --* acc(some.f) && acc(y.f)
+    assert y.f == 42
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
+
+method test16c(xs: Seq[Ref], some: Ref, y: Ref)
+    requires forall x: Ref :: x in xs ==> acc(x.f)
+    requires some in xs && some.f == 0
+    requires acc(y.f) && y.f == 42
+{
+    package acc(y.f) --* acc(some.f) && acc(y.f)
+
+    var completed: Seq[Ref] := Seq(some)
+    assert forall z: Ref :: z in completed ==> acc(y.f) --* acc(z.f) && acc(y.f)
+
+    apply acc(y.f) --* acc(some.f) && acc(y.f)
+    assert some.f == 0
+    assert y.f == 42
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
+
+method test17a(xs: Seq[Ref], some: Ref, y: Ref)
+    requires forall x: Ref :: x in xs ==> Cell(x)
+    requires some in xs && get(some) == 0
+    requires Cell(y)
+{
+    package Cell(y) --* Cell(some)
+
+    var completed: Seq[Ref] := Seq(some)
+    assert forall z: Ref :: z in completed ==> Cell(y) --* Cell(z)
+
+    apply Cell(y) --* Cell(some)
+    assert get(some) == 0
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
+
+method test17b(xs: Seq[Ref], some: Ref, y: Ref)
+    requires forall x: Ref :: x in xs ==> Cell(x)
+    requires some in xs
+    requires Cell(y) && get(y) == 42
+{
+    package Cell(y) --* Cell(some) && Cell(y)
+
+    var completed: Seq[Ref] := Seq(some)
+    assert forall z: Ref :: z in completed ==> Cell(y) --* Cell(z) && Cell(y)
+
+    apply Cell(y) --* Cell(some) && Cell(y)
+    assert get(y) == 42
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
+
+method test17c(xs: Seq[Ref], some: Ref, y: Ref)
+    requires forall x: Ref :: x in xs ==> Cell(x)
+    requires some in xs && get(some) == 0
+    requires Cell(y) && get(y) == 42
+{
+    package Cell(y) --* Cell(some) && Cell(y)
+
+    var completed: Seq[Ref] := Seq(some)
+    assert forall z: Ref :: z in completed ==> Cell(y) --* Cell(z) && Cell(y)
+
+    apply Cell(y) --* Cell(some) && Cell(y)
+    assert get(some) == 0
+    assert get(y) == 42
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
diff --git a/src/test/resources/wands/new_syntax/QPWands.vpr b/src/test/resources/wands/new_syntax/QPWands.vpr
index 13a12211f..c80743476 100644
--- a/src/test/resources/wands/new_syntax/QPWands.vpr
+++ b/src/test/resources/wands/new_syntax/QPWands.vpr
@@ -23,7 +23,6 @@ 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/000/)
     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) {
@@ -89,12 +88,11 @@ requires acc(y.f) {
     package acc(y.f) --* acc(some.f) && acc(y.f)
     var completed: Seq[Ref] := Seq(some)
     assert forall x: Ref :: x in completed ==> acc(y.f) --* acc(x.f) && acc(y.f)
-    //:: UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/000/)
     assert applying (acc(y.f) --* acc(some.f) && acc(y.f)) in some.f == 0
     assert applying (acc(y.f) --* acc(some.f) && acc(y.f)) in y.f == 1
     assert forall x: Ref :: x in xs[1..] ==> acc(x.f)
 
-    //:: MissingOutput(assert.failed:insufficient.permission, /silicon/issue/000/)
+    //:: ExpectedOutput(assert.failed:insufficient.permission)
     assert forall x: Ref :: x in xs ==> acc(x.f)
 }