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] 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
+}