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
 }
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
diff --git a/src/test/resources/wands/mwsf/README.md b/src/test/resources/wands/mwsf/README.md
new file mode 100644
index 000000000..53788dd77
--- /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-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                        | ×               |
+| [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/mwsf/applying-twice-bool.vpr b/src/test/resources/wands/mwsf/applying-twice-bool.vpr
new file mode 100644
index 000000000..2b666f1d6
--- /dev/null
+++ b/src/test/resources/wands/mwsf/applying-twice-bool.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/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/mwsf/applying-twice-qp-predicates.vpr b/src/test/resources/wands/mwsf/applying-twice-qp-predicates.vpr
new file mode 100644
index 000000000..db04268ae
--- /dev/null
+++ b/src/test/resources/wands/mwsf/applying-twice-qp-predicates.vpr
@@ -0,0 +1,73 @@
+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
+}
+
+// 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
+}
diff --git a/src/test/resources/wands/mwsf/applying-twice-quantified-lhs.vpr b/src/test/resources/wands/mwsf/applying-twice-quantified-lhs.vpr
new file mode 100644
index 000000000..c229473f5
--- /dev/null
+++ b/src/test/resources/wands/mwsf/applying-twice-quantified-lhs.vpr
@@ -0,0 +1,85 @@
+field f: Int
+
+method test13a(xs: Seq[Ref])
+    requires forall x: Ref :: x in xs ==> acc(x.f)
+    requires |xs| >= 1
+{
+    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])
+    requires forall x: Ref :: x in xs ==> acc(x.f)
+    requires |xs| >= 1
+{
+    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)
+}
diff --git a/src/test/resources/wands/mwsf/applying-twice-quantified-wand.vpr b/src/test/resources/wands/mwsf/applying-twice-quantified-wand.vpr
new file mode 100644
index 000000000..0c4aafed6
--- /dev/null
+++ b/src/test/resources/wands/mwsf/applying-twice-quantified-wand.vpr
@@ -0,0 +1,103 @@
+// Test cases showing unsound behaviour of current Viper
+// Related to wands/new_syntax/QPWands.vpr
+
+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
+    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)
+    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)
+    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)
+    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/assign-applying-bool.vpr b/src/test/resources/wands/mwsf/assign-applying-bool.vpr
new file mode 100644
index 000000000..f5c07ae7d
--- /dev/null
+++ b/src/test/resources/wands/mwsf/assign-applying-bool.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/mwsf/assign-applying-int.vpr b/src/test/resources/wands/mwsf/assign-applying-int.vpr
new file mode 100644
index 000000000..7a9185b0f
--- /dev/null
+++ b/src/test/resources/wands/mwsf/assign-applying-int.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/mwsf/basic-bool.vpr b/src/test/resources/wands/mwsf/basic-bool.vpr
new file mode 100644
index 000000000..5ede73fad
--- /dev/null
+++ b/src/test/resources/wands/mwsf/basic-bool.vpr
@@ -0,0 +1,50 @@
+field b: Bool
+
+method test01a(x: Ref)
+{
+    inhale acc(x.b) && x.b
+
+    package true --* acc(x.b)
+
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
+    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)
+
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
+    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)
+
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
+    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/mwsf/basic-int.vpr b/src/test/resources/wands/mwsf/basic-int.vpr
new file mode 100644
index 000000000..789669d7a
--- /dev/null
+++ b/src/test/resources/wands/mwsf/basic-int.vpr
@@ -0,0 +1,50 @@
+field f: Int
+
+method test02a(x: Ref)
+{
+    inhale acc(x.f) && x.f == 42
+
+    package true --* acc(x.f)
+
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
+    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)
+
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
+    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)
+
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
+    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/mwsf/basic-lhs-equal-to-rhs.vpr b/src/test/resources/wands/mwsf/basic-lhs-equal-to-rhs.vpr
new file mode 100644
index 000000000..e673a5984
--- /dev/null
+++ b/src/test/resources/wands/mwsf/basic-lhs-equal-to-rhs.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/mwsf/basic-lhs-larger-than-rhs.vpr b/src/test/resources/wands/mwsf/basic-lhs-larger-than-rhs.vpr
new file mode 100644
index 000000000..3ce73962d
--- /dev/null
+++ b/src/test/resources/wands/mwsf/basic-lhs-larger-than-rhs.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/mwsf/basic-lhs-smaller-than-rhs.vpr b/src/test/resources/wands/mwsf/basic-lhs-smaller-than-rhs.vpr
new file mode 100644
index 000000000..7c80ab883
--- /dev/null
+++ b/src/test/resources/wands/mwsf/basic-lhs-smaller-than-rhs.vpr
@@ -0,0 +1,50 @@
+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)
+
+    //:: 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
+}
+
+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)
+
+    //:: 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)
+
+    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)
+
+    //:: 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)
+
+    assert x.f == a && y.f == b
+}
\ No newline at end of file
diff --git a/src/test/resources/wands/mwsf/example-list.vpr b/src/test/resources/wands/mwsf/example-list.vpr
new file mode 100644
index 000000000..3e5751e7e
--- /dev/null
+++ b/src/test/resources/wands/mwsf/example-list.vpr
@@ -0,0 +1,89 @@
+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
+  //:: UnexpectedOutput(assert.failed:assertion.false, /Carbon/issue/000/)
+  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
+
+      //:: 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)
+
+        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)
+  }
+}
diff --git a/src/test/resources/wands/mwsf/inhaling-magic-wand.vpr b/src/test/resources/wands/mwsf/inhaling-magic-wand.vpr
new file mode 100644
index 000000000..081fbdbdd
--- /dev/null
+++ b/src/test/resources/wands/mwsf/inhaling-magic-wand.vpr
@@ -0,0 +1,27 @@
+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
+{
+    //:: 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
+}
+
+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/mwsf/predicates-in-magic-wands.vpr b/src/test/resources/wands/mwsf/predicates-in-magic-wands.vpr
new file mode 100644
index 000000000..7e01925a1
--- /dev/null
+++ b/src/test/resources/wands/mwsf/predicates-in-magic-wands.vpr
@@ -0,0 +1,31 @@
+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)
+
+    //:: 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/mwsf/quantified-magic-wands.vpr b/src/test/resources/wands/mwsf/quantified-magic-wands.vpr
new file mode 100644
index 000000000..a0445e71b
--- /dev/null
+++ b/src/test/resources/wands/mwsf/quantified-magic-wands.vpr
@@ -0,0 +1,162 @@
+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)
+  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)
+}
+
+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(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/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/new_syntax/QPWands.vpr b/src/test/resources/wands/new_syntax/QPWands.vpr
index a48a4660d..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
-
     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) {
@@ -97,6 +96,40 @@ requires acc(y.f) {
     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)
+
+    //:: ExpectedOutput(assert.failed:insufficient.permission)
+    assert forall x: Ref :: x in xs ==> acc(x.f)
+}
+
 method test6(xs: Seq[Ref])
 requires forall x: Ref :: x in xs ==> true --* acc(x.f)
 requires |xs| > 0 {