From 2209768c25920f11db43045af2e2a3e7b6cd7fb0 Mon Sep 17 00:00:00 2001
From: Marco Eilers <marcoeilers@users.noreply.github.com>
Date: Fri, 7 Jun 2024 17:31:39 +0200
Subject: [PATCH 01/13] Fixing issue #845 (#846)

Reusing more cached snapshot maps
---
 src/main/scala/rules/QuantifiedChunkSupport.scala | 4 ++--
 src/main/scala/state/SnapshotMapCache.scala       | 5 ++++-
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala
index 57929b71d..ae427d057 100644
--- a/src/main/scala/rules/QuantifiedChunkSupport.scala
+++ b/src/main/scala/rules/QuantifiedChunkSupport.scala
@@ -1287,7 +1287,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
             codomainQVars,
             relevantChunks,
             v1,
-            optSmDomainDefinitionCondition = if (s2.smDomainNeeded) Some(True) else None,
+            optSmDomainDefinitionCondition = None,
             optQVarsInstantiations = Some(arguments))
         val permsTaken = result match {
           case Complete() => rPerm
@@ -1332,7 +1332,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
               resource = resource,
               codomainQVars = codomainQVars,
               relevantChunks = relevantChunks,
-              optSmDomainDefinitionCondition = if (s1.smDomainNeeded) Some(True) else None,
+              optSmDomainDefinitionCondition = None,
               optQVarsInstantiations = Some(arguments),
               v = v)
           val s2 = s1.copy(functionRecorder = s1.functionRecorder.recordFvfAndDomain(smDef1),
diff --git a/src/main/scala/state/SnapshotMapCache.scala b/src/main/scala/state/SnapshotMapCache.scala
index 5a7f313ee..5672e453b 100644
--- a/src/main/scala/state/SnapshotMapCache.scala
+++ b/src/main/scala/state/SnapshotMapCache.scala
@@ -46,7 +46,10 @@ case class SnapshotMapCache private (
          : Option[SnapshotMapCache.Value] = {
 
     cache.get(key) match {
-      case Some((smDef, totalPermissions, `optSmDomainDefinitionCondition`)) =>
+      case Some((smDef, totalPermissions, cachedSmDomainDefinitionCondition))
+          if cachedSmDomainDefinitionCondition == optSmDomainDefinitionCondition ||  // defined under the same condition
+            (cachedSmDomainDefinitionCondition.contains(terms.True) && optSmDomainDefinitionCondition.isEmpty) // cached is always defined and we don't need a domain
+            =>
         Some((smDef, totalPermissions))
 
       case _ =>

From a036ba20c5d7222b6aa27f512f9b406cc75c82fd Mon Sep 17 00:00:00 2001
From: Silver Bot <bot@noreply.github.com>
Date: Tue, 11 Jun 2024 15:47:04 +0000
Subject: [PATCH 02/13] Update silver submodule

---
 silver | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/silver b/silver
index 1b588f0db..46513effe 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 1b588f0db96acd641a35c9eb1424acda80084561
+Subproject commit 46513effe745627f75684fdd8e0527415435cff6

From 4a0c07e5582a8362a986742f6b31cbfb2f93ae69 Mon Sep 17 00:00:00 2001
From: Silver Bot <bot@noreply.github.com>
Date: Tue, 11 Jun 2024 16:32:57 +0000
Subject: [PATCH 03/13] Update silver submodule

---
 silver | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/silver b/silver
index 46513effe..e51a7aad2 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 46513effe745627f75684fdd8e0527415435cff6
+Subproject commit e51a7aad25c1e8278913b777e7cd4d619a801bd6

From f8cc4843efa275189fa84dc8c735a80adb7421a3 Mon Sep 17 00:00:00 2001
From: manud99 <19774382+manud99@users.noreply.github.com>
Date: Wed, 12 Jun 2024 15:26:11 +0200
Subject: [PATCH 04/13] Use a Map from Snap to Snap to represent a magic wand
 snapshot. (#836)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* Use a Map from Snap to Snap to represent a magic wand snapshot.

* Fix failing test cases.

* Fix broken links in comments.

* First optimization: Create sort MagicWandSnapFunction (MWSF) with its own function definitions to replace wand maps.

* Second optimization: When there is no applying expression use the original approach using MagicWandSnapSingleton.

* Revert "Second optimization: When there is no applying expression use the original approach using MagicWandSnapSingleton."

This reverts commit fd87482c7f9af2d31f32add3ba77c221917640b7.

* Apply suggested changes from code review.

* Fix test cases with quasihavoc statements.

* Update submodule to use branch with both testcase changes

* Remove abstractLhs and rhsSnapshot from MagicWandSnapshot.

* Reduce diff

* Simplify havoc

* Simplify production of a MWSF.

* Rename variable in Producer.

* Update silver branch magic-wand-fixes.

---------

Co-authored-by: Jonáš Fiala <jonas.fiala@inf.ethz.ch>
---
 silver                                        |   2 +-
 ...agic_wand_snap_functions_declarations.smt2 |   1 +
 src/main/scala/Utils.scala                    |   1 +
 .../decider/TermToSMTLib2Converter.scala      |   7 +-
 .../scala/decider/TermToZ3APIConverter.scala  |   2 +
 src/main/scala/rules/HavocSupporter.scala     |  15 +-
 src/main/scala/rules/MagicWandSupporter.scala | 333 +++++++++++-------
 .../rules/MoreCompleteExhaleSupporter.scala   |   2 +-
 src/main/scala/rules/Producer.scala           |   2 +-
 .../scala/rules/QuantifiedChunkSupport.scala  |   1 -
 src/main/scala/state/Chunks.scala             |   7 +-
 src/main/scala/state/Terms.scala              | 108 +++---
 src/main/scala/state/Utils.scala              |   5 +-
 .../BuiltinDomainsContributor.scala           |  95 +++--
 .../MagicWandSnapFunctionsContributor.scala   |  92 +++++
 ...icateAndWandSnapFunctionsContributor.scala |   4 +-
 .../scala/verifier/DefaultMainVerifier.scala  |   7 +
 17 files changed, 442 insertions(+), 242 deletions(-)
 create mode 100644 src/main/resources/magic_wand_snap_functions_declarations.smt2
 create mode 100644 src/main/scala/supporters/MagicWandSnapFunctionsContributor.scala

diff --git a/silver b/silver
index e51a7aad2..d29ac2738 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit e51a7aad25c1e8278913b777e7cd4d619a801bd6
+Subproject commit d29ac2738d27232edaeb3d3a24952928f4006299
diff --git a/src/main/resources/magic_wand_snap_functions_declarations.smt2 b/src/main/resources/magic_wand_snap_functions_declarations.smt2
new file mode 100644
index 000000000..988585407
--- /dev/null
+++ b/src/main/resources/magic_wand_snap_functions_declarations.smt2
@@ -0,0 +1 @@
+(declare-fun MWSF_apply ($MWSF $Snap) $Snap)
diff --git a/src/main/scala/Utils.scala b/src/main/scala/Utils.scala
index 56a773538..f7f817f2d 100644
--- a/src/main/scala/Utils.scala
+++ b/src/main/scala/Utils.scala
@@ -222,6 +222,7 @@ package object utils {
     case class ViperEmbedding(embeddedSort: Sort) extends silver.ast.ExtensionType {
       def substitute(typVarsMap: Predef.Map[silver.ast.TypeVar, silver.ast.Type]): silver.ast.Type = this
       def isConcrete: Boolean = true
+      override def toString: String = s"ViperEmbedding(sorts.$embeddedSort)"
     }
   }
 
diff --git a/src/main/scala/decider/TermToSMTLib2Converter.scala b/src/main/scala/decider/TermToSMTLib2Converter.scala
index b8f6c0f89..d876d1db7 100644
--- a/src/main/scala/decider/TermToSMTLib2Converter.scala
+++ b/src/main/scala/decider/TermToSMTLib2Converter.scala
@@ -61,6 +61,8 @@ class TermToSMTLib2Converter
 
     case sorts.FieldPermFunction() => text("$FPM")
     case sorts.PredicatePermFunction() => text("$PPM")
+
+    case sorts.MagicWandSnapFunction => text("$MWSF")
   }
 
   def convert(d: Decl): String = {
@@ -263,7 +265,7 @@ class TermToSMTLib2Converter
 
     case Lookup(field, fvf, at) => //fvf.sort match {
 //      case _: sorts.PartialFieldValueFunction =>
-        parens(text("$FVF.lookup_") <> field <+> render(fvf) <+> render(at))
+      parens(text("$FVF.lookup_") <> field <+> render(fvf) <+> render(at))
 //      case _: sorts.TotalFieldValueFunction =>
 //        render(Apply(fvf, Seq(at)))
 //        parens("$FVF.lookup_" <> field <+> render(fvf) <+> render(at))
@@ -313,6 +315,9 @@ class TermToSMTLib2Converter
       val docBindings = ssep((bindings.toSeq map (p => parens(render(p._1) <+> render(p._2)))).to(collection.immutable.Seq), space)
       parens(text("let") <+> parens(docBindings) <+> render(body))
 
+    case MagicWandSnapshot(mwsf) => render(mwsf)
+    case MWSFLookup(mwsf, snap) => renderApp("MWSF_apply", Seq(mwsf, snap), sorts.Snap)
+
     case _: MagicWandChunkTerm
        | _: Quantification =>
       sys.error(s"Unexpected term $term cannot be translated to SMTLib code")
diff --git a/src/main/scala/decider/TermToZ3APIConverter.scala b/src/main/scala/decider/TermToZ3APIConverter.scala
index 3766ee49f..152bf1d64 100644
--- a/src/main/scala/decider/TermToZ3APIConverter.scala
+++ b/src/main/scala/decider/TermToZ3APIConverter.scala
@@ -445,6 +445,8 @@ class TermToZ3APIConverter
       case Let(bindings, body) =>
         convert(body.replace(bindings))
 
+      case MWSFLookup(mwsf, snap) => createApp("MWSF_apply", Seq(mwsf, snap), sorts.Snap)
+
       case _: MagicWandChunkTerm
          | _: Quantification =>
         sys.error(s"Unexpected term $term cannot be translated to SMTLib code")
diff --git a/src/main/scala/rules/HavocSupporter.scala b/src/main/scala/rules/HavocSupporter.scala
index e23472e23..d146c72ee 100644
--- a/src/main/scala/rules/HavocSupporter.scala
+++ b/src/main/scala/rules/HavocSupporter.scala
@@ -181,10 +181,17 @@ object havocSupporter extends SymbolicExecutionRules {
     val id = ChunkIdentifier(resource, s.program)
     val (relevantChunks, otherChunks) = chunkSupporter.splitHeap[NonQuantifiedChunk](s.h, id)
 
-    val newChunks = relevantChunks.map { ch =>
-      val havockedSnap = freshSnap(ch.snap.sort, v)
-      val cond = replacementCond(lhs, ch.args, condInfo)
-      ch.withSnap(Ite(cond, havockedSnap, ch.snap))
+    val newChunks = relevantChunks.map {
+      case ch: MagicWandChunk =>
+        val havockedSnap = v.decider.fresh("mwsf", sorts.MagicWandSnapFunction)
+        val cond = replacementCond(lhs, ch.args, condInfo)
+        val magicWandSnapshot = MagicWandSnapshot(Ite(cond, havockedSnap, ch.snap.mwsf))
+        ch.withSnap(magicWandSnapshot)
+
+      case ch =>
+        val havockedSnap = freshSnap(ch.snap.sort, v)
+        val cond = replacementCond(lhs, ch.args, condInfo)
+        ch.withSnap(Ite(cond, havockedSnap, ch.snap))
     }
     otherChunks ++ newChunks
   }
diff --git a/src/main/scala/rules/MagicWandSupporter.scala b/src/main/scala/rules/MagicWandSupporter.scala
index 844f67a74..98ade45ff 100644
--- a/src/main/scala/rules/MagicWandSupporter.scala
+++ b/src/main/scala/rules/MagicWandSupporter.scala
@@ -79,25 +79,9 @@ object magicWandSupporter extends SymbolicExecutionRules {
 //    result
 //  }
 
-  //TODO: needs to calculate a snapshot that preserves values from the lhs
-  def createChunk(s: State,
-                  wand: ast.MagicWand,
-                  pve: PartialVerificationError,
-                  v: Verifier)
-                  (Q: (State, MagicWandChunk, Verifier) => VerificationResult)
-                  : VerificationResult =
-    createChunk(s, wand, MagicWandSnapshot(freshSnap(sorts.Snap, v), freshSnap(sorts.Snap, v)), pve, v)(Q)
-
-  def createChunk(s: State,
-                  wand: ast.MagicWand,
-                  abstractLhs: Term,
-                  rhsSnapshot: Term,
-                  pve: PartialVerificationError,
-                  v: Verifier)
-                  (Q: (State, MagicWandChunk, Verifier) => VerificationResult)
-                  : VerificationResult =
-    createChunk(s, wand, MagicWandSnapshot(abstractLhs, rhsSnapshot), pve, v)(Q)
-
+  /**
+   * Evaluate the wand's arguments and create a [[viper.silicon.state.MagicWandChunk]] out of it.
+   */
   def createChunk(s: State,
                   wand: ast.MagicWand,
                   snap: MagicWandSnapshot,
@@ -110,6 +94,37 @@ object magicWandSupporter extends SymbolicExecutionRules {
     )
   }
 
+  /**
+   * Create a new [[viper.silicon.state.terms.MagicWandSnapshot]]
+   * and add the corresponding [[viper.silicon.state.terms.sorts.MagicWandSnapFunction]] definition to the state.
+   *
+   * It defines that when we apply the MagicWandSnapFunction to a snapshot `snap`
+   * we will get back `rhsSnapshot` that includes the values from that snapshot `snap`.
+   *
+   * @param abstractLhs The term that represent the snapshot of the consumed left-hand side of the magic wand.
+   *                    It is used as a bound variable in a forall quantifier.
+   * @param rhsSnapshot The term that integrates the left-hand side in the snapshot that is produced after applying the magic wand.
+   * @param v           Verifier instance
+   * @return Fresh instance of [[viper.silicon.state.terms.MagicWandSnapshot]]
+   */
+  def createMagicWandSnapshot(abstractLhs: Var, rhsSnapshot: Term, v: Verifier): MagicWandSnapshot = {
+    val mwsf = v.decider.fresh("mwsf", sorts.MagicWandSnapFunction)
+    val magicWandSnapshot = MagicWandSnapshot(mwsf)
+    v.decider.assumeDefinition(Forall(
+      abstractLhs,
+      MWSFLookup(mwsf, abstractLhs) === rhsSnapshot,
+      Trigger(MWSFLookup(mwsf, abstractLhs))
+    ))
+    magicWandSnapshot
+  }
+
+  /**
+   * Evaluate all expressions inside the given magic wand instance in the current state.
+   *
+   * @param s State in which to expressions are evaluated.
+   * @param wand Magic Wand instance.
+   * @param Q Method whose second argument is used to return the evaluated terms of all expressions.
+   */
   def evaluateWandArguments(s: State,
                             wand: ast.MagicWand,
                             pve: PartialVerificationError,
@@ -147,7 +162,7 @@ object magicWandSupporter extends SymbolicExecutionRules {
     val initial = (initialConsumptionResult, s, Stack.empty[Heap], Stack.empty[Option[CH]])
     val (result, s1, heaps, consumedChunks) =
       hs.foldLeft[(ConsumptionResult, State, Stack[Heap], Stack[Option[CH]])](initial)((partialResult, heap) =>
-        partialResult match  {
+        partialResult match {
           case (r: Complete, sIn, hps, cchs)  => (r, sIn, heap +: hps, None +: cchs)
           case (Incomplete(permsNeeded), sIn, hps, cchs) =>
             val (success, sOut, h, cch) = consumeFunction(sIn, heap, permsNeeded, v)
@@ -191,9 +206,25 @@ object magicWandSupporter extends SymbolicExecutionRules {
     }
   }
 
-//  private var cnt = 0L
-//  private val packageLogger = LoggerFactory.getLogger("package")
-
+  /**
+   * Package a magic wand into a chunk. It performs the computation of the wand's footprint
+   * and captures all values associated to these locations inside the wand's snapshot.
+   *
+   * {{{
+   * package A --* B { <proofScript> }
+   * }}}
+   *
+   * For reference see Chapter 3 and 5 of [[http://malte.schwerhoff.de/docs/phd_thesis.pdf Malte Schwerhoff's PhD thesis]]
+   * and [[https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Education/Theses/Nils_Becker_BA_report.pdf Nils Becker's Bachelor report]]
+   *
+   * @param state Current state.
+   * @param wand AST representation of the magic wand.
+   * @param proofScript AST of the proof script. The proof script contains instructions how we can construct the RHS given the LHS.
+   * @param pve Partial Verification Error that is used to report errors.
+   * @param v Verifier instance.
+   * @param Q Continuation-style function that is called with the resulting state and the chunk that was created.
+   * @return Result of the overall verification process.
+   */
   def packageWand(state: State,
                   wand: ast.MagicWand,
                   proofScript: ast.Seqn,
@@ -202,42 +233,16 @@ object magicWandSupporter extends SymbolicExecutionRules {
                  (Q: (State, Chunk, Verifier) => VerificationResult)
                  : VerificationResult = {
 
-    /* TODO: Logging code is very similar to that in HeuristicsSupporter. Unify. */
-
-//    val myId = cnt; cnt += 1
-//    val baseIdent = "  "
-//    var printedHeader = false
-
-//    def lnsay(msg: String, ident: Int = 1) {
-//      val prefix = "\n" + (if (ident == 0) "" else baseIdent)
-//      dosay(prefix, msg, ident - 1)
-//    }
-//
-//    def say(msg: String, ident: Int = 1) {
-//      val prefix = if (ident == 0) "" else baseIdent
-//      dosay(prefix, msg, ident - 1)
-//    }
-//
-//    def dosay(prefix: String, msg: String, ident: Int) {
-//      if (!printedHeader) {
-//        packageLogger.debug(s"\n[packageWand $myId]")
-//        printedHeader = true
-//      }
-//
-//      val messagePrefix = baseIdent * ident
-//      packageLogger.debug(s"$prefix$messagePrefix $msg")
-//    }
-//
-//    say(s"wand = $wand")
-//    say("c.reserveHeaps:")
-//    s.reserveHeaps.map(v.stateFormatter.format).foreach(str => say(str, 2))
-
     val s = if (state.exhaleExt) state else
       state.copy(reserveHeaps = Heap() :: state.h :: Nil)
 
+    // v.logger.debug(s"wand = $wand")
+    // v.logger.debug("c.reserveHeaps:")
+    // s.reserveHeaps.map(v.stateFormatter.format).foreach(str => v.logger.debug(str, 2))
+
     val stackSize = 3 + s.reserveHeaps.tail.size
-      /* IMPORTANT: Size matches structure of reserveHeaps at [State RHS] below */
-    var results: Seq[(State, Stack[Term], Stack[Option[Exp]], Vector[RecordedPathConditions], Chunk)] = Nil
+    // IMPORTANT: Size matches structure of reserveHeaps at [State RHS] below
+    var recordedBranches: Seq[(State, Stack[Term], Stack[Option[Exp]], Vector[Term], Chunk)] = Nil
 
     /* TODO: When parallelising branches, some of the runtime assertions in the code below crash
      *       during some executions - since such crashes are hard to debug, branch parallelisation
@@ -250,67 +255,84 @@ object magicWandSupporter extends SymbolicExecutionRules {
                       recordPcs = true,
                       parallelizeBranches = false)
 
-    def createWandChunkAndRecordResults(s4: State,
-                                        freshSnapRoot: Var,
-                                        snap: Term,
-                                        v3: Verifier)
-                                       : VerificationResult = {
+    def appendToResults(s5: State, ch: Chunk, pcs: RecordedPathConditions, conservedPcs: Vector[Term], v4: Verifier): Unit = {
+      assert(s5.conservedPcs.nonEmpty, s"Unexpected structure of s5.conservedPcs: ${s5.conservedPcs}")
 
-      def appendToResults(s5: State, ch: Chunk, pcs: RecordedPathConditions, v4: Verifier): Unit = {
-        assert(s5.conservedPcs.nonEmpty, s"Unexpected structure of s5.conservedPcs: ${s5.conservedPcs}")
+      var conservedPcsStack: Stack[Vector[RecordedPathConditions]] = s5.conservedPcs
 
-        var conservedPcs: Vector[RecordedPathConditions] = Vector.empty
-        var conservedPcsStack: Stack[Vector[RecordedPathConditions]] = s5.conservedPcs
+      // Producing a wand's LHS and executing the packaging proof code can introduce definitional path conditions, e.g.
+      // new permission and snapshot maps, which are in general necessary to proceed after the
+      // package statement, e.g. to know which permissions have been consumed.
+      // Here, we want to keep *only* the definitions, but no other path conditions.
 
-        // Producing a wand's LHS and executing the packaging proof code can introduce definitional path conditions, e.g.
-        // new permission and snapshot maps, which are in general necessary to proceed after the
-        // package statement, e.g. to know which permissions have been consumed.
-        // Here, we want to keep *only* the definitions, but no other path conditions.
+      conservedPcsStack =
+        s5.conservedPcs.tail match {
+          case empty @ Seq() => empty
+          case head +: tail => (head ++ (s5.conservedPcs.head :+ pcs.definitionsOnly)) +: tail
+        }
 
-        conservedPcs = s5.conservedPcs.head :+ pcs.definitionsOnly
+      val s6 = s5.copy(conservedPcs = conservedPcsStack, recordPcs = s.recordPcs)
 
-        conservedPcsStack =
-          s5.conservedPcs.tail match {
-            case empty @ Seq() => empty
-            case head +: tail => (head ++ conservedPcs) +: tail
-          }
+      recordedBranches :+= (s6, v4.decider.pcs.branchConditions, v4.decider.pcs.branchConditionExps, conservedPcs, ch)
+    }
 
-        val s6 = s5.copy(conservedPcs = conservedPcsStack, recordPcs = s.recordPcs)
+    def createWandChunkAndRecordResults(s4: State,
+                                        freshSnapRoot: Var,
+                                        snapRhs: Term,
+                                        v3: Verifier)
+                                       : VerificationResult = {
+      val preMark = v3.decider.setPathConditionMark()
 
-        results :+= (s6, v4.decider.pcs.branchConditions, v4.decider.pcs.branchConditionExps, conservedPcs, ch)
-      }
+      v3.decider.prover.comment(s"Create MagicWandSnapFunction for wand $wand")
+      val wandSnapshot = this.createMagicWandSnapshot(freshSnapRoot, snapRhs, v3)
 
-      val preMark = v3.decider.setPathConditionMark()
+      // If the wand is used as a quantified resource anywhere in the program
       if (s4.qpMagicWands.contains(MagicWandIdentifier(wand, s.program))) {
         val bodyVars = wand.subexpressionsToEvaluate(s.program)
         val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ), false))
+
         evals(s4, bodyVars, _ => pve, v3)((s5, args, v4) => {
-          val (sm, smValueDef) =
-            quantifiedChunkSupporter.singletonSnapshotMap(s5, wand, args, MagicWandSnapshot(freshSnapRoot, snap), v4)
+          val snapshotTerm = Combine(freshSnapRoot, snapRhs)
+          val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s5, wand, args, snapshotTerm, v4)
           v4.decider.prover.comment("Definitional axioms for singleton-SM's value")
           v4.decider.assumeDefinition(smValueDef)
           val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalVars, wand, args, FullPerm, sm, s.program)
-          appendToResults(s5, ch, v4.decider.pcs.after(preMark), v4)
+          val conservedPcs = (s5.conservedPcs.head :+ v4.decider.pcs.after(preMark).definitionsOnly).flatMap(_.conditionalized)
+          appendToResults(s5, ch, v4.decider.pcs.after(preMark), conservedPcs, v4)
           Success()
         })
       } else {
-        magicWandSupporter.createChunk(s4, wand, freshSnapRoot, snap, pve, v3)((s5, ch, v4) => {
-//          say(s"done: create wand chunk: $ch")
-          appendToResults(s5, ch, v4.decider.pcs.after(preMark), v4)
+        this.createChunk(s4, wand, wandSnapshot, pve, v3)((s5, ch, v4) => {
+          val conservedPcs = s5.conservedPcs.head :+ v4.decider.pcs.after(preMark).definitionsOnly
+          // Partition path conditions into a set which include the freshSnapRoot and those which do not
+          val (pcsWithFreshSnapRoot, pcsWithoutFreshSnapRoot) = conservedPcs.flatMap(_.conditionalized).partition(pcs => pcs.contains(freshSnapRoot))
+          // For all path conditions which include the freshSnapRoot, add those as part of the definition of the MWSF in the same forall quantifier
+          val pcsQuantified = Forall(
+            freshSnapRoot,
+            And(pcsWithFreshSnapRoot.map {
+              // Remove forall quantifiers with the same quantified variable
+              case Quantification(Forall, v :: Nil, body: Term, _, _, _, _) if v == freshSnapRoot => body
+              case p => p
+            }),
+            Trigger(MWSFLookup(wandSnapshot.mwsf, freshSnapRoot)),
+          )
+
+          appendToResults(s5, ch, v4.decider.pcs.after(preMark), pcsQuantified +: pcsWithoutFreshSnapRoot, v4)
           Success()
         })
       }
     }
 
-    val r = executionFlowController.locally(sEmp, v)((s1, v1) => {
-      /* Using conservingSnapshotGeneration a snapshot (binary tree) will be
-       * constructed using First/Second datatypes, that preserves the original root.
-       * The leafs of this tree will later appear in the snapshot of the rhs at the
-       * appropriate places. Thus equating freshSnapRoot with the snapshot received
-       * from consuming the lhs when applying the wand preserves values from the lhs
-       * into the rhs.
+    val tempResult = executionFlowController.locally(sEmp, v)((s1, v1) => {
+      /* A snapshot (binary tree) will be constructed using First/Second datatypes,
+       * that preserves the original root. The leafs of this tree will later appear
+       * in the snapshot of the RHS at the appropriate places. Thus equating
+       * `freshSnapRoot` with the snapshot received from consuming the LHS when
+       * applying the wand preserves values from the LHS into the RHS.
        */
       val freshSnapRoot = freshSnap(sorts.Snap, v1)
+
+      // Produce the wand's LHS.
       produce(s1.copy(conservingSnapshotGeneration = true), toSf(freshSnapRoot), wand.left, pve, v1)((sLhs, v2) => {
         val proofScriptCfg = proofScript.toCfg()
 
@@ -331,26 +353,31 @@ object magicWandSupporter extends SymbolicExecutionRules {
          * empty, and where the dots represent the heaps belonging to surrounding package/packaging
          * operations. hOps will be populated while processing the RHS of the wand to package.
          * More precisely, each ghost operation (folding, applying, etc.) that is executed
-         * populates hUsed (by transferring permissions from heaps lower in the stack, and by
-         * adding new chunks, e.g. a folded predicate) during its execution, and afterwards
-         * merges hUsed and hOps, the result of which replaces hOps, and hUsed is replaced by a
-         * new empty heap (see also the final state updates in, e.g. method `applyingWand`
-         * or `unfoldingPredicate` below).
+         * populates hUsed during its execution. This is done by transferring permissions
+         * from heaps lower in the stack, and by adding new chunks, e.g. a folded predicate.
+         * Afterwards, it merges hUsed and hOps, which replaces hOps. hUsed is replaced by a
+         * new empty heap. See also the final state updates in, e.g. method `applyingWand`
+         * or `unfoldingPredicate` below.
          */
         assert(stackSize == s2.reserveHeaps.length)
 
-//        say(s"done: produced LHS ${wand.left}")
-//        say(s"next: consume RHS ${wand.right}")
+        // Execute proof script, i.e. the part written after the magic wand wrapped by curly braces.
+        // The proof script should transform the current state such that we can consume the wand's RHS.
         executor.exec(s2, proofScriptCfg, v2)((proofScriptState, proofScriptVerifier) => {
-          consume(proofScriptState.copy(oldHeaps = s2.oldHeaps, reserveCfgs = proofScriptState.reserveCfgs.tail), wand.right, pve, proofScriptVerifier)((s3, snap, v3) => {
-//            say(s"done: consumed RHS ${wand.right}")
-            val s4 = s3.copy(//h = s.h, /* Temporarily */
-                             exhaleExt = false,
-                             oldHeaps = s.oldHeaps)
-//            say(s"next: create wand chunk")
-            createWandChunkAndRecordResults(s4, freshSnapRoot, snap, v3)})})})})
-
-    if (results.isEmpty) {
+          // Consume the wand's RHS and produce a snapshot which records all the values of variables on the RHS.
+          // This part indirectly calls the methods `this.transfer` and `this.consumeFromMultipleHeaps`.
+          consume(
+            proofScriptState.copy(oldHeaps = s2.oldHeaps, reserveCfgs = proofScriptState.reserveCfgs.tail),
+            wand.right, pve, proofScriptVerifier
+          )((s3, snapRhs, v3) => {
+
+            createWandChunkAndRecordResults(s3.copy(exhaleExt = false, oldHeaps = s.oldHeaps), freshSnapRoot, snapRhs, v3)
+          })
+        })
+      })
+    })
+
+    if (recordedBranches.isEmpty) {
       // No results mean that packaging the wand resulted in inconsistent states on all paths,
       // and thus, that no wand chunk was created. In order to continue, we create one now.
       // Moreover, we need to set reserveHeaps to structurally match [State RHS] below.
@@ -358,41 +385,83 @@ object magicWandSupporter extends SymbolicExecutionRules {
       createWandChunkAndRecordResults(s1, freshSnap(sorts.Snap, v), freshSnap(sorts.Snap, v), v)
     }
 
-    results.foldLeft(r)((res, packageOut) => {
-      res && {
-        val state = packageOut._1
-        val branchConditions = packageOut._2
-        val branchConditionsExp = packageOut._3
-        val conservedPcs = packageOut._4
-        val magicWandChunk = packageOut._5
-        val s1 = state.copy(reserveHeaps = state.reserveHeaps.drop(3),
+    recordedBranches.foldLeft(tempResult)((prevRes, recordedState) => {
+      prevRes && {
+        val (state, branchConditions, branchConditionsExp, conservedPcs, magicWandChunk) = recordedState
+        val s1 = state.copy(
+          reserveHeaps = state.reserveHeaps.drop(3),
           parallelizeBranches = s.parallelizeBranches /* See comment above */
-          /*branchConditions = c.branchConditions*/)
+        )
+
+        // We execute the continuation Q in a new scope with all branch conditions and all conserved path conditions.
         executionFlowController.locally(s1, v)((s2, v1) => {
+          // Set the branch conditions
           v1.decider.setCurrentBranchCondition(And(branchConditions), Some(viper.silicon.utils.ast.BigAnd(branchConditionsExp.flatten)))
-          conservedPcs.foreach(pcs => v1.decider.assume(pcs.conditionalized))
-          Q(s2, magicWandChunk, v1)})}})
+
+          // Recreate all path conditions in the Z3 proof script that we recorded for that branch
+          conservedPcs.foreach(pcs => v1.decider.assume(pcs))
+
+          // Execute the continuation Q
+          Q(s2, magicWandChunk, v1)
+        })
+      }
+    })
   }
 
+  /**
+   * Apply a magic wand to the current state. This consumes the magic wand itself and the LHS of the wand, and then produces the RHS.
+   *
+   * @param s Current state.
+   * @param wand The AST instance of the magic wand to apply.
+   * @param pve Partial Verification Error that is used to report errors.
+   * @param v Verifier instance.
+   * @param Q Continuation-style function that is called with the resulting state and the verification result.
+   * @return Result of the overall verification process.
+   */
   def applyWand(s: State,
                 wand: ast.MagicWand,
                 pve: PartialVerificationError,
                 v: Verifier)
                (Q: (State, Verifier) => VerificationResult)
                : VerificationResult = {
-        consume(s, wand, pve, v)((s1, snap, v1) => {
-          val wandSnap = MagicWandSnapshot(snap)
-          consume(s1, wand.left, pve, v1)((s2, snap, v2) => {
-            /* It is assumed that snap and wandSnap.abstractLhs are structurally the same.
-             * Since a wand can only be applied once, equating the two snapshots is sound.
-             */
-            assert(snap.sort == sorts.Snap, s"expected snapshot but found: $snap")
-            v2.decider.assume(snap === wandSnap.abstractLhs)
-            val s3 = s2.copy(oldHeaps = s1.oldHeaps + (Verifier.MAGIC_WAND_LHS_STATE_LABEL -> magicWandSupporter.getEvalHeap(s1)))
-            produce(s3.copy(conservingSnapshotGeneration = true), toSf(wandSnap.rhsSnapshot), wand.right, pve, v2)((s4, v3) => {
-              val s5 = s4.copy(g = s1.g, conservingSnapshotGeneration = s3.conservingSnapshotGeneration)
-              val s6 = v3.stateConsolidator(s5).consolidate(s5, v3).copy(oldHeaps = s1.oldHeaps)
-              Q(s6, v3)})})})}
+    // Consume the magic wand instance "A --* B".
+    consume(s, wand, pve, v)((s1, snapWand, v1) => {
+      // Consume the wand's LHS "A".
+      consume(s1, wand.left, pve, v1)((s2, snapLhs, v2) => {
+        /* It is assumed that snap and MagicWandSnapshot.abstractLhs are structurally the same.
+         * Equating the two snapshots is sound iff a wand is applied only once.
+         * The old solution in this case did use this assumption:
+         * v2.decider.assume(snap === snapWand.abstractLhs)
+         */
+        assert(snapLhs.sort == sorts.Snap, s"expected snapshot but found: $snapLhs")
+
+        // Create copy of the state with a new labelled heap (i.e. `oldHeaps`) called "lhs".
+        val s3 = s2.copy(oldHeaps = s1.oldHeaps + (Verifier.MAGIC_WAND_LHS_STATE_LABEL -> this.getEvalHeap(s1)))
+
+        // If the snapWand is a (wrapped) MagicWandSnapshot then lookup the snapshot of the right-hand side by applying snapLhs.
+        val magicWandSnapshotLookup = snapWand match {
+          case snapshot: MagicWandSnapshot => snapshot.applyToMWSF(snapLhs)
+          case SortWrapper(snapshot: MagicWandSnapshot, _) => snapshot.applyToMWSF(snapLhs)
+          // Fallback solution for quantified magic wands
+          case predicateLookup: PredicateLookup =>
+            v2.decider.assume(snapLhs === First(snapWand))
+            Second(predicateLookup)
+          case _ => snapWand
+        }
+
+        // Produce the wand's RHS.
+        produce(s3.copy(conservingSnapshotGeneration = true), toSf(magicWandSnapshotLookup), wand.right, pve, v2)((s4, v3) => {
+          // Recreate old state without the magic wand, and the state with the oldHeap called lhs.
+          val s5 = s4.copy(g = s1.g, conservingSnapshotGeneration = s3.conservingSnapshotGeneration)
+
+          // Consolidate the state and remove labelled old heap "lhs".
+          val s6 = v3.stateConsolidator(s5).consolidate(s5, v3).copy(oldHeaps = s1.oldHeaps)
+
+          Q(s6, v3)
+        })
+      })
+    })
+  }
 
   def transfer[CH <: Chunk]
               (s: State,
@@ -416,7 +485,7 @@ object magicWandSupporter extends SymbolicExecutionRules {
      */
     val preMark = v.decider.setPathConditionMark()
     executionFlowController.tryOrFail2[Stack[Heap], Stack[Option[CH]]](s, v)((s1, v1, QS) =>
-      magicWandSupporter.consumeFromMultipleHeaps(s1, s1.reserveHeaps.tail, perms, failure, qvars, v1)(consumeFunction)(QS)
+      this.consumeFromMultipleHeaps(s1, s1.reserveHeaps.tail, perms, failure, qvars, v1)(consumeFunction)(QS)
     )((s2, hs2, chs2, v2) => {
       val conservedPcs = s2.conservedPcs.head :+ v2.decider.pcs.after(preMark)
       val s3 = s2.copy(conservedPcs = conservedPcs +: s2.conservedPcs.tail, reserveHeaps = s.reserveHeaps.head +: hs2)
diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala
index 5c7173c8a..8e983f573 100644
--- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala
+++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala
@@ -55,7 +55,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
       resource match {
         case f: ast.Field => v.symbolConverter.toSort(f.typ)
         case _: ast.Predicate => sorts.Snap
-        case _: ast.MagicWand => sorts.Snap
+        case _: ast.MagicWand => sorts.MagicWandSnapFunction
       }
 
     val `?s` = Var(Identifier("?s"), sort, false)
diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala
index 33d8a1126..f3976c827 100644
--- a/src/main/scala/rules/Producer.scala
+++ b/src/main/scala/rules/Producer.scala
@@ -397,7 +397,7 @@ object producer extends ProductionRules {
           Q(s2, v1)})
 
       case wand: ast.MagicWand =>
-        val snap = sf(sorts.Snap, v)
+        val snap = sf(sorts.MagicWandSnapFunction, v)
         magicWandSupporter.createChunk(s, wand, MagicWandSnapshot(snap), pve, v)((s1, chWand, v1) =>
           chunkSupporter.produce(s1, s1.h, chWand, v1)((s2, h2, v2) =>
             Q(s2.copy(h = h2), v2)))
diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala
index ae427d057..4f8902dbc 100644
--- a/src/main/scala/rules/QuantifiedChunkSupport.scala
+++ b/src/main/scala/rules/QuantifiedChunkSupport.scala
@@ -637,7 +637,6 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
 
   /* Snapshots */
 
-  /** @inheritdoc */
   def singletonSnapshotMap(s: State,
                            resource: ast.Resource,
                            arguments: Seq[Term],
diff --git a/src/main/scala/state/Chunks.scala b/src/main/scala/state/Chunks.scala
index 2385d7935..44b907031 100644
--- a/src/main/scala/state/Chunks.scala
+++ b/src/main/scala/state/Chunks.scala
@@ -176,13 +176,16 @@ case class MagicWandChunk(id: MagicWandIdentifier,
   override val resourceID = MagicWandID
 
   override def withPerm(newPerm: Term) = MagicWandChunk(id, bindings, args, snap, newPerm)
-  override def withSnap(newSnap: Term) = MagicWandChunk(id, bindings, args, MagicWandSnapshot(newSnap), perm)
+  override def withSnap(newSnap: Term) = newSnap match {
+    case s: MagicWandSnapshot => MagicWandChunk(id, bindings, args, s, perm)
+    case _ => sys.error(s"MagicWand snapshot has to be of type MagicWandSnapshot but found ${newSnap.getClass}")
+  }
 
   override lazy val toString = {
     val pos = id.ghostFreeWand.pos match {
       case rp: viper.silver.ast.HasLineColumn => s"${rp.line}:${rp.column}"
       case other => other.toString
     }
-    s"wand@$pos[$snap; ${args.mkString(",")}]"
+    s"wand@$pos[$snap; ${args.mkString(", ")}]"
   }
 }
diff --git a/src/main/scala/state/Terms.scala b/src/main/scala/state/Terms.scala
index ed00e5541..e08f4854b 100644
--- a/src/main/scala/state/Terms.scala
+++ b/src/main/scala/state/Terms.scala
@@ -76,6 +76,11 @@ object sorts {
     override lazy val toString = id.toString
   }
 
+  object MagicWandSnapFunction extends Sort {
+    val id: Identifier = Identifier("MWSF")
+    override lazy val toString: String = id.toString
+  }
+
   case class FieldPermFunction() extends Sort  {
     val id = Identifier("FPM")
     override lazy val toString = id.toString
@@ -321,39 +326,39 @@ sealed trait Term extends Node {
 
   lazy val subterms: Seq[Term] = state.utils.subterms(this)
 
-  /** @see [[ast.utility.Visitor.visit()]] */
+  /** @see [[ast.utility.Visitor.visit]] */
   def visit(f: PartialFunction[Term, Any]): Unit =
     ast.utility.Visitor.visit(this, state.utils.subterms)(f)
 
-  /** @see [[ast.utility.Visitor.visitOpt()]] */
+  /** @see [[ast.utility.Visitor.visitOpt]] */
   def visitOpt(f: Term => Boolean): Unit =
     ast.utility.Visitor.visitOpt(this, state.utils.subterms)(f)
 
-  /** @see [[ast.utility.Visitor.reduceTree()]] */
+  /** @see [[ast.utility.Visitor.reduceTree]] */
   def reduceTree[R](f: (Term, Seq[R]) => R): R =
     ast.utility.Visitor.reduceTree(this, state.utils.subterms)(f)
 
-  /** @see [[ast.utility.Visitor.existsDefined()]] */
+  /** @see [[ast.utility.Visitor.existsDefined]] */
   def existsDefined(f: PartialFunction[Term, Any]): Boolean =
     ast.utility.Visitor.existsDefined(this, state.utils.subterms)(f)
 
-  /** @see [[ast.utility.Visitor.hasSubnode()]] */
+  /** @see [[ast.utility.Visitor.hasSubnode]] */
   def hasSubterm(subterm: Term): Boolean =
     ast.utility.Visitor.hasSubnode(this, subterm, state.utils.subterms)
 
-  /** @see [[ast.utility.Visitor.deepCollect()]] */
+  /** @see [[ast.utility.Visitor.deepCollect]] */
   def deepCollect[R](f: PartialFunction[Term, R]) : Seq[R] =
     ast.utility.Visitor.deepCollect(Seq(this), state.utils.subterms)(f)
 
-  /** @see [[ast.utility.Visitor.shallowCollect()]] */
+  /** @see [[ast.utility.Visitor.shallowCollect]] */
   def shallowCollect[R](f: PartialFunction[Term, R]): Seq[R] =
     ast.utility.Visitor.shallowCollect(Seq(this), state.utils.subterms)(f)
 
-  /** @see [[ast.utility.Visitor.find()]] */
+  /** @see [[ast.utility.Visitor.find]] */
   def find[R](f: PartialFunction[Term, R]): Option[R] =
     ast.utility.Visitor.find(this, state.utils.subterms)(f)
 
-  /** @see [[state.utils.transform()]] */
+  /** @see [[state.utils.transform]] */
   def transform(pre: PartialFunction[Term, Term] = PartialFunction.empty)
                (recursive: Term => Boolean = !pre.isDefinedAt(_),
                 post: PartialFunction[Term, Term] = PartialFunction.empty)
@@ -2295,48 +2300,63 @@ object PredicateTrigger extends PreciseCondFlyweightFactory[(String, Term, Seq[T
 
 /* Magic wands */
 
-class MagicWandSnapshot(val abstractLhs: Term, val rhsSnapshot: Term) extends Combine(abstractLhs, rhsSnapshot) {
-  utils.assertSort(abstractLhs, "abstract lhs", sorts.Snap)
-  utils.assertSort(rhsSnapshot, "rhs", sorts.Snap)
+/**
+ * Represents a snapshot of a magic wand, which is a function from `Snap` to `Snap`.
+ *
+ * @param mwsf The function that represents the snapshot of the magic wand. It is a variable of sort [[sorts.MagicWandSnapFunction]].
+ *             In the symbolic execution when we apply a magic wand, it consumes the left-hand side
+ *             and uses this function and the resulting snapshot to look up which right-hand side to produce.
+ */
+class MagicWandSnapshot(val mwsf: Term) extends Term with ConditionalFlyweight[Term, MagicWandSnapshot] {
+  utils.assertSort(mwsf, "magic wand snap function", sorts.MagicWandSnapFunction)
 
-  override lazy val toString = s"wandSnap(lhs = $abstractLhs, rhs = $rhsSnapshot)"
+  override val sort: Sort = sorts.MagicWandSnapFunction
 
-  def merge(other: MagicWandSnapshot, branchConditions: Stack[Term]): MagicWandSnapshot = {
-    assert(this.abstractLhs == other.abstractLhs)
-    val condition = And(branchConditions)
-    MagicWandSnapshot(this.abstractLhs, if (this.rhsSnapshot == other.rhsSnapshot)
-      this.rhsSnapshot
-    else
-      Ite(condition, other.rhsSnapshot, this.rhsSnapshot))
-  }
+  override lazy val toString = s"wandSnap($mwsf)"
+
+  override val equalityDefiningMembers: Term = mwsf
+
+  /**
+   * Apply the given snapshot of the left-hand side to the magic wand map to get the snapshot of the right-hand side
+   * which includes the values of the left-hand side.
+   *
+   * @param snapLhs The snapshot of the left-hand side that should be applied to the magic wand map.
+   * @return The snapshot of the right-hand side that preserves the values of the left-hand side.
+   */
+  def applyToMWSF(snapLhs: Term): Term = MWSFLookup(mwsf, snapLhs)
 }
 
-object MagicWandSnapshot  {
-  def apply(snapshot: Term): MagicWandSnapshot = {
-    assert(snapshot.sort == sorts.Snap)
-    snapshot match {
-      case snap: MagicWandSnapshot => snap
-      case _ =>
-        MagicWandSnapshot(First(snapshot), Second(snapshot))
-    }
-  }
+object MagicWandSnapshot extends PreciseCondFlyweightFactory[Term, MagicWandSnapshot]  {
+  /** Create an instance of [[viper.silicon.state.terms.MagicWandSnapshot]]. */
+  override def actualCreate(arg: Term): MagicWandSnapshot =
+    new MagicWandSnapshot(arg)
+}
 
-  // Since MagicWandSnapshot subclasses Combine, we apparently cannot inherit the normal subclass, so we
-  // have to copy paste the code here.
-  var pool = new TrieMap[(Term, Term), MagicWandSnapshot]()
+/**
+ * Term that applies a [[sorts.MagicWandSnapFunction]] to a snapshot.
+ * It returns a snapshot for the RHS of a magic wand that includes that values of the given snapshot.
+ *
+ * @param mwsf Term of sort [[sorts.MagicWandSnapFunction]]. Function from `Snap` to `Snap`.
+ * @param snap Term of sort [[sorts.Snap]] to which the MWSF is applied to. It represents the values of the wand's LHS.
+ */
+class MWSFLookup(val mwsf: Term, val snap: Term) extends Term with ConditionalFlyweightBinaryOp[MWSFLookup] {
+  val sort: Sort = sorts.Snap
+  override def p0: Term = mwsf
+  override def p1: Term = snap
+  override lazy val toString = s"$mwsf[$snap]"
+}
 
-  def createIfNonExistent(args: (Term, Term)): MagicWandSnapshot = {
-    if (Verifier.config.useFlyweight) {
-      pool.getOrElseUpdate(args, actualCreate(args))
-    } else {
-      actualCreate(args)
-    }
+object MWSFLookup extends PreciseCondFlyweightFactory[(Term, Term), MWSFLookup] {
+  override def apply(pair: (Term, Term)): MWSFLookup = {
+    val (mwsf, snap) = pair
+    utils.assertSort(mwsf, "mwsf", sorts.MagicWandSnapFunction)
+    utils.assertSort(snap, "snap", sorts.Snap)
+    createIfNonExistent(pair)
   }
 
-  def actualCreate(tuple: (Term, Term)) = new MagicWandSnapshot(tuple._1, tuple._2)
-  def apply(fst: Term, snd: Term): MagicWandSnapshot = createIfNonExistent((fst, snd))
-
-  def unapply(mws: MagicWandSnapshot) = Some((mws.abstractLhs, mws.rhsSnapshot))
+  /** Create an instance of [[viper.silicon.state.terms.MWSFLookup]]. */
+  override def actualCreate(args: (Term, Term)): MWSFLookup =
+    new MWSFLookup(args._1, args._2)
 }
 
 class MagicWandChunkTerm(val chunk: MagicWandChunk) extends Term with ConditionalFlyweight[MagicWandChunk, MagicWandChunkTerm] {
@@ -2461,7 +2481,7 @@ object PsfTop extends (String => Identifier) {
  */
 
 /* Note: Sort wrappers should probably not be used as (outermost) triggers
- * because they are optimised away if wrappee `t` already has sort `to`.
+ * because they are optimised away if wrapped `t` already has sort `to`.
  */
 class SortWrapper(val t: Term, val to: Sort)
     extends Term
diff --git a/src/main/scala/state/Utils.scala b/src/main/scala/state/Utils.scala
index 38a1abbff..d2667e8cd 100644
--- a/src/main/scala/state/Utils.scala
+++ b/src/main/scala/state/Utils.scala
@@ -94,7 +94,7 @@ package object utils {
 
   }
 
-  /** @see [[viper.silver.ast.utility.Transformer.simplify()]] */
+  /** @see [[viper.silver.ast.utility.Simplifier.simplify]] */
   def transform[T <: Term](term: T,
                            pre: PartialFunction[Term, Term] = PartialFunction.empty)
                           (recursive: Term => Boolean = !pre.isDefinedAt(_),
@@ -196,7 +196,8 @@ package object utils {
       case MapUpdate(t0, t1, t2) => MapUpdate(go(t0), go(t1), go(t2))
       case MapDomain(t) => MapDomain(go(t))
       case MapRange(t) => MapRange(go(t))
-      case MagicWandSnapshot(lhs, rhs) => MagicWandSnapshot(go(lhs), go(rhs))
+      case MagicWandSnapshot(t) => MagicWandSnapshot(go(t))
+      case MWSFLookup(t0, t1) => MWSFLookup(go(t0), go(t1))
       case Combine(t0, t1) => Combine(go(t0), go(t1))
       case First(t) => First(go(t))
       case Second(t) => Second(go(t))
diff --git a/src/main/scala/supporters/BuiltinDomainsContributor.scala b/src/main/scala/supporters/BuiltinDomainsContributor.scala
index f181a298a..bb01d2fd0 100644
--- a/src/main/scala/supporters/BuiltinDomainsContributor.scala
+++ b/src/main/scala/supporters/BuiltinDomainsContributor.scala
@@ -8,7 +8,6 @@ package viper.silicon.supporters
 
 import java.io.File
 import java.net.URL
-
 import scala.annotation.unused
 import scala.reflect.ClassTag
 import viper.silver.ast
@@ -57,38 +56,20 @@ abstract class BuiltinDomainsContributor extends PreambleContributor[Sort, Domai
 
   def analyze(program: ast.Program): Unit = {
     val builtinDomainTypeInstances = computeGroundTypeInstances(program)
-    val sourceProgram = utils.loadProgramFromUrl(sourceUrl)
+    val sourceProgram = loadProgramFromUrl(sourceUrl)
     val sourceDomain = transformSourceDomain(sourceProgram.findDomain(sourceDomainName))
 
+    // List of all domains found in the program with their instantiations, i.e. the types they are used with
     val sourceDomainTypeInstances =
       builtinDomainTypeInstances map (builtinTypeInstance => {
-        val instantiation : Map[viper.silver.ast.TypeVar,viper.silver.ast.Type] = sourceDomain.typVars.zip(builtinTypeInstance.typeArguments).toMap
-        //(instantiation, ast.DomainType(sourceDomain, instantiation))
+        val instantiation: Map[viper.silver.ast.TypeVar, viper.silver.ast.Type] = sourceDomain.typVars.zip(builtinTypeInstance.typeArguments).toMap
         ast.DomainType(sourceDomain, instantiation)
       })
 
-    /* For each necessary domain type, instantiate the corresponding domain */
-    val sourceDomainInstantiationsWithType =
-      sourceDomainTypeInstances map (mdt => {
-        /* TODO: Copied from DomainInstances.getInstanceMembers.
-         *       Cannot directly use that because it filters according to which domain instances
-         *       are used in the program from which the source domain was loaded, whereas the
-         *       instances should be filtered according to which are used in the program under
-         *       verification.
-         */
-        val functions = sourceDomain.functions.map(ast.utility.DomainInstances.substitute(_, mdt.typVarsMap, sourceProgram)).distinct
-        val axioms = sourceDomain.axioms.map(ast.utility.DomainInstances.substitute(_, mdt.typVarsMap, sourceProgram)).distinct
-
-        val instance =
-          sourceDomain.copy(functions = functions, axioms = axioms)(sourceDomain.pos, sourceDomain.info, sourceDomain.errT)
-
-        (mdt, transformSourceDomainInstance(instance, mdt))
-      })
-
-    val sourceDomainInstantiations = sourceDomainInstantiationsWithType.map(x => x._2)
+    val sourceDomainInstantiationsWithType = instantiateWithDomain(sourceProgram, sourceDomain, sourceDomainTypeInstances)
 
     collectSorts(sourceDomainTypeInstances)
-    collectFunctions(sourceDomainInstantiations, program)
+    collectFunctions(sourceDomainInstantiationsWithType, program)
     collectAxioms(sourceDomainInstantiationsWithType)
   }
 
@@ -97,6 +78,26 @@ abstract class BuiltinDomainsContributor extends PreambleContributor[Sort, Domai
       case builtinDomainTypeTag(s) => s
     })
 
+  /**
+   * For each necessary domain type, instantiate the corresponding domain
+   */
+  private def instantiateWithDomain(sourceProgram: ast.Program, sourceDomain: ast.Domain, sourceDomainTypeInstances: InsertionOrderedSet[ast.DomainType]): Set[(ast.DomainType, ast.Domain)] = {
+    sourceDomainTypeInstances map (domainType => {
+      /* TODO: Copied from DomainInstances.getInstanceMembers.
+       *       Cannot directly use that because it filters according to which domain instances
+       *       are used in the program from which the source domain was loaded, whereas the
+       *       instances should be filtered according to which are used in the program under
+       *       verification.
+       */
+      val functions = sourceDomain.functions.map(ast.utility.DomainInstances.substitute(_, domainType.typVarsMap, sourceProgram)).distinct
+      val axioms = sourceDomain.axioms.map(ast.utility.DomainInstances.substitute(_, domainType.typVarsMap, sourceProgram)).distinct
+
+      val instance = sourceDomain.copy(functions = functions, axioms = axioms)(sourceDomain.pos, sourceDomain.info, sourceDomain.errT)
+
+      (domainType, transformSourceDomainInstance(instance, domainType))
+    })
+  }
+
   protected def transformSourceDomain(sourceDomain: ast.Domain): ast.Domain = sourceDomain
 
   protected def transformSourceDomainInstance(sourceDomain: ast.Domain, @unused typ: ast.DomainType): ast.Domain = sourceDomain
@@ -110,9 +111,9 @@ abstract class BuiltinDomainsContributor extends PreambleContributor[Sort, Domai
     })
   }
 
-  protected def collectFunctions(domains: Set[ast.Domain], program: ast.Program): Unit = {
-    domains foreach (
-      _.functions foreach (df =>
+  protected def collectFunctions(domains: Set[(ast.DomainType, ast.Domain)], program: ast.Program): Unit = {
+    domains foreach (d =>
+      d._2.functions foreach (df =>
         if (df.interpretation.isEmpty)
           collectedFunctions += symbolConverter.toFunction(df, program).asInstanceOf[DomainFun]))
   }
@@ -129,7 +130,7 @@ abstract class BuiltinDomainsContributor extends PreambleContributor[Sort, Domai
      * are preserved.
      */
     val domainName = f"${d.domainName}[${d.typVarsMap.values.map(t => symbolConverter.toSort(t)).mkString(",")}]"
-    domainTranslator.translateAxiom(ax, symbolConverter.toSort, true).transform {
+    domainTranslator.translateAxiom(ax, symbolConverter.toSort, builtin = true).transform {
       case q@Quantification(_,_,_,_,name,_,_) if name != "" =>
         q.copy(name = f"${domainName}_${name}")
       case Equals(t1, t2) => BuiltinEquals(t1, t2)
@@ -146,37 +147,19 @@ abstract class BuiltinDomainsContributor extends PreambleContributor[Sort, Domai
     collectedFunctions
 
   def declareSymbolsAfterAnalysis(sink: ProverLike): Unit = {
-    collectedFunctions foreach (f => sink.declare(FunctionDecl(f)))
+    symbolsAfterAnalysis foreach (f => sink.declare(FunctionDecl(f)))
   }
 
   def axiomsAfterAnalysis: Iterable[Term] = collectedAxioms
 
   def emitAxiomsAfterAnalysis(sink: ProverLike): Unit = {
-    collectedAxioms foreach (ax => sink.assume(ax))
-  }
-
-  def updateGlobalStateAfterAnalysis(): Unit = { /* Nothing to contribute*/ }
-}
-
-class BuiltinDomainAwareSymbolConverter(sourceDomainName: String,
-                                        targetSortFactory: Iterable[Sort] => Sort)
-    extends DefaultSymbolConverter {
-
-  override def toSort(typ: ast.Type): Sort = typ match {
-    case dt: ast.DomainType if dt.domainName == sourceDomainName =>
-      targetSortFactory(dt.typVarsMap.values map toSort)
-    case other =>
-      super.toSort(other)
+    axiomsAfterAnalysis foreach (ax => sink.assume(ax))
   }
-}
 
-private object utils {
-  def loadProgramFromResource(resource: String): ast.Program = {
-    loadProgramFromUrl(getClass.getResource(resource))
-  }
+  /* Utility */
 
   // TODO: Check that Silver's parser doesn't already provide suitable functionality.
-  def loadProgramFromUrl(url: URL): ast.Program = {
+  private def loadProgramFromUrl(url: URL): ast.Program = {
     assert(url != null, s"Unexpectedly found sourceUrl == null")
 
     val fromPath = viper.silver.utility.Paths.pathFromResource(url)
@@ -204,3 +187,15 @@ private object utils {
     program
   }
 }
+
+class BuiltinDomainAwareSymbolConverter(sourceDomainName: String,
+                                        targetSortFactory: Iterable[Sort] => Sort)
+    extends DefaultSymbolConverter {
+
+  override def toSort(typ: ast.Type): Sort = typ match {
+    case dt: ast.DomainType if dt.domainName == sourceDomainName =>
+      targetSortFactory(dt.typVarsMap.values map toSort)
+    case other =>
+      super.toSort(other)
+  }
+}
diff --git a/src/main/scala/supporters/MagicWandSnapFunctionsContributor.scala b/src/main/scala/supporters/MagicWandSnapFunctionsContributor.scala
new file mode 100644
index 000000000..c2b925c6a
--- /dev/null
+++ b/src/main/scala/supporters/MagicWandSnapFunctionsContributor.scala
@@ -0,0 +1,92 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2024 ETH Zurich.
+
+package viper.silicon.supporters
+
+import viper.silicon.common.collections.immutable.InsertionOrderedSet
+import viper.silicon.interfaces.{PreambleContributor, PreambleReader}
+import viper.silicon.interfaces.decider.ProverLike
+import viper.silicon.state.terms.{Sort, SortDecl, sorts}
+import viper.silver.ast
+import viper.silver.ast.Program
+
+/**
+ * Add function declarations when the proof makes use of MagicWandSnapFunctions (MWSF).
+ * Those are used to preserve values across multiple applications of a magic wand, e.g. by using an applying expression.
+ *
+ * @param preambleReader Reader that returns the content of some given SMT2 files.
+ */
+class MagicWandSnapFunctionsContributor(preambleReader: PreambleReader[String, String])
+  extends PreambleContributor[Sort, String, String] {
+
+  /** File which contains all function declarations in the SMT2 syntax. */
+  private val FILE_DECLARATIONS = "/magic_wand_snap_functions_declarations.smt2"
+
+  /** Set for the sort [[viper.silicon.state.terms.sorts.MagicWandSnapFunction]] */
+  private var collectedSorts: InsertionOrderedSet[Sort] = InsertionOrderedSet.empty
+
+  /** Set for all function declaration related to [[viper.silicon.state.terms.sorts.MagicWandSnapFunction]] */
+  private var collectedFunctionDecls: Iterable[String] = Seq.empty
+
+  /* Functionality */
+
+  /**
+   * Add all function declarations when a program contains magic wands.
+   *
+   * @param program AST of the program to prove.
+   */
+  override def analyze(program: Program): Unit = {
+    // If there are not magic wands, do not add any definitions or axioms
+    if (!program.existsDefined { case ast.MagicWand(_, _) => true }) return
+
+    collectedSorts = InsertionOrderedSet(sorts.MagicWandSnapFunction)
+    collectedFunctionDecls = preambleReader.readPreamble(FILE_DECLARATIONS)
+  }
+
+  /** Sorts to add to the preamble of the SMT proof script. */
+  override def sortsAfterAnalysis: Iterable[Sort] = collectedSorts
+
+  /** Add all sorts needed to the preamble using `sink`. */
+  override def declareSortsAfterAnalysis(sink: ProverLike): Unit = {
+    sortsAfterAnalysis foreach (s => sink.declare(SortDecl(s)))
+  }
+
+  /** Symbols to add to the preamble of the SMT proof script. */
+  override def symbolsAfterAnalysis: Iterable[String] =
+    extractPreambleLines(collectedFunctionDecls)
+
+  /** Add all symbols needed to the preamble using `sink`. */
+  override def declareSymbolsAfterAnalysis(sink: ProverLike): Unit =
+    emitPreambleLines(sink, collectedFunctionDecls)
+
+  /** Axioms to add to the preamble of the SMT proof script. Currently, there are none. */
+  override def axiomsAfterAnalysis: Iterable[String] = Seq.empty
+
+  /** Add all axioms needed to the preamble using `sink`. Currently, there are none. */
+  override def emitAxiomsAfterAnalysis(sink: ProverLike): Unit = {}
+
+  /** Helper function to transform the lines returned by the `PreambleReader`. */
+  private def extractPreambleLines(lines: Iterable[String]*): Iterable[String] =
+    lines.flatten
+
+  /** Helper function to emit all lines using `sink`. */
+  private def emitPreambleLines(sink: ProverLike, lines: Iterable[String]*): Unit = {
+    lines foreach { declaration =>
+      sink.emit(declaration)
+    }
+  }
+
+  /* Lifetime */
+
+  def reset(): Unit = {
+    collectedSorts = InsertionOrderedSet.empty
+    collectedFunctionDecls = Seq.empty
+  }
+
+  def stop(): Unit = {}
+
+  def start(): Unit = {}
+}
diff --git a/src/main/scala/supporters/qps/PredicateAndWandSnapFunctionsContributor.scala b/src/main/scala/supporters/qps/PredicateAndWandSnapFunctionsContributor.scala
index 920405ec6..3da5802d1 100644
--- a/src/main/scala/supporters/qps/PredicateAndWandSnapFunctionsContributor.scala
+++ b/src/main/scala/supporters/qps/PredicateAndWandSnapFunctionsContributor.scala
@@ -21,7 +21,6 @@ import viper.silicon.state.terms.{Sort, SortDecl, sorts}
 import viper.silver.ast.PredicateAccess
 
 trait PredicateSnapFunctionsContributor[SO, SY, AX] extends PreambleContributor[SO, SY, AX]
-trait MagicWandSnapFunctionsContributor[SO, SY, AX] extends PreambleContributor[SO, SY, AX]
 
 /** Creates background definitions for n-tuples of predicate and wand arguments. Currently,
   * snapshot trees are used to built n-tuples.
@@ -45,8 +44,7 @@ class DefaultPredicateAndWandSnapFunctionsContributor(preambleReader: PreambleRe
                                                       termConverter: TermConverter[String, String, String],
                                                       predicateSnapGenerator: PredicateSnapGenerator,
                                                       config: Config)
-    extends PredicateSnapFunctionsContributor[Sort, String, String]
-       with MagicWandSnapFunctionsContributor[Sort, String, String] {
+    extends PredicateSnapFunctionsContributor[Sort, String, String] {
 
   /* PreambleBlock = Comment x Lines */
   private type PreambleBlock = (String, Iterable[String])
diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala
index 61c4e31f5..a7d69656d 100644
--- a/src/main/scala/verifier/DefaultMainVerifier.scala
+++ b/src/main/scala/verifier/DefaultMainVerifier.scala
@@ -73,6 +73,7 @@ class DefaultMainVerifier(config: Config,
   protected val fieldValueFunctionsContributor = new DefaultFieldValueFunctionsContributor(preambleReader, symbolConverter, termConverter, config)
   protected val predSnapGenerator = new PredicateSnapGenerator(symbolConverter, snapshotSupporter)
   protected val predicateAndWandSnapFunctionsContributor = new DefaultPredicateAndWandSnapFunctionsContributor(preambleReader, termConverter, predSnapGenerator, config)
+  protected val magicWandSnapFunctionsContributor = new MagicWandSnapFunctionsContributor(preambleReader)
 
   private val _verificationPoolManager: VerificationPoolManager = new VerificationPoolManager(this)
   def verificationPoolManager: VerificationPoolManager = _verificationPoolManager
@@ -82,6 +83,7 @@ class DefaultMainVerifier(config: Config,
     sequencesContributor, setsContributor, multisetsContributor, mapsContributor, domainsContributor,
     fieldValueFunctionsContributor,
     predSnapGenerator, predicateAndWandSnapFunctionsContributor,
+    magicWandSnapFunctionsContributor,
     functionsSupporter, predicateSupporter,
     _verificationPoolManager,
     MultiRunRecorders /* In lieu of a better place, include MultiRunRecorders singleton here */
@@ -459,6 +461,7 @@ class DefaultMainVerifier(config: Config,
     domainsContributor,
     fieldValueFunctionsContributor,
     predicateAndWandSnapFunctionsContributor,
+    magicWandSnapFunctionsContributor,
     functionsSupporter,
     predicateSupporter
   )
@@ -471,6 +474,7 @@ class DefaultMainVerifier(config: Config,
     domainsContributor,
     fieldValueFunctionsContributor,
     predicateAndWandSnapFunctionsContributor,
+    magicWandSnapFunctionsContributor,
     functionsSupporter,
     predicateSupporter
   )
@@ -483,6 +487,7 @@ class DefaultMainVerifier(config: Config,
     domainsContributor,
     fieldValueFunctionsContributor,
     predicateAndWandSnapFunctionsContributor,
+    magicWandSnapFunctionsContributor,
     functionsSupporter,
     predicateSupporter
   )
@@ -500,6 +505,7 @@ class DefaultMainVerifier(config: Config,
     domainsContributor,
     fieldValueFunctionsContributor,
     predicateAndWandSnapFunctionsContributor,
+    magicWandSnapFunctionsContributor,
     functionsSupporter,
     predicateSupporter
   )
@@ -512,6 +518,7 @@ class DefaultMainVerifier(config: Config,
     domainsContributor,
     fieldValueFunctionsContributor,
     predicateAndWandSnapFunctionsContributor,
+    magicWandSnapFunctionsContributor,
     functionsSupporter,
     predicateSupporter
   )

From 393943ed2dbea82498b774998b9606f9bbc537f7 Mon Sep 17 00:00:00 2001
From: Silver Bot <bot@noreply.github.com>
Date: Wed, 12 Jun 2024 23:11:52 +0000
Subject: [PATCH 05/13] Update silver submodule

---
 silver | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/silver b/silver
index d29ac2738..86742da30 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit d29ac2738d27232edaeb3d3a24952928f4006299
+Subproject commit 86742da3001d99b88df3777a8b39f682bf911451

From 64540554c3d3636c6d8fc5af95af169639b4d421 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 13 Jun 2024 19:57:49 +0200
Subject: [PATCH 06/13] Recording constraints for newly-introduced variables
 during state consolidation. Also renaming the function we use for that.

---
 src/main/scala/rules/Evaluator.scala           |  2 +-
 .../rules/MoreCompleteExhaleSupporter.scala    |  2 +-
 src/main/scala/rules/StateConsolidator.scala   |  2 +-
 .../supporters/functions/FunctionData.scala    | 10 +++++-----
 .../functions/FunctionRecorder.scala           | 18 +++++++++---------
 5 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala
index 0b999061a..23679f6ef 100644
--- a/src/main/scala/rules/Evaluator.scala
+++ b/src/main/scala/rules/Evaluator.scala
@@ -185,7 +185,7 @@ object evaluator extends EvaluationRules {
          *       term returned by eval, mark as constrainable on client-side (e.g. in consumer).
          */
         val s1 =
-          s.copy(functionRecorder = s.functionRecorder.recordArp(tVar, tConstraints))
+          s.copy(functionRecorder = s.functionRecorder.recordConstrainedVar(tVar, tConstraints))
            .setConstrainable(Seq(tVar), true)
         Q(s1, tVar, v)
 
diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala
index 5c7173c8a..c08ac4659 100644
--- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala
+++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala
@@ -365,7 +365,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
         )
 
         v.decider.assume(constraint)
-        newFr = newFr.recordArp(permTaken, constraint)
+        newFr = newFr.recordConstrainedVar(permTaken, constraint)
 
         ch.withPerm(PermMinus(ch.perm, permTaken))
       })
diff --git a/src/main/scala/rules/StateConsolidator.scala b/src/main/scala/rules/StateConsolidator.scala
index 452d0c7b3..49e22100c 100644
--- a/src/main/scala/rules/StateConsolidator.scala
+++ b/src/main/scala/rules/StateConsolidator.scala
@@ -216,7 +216,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol
          * to use t1 or t2 and constrain it.
          */
         val t3 = v.decider.fresh(t1.sort)
-        (fr.recordFreshSnapshot(t3), t3, And(Implies(b1, t3 === t1), Implies(b2, t3 === t2)))
+        (fr.recordConstrainedVar(t3, And(Implies(b1, t3 === t1), Implies(b2, t3 === t2))), t3, And(Implies(b1, t3 === t1), Implies(b2, t3 === t2)))
     }
   }
 
diff --git a/src/main/scala/supporters/functions/FunctionData.scala b/src/main/scala/supporters/functions/FunctionData.scala
index 41f884e0a..1bf87874a 100644
--- a/src/main/scala/supporters/functions/FunctionData.scala
+++ b/src/main/scala/supporters/functions/FunctionData.scala
@@ -93,7 +93,7 @@ class FunctionData(val programFunction: ast.Function,
   private[functions] var fappToSnap: Map[ast.FuncApp, Term] = Map.empty
   private[this] var freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition] = InsertionOrderedSet.empty
   private[this] var freshFieldInvs: InsertionOrderedSet[InverseFunctions] = InsertionOrderedSet.empty
-  private[this] var freshArps: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet.empty
+  private[this] var freshConstrainedVars: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet.empty
   private[this] var freshConstraints: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
   private[this] var freshSnapshots: InsertionOrderedSet[Function] = InsertionOrderedSet.empty
   private[this] var freshPathSymbols: InsertionOrderedSet[Function] = InsertionOrderedSet.empty
@@ -101,7 +101,7 @@ class FunctionData(val programFunction: ast.Function,
   private[this] var freshSymbolsAcrossAllPhases: InsertionOrderedSet[Decl] = InsertionOrderedSet.empty
 
   private[functions] def getFreshFieldInvs: InsertionOrderedSet[InverseFunctions] = freshFieldInvs
-  private[functions] def getFreshArps: InsertionOrderedSet[Var] = freshArps.map(_._1)
+  private[functions] def getFreshConstrainedVars: InsertionOrderedSet[Var] = freshConstrainedVars.map(_._1)
   private[functions] def getFreshSymbolsAcrossAllPhases: InsertionOrderedSet[Decl] = freshSymbolsAcrossAllPhases
 
   private[functions] def advancePhase(recorders: Seq[FunctionRecorder]): Unit = {
@@ -117,14 +117,14 @@ class FunctionData(val programFunction: ast.Function,
     fappToSnap = mergedFunctionRecorder.fappToSnap
     freshFvfsAndDomains = mergedFunctionRecorder.freshFvfsAndDomains
     freshFieldInvs = mergedFunctionRecorder.freshFieldInvs
-    freshArps = mergedFunctionRecorder.freshArps
+    freshConstrainedVars = mergedFunctionRecorder.freshConstrainedVars
     freshConstraints = mergedFunctionRecorder.freshConstraints
     freshSnapshots = mergedFunctionRecorder.freshSnapshots
     freshPathSymbols = mergedFunctionRecorder.freshPathSymbols
     freshMacros = mergedFunctionRecorder.freshMacros
 
     freshSymbolsAcrossAllPhases ++= freshPathSymbols map FunctionDecl
-    freshSymbolsAcrossAllPhases ++= freshArps.map(pair => FunctionDecl(pair._1))
+    freshSymbolsAcrossAllPhases ++= freshConstrainedVars.map(pair => FunctionDecl(pair._1))
     freshSymbolsAcrossAllPhases ++= freshSnapshots map FunctionDecl
     freshSymbolsAcrossAllPhases ++= freshFieldInvs.flatMap(i => (i.inverses ++ i.images) map FunctionDecl)
     freshSymbolsAcrossAllPhases ++= freshMacros
@@ -145,7 +145,7 @@ class FunctionData(val programFunction: ast.Function,
     val nested = (
          freshFieldInvs.flatMap(_.definitionalAxioms)
       ++ freshFvfsAndDomains.flatMap (fvfDef => fvfDef.domainDefinitions ++ fvfDef.valueDefinitions)
-      ++ freshArps.map(_._2)
+      ++ freshConstrainedVars.map(_._2)
       ++ freshConstraints)
 
     // Filter out nested definitions that contain free variables.
diff --git a/src/main/scala/supporters/functions/FunctionRecorder.scala b/src/main/scala/supporters/functions/FunctionRecorder.scala
index 48c0ee2d8..756cb3545 100644
--- a/src/main/scala/supporters/functions/FunctionRecorder.scala
+++ b/src/main/scala/supporters/functions/FunctionRecorder.scala
@@ -25,7 +25,7 @@ trait FunctionRecorder extends Mergeable[FunctionRecorder] {
   def fappToSnap: Map[ast.FuncApp, Term]
   def freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition]
   def freshFieldInvs: InsertionOrderedSet[InverseFunctions]
-  def freshArps: InsertionOrderedSet[(Var, Term)]
+  def freshConstrainedVars: InsertionOrderedSet[(Var, Term)]
   def freshConstraints: InsertionOrderedSet[Term]
   def freshSnapshots: InsertionOrderedSet[Function]
   def freshPathSymbols: InsertionOrderedSet[Function]
@@ -34,7 +34,7 @@ trait FunctionRecorder extends Mergeable[FunctionRecorder] {
   def recordSnapshot(fapp: ast.FuncApp, guards: Stack[Term], snap: Term): FunctionRecorder
   def recordFvfAndDomain(fvfDef: SnapshotMapDefinition): FunctionRecorder
   def recordFieldInv(inv: InverseFunctions): FunctionRecorder
-  def recordArp(arp: Var, constraint: Term): FunctionRecorder
+  def recordConstrainedVar(v: Var, constraint: Term): FunctionRecorder
   def recordConstraint(constraint: Term): FunctionRecorder
   def recordFreshSnapshot(snap: Function): FunctionRecorder
   def recordPathSymbol(symbol: Function): FunctionRecorder
@@ -48,7 +48,7 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
                                   private[functions] val fappToSnaps: Map[ast.FuncApp, InsertionOrderedSet[(Stack[Term], Term)]] = Map(),
                                   freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition] = InsertionOrderedSet(),
                                   freshFieldInvs: InsertionOrderedSet[InverseFunctions] = InsertionOrderedSet(),
-                                  freshArps: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet(),
+                                  freshConstrainedVars: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet(),
                                   freshConstraints: InsertionOrderedSet[Term] = InsertionOrderedSet(),
                                   freshSnapshots: InsertionOrderedSet[Function] = InsertionOrderedSet(),
                                   freshPathSymbols: InsertionOrderedSet[Function] = InsertionOrderedSet(),
@@ -189,8 +189,8 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
     if (depth <= 2) copy(freshFieldInvs = freshFieldInvs + inv)
     else this
 
-  def recordArp(arp: Var, constraint: Term): ActualFunctionRecorder =
-    if (depth <= 2) copy(freshArps = freshArps + ((arp, constraint)))
+  def recordConstrainedVar(arp: Var, constraint: Term): ActualFunctionRecorder =
+    if (depth <= 2) copy(freshConstrainedVars = freshConstrainedVars + ((arp, constraint)))
     else this
 
   def recordConstraint(constraint: Term): ActualFunctionRecorder =
@@ -237,7 +237,7 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
 
     val fvfs = freshFvfsAndDomains ++ other.freshFvfsAndDomains
     val fieldInvs = freshFieldInvs ++ other.freshFieldInvs
-    val arps = freshArps ++ other.freshArps
+    val arps = freshConstrainedVars ++ other.freshConstrainedVars
     val constraints = freshConstraints ++ other.freshConstraints
     val snaps = freshSnapshots ++ other.freshSnapshots
     val symbols = freshPathSymbols ++ other.freshPathSymbols
@@ -247,7 +247,7 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
          fappToSnaps = fts,
          freshFvfsAndDomains = fvfs,
          freshFieldInvs = fieldInvs,
-         freshArps = arps,
+         freshConstrainedVars = arps,
          freshConstraints = constraints,
          freshSnapshots = snaps,
          freshPathSymbols = symbols,
@@ -277,7 +277,7 @@ case object NoopFunctionRecorder extends FunctionRecorder {
   val locToSnap: Map[ast.LocationAccess, Term] = Map.empty
   val freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition] = InsertionOrderedSet.empty
   val freshFieldInvs: InsertionOrderedSet[InverseFunctions] = InsertionOrderedSet.empty
-  val freshArps: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet.empty
+  val freshConstrainedVars: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet.empty
   val freshConstraints: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
   val freshSnapshots: InsertionOrderedSet[Function] = InsertionOrderedSet.empty
   val freshPathSymbols: InsertionOrderedSet[Function] = InsertionOrderedSet.empty
@@ -294,7 +294,7 @@ case object NoopFunctionRecorder extends FunctionRecorder {
   def recordFvfAndDomain(fvfDef: SnapshotMapDefinition): NoopFunctionRecorder.type = this
   def recordFieldInv(inv: InverseFunctions): NoopFunctionRecorder.type = this
   def recordSnapshot(fapp: ast.FuncApp, guards: Stack[Term], snap: Term): NoopFunctionRecorder.type = this
-  def recordArp(arp: Var, constraint: Term): NoopFunctionRecorder.type = this
+  def recordConstrainedVar(arp: Var, constraint: Term): NoopFunctionRecorder.type = this
   def recordConstraint(constraint: Term): NoopFunctionRecorder.type = this
   def recordFreshSnapshot(snap: Function): NoopFunctionRecorder.type = this
   def recordPathSymbol(symbol: Function): NoopFunctionRecorder.type = this

From 5a1fc0cfc215b06416d7d94eb0fe578d2043f434 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 13 Jun 2024 20:16:56 +0200
Subject: [PATCH 07/13] Not pushing conditions using permission introspection
 further in

---
 silver                                          |  2 +-
 .../ConditionalPermissionRewriter.scala         | 17 ++++++++++++-----
 2 files changed, 13 insertions(+), 6 deletions(-)

diff --git a/silver b/silver
index 1b588f0db..f33876143 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 1b588f0db96acd641a35c9eb1424acda80084561
+Subproject commit f3387614386d817804d3e66326bc1914e0d78c6d
diff --git a/src/main/scala/extensions/ConditionalPermissionRewriter.scala b/src/main/scala/extensions/ConditionalPermissionRewriter.scala
index 1841465e2..817c5c036 100644
--- a/src/main/scala/extensions/ConditionalPermissionRewriter.scala
+++ b/src/main/scala/extensions/ConditionalPermissionRewriter.scala
@@ -30,7 +30,9 @@ class ConditionalPermissionRewriter {
     case (i@Implies(cond, acc: AccessPredicate), cc) =>
       // Found an implication b ==> acc(...)
       // Transformation causes issues if the permission involve a wildcard, so we avoid that case.
-      val res = if (!acc.perm.contains[WildcardPerm])
+      // Also, we cannot push perm and forperm expressions further in, since their value may be different at different
+      // places in the same assertion.
+      val res = if (!acc.perm.contains[WildcardPerm] && !Expressions.containsPermissionIntrospection(cond))
         (conditionalize(acc, cc.c &*& cond), cc) // Won't recurse into acc's children (see recurseFunc below)
       else
         (Implies(And(cc.c.exp, cond)(), acc)(i.pos, i.info, i.errT), cc)
@@ -38,10 +40,10 @@ class ConditionalPermissionRewriter {
       res
 
     case (i@Implies(cond, l: Let), cc) if !l.isPure =>
-      if (Expressions.proofObligations(l.exp)(p).isEmpty) {
+      if (Expressions.proofObligations(l.exp)(p).isEmpty && !Expressions.containsPermissionIntrospection(cond)) {
         (l, cc.updateContext(cc.c &*& cond))
       } else {
-        // bound expression might only be well-defined under context conditiond;
+        // bound expression might only be well-defined under context condition;
         // thus, don't push conditions further in.
         val res = (Implies(And(cc.c.exp, cond)(), l)(i.pos, i.info, i.errT), cc)
         alreadySeen.add(res._1)
@@ -50,7 +52,11 @@ class ConditionalPermissionRewriter {
 
     case (impl: Implies, cc) if !impl.right.isPure =>
       // Entering an implication b ==> A, where A is not pure, i.e. contains an accessibility accessibility
-      (impl.right, cc.updateContext(cc.c &*& impl.left))
+      if (Expressions.containsPermissionIntrospection(impl.left)) {
+        (Implies(And(cc.c.exp, impl.left)(), impl.right)(impl.pos, impl.info, impl.errT), cc)
+      } else {
+        (impl.right, cc.updateContext(cc.c &*& impl.left))
+      }
 
     case (acc: AccessPredicate, cc) if cc.c.optExp.nonEmpty =>
       // Found an accessibility predicate nested under some conditionals
@@ -86,7 +92,8 @@ class ConditionalPermissionRewriter {
   // Rewrite impure ternary expressions to a conjuction of implications in order to be able to use the implication
   // rewriter above.
   private val ternaryRewriter = ViperStrategy.Slim{
-    case ce@CondExp(cond, tExp, fExp) if !tExp.isPure || !fExp.isPure =>
+    case ce@CondExp(cond, tExp, fExp)
+        if (!tExp.isPure || !fExp.isPure) && !Expressions.containsPermissionIntrospection(cond) =>
       And(Implies(cond, tExp)(ce.pos, ce.info, ce.errT),
         Implies(Not(cond)(cond.pos, cond.info, cond.errT), fExp)(ce.pos, ce.info, ce.errT))(ce.pos, ce.info, ce.errT)
   }

From a5bd224303a8fb9a96af03c7a9698bfd1fb9f502 Mon Sep 17 00:00:00 2001
From: Silver Bot <bot@noreply.github.com>
Date: Thu, 13 Jun 2024 18:34:41 +0000
Subject: [PATCH 08/13] Update silver submodule

---
 silver | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/silver b/silver
index 86742da30..9cd85c01c 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 86742da3001d99b88df3777a8b39f682bf911451
+Subproject commit 9cd85c01c10f5f846ed2754d64de08fcc59207ee

From 17b09114fb5ac2ee092d0c61406e3f0fc6757a69 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 13 Jun 2024 21:31:04 +0200
Subject: [PATCH 09/13] Adding tests

---
 .../conditionalizePermissions/carbon_0179.vpr | 19 +++++++++++++
 .../conditionalizePermissions/let.vpr         | 15 +++++++++++
 .../silicon_0008.vpr                          | 15 +++++++++++
 .../silicon_0713.vpr                          | 27 +++++++++++++++++++
 .../conditionalizePermissions/welldef.vpr     | 16 +++++++++++
 ...iliconTestsConditionalizePermissions.scala | 15 +++++++++++
 6 files changed, 107 insertions(+)
 create mode 100644 src/test/resources/conditionalizePermissions/carbon_0179.vpr
 create mode 100644 src/test/resources/conditionalizePermissions/let.vpr
 create mode 100644 src/test/resources/conditionalizePermissions/silicon_0008.vpr
 create mode 100644 src/test/resources/conditionalizePermissions/silicon_0713.vpr
 create mode 100644 src/test/resources/conditionalizePermissions/welldef.vpr
 create mode 100644 src/test/scala/SiliconTestsConditionalizePermissions.scala

diff --git a/src/test/resources/conditionalizePermissions/carbon_0179.vpr b/src/test/resources/conditionalizePermissions/carbon_0179.vpr
new file mode 100644
index 000000000..342935e50
--- /dev/null
+++ b/src/test/resources/conditionalizePermissions/carbon_0179.vpr
@@ -0,0 +1,19 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+predicate P1(r$: Ref)
+
+predicate P3(r$: Ref)
+
+method test2()
+{
+    var b: Ref
+    var k: Perm
+
+    inhale acc(P1(b))
+    inhale acc(P3(b))
+
+    exhale perm(P3(b)) >= write ? acc(P3(b)) : (perm(P1(b)) > none ? acc(P1(b), write - perm(P3(b))) : true)
+
+    assert perm(P1(b)) == write
+}
diff --git a/src/test/resources/conditionalizePermissions/let.vpr b/src/test/resources/conditionalizePermissions/let.vpr
new file mode 100644
index 000000000..414b21add
--- /dev/null
+++ b/src/test/resources/conditionalizePermissions/let.vpr
@@ -0,0 +1,15 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+function ok(): Bool
+
+
+function val(): Ref
+    requires ok()
+
+method test()
+{
+    inhale ok() ==> let x == (val()) in acc(x.f)
+}
\ No newline at end of file
diff --git a/src/test/resources/conditionalizePermissions/silicon_0008.vpr b/src/test/resources/conditionalizePermissions/silicon_0008.vpr
new file mode 100644
index 000000000..dd18676ef
--- /dev/null
+++ b/src/test/resources/conditionalizePermissions/silicon_0008.vpr
@@ -0,0 +1,15 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+field f: Int
+
+method deAlias(x: Ref, y: Ref, k: Perm)
+  requires k >= none
+  requires acc(x.f, k) && acc(y.f, k)
+  // The following postcondition should fail in default greedy Silicon because --conditionalizePermissions creates a
+  // situation where the two chunks may or may not alias in the same branch, so they cannot definitively be merged,
+  // so greedy Silicon cannot prove the postcondition using any individual chunk.
+  //:: ExpectedOutput(postcondition.violated:insufficient.permission)
+  ensures x == y ==> acc(x.f, 2 * k)
+{}
\ No newline at end of file
diff --git a/src/test/resources/conditionalizePermissions/silicon_0713.vpr b/src/test/resources/conditionalizePermissions/silicon_0713.vpr
new file mode 100644
index 000000000..741df6373
--- /dev/null
+++ b/src/test/resources/conditionalizePermissions/silicon_0713.vpr
@@ -0,0 +1,27 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+field int: Int
+field unrelated: Int
+
+method conv_layer(a: Set[Ref])
+  requires (forall r: Ref :: r in a ==> acc(r.int, write))
+{
+  label beforeFrame
+  while (true)
+    invariant true ==>
+      (forall r: Ref :: r in a ==> acc(r.int, write)) &&
+      [
+        // on inhale
+        (forperm
+          obj: Ref [obj.unrelated] :: obj.unrelated ==
+          old[beforeFrame](obj.unrelated)) &&
+        (forperm
+          obj: Ref [obj.int] :: obj.int == old[beforeFrame](obj.int)),
+
+        // on exhale
+        true
+      ]
+  { inhale false }
+}
\ No newline at end of file
diff --git a/src/test/resources/conditionalizePermissions/welldef.vpr b/src/test/resources/conditionalizePermissions/welldef.vpr
new file mode 100644
index 000000000..3e96ec452
--- /dev/null
+++ b/src/test/resources/conditionalizePermissions/welldef.vpr
@@ -0,0 +1,16 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+function ok(): Bool
+
+
+function val(): Ref
+    requires ok()
+
+
+method test()
+{
+    inhale ok() ==> acc(val().f)
+}
\ No newline at end of file
diff --git a/src/test/scala/SiliconTestsConditionalizePermissions.scala b/src/test/scala/SiliconTestsConditionalizePermissions.scala
new file mode 100644
index 000000000..5e41c20a2
--- /dev/null
+++ b/src/test/scala/SiliconTestsConditionalizePermissions.scala
@@ -0,0 +1,15 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2022 ETH Zurich.
+
+package viper.silicon.tests
+
+class SiliconTestsConditionalizePermissions extends SiliconTests {
+  override val testDirectories: Seq[String] = Seq("conditionalizePermissions")
+
+ override val commandLineArguments: Seq[String] = Seq(
+    "--timeout", "300" /* seconds */,
+    "--conditionalizePermissions")
+}

From 1e738023a374256267e1ff4c5ddb3695655c4b8b Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Mon, 17 Jun 2024 16:06:29 +0200
Subject: [PATCH 10/13] Add comment to explain test

---
 src/test/resources/conditionalizePermissions/let.vpr | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/test/resources/conditionalizePermissions/let.vpr b/src/test/resources/conditionalizePermissions/let.vpr
index 414b21add..840932f45 100644
--- a/src/test/resources/conditionalizePermissions/let.vpr
+++ b/src/test/resources/conditionalizePermissions/let.vpr
@@ -11,5 +11,8 @@ function val(): Ref
 
 method test()
 {
+    // Test that the condition is not pushed inside the let expression to get e.g.
+    // inhale let x == (val()) in acc(x.f, ok() ? write : none)
+    // which would not be well-defined.
     inhale ok() ==> let x == (val()) in acc(x.f)
 }
\ No newline at end of file

From 422c43194be12ae3d571edc6952782bc9c72490d Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Mon, 17 Jun 2024 16:11:44 +0200
Subject: [PATCH 11/13] Avoid computing join points when it's not needed

---
 src/main/scala/rules/Executor.scala | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala
index b36dbca5b..c8b41d4e8 100644
--- a/src/main/scala/rules/Executor.scala
+++ b/src/main/scala/rules/Executor.scala
@@ -106,8 +106,12 @@ object executor extends ExecutionRules {
                      (Q: (State, Verifier) => VerificationResult)
                      : VerificationResult = {
 
-    // Find join point if it exists.
-    val jp: Option[SilverBlock] = edges.headOption.flatMap(edge => s.methodCfg.joinPoints.get(edge.source))
+    // If joining branches is enabled, find join point if it exists.
+    val jp: Option[SilverBlock] = if (s.moreJoins.id >= JoinMode.All.id) {
+      edges.headOption.flatMap(edge => s.methodCfg.joinPoints.get(edge.source))
+    } else {
+      None
+    }
 
     (edges, jp) match {
       case (Seq(), _) => Q(s, v)

From 4033dd21614b3bbba9c7615655e41c6cf0b9d80b Mon Sep 17 00:00:00 2001
From: Silver Bot <bot@noreply.github.com>
Date: Mon, 17 Jun 2024 16:45:42 +0000
Subject: [PATCH 12/13] Update silver submodule

---
 silver | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/silver b/silver
index 9cd85c01c..4a8065758 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 9cd85c01c10f5f846ed2754d64de08fcc59207ee
+Subproject commit 4a8065758868eae3414f86f3d96e843a283444fc

From 1b11869ee8c2d85eb766418c5d02fc9615a3f9f1 Mon Sep 17 00:00:00 2001
From: Silver Bot <bot@noreply.github.com>
Date: Tue, 25 Jun 2024 19:23:35 +0000
Subject: [PATCH 13/13] Update silver submodule

---
 silver | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/silver b/silver
index 4a8065758..93bc9b751 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit 4a8065758868eae3414f86f3d96e843a283444fc
+Subproject commit 93bc9b7516a710c8f01438e430058c4a54e20512