Add unsound example illustrating issue viperproject/silicon#307.

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)

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