Add test case 16.

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)

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