diff --git a/src/main/scala/debugger/DebugExp.scala b/src/main/scala/debugger/DebugExp.scala
index 1a98b97c4..d88d38f07 100644
--- a/src/main/scala/debugger/DebugExp.scala
+++ b/src/main/scala/debugger/DebugExp.scala
@@ -85,6 +85,7 @@ object DebugExp {
     debugExp
   }
 }
+
 class DebugExp(val id: Int,
                val description : Option[String],
                val originalExp : Option[ast.Exp],
@@ -173,7 +174,6 @@ class DebugExp(val id: Int,
 
 }
 
-
 class ImplicationDebugExp(id: Int,
                           description : Option[String],
                           originalExp : Option[ast.Exp],
@@ -203,7 +203,6 @@ class ImplicationDebugExp(id: Int,
   }
 }
 
-
 class QuantifiedDebugExp(id: Int,
                          description : Option[String],
                          isInternal_ : Boolean,
@@ -234,7 +233,6 @@ class QuantifiedDebugExp(id: Int,
   }
 }
 
-
 class DebugExpPrintConfiguration {
   var isPrintInternalEnabled: Boolean = false
   var nChildrenToShow: Int = 5
@@ -284,7 +282,6 @@ class DebugExpPrintConfiguration {
 }
 
 class DebugAxiom(val description: String, val terms: InsertionOrderedSet[Term]){
-
   override def toString: String = {
     s"$description:\n\t\t${terms.mkString("\n\t\t")}\n"
   }
diff --git a/src/main/scala/debugger/SiliconDebugger.scala b/src/main/scala/debugger/SiliconDebugger.scala
index 1efe421b2..20938b42e 100644
--- a/src/main/scala/debugger/SiliconDebugger.scala
+++ b/src/main/scala/debugger/SiliconDebugger.scala
@@ -6,9 +6,8 @@ import viper.silicon.interfaces.state.Chunk
 import viper.silicon.interfaces.{Failure, SiliconDebuggingFailureContext, Success, VerificationResult}
 import viper.silicon.resources.{FieldID, PredicateID}
 import viper.silicon.rules.evaluator
-import viper.silicon.state.Heap
+import viper.silicon.state._
 import viper.silicon.state.terms.{Term, True}
-import viper.silicon.state.{BasicChunk, IdentifierFactory, MagicWandChunk, QuantifiedFieldChunk, QuantifiedMagicWandChunk, QuantifiedPredicateChunk, State}
 import viper.silicon.utils.ast.simplifyVariableName
 import viper.silicon.verifier.{MainVerifier, Verifier, WorkerVerifier}
 import viper.silver.ast
@@ -54,26 +53,60 @@ case class ProofObligation(s: State,
       }) +
       s"\n\t\t${originalErrorReason.readableMessage}\n\n"
 
-  private def stateString: String = {
-    val storeString = if (printConfig.printInternalTermRepresentation)
+  private def storeString: String = {
+    if (printConfig.printInternalTermRepresentation)
       s"Store:\n\t\t${s.g.values.map(v => s"${v._1} -> ${v._2._1}").mkString("\n\t\t")}\n\n"
     else
       s"Store:\n\t\t${s.g.values.map(v => s"${v._1} -> ${v._2._2.get}").mkString("\n\t\t")}\n\n"
+  }
 
-    def heapToString(h: Heap): String = h.values.map(chunkString).mkString("\n\t\t")
-    val heapString = if (printConfig.printOldHeaps)
-      s"Current Heap:\n\t\t${heapToString(s.h)}\n\n" + s.oldHeaps.map {case (k, v) => s"Heap $k:\n\t\t${heapToString(v)}\n\n"}.mkString("")
-    else
-      s"Heap:\n\t\t${s.h.values.map(chunkString).mkString("\n\t\t")}\n\n"
+  private def heapToString(h: Heap): String =
+    if (h.values.nonEmpty) h.values.map(c => s"\t\t${chunkString(c)}\n").mkString("")
+    else "\t\t(Empty heap)\n"
+
+  private def debugHeapString(label: String, debugHeap: DebugHeap): String = {
+    val condString = if (debugHeap.branchConds.nonEmpty)
+      "\tNew branch conditions: " + debugHeap.branchConds.map(bc => bc._1.toString).mkString(", ") + "\n"
+    else ""
+    val causeString = debugHeap.cause match {
+      case InhalePre() => "inhale precondition"
+      case ExhalePost() => "exhale postcondition"
+      case InhaleInv() => "inhale loop invariants"
+      case ExhaleInv() => "exhale loop invariants"
+      case MergeContext() => "merge framed heap"
+      case CreateLabel() => "heap label"
+      case StateConsolidation() => "state consolidation"
+      case ExecStmt(stmt) => s"\"$stmt\""
+      case EvalExp(exp) => s"\"$exp\""
+    }
+    val causeString2 = debugHeap.intermediateCause match {
+      case Some(exp) => s"\"$exp\" during $causeString"
+      case None => causeString
+    }
+    s"Heap $label:\n" +
+      s"\tParent: ${debugHeap.parentLabel}\n" +
+      s"\tCause: $causeString2\n" +
+      condString +
+      heapToString(debugHeap.heap) + "\n"
+  }
 
-    storeString + heapString
+  private def heapString: String = {
+    if (!printConfig.printOldHeaps)
+      s"Heap:\n${heapToString(s.h)}\n"
+    else {
+      s"Current Heap:\n${heapToString(s.h)}\n" +
+        s.debugOldHeaps.map { case (label, dh) => debugHeapString(label, dh) }.mkString("")
+    }
   }
 
+  private def simplify[N <: Node](n: N): N = Simplifier.simplify(n, assumeWelldefinedness = true)
+
   private def branchConditionString: String = {
     if (printConfig.printInternalTermRepresentation)
       s"Branch Conditions:\n\t\t${branchConditions.filter(bc => bc != True).mkString("\n\t\t")}\n\n"
     else
-      s"Branch Conditions:\n\t\t${branchConditionExps.map(bc => Simplifier.simplify(bc._2, true)).filter(bc => bc != ast.TrueLit()()).mkString("\n\t\t")}\n\n"
+      s"Branch Conditions:\n\t\t${branchConditionExps.map(bc => simplify(bc._2))
+        .filter(bc => bc != ast.TrueLit()()).mkString("\n\t\t")}\n\n"
   }
 
   private def chunkString(c: Chunk): String = {
@@ -82,51 +115,51 @@ case class ProofObligation(s: State,
     val res = c match {
       case bc: BasicChunk =>
         val snapExpString = bc.snapExp match {
-          case Some(e) => s" -> ${Simplifier.simplify(e, true)}"
+          case Some(e) => s" -> ${simplify(e)}"
           case _ => ""
         }
         bc.resourceID match {
-          case FieldID => s"acc(${bc.argsExp.get.head}.${bc.id}, ${Simplifier.simplify(bc.permExp.get, true)})$snapExpString"
-          case PredicateID => s"acc(${bc.id}(${bc.argsExp.mkString(", ")}), ${Simplifier.simplify(bc.permExp.get, true)})"
+          case FieldID => s"acc(${bc.argsExp.get.head}.${bc.id}, ${simplify(bc.permExp.get)})$snapExpString"
+          case PredicateID => s"acc(${bc.id}(${bc.argsExp.mkString(", ")}), ${simplify(bc.permExp.get)})"
         }
       case mwc: MagicWandChunk =>
         val shape = mwc.id.ghostFreeWand
         val expBindings = mwc.bindings.map(b => b._1 -> b._2._2.get)
         val instantiated = shape.replace(expBindings)
-        s"acc(${instantiated.toString}, ${Simplifier.simplify(mwc.permExp.get, true)})"
+        s"acc(${instantiated.toString}, ${simplify(mwc.permExp.get)})"
       case qfc: QuantifiedFieldChunk =>
         if (qfc.singletonRcvrExp.isDefined) {
-          val receiver = Simplifier.simplify(qfc.singletonRcvrExp.get, true)
-          val perm = Simplifier.simplify(qfc.permExp.get.replace(qfc.quantifiedVarExps.get.head.localVar, receiver), true)
-          s"acc(${receiver}.${qfc.id}, ${perm})"
+          val receiver = simplify(qfc.singletonRcvrExp.get)
+          val perm = simplify(qfc.permExp.get.replace(qfc.quantifiedVarExps.get.head.localVar, receiver))
+          s"acc($receiver.${qfc.id}, $perm)"
         } else {
           val varsString = qfc.quantifiedVarExps.get.map(v => s"${v.name}: ${v.typ}").mkString(", ")
           val qvarsString = "forall " + qfc.invs.get.qvarExps.get.map(v => s"${v.name}: ${v.typ}").mkString(", ")
-          val varsEqualString = qfc.quantifiedVarExps.get.zip(qfc.invs.get.invertibleExps.get).map(v => s"${v._1.name} == ${Simplifier.simplify(v._2, true)}").mkString(" && ")
-          s"forall ${varsString} :: ${qvarsString} :: ${varsEqualString} ==> acc(${qfc.quantifiedVarExps.get.head.name}.${qfc.id}, ${Simplifier.simplify(qfc.permExp.get, true)})"
+          val varsEqualString = qfc.quantifiedVarExps.get.zip(qfc.invs.get.invertibleExps.get).map(v => s"${v._1.name} == ${simplify(v._2)}").mkString(" && ")
+          s"forall $varsString :: $qvarsString :: $varsEqualString ==> acc(${qfc.quantifiedVarExps.get.head.name}.${qfc.id}, ${simplify(qfc.permExp.get)})"
         }
       case qpc: QuantifiedPredicateChunk =>
         if (qpc.singletonArgExps.isDefined) {
-          s"acc(${qpc.id}(${qpc.singletonArgExps.get.map(e => Simplifier.simplify(e, true)).mkString(", ")}), ${Simplifier.simplify(qpc.permExp.get, true)})"
+          s"acc(${qpc.id}(${qpc.singletonArgExps.get.map(e => simplify(e)).mkString(", ")}), ${simplify(qpc.permExp.get)})"
         } else {
           val varsString = qpc.quantifiedVarExps.get.map(v => s"${v.name}: ${v.typ}").mkString(", ")
           val qvarsString = "forall " + qpc.invs.get.qvarExps.get.map(v => s"${v.name}: ${v.typ}").mkString(", ")
-          val varsEqualString = qpc.quantifiedVarExps.get.zip(qpc.invs.get.invertibleExps.get).map(v => s"${v._1.name} == ${Simplifier.simplify(v._2, true)}").mkString(" && ")
-          s"forall ${varsString} :: ${qvarsString} :: ${varsEqualString} ==> acc(${qpc.id}(${qpc.quantifiedVarExps.get.map(_.name).mkString(", ")}), ${Simplifier.simplify(qpc.permExp.get, true)})"
+          val varsEqualString = qpc.quantifiedVarExps.get.zip(qpc.invs.get.invertibleExps.get).map(v => s"${v._1.name} == ${simplify(v._2)}").mkString(" && ")
+          s"forall $varsString :: $qvarsString :: $varsEqualString ==> acc(${qpc.id}(${qpc.quantifiedVarExps.get.map(_.name).mkString(", ")}), ${simplify(qpc.permExp.get)})"
         }
       case qwc: QuantifiedMagicWandChunk =>
         val shape = qwc.id.ghostFreeWand
         if (qwc.singletonArgExps.isDefined) {
-          val instantiated = shape.replace(shape.subexpressionsToEvaluate(s.program).zip(qwc.singletonArgExps.get).map(e => e._1 -> Simplifier.simplify(e._2, true)).toMap)
-          val permReplaced = Simplifier.simplify(qwc.permExp.get.replace(qwc.quantifiedVarExps.get.zip(qwc.singletonArgExps.get).map(e => e._1.localVar -> e._2).toMap), true)
+          val instantiated = shape.replace(shape.subexpressionsToEvaluate(s.program).zip(qwc.singletonArgExps.get).map(e => e._1 -> simplify(e._2)).toMap)
+          val permReplaced = simplify(qwc.permExp.get.replace(qwc.quantifiedVarExps.get.zip(qwc.singletonArgExps.get).map(e => e._1.localVar -> e._2).toMap))
 
-          s"acc(${instantiated.toString}, ${permReplaced})"
+          s"acc(${instantiated.toString}, $permReplaced)"
         } else{
           val varsString = qwc.quantifiedVarExps.get.map(v => s"${v.name}: ${v.typ}").mkString(", ")
           val qvarsString = "forall " + qwc.invs.get.qvarExps.get.map(v => s"${v.name}: ${v.typ}").mkString(", ")
-          val varsEqualString = qwc.quantifiedVarExps.get.zip(qwc.invs.get.invertibleExps.get).map(v => s"${v._1.name} == ${Simplifier.simplify(v._2, true)}").mkString(" && ")
-          val instantiated = shape.replace(shape.subexpressionsToEvaluate(s.program).zip(qwc.invs.get.invertibleExps.get).map(e => e._1 -> Simplifier.simplify(e._2, true)).toMap)
-          s"forall ${varsString} :: ${qvarsString} :: ${varsEqualString} ==> acc(${instantiated}, ${Simplifier.simplify(qwc.permExp.get, true)})"
+          val varsEqualString = qwc.quantifiedVarExps.get.zip(qwc.invs.get.invertibleExps.get).map(v => s"${v._1.name} == ${simplify(v._2)}").mkString(" && ")
+          val instantiated = shape.replace(shape.subexpressionsToEvaluate(s.program).zip(qwc.invs.get.invertibleExps.get).map(e => e._1 -> simplify(e._2)).toMap)
+          s"forall $varsString :: $qvarsString :: $varsEqualString ==> acc($instantiated, ${simplify(qwc.permExp.get)})"
         }
     }
     res
@@ -166,7 +199,8 @@ case class ProofObligation(s: State,
   }
 
   override def toString: String = {
-    "\n" + originalErrorInfo + branchConditionString + stateString + axiomsString + declarationsString + assumptionString + assertionString
+    "\n" + originalErrorInfo + branchConditionString + storeString + heapString +
+      axiomsString + declarationsString + assumptionString + assertionString
   }
 }
 
@@ -306,10 +340,10 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
             obl = removeAssumptions(obl)
             println(s"Current obligation:\n$obl")
           case "af" | "assume" | "add free assumption" =>
-            obl = addAssumptions(obl, true)
+            obl = addAssumptions(obl, free = true)
             println(s"Current obligation:\n$obl")
           case "ap" | "assert" | "add and prove assumption" =>
-            obl = addAssumptions(obl, false)
+            obl = addAssumptions(obl, free = false)
             println(s"Current obligation:\n$obl")
           //case "ass" | "assertion" | "set assertion" =>
           //  obl = chooseAssertion(obl)
@@ -367,7 +401,7 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
     }
   }
 
-  private def showAssumptions(obl: ProofObligation) = {
+  private def showAssumptions(obl: ProofObligation): Unit = {
     println(s"Enter the assumption you want to zoom in on:")
     val userInput = readLine()
     val indexOpt = userInput.trim.toIntOption
@@ -570,12 +604,9 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
       case "false" | "0" | "f" => obl.printConfig.printOldHeaps = false
       case _ =>
     }
-
-    //println(s"Enter the new value for nodeToHierarchyLevelMap:")
-    //obl.printConfig.addHierarchyLevelForId(readLine())
   }
 
-  private def printSingleAssumption(obl: ProofObligation): Unit={
+  private def printSingleAssumption(obl: ProofObligation): Unit = {
     println(s"Enter the id of the assumption that should be printed:")
     val userInput = readLine()
     userInput.toIntOption match {
diff --git a/src/main/scala/rules/ChunkSupporter.scala b/src/main/scala/rules/ChunkSupporter.scala
index 6988b2d87..bcc26d107 100644
--- a/src/main/scala/rules/ChunkSupporter.scala
+++ b/src/main/scala/rules/ChunkSupporter.scala
@@ -91,7 +91,7 @@ object chunkSupporter extends ChunkSupportRules {
            * registered with the function recorder. However, since nothing was consumed,
            * returning the unit snapshot seems more appropriate.
            */
-          val fresh = v2.decider.fresh(sorts.Snap, Option.when(withExp)(PUnknown()))
+          val fresh = v2.decider.fresh(sorts.Snap, Option.when(debugOn)(PUnknown()))
           val s3 = s2.copy(functionRecorder = s2.functionRecorder.recordFreshSnapshot(fresh.applicable))
           Q(s3, h2, Some(fresh), v2)
         case None => Q(s2, h2, None, v2)
@@ -164,7 +164,7 @@ object chunkSupporter extends ChunkSupportRules {
       val interpreter = new NonQuantifiedPropertyInterpreter(heap.values, v)
       val resource = Resources.resourceDescriptions(chunk.resourceID)
       val pathCond = interpreter.buildPathConditionsForChunk(chunk, resource.instanceProperties(s.mayAssumeUpperBounds))
-      pathCond.foreach(p => v.decider.assume(p._1, Option.when(withExp)(DebugExp.createInstance(p._2, p._2))))
+      pathCond.foreach(p => v.decider.assume(p._1, Option.when(debugOn)(DebugExp.createInstance(p._2, p._2))))
     }
 
     findChunk[NonQuantifiedChunk](h.values, id, args, v) match {
@@ -191,7 +191,7 @@ object chunkSupporter extends ChunkSupportRules {
         } else {
           if (v.decider.check(ch.perm !== NoPerm, Verifier.config.checkTimeout())) {
             val constraintExp = permsExp.map(pe => ast.PermLtCmp(pe, ch.permExp.get)(pe.pos, pe.info, pe.errT))
-            v.decider.assume(PermLess(perms, ch.perm), Option.when(withExp)(DebugExp.createInstance(constraintExp, constraintExp)))
+            v.decider.assume(PermLess(perms, ch.perm), Option.when(debugOn)(DebugExp.createInstance(constraintExp, constraintExp)))
             val newPermExp = permsExp.map(pe => ast.PermSub(ch.permExp.get, pe)(pe.pos, pe.info, pe.errT))
             val newChunk = ch.withPerm(PermMinus(ch.perm, perms), newPermExp)
             val takenChunk = ch.withPerm(perms, permsExp)
@@ -257,7 +257,7 @@ object chunkSupporter extends ChunkSupportRules {
         Q(s, ch.snap, v)
       case _ if v.decider.checkSmoke(true) =>
         if (s.isInPackage) {
-          val snap = v.decider.fresh(v.snapshotSupporter.optimalSnapshotSort(resource, s, v), Option.when(withExp)(PUnknown()))
+          val snap = v.decider.fresh(v.snapshotSupporter.optimalSnapshotSort(resource, s, v), Option.when(debugOn)(PUnknown()))
           Q(s, snap, v)
         } else {
           Success() // TODO: Mark branch as dead?
diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala
index ce1306791..84171cbce 100644
--- a/src/main/scala/rules/Consumer.scala
+++ b/src/main/scala/rules/Consumer.scala
@@ -253,9 +253,9 @@ object consumer extends ConsumptionRules {
               val lossExp = ePermNew.map(p => ast.PermMul(p, s2.permissionScalingFactorExp.get)(p.pos, p.info, p.errT))
               val s3 = v2.heapSupporter.triggerResourceIfNeeded(s2, accPred.loc, tArgs, eArgsNew, v2)
               v2.heapSupporter.consumeSingle(s3, h, accPred.loc, tArgs, eArgsNew, loss, lossExp, returnSnap, pve, v2)((s4, h4, snap, v4) => {
-                val s5 = s4.copy(constrainableARPs = s.constrainableARPs,
+                val s4a = s4.copy(constrainableARPs = s.constrainableARPs,
                                  partiallyConsumedHeap = Some(h4))
-                Q(s5, h4, snap, v4)
+                Q(s4a, h4, snap, v4)
               })
             })))
 
@@ -277,7 +277,7 @@ object consumer extends ConsumptionRules {
           }
         val resource = resAcc.res(s.program)
         val tFormalArgs = s.getFormalArgVars(resource, v)
-        val eFormalArgs = Option.when(withExp)(s.getFormalArgDecls(resource))
+        val eFormalArgs = Option.when(debugOn)(s.getFormalArgDecls(resource))
         val optTrigger =
           if (forall.triggers.isEmpty) None
           else Some(forall.triggers)
@@ -311,10 +311,11 @@ object consumer extends ConsumptionRules {
               notInjectiveReason = QPAssertionNotInjective(resAcc),
               insufficientPermissionReason = insuffReason,
               v1)((s2, h2, snap, v2) => {
-              val s3 = s2.copy(constrainableARPs = s.constrainableARPs, functionRecorder = s2.functionRecorder.leaveQuantifiedExp(qpa))
-              Q(s3, h2, snap, v2)
+              val s2a = s2.copy(constrainableARPs = s.constrainableARPs, functionRecorder = s2.functionRecorder.leaveQuantifiedExp(qpa))
+              Q(s2a, h2, snap, v2)
             })
-          case (s1, _, _, _, _, None, v1) => Q(s1, h, if (returnSnap) Some(Unit) else None, v1)
+          case (s1, _, _, _, _, None, v1) =>
+            Q(s1, h, if (returnSnap) Some(Unit) else None, v1)
         }
 
       case let: ast.Let if !let.isPure =>
@@ -364,8 +365,8 @@ object consumer extends ConsumptionRules {
           case Seq(entry1, entry2) => // Both branches are alive
             val mergedData = (
               State.mergeHeap(
-                entry1.data._1, And(entry1.pathConditions.branchConditions), Option.when(withExp)(BigAnd(entry1.pathConditions.branchConditionExps.map(_._2.get))),
-                entry2.data._1, And(entry2.pathConditions.branchConditions), Option.when(withExp)(BigAnd(entry2.pathConditions.branchConditionExps.map(_._2.get))),
+                entry1.data._1, And(entry1.pathConditions.branchConditions), Option.when(debugOn)(BigAnd(entry1.pathConditions.branchConditionExps.map(_._2.get))),
+                entry2.data._1, And(entry2.pathConditions.branchConditions), Option.when(debugOn)(BigAnd(entry2.pathConditions.branchConditionExps.map(_._2.get))),
               ),
               // Assume that entry1.pcs is inverse of entry2.pcs
               (entry1.data._2, entry2.data._2) match {
@@ -409,18 +410,18 @@ object consumer extends ConsumptionRules {
         val termToAssert = t match {
           case Quantification(q, vars, body, trgs, name, isGlob, weight) =>
             val transformed = FunctionPreconditionTransformer.transform(body, s3.program)
-            v2.decider.assume(Quantification(q, vars, transformed, trgs, name+"_precondition", isGlob, weight), Option.when(withExp)(e), eNew)
+            v2.decider.assume(Quantification(q, vars, transformed, trgs, name+"_precondition", isGlob, weight), Option.when(debugOn)(e), eNew)
             Quantification(q, vars, Implies(transformed, body), trgs, name, isGlob, weight)
           case _ => t
         }
         v2.decider.assert(termToAssert) {
           case true =>
-            v2.decider.assume(t, Option.when(withExp)(e), eNew)
+            v2.decider.assume(t, Option.when(debugOn)(e), eNew)
             QS(s3, v2)
           case false =>
             val failure = createFailure(pve dueTo AssertionFalse(e), v2, s3, termToAssert, eNew)
             if (s3.retryLevel == 0 && v2.reportFurtherErrors()){
-              v2.decider.assume(t, Option.when(withExp)(e), eNew)
+              v2.decider.assume(t, Option.when(debugOn)(e), eNew)
               failure combine QS(s3, v2)
             } else failure}})
     })((s4, v4) => {
diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala
index 53713fab3..833edf3dd 100644
--- a/src/main/scala/rules/Evaluator.scala
+++ b/src/main/scala/rules/Evaluator.scala
@@ -72,7 +72,7 @@ object evaluator extends EvaluationRules {
                     : VerificationResult = {
 
     if (es.isEmpty)
-      Q(s, ts.reverse, if (withExp) Some(List.empty) else None, v)
+      Q(s, ts.reverse, if (debugOn) Some(List.empty) else None, v)
     else
       eval(s, es.head, pvef(es.head), v)((s1, t, eNew, v1) =>
         evals2(s1, es.tail, t :: ts,  pvef, v1)((s2, ts2, es2, v2) => Q(s2, ts2, eNew.map(eN => eN :: es2.get), v2)))
@@ -145,7 +145,8 @@ object evaluator extends EvaluationRules {
   protected def eval2(s: State, e: ast.Exp, pve: PartialVerificationError, v: Verifier)
                      (Q: (State, Term, Option[ast.Exp], Verifier) => VerificationResult)
                      : VerificationResult = {
-    val eOpt = Option.when(withExp)(e)
+    val eOpt = Option.when(debugOn)(e)
+
     val resultTerm = e match {
       case _: ast.TrueLit => Q(s, True, eOpt, v)
       case _: ast.FalseLit => Q(s, False, eOpt, v)
@@ -154,9 +155,9 @@ object evaluator extends EvaluationRules {
       case ast.IntLit(bigval) => Q(s, IntLiteral(bigval), eOpt, v)
 
       case ast.EqCmp(e0, e1) => evalBinOp(s, e0, e1, Equals, pve, v)((s1, t, e0New, e1New, v1) =>
-        Q(s1, t, Option.when(withExp)(ast.EqCmp(e0New.get, e1New.get)(e.pos, e.info, e.errT)), v1))
+        Q(s1, t, Option.when(debugOn)(ast.EqCmp(e0New.get, e1New.get)(e.pos, e.info, e.errT)), v1))
       case ast.NeCmp(e0, e1) => evalBinOp(s, e0, e1, (p0: Term, p1: Term) => Not(Equals(p0, p1)), pve, v)((s1, t, e0New, e1New, v1) =>
-        Q(s1, t, Option.when(withExp)(ast.NeCmp(e0New.get, e1New.get)(e.pos, e.info, e.errT)), v1))
+        Q(s1, t, Option.when(debugOn)(ast.NeCmp(e0New.get, e1New.get)(e.pos, e.info, e.errT)), v1))
 
       case x: ast.LocalVarWithVersion =>
         val sort = v.symbolConverter.toSort(x.typ)
@@ -181,7 +182,7 @@ object evaluator extends EvaluationRules {
 
       case _: ast.WildcardPerm =>
         val (tVar, tConstraints, eVar) = v.decider.freshARP()
-        val constraintExp = Option.when(withExp)(DebugExp.createInstance(s"${eVar.get.toString} > none", true))
+        val constraintExp = Option.when(debugOn)(DebugExp.createInstance(s"${eVar.get.toString} > none", true))
         v.decider.assumeDefinition(tConstraints, constraintExp)
         /* TODO: Only record wildcards in State.constrainableARPs that are used in exhale
          *       position. Currently, wildcards used in inhale position (only) may not be removed
@@ -204,15 +205,13 @@ object evaluator extends EvaluationRules {
 
           val ve = pve dueTo InsufficientPermission(fa)
           v.heapSupporter.evalFieldAccess(s1, fa, tRcvr, eRcvr, ve, v1)((s2, snap, v2) => {
-            val (debugHeapName, debugLabel) = v1.getDebugOldLabel(s2, fa.pos, Some(magicWandSupporter.getEvalHeap(s2)))
-            val newFa = Option.when(withExp)({
+            val s2a = if (debugOn && s.recordIntermediateHeaps) v2.recordIntermediateHeap(s2, fa) else s2
+            val newFa = Option.when(debugOn)({
+              val debugLabel = v2.getDebugOldLabel(s2a, fa.pos)
               if (s1.isEvalInOld) ast.FieldAccess(eRcvr.get, fa.field)(fa.pos, fa.info, fa.errT)
               else ast.DebugLabelledOld(ast.FieldAccess(eRcvr.get, fa.field)(), debugLabel)(fa.pos, fa.info, fa.errT)
             })
-            val s3 = if (Verifier.config.enableDebugging() && !s2.isEvalInOld)
-              s2.copy(oldHeaps = s2.oldHeaps + (debugHeapName -> magicWandSupporter.getEvalHeap(s2)))
-            else s2
-            Q(s3, snap, newFa, v2)
+            Q(s2a, snap, newFa, v2)
           })
         })
 
@@ -252,7 +251,7 @@ object evaluator extends EvaluationRules {
       case l@ast.Let(x, e0, e1) =>
         eval(s, e0, pve, v)((s1, t0, e0New, v1) => {
           val t = v1.decider.appliedFresh("letvar", v1.symbolConverter.toSort(x.typ), s1.relevantQuantifiedVariables.map(_._1))
-          val debugExp = Option.when(withExp)(DebugExp.createInstance("letvar assignment", InsertionOrderedSet(DebugExp.createInstance(ast.EqCmp(x.localVar, e0)(), ast.EqCmp(x.localVar, e0New.get)()))))
+          val debugExp = Option.when(debugOn)(DebugExp.createInstance("letvar assignment", InsertionOrderedSet(DebugExp.createInstance(ast.EqCmp(x.localVar, e0)(), ast.EqCmp(x.localVar, e0New.get)()))))
           v1.decider.assumeDefinition(BuiltinEquals(t, t0), debugExp)
           val newFuncRec = s1.functionRecorder.recordFreshSnapshot(t.applicable.asInstanceOf[Function]).enterLet(l)
           val possibleTriggersBefore = if (s1.recordPossibleTriggers) s1.possibleTriggers else Map.empty
@@ -414,21 +413,22 @@ object evaluator extends EvaluationRules {
           val inSorts = tArgs map (_.sort)
           val outSort = v1.symbolConverter.toSort(dfa.typ)
           val fi = v1.symbolConverter.toFunction(s.program.findDomainFunction(funcName), inSorts :+ outSort, s.program)
-          val dfaP = Option.when(withExp)(ast.DomainFuncApp(funcName, eArgsNew.get, m)(dfa.pos, dfa.info, dfa.typ, dfa.domainName, dfa.errT))
+          val dfaP = Option.when(debugOn)(ast.DomainFuncApp(funcName, eArgsNew.get, m)(dfa.pos, dfa.info, dfa.typ, dfa.domainName, dfa.errT))
           Q(s1, App(fi, tArgs), dfaP, v1)})
 
       case bf @ ast.BackendFuncApp(funcName, eArgs) =>
         evals(s, eArgs, _ => pve, v)((s1, tArgs, eArgsNew, v1) => {
           val func = s.program.findDomainFunction(funcName)
           val fi = v1.symbolConverter.toFunction(func, s.program)
-          val bfP = Option.when(withExp)(ast.BackendFuncApp(funcName, eArgsNew.get)(bf.pos, bf.info, bf.typ, bf.interpretation, bf.errT))
+          val bfP = Option.when(debugOn)(ast.BackendFuncApp(funcName, eArgsNew.get)(bf.pos, bf.info, bf.typ, bf.interpretation, bf.errT))
           Q(s1, App(fi, tArgs), bfP, v1)})
 
-      case ast.CurrentPerm(resacc) =>
+      case cp @ ast.CurrentPerm(resacc) =>
         val h = s.partiallyConsumedHeap.getOrElse(s.h)
         evalResourceAccess(s, resacc, pve, v)((s1, identifier, args, eArgsNew, v1) => {
-          v1.heapSupporter.evalCurrentPerm(s1, h, resacc, identifier, args, eArgsNew, v1)((s2, t, v2) =>
-          Q(s2, t, Option.when(withExp)(e), v2))
+          val s1a = if (debugOn && s1.recordIntermediateHeaps) v1.recordIntermediateHeap(s1, cp) else s1
+          v1.heapSupporter.evalCurrentPerm(s1a, h, resacc, identifier, args, eArgsNew, v1)((s2, t, v2) =>
+          Q(s2, t, Option.when(debugOn)(e), v2))
         })
 
       case ast.ForPerm(vars, resourceAccess, body) =>
@@ -439,14 +439,14 @@ object evaluator extends EvaluationRules {
 
         val localVars = vars map (_.localVar)
         val varPairs: Seq[(Var, ast.LocalVar)] = localVars map (x =>
-          (v.decider.fresh(x.name, v.symbolConverter.toSort(x.typ), Option.when(withExp)(extractPTypeFromExp(x))), x))
+          (v.decider.fresh(x.name, v.symbolConverter.toSort(x.typ), Option.when(debugOn)(extractPTypeFromExp(x))), x))
 
-        val varsNew = Option.when(withExp)(varPairs.map(tv => ast.LocalVarDecl(tv._1.id.name, tv._2.typ)(tv._2.pos, tv._2.info, tv._2.errT)))
+        val varsNew = Option.when(debugOn)(varPairs.map(tv => ast.LocalVarDecl(tv._1.id.name, tv._2.typ)(tv._2.pos, tv._2.info, tv._2.errT)))
         val termExpPair: Seq[(Term, Option[ast.Exp])] = varPairs map (x =>
-          (x._1.asInstanceOf[Term], Option.when(withExp)(LocalVarWithVersion(simplifyVariableName(x._1.id.name), x._2.typ)(x._2.pos, x._2.info, x._2.errT).asInstanceOf[ast.Exp])))
+          (x._1.asInstanceOf[Term], Option.when(debugOn)(LocalVarWithVersion(simplifyVariableName(x._1.id.name), x._2.typ)(x._2.pos, x._2.info, x._2.errT).asInstanceOf[ast.Exp])))
         val gVars = Store(localVars zip termExpPair)
 
-        val s2 = s1.copy(s1.g + gVars, quantifiedVariables = varPairs.map(v => v._1 -> Option.when(withExp)(v._2)) ++ s1.quantifiedVariables)
+        val s2 = s1.copy(s1.g + gVars, quantifiedVariables = varPairs.map(v => v._1 -> Option.when(debugOn)(v._2)) ++ s1.quantifiedVariables)
 
         evals(s2, args, _ => pve, v)((s3, ts, es, v3) => {
           val possibleConds = v3.heapSupporter.collectForPermConditions(s3, resource, varPairs, ts, es)
@@ -463,18 +463,18 @@ object evaluator extends EvaluationRules {
               val (t, (e0, e1), qVars, defs, triggers) = conds.head
               evalImplies(s.copy(g = s.g + defs), t, (e0, e1), body, false, pve, v)((sNext, tImplies, bodyNew, vNext) => {
                 val tQuant = SimplifyingForall(qVars, tImplies, triggers)
-                val eQuantNew = Option.when(withExp)(ast.Forall(varsNew.get, Seq(), ast.Implies(e0, bodyNew.get)())())
+                val eQuantNew = Option.when(debugOn)(ast.Forall(varsNew.get, Seq(), ast.Implies(e0, bodyNew.get)())())
                 v.symbExLog.closeScope(uidImplies)
-                evalOptions(sNext.copy(g = s3.g), conds.tail, tQuant +: ts, Option.when(withExp)(eQuantNew.get +: es.get), vNext)(QB)
+                evalOptions(sNext.copy(g = s3.g), conds.tail, tQuant +: ts, Option.when(debugOn)(eQuantNew.get +: es.get), vNext)(QB)
               })
             } else {
               QB(s, ts, es, v)
             }
           }
 
-          evalOptions(s3, possibleConds, Seq.empty, Option.when(withExp)(Seq.empty), v3)((s4, tConjuncts, eConjuncts, v4) => {
+          evalOptions(s3, possibleConds, Seq.empty, Option.when(debugOn)(Seq.empty), v3)((s4, tConjuncts, eConjuncts, v4) => {
             val s5 = s4.copy(h = s.h, g = s.g, quantifiedVariables = s.quantifiedVariables)
-            Q(s5, And(tConjuncts), Option.when(withExp)(BigAnd(eConjuncts.get)), v4)
+            Q(s5, And(tConjuncts), Option.when(debugOn)(BigAnd(eConjuncts.get)), v4)
           })
         })
 
@@ -535,10 +535,10 @@ object evaluator extends EvaluationRules {
             val auxNonGlobalsExp = auxExps.map(_._2)
             val commentGlobal = "Nested auxiliary terms: globals (aux)"
             v1.decider.prover.comment(commentGlobal)
-            v1.decider.assume(tAuxGlobal, Option.when(withExp)(DebugExp.createInstance(description=commentGlobal, children=auxGlobalsExp.get)), enforceAssumption = false)
+            v1.decider.assume(tAuxGlobal, Option.when(debugOn)(DebugExp.createInstance(description=commentGlobal, children=auxGlobalsExp.get)), enforceAssumption = false)
             val commentNonGlobals = "Nested auxiliary terms: non-globals (aux)"
             v1.decider.prover.comment(commentNonGlobals)
-            v1.decider.assume(tAuxHeapIndep/*tAux*/, Option.when(withExp)(DebugExp.createInstance(description=commentNonGlobals, children=auxNonGlobalsExp.get)), enforceAssumption = false)
+            v1.decider.assume(tAuxHeapIndep/*tAux*/, Option.when(debugOn)(DebugExp.createInstance(description=commentNonGlobals, children=auxNonGlobalsExp.get)), enforceAssumption = false)
 
             if (qantOp == Exists) {
               // For universal quantification, the non-global auxiliary assumptions will contain the information that
@@ -547,7 +547,7 @@ object evaluator extends EvaluationRules {
               // all function preconditions hold. This is not enough: We need to know (and have checked that)
               // function preconditions hold for *all* possible values of the quantified variables.
               // So we explicitly add this assumption here.
-              val debugExp = Option.when(withExp)({
+              val debugExp = Option.when(debugOn)({
                 val expNew = ast.Forall(eQuant.variables, eTriggers, bodyNew.get.head)(sourceQuant.pos, sourceQuant.info, sourceQuant.errT)
                 val exp = ast.Forall(eQuant.variables, eTriggers, body)(sourceQuant.pos, sourceQuant.info, sourceQuant.errT)
                 DebugExp.createInstance(exp, expNew)
@@ -556,7 +556,7 @@ object evaluator extends EvaluationRules {
             }
 
             val tQuant = Quantification(qantOp, tVars, tBody, tTriggers, name, quantWeight)
-            val eQuantNew = Option.when(withExp)(buildQuantExp(qantOp, eVars.get, bodyNew.get.head, Seq.empty))
+            val eQuantNew = Option.when(debugOn)(buildQuantExp(qantOp, eVars.get, bodyNew.get.head, Seq.empty))
             val s2 = s1.copy(functionRecorder = s1.functionRecorder.leaveQuantifiedExp(sourceQuant))
             Q(s2, tQuant, eQuantNew, v1)
           case (s1, _, _, _, _, None, v1) =>
@@ -571,17 +571,16 @@ object evaluator extends EvaluationRules {
       case fapp @ ast.FuncApp(funcName, eArgs) =>
         val func = s.program.findFunction(funcName)
         evals2(s, eArgs, Nil, _ => pve, v)((s1, tArgs, eArgsNew, v1) => {
+          val s1a = if (debugOn && s.recordIntermediateHeaps) v1.recordIntermediateHeap(s1, fapp) else s1
 //          bookkeeper.functionApplications += 1
           val joinFunctionArgs = tArgs //++ c2a.quantifiedVariables.filterNot(tArgs.contains)
-          val (debugHeapName, debugLabel) = v1.getDebugOldLabel(s1, fapp.pos)
+          val debugLabel = v1.getDebugOldLabel(s1a, fapp.pos)
 
           val funcAppNew = eArgsNew.map(args => ast.FuncApp(funcName, args)(fapp.pos, fapp.info, fapp.typ, fapp.errT))
-          val joinExp = Option.when(withExp)({
-            if (s1.isEvalInOld || func.pres.forall(_.isPure)) funcAppNew.get
+          val joinExp = Option.when(debugOn)({
+            if (s1a.isEvalInOld || func.pres.forall(_.isPure)) funcAppNew.get
             else ast.DebugLabelledOld(funcAppNew.get, debugLabel)(fapp.pos, fapp.info, fapp.errT)
           })
-
-          val s1a = if (Verifier.config.enableDebugging()) s1.copy(oldHeaps = s1.oldHeaps + (debugHeapName -> s1.h)) else s1
           /* TODO: Does it matter that the above filterNot does not filter out quantified
            *       variables that are not "raw" function arguments, but instead are used
            *       in an expression that is used as a function argument?
@@ -620,7 +619,7 @@ object evaluator extends EvaluationRules {
             val pvePre =
               ErrorWrapperWithExampleTransformer(PreconditionInAppFalse(fapp).withReasonNodeTransformed(reasonOffendingNode =>
                 reasonOffendingNode.replace(formalsToActuals)), exampleTrafo)
-            val argsPairs: Seq[(Term, Option[ast.Exp])] = if (withExp) tArgs.zip(eArgsNew.get.map(Some(_))) else tArgs.zip(Seq.fill(tArgs.size)(None))
+            val argsPairs: Seq[(Term, Option[ast.Exp])] = if (debugOn) tArgs.zip(eArgsNew.get.map(Some(_))) else tArgs.zip(Seq.fill(tArgs.size)(None))
             val s3 = s2.copy(g = Store(fargs.zip(argsPairs)),
                              recordVisited = true,
                              functionRecorder = s2.functionRecorder.changeDepthBy(+1),
@@ -653,7 +652,7 @@ object evaluator extends EvaluationRules {
             consumes(s3, pres, true, _ => pvePre, v2)((s4, snap, v3) => {
               val snap1 = snap.get.convert(sorts.Snap)
               val preFApp = App(functionSupporter.preconditionVersion(v3.symbolConverter.toFunction(func)), snap1 :: tArgs)
-              val preExp = Option.when(withExp)({
+              val preExp = Option.when(debugOn)({
                 DebugExp.createInstance(Some(s"precondition of ${func.name}(${eArgsNew.get.mkString(", ")}) holds"), None, None, InsertionOrderedSet.empty)
               })
               v3.decider.assume(preFApp, preExp)
@@ -677,7 +676,7 @@ object evaluator extends EvaluationRules {
                                smDomainNeeded = s2.smDomainNeeded,
                                moreJoins = s2.moreJoins,
                                assertReadAccessOnly = s2.assertReadAccessOnly)
-              val funcAppNewOld = Option.when(withExp)({
+              val funcAppNewOld = Option.when(debugOn)({
                 if (s5.isEvalInOld || pres.forall(_.isPure)) funcAppNew.get
                 else ast.DebugLabelledOld(funcAppNew.get, debugLabel)(fapp.pos, fapp.info, fapp.errT)
               })
@@ -698,15 +697,13 @@ object evaluator extends EvaluationRules {
           v.decider.startDebugSubExp()
           evals(s, eArgs, _ => pve, v)((s1, tArgs, eArgsNew, v1) =>
             eval(s1, ePerm.getOrElse(ast.FullPerm()()), pve, v1)((s2, tPerm, ePermNew, v2) => {
-              val (debugHeapName, debugLabel) = v1.getDebugOldLabel(s2, uf.pos)
-
+              val s2a = if (debugOn && s1.recordIntermediateHeaps) v2.recordIntermediateHeap(s2, uf) else s2
               val unfoldingNew = eArgsNew.map(args => uf.copy(acc = acc.copy(loc = pa.copy(args = args)(pa.pos, pa.info, pa.errT),
                 permExp = Some(ePermNew.get))(acc.pos, acc.info, acc.errT))(uf.pos, uf.info, uf.errT))
-              val joinExp = Option.when(withExp)({
+              val joinExp = Option.when(debugOn)({
                 if (s1.isEvalInOld) unfoldingNew.get
-                else ast.DebugLabelledOld(unfoldingNew.get, debugLabel)(uf.pos, uf.info, uf.errT)
+                else ast.DebugLabelledOld(unfoldingNew.get, v2.getDebugOldLabel(s2, uf.pos))(uf.pos, uf.info, uf.errT)
               })
-              val s2a = if (Verifier.config.enableDebugging()) s2.copy(oldHeaps = s2.oldHeaps + (debugHeapName -> s2.h)) else s2
               v2.decider.assert(IsPositive(tPerm)) { // TODO: Replace with permissionSupporter.assertNotNegative
                 case true =>
                   joiner.join[(Term, Option[ast.Exp]), (Term, Option[ast.Exp])](s2a, v2)((s3, v3, QB) => {
@@ -735,12 +732,12 @@ object evaluator extends EvaluationRules {
                          */
                       if (!Verifier.config.disableFunctionUnfoldTrigger()) {
                         val eArgsString = eArgsNew.mkString(", ")
-                        val debugExp = Option.when(withExp)(DebugExp.createInstance(s"PredicateTrigger(${predicate.name}($eArgsString))", isInternal_ = true))
+                        val debugExp = Option.when(debugOn)(DebugExp.createInstance(s"PredicateTrigger(${predicate.name}($eArgsString))", isInternal_ = true))
                         v4.decider.assume(App(s.predicateData(predicate.name).triggerFunction, snap.get.convert(terms.sorts.Snap) +: tArgs), debugExp)
                       }
                       val body = predicate.body.get /* Only non-abstract predicates can be unfolded */
                       val s7 = s6.scalePermissionFactor(tPerm, ePermNew)
-                      val argsPairs: List[(Term, Option[ast.Exp])] = if (withExp) tArgs zip eArgsNew.get.map(Some(_)) else tArgs zip Seq.fill(tArgs.size)(None)
+                      val argsPairs: List[(Term, Option[ast.Exp])] = if (debugOn) tArgs zip eArgsNew.get.map(Some(_)) else tArgs zip Seq.fill(tArgs.size)(None)
                       val insg = s7.g + Store(predicate.formalArgs map (_.localVar) zip argsPairs)
                       val s7a = s7.copy(g = insg).setConstrainable(s7.constrainableARPs, false)
 
@@ -755,7 +752,8 @@ object evaluator extends EvaluationRules {
                             constrainableARPs = s1.constrainableARPs)
                             .decCycleCounter(predicate)
                           val s10 = v5.stateConsolidator(s9).consolidateOptionally(s9, v5)
-                          eval(s10, eIn, pve, v5)((s9, t9, e9, v9) => QB(s9, (t9, e9), v9))
+                          val s11 = if (debugOn && s10.recordIntermediateHeaps) v5.recordIntermediateHeap(s10, uf) else s10
+                          eval(s11, eIn, pve, v5)((s9, t9, e9, v9) => QB(s9, (t9, e9), v9))
                         })
                       } else {
                         produce(s7a, toSf(snap.get), body, pve, v4)((s8, v5) => {
@@ -767,36 +765,39 @@ object evaluator extends EvaluationRules {
                                            constrainableARPs = s1.constrainableARPs)
                                      .decCycleCounter(predicate)
                           val s10 = v5.stateConsolidator(s9).consolidateOptionally(s9, v5)
-                          eval(s10, eIn, pve, v5)((s9, t9, e9, v9) => QB(s9, (t9, e9), v9))})
+                          val s11 = if (debugOn && s10.recordIntermediateHeaps) v5.recordIntermediateHeap(s10, uf) else s10
+                          eval(s11, eIn, pve, v5)((s9, t9, e9, v9) => QB(s9, (t9, e9), v9))})
                       }
                     })
-                  })(join(eIn.typ, "joined_unfolding", s2a.relevantQuantifiedVariables.map(_._1),
+                  })(join(eIn.typ, "joined_unfolding", s2.relevantQuantifiedVariables.map(_._1),
                     joinExp, v2))((s12, r12, v7)
                     => {
                     v7.decider.finishDebugSubExp(s"unfolded(${predicate.name})")
-                    Q(s12, r12._1, r12._2, v7)})
+                    Q(s12.copy(intermediateHeapCause = s.intermediateHeapCause), r12._1, r12._2, v7)})
                 case false =>
                   v2.decider.finishDebugSubExp(s"unfolded(${predicate.name})")
-                  createFailure(pve dueTo NonPositivePermission(ePerm.get), v2, s2a, IsPositive(tPerm), ePermNew.map(p => ast.PermGtCmp(p, ast.NoPerm()())(p.pos, p.info, p.errT)))}}))
+                  createFailure(pve dueTo NonPositivePermission(ePerm.get), v2, s2, IsPositive(tPerm), ePermNew.map(p => ast.PermGtCmp(p, ast.NoPerm()())(p.pos, p.info, p.errT)))}}))
         } else {
           val unknownValue = v.decider.appliedFresh("recunf", v.symbolConverter.toSort(eIn.typ), s.relevantQuantifiedVariables.map(_._1))
           val newFuncRec = s.functionRecorder.recordFreshSnapshot(unknownValue.applicable.asInstanceOf[Function])
-          Q(s.copy(functionRecorder = newFuncRec), unknownValue, Option.when(withExp)(ast.LocalVarWithVersion("unknownValue", eIn.typ)(eIn.pos, eIn.info, eIn.errT)), v)
+          Q(s.copy(functionRecorder = newFuncRec), unknownValue, Option.when(debugOn)(ast.LocalVarWithVersion("unknownValue", eIn.typ)(eIn.pos, eIn.info, eIn.errT)), v)
         }
 
       case apl@ast.Applying(wand, eIn) =>
-        val (debugHeapName, debugLabel) = v.getDebugOldLabel(s, apl.pos)
-        val joinExp = Option.when(withExp)({
+        val joinExp = Option.when(debugOn)({
           if (s.isEvalInOld) apl
-          else ast.DebugLabelledOld(apl, debugLabel)(apl.pos, apl.info, apl.errT)
+          else ast.DebugLabelledOld(apl, v.getDebugOldLabel(s, apl.pos))(apl.pos, apl.info, apl.errT)
         })
-        val sa = if (Verifier.config.enableDebugging()) s.copy(oldHeaps = s.oldHeaps + (debugHeapName -> s.h)) else s
-        joiner.join[(Term, Option[ast.Exp]), (Term, Option[ast.Exp])](sa, v)((s1, v1, QB) =>
+        val s0 = if (debugOn && s.recordIntermediateHeaps) v.recordIntermediateHeap(s, apl) else s
+        joiner.join[(Term, Option[ast.Exp]), (Term, Option[ast.Exp])](s0, v)((s1, v1, QB) =>
           magicWandSupporter.applyWand(s1, wand, pve, v1)((s2, v2) => {
-            eval(s2, eIn, pve, v2)((s3, t, eInNew, v3) => QB(s3, (t, eInNew), v3))
-        }))(join(eIn.typ, "joined_applying", s.relevantQuantifiedVariables.map(_._1),
-          joinExp, v))((s4, r4, v4)
-          => Q(s4, r4._1, r4._2, v4))
+            val s2a = if (debugOn) {
+              val (parentLabel, _, interPCS) = s2.intermediateHeapCause.get
+              v2.recordDebugHeap(s2, parentLabel, EvalExp(apl), interPCS)
+            } else s2
+            eval(s2a, eIn, pve, v2)((s3, t, eInNew, v3) => QB(s3, (t, eInNew), v3))
+          }))(join(eIn.typ, "joined_applying", s.relevantQuantifiedVariables.map(_._1), joinExp, v))((s4, r4, v4) =>
+            Q(s4.copy(intermediateHeapCause = s.intermediateHeapCause), r4._1, r4._2, v4))
 
       case ast.Asserting(eAss, eIn) =>
         consume(s, eAss, false, pve, v)((s2, _, v2) => {
@@ -822,22 +823,22 @@ object evaluator extends EvaluationRules {
                   case true =>
                     Q(s1, SeqAt(t0, t1), eNew, v1)
                   case false =>
-                    val assertExp2 = Option.when(withExp)(ast.LtCmp(e1, ast.SeqLength(e0)())(e1.pos, e1.info, e1.errT))
+                    val assertExp2 = Option.when(debugOn)(ast.LtCmp(e1, ast.SeqLength(e0)())(e1.pos, e1.info, e1.errT))
                     val failure = createFailure(pve dueTo SeqIndexExceedsLength(e0, e1), v1, s1, Less(t1, SeqLength(t0)), assertExp2)
                     if (s1.retryLevel == 0 && v1.reportFurtherErrors()) {
-                      val assertExp2 = Option.when(withExp)(ast.LeCmp(e1, ast.SeqLength(e0)())())
+                      val assertExp2 = Option.when(debugOn)(ast.LeCmp(e1, ast.SeqLength(e0)())())
                       val assertExp2New = esNew.map(es => ast.LeCmp(es(1), ast.SeqLength(es.head)())())
                       v1.decider.assume(Less(t1, SeqLength(t0)), assertExp2, assertExp2New)
                       failure combine Q(s1, SeqAt(t0, t1), eNew, v1)
                     } else failure}
               case false =>
-                val assertExp1 = Option.when(withExp)(ast.GeCmp(e1, ast.IntLit(0)())(e1.pos, e1.info, e1.errT))
-                val assertExp1New = Option.when(withExp)(ast.GeCmp(esNew.get(1), ast.IntLit(0)())(e1.pos, e1.info, e1.errT))
+                val assertExp1 = Option.when(debugOn)(ast.GeCmp(e1, ast.IntLit(0)())(e1.pos, e1.info, e1.errT))
+                val assertExp1New = Option.when(debugOn)(ast.GeCmp(esNew.get(1), ast.IntLit(0)())(e1.pos, e1.info, e1.errT))
                 val failure1 = createFailure(pve dueTo SeqIndexNegative(e0, e1), v1, s1, AtLeast(t1, IntLiteral(0)), assertExp1New)
                 if (s1.retryLevel == 0 && v1.reportFurtherErrors()) {
                   v1.decider.assume(AtLeast(t1, IntLiteral(0)), assertExp1, assertExp1New)
-                  val assertExp2 = Option.when(withExp)(ast.LtCmp(e1, ast.SeqLength(e0)())(e1.pos, e1.info, e1.errT))
-                  val assertExp2New = Option.when(withExp)(ast.LtCmp(esNew.get(1), ast.SeqLength(esNew.get(0))())(e1.pos, e1.info, e1.errT))
+                  val assertExp2 = Option.when(debugOn)(ast.LtCmp(e1, ast.SeqLength(e0)())(e1.pos, e1.info, e1.errT))
+                  val assertExp2New = Option.when(debugOn)(ast.LtCmp(esNew.get(1), ast.SeqLength(esNew.get(0))())(e1.pos, e1.info, e1.errT))
                   v1.decider.assert(Less(t1, SeqLength(t0))) {
                     case true =>
                       failure1 combine Q(s1, SeqAt(t0, t1), eNew, v1)
@@ -857,7 +858,7 @@ object evaluator extends EvaluationRules {
         Q(s1, t, e0New.map(e0p => ast.SeqTake(e0p, e1New.get)(e.pos, e.info, e.errT)), v1))
       case ast.SeqLength(e0) => eval(s, e0, pve, v)((s1, t0, e0New, v1) =>
         Q(s1, SeqLength(t0), e0New.map(e0p => ast.SeqLength(e0p)(e.pos, e.info, e.errT)), v1))
-      case ast.EmptySeq(typ) => Q(s, SeqNil(v.symbolConverter.toSort(typ)), Option.when(withExp)(e), v)
+      case ast.EmptySeq(typ) => Q(s, SeqNil(v.symbolConverter.toSort(typ)), Option.when(debugOn)(e), v)
       case ast.RangeSeq(e0, e1) => evalBinOp(s, e0, e1, SeqRanged, pve, v)((s1, t, e0New, e1New, v1) =>
         Q(s1, t, e0New.map(e0p => ast.RangeSeq(e0p, e1New.get)(e.pos, e.info, e.errT)), v1))
 
@@ -867,19 +868,19 @@ object evaluator extends EvaluationRules {
           if (s1.triggerExp) {
             Q(s1, SeqUpdate(t0, t1, t2), eNew, v1)
           } else {
-            val assertExp = Option.when(withExp)(ast.GeCmp(e1, ast.IntLit(0)())(e1.pos, e1.info, e1.errT))
-            val assertExpNew = Option.when(withExp)(ast.GeCmp(esNew.get(1), ast.IntLit(0)())(e1.pos, e1.info, e1.errT))
+            val assertExp = Option.when(debugOn)(ast.GeCmp(e1, ast.IntLit(0)())(e1.pos, e1.info, e1.errT))
+            val assertExpNew = Option.when(debugOn)(ast.GeCmp(esNew.get(1), ast.IntLit(0)())(e1.pos, e1.info, e1.errT))
             v1.decider.assert(AtLeast(t1, IntLiteral(0))) {
               case true =>
-                val assertExp2New = Option.when(withExp)(ast.LtCmp(esNew.get(1), ast.SeqLength(esNew.get(0))())(e1.pos, e1.info, e1.errT))
+                val assertExp2New = Option.when(debugOn)(ast.LtCmp(esNew.get(1), ast.SeqLength(esNew.get(0))())(e1.pos, e1.info, e1.errT))
                 v1.decider.assert(Less(t1, SeqLength(t0))) {
                   case true =>
                     Q(s1, SeqUpdate(t0, t1, t2), eNew, v1)
                   case false =>
                     val failure = createFailure(pve dueTo SeqIndexExceedsLength(e0, e1), v1, s1, Less(t1, SeqLength(t0)), assertExp2New)
                     if (s1.retryLevel == 0 && v1.reportFurtherErrors()) {
-                      val assertExp3 = Option.when(withExp)(ast.LeCmp(e1, ast.SeqLength(e0)())())
-                      val assertExp3New = Option.when(withExp)(ast.LeCmp(esNew.get(1), ast.SeqLength(esNew.get(0))())())
+                      val assertExp3 = Option.when(debugOn)(ast.LeCmp(e1, ast.SeqLength(e0)())())
+                      val assertExp3New = Option.when(debugOn)(ast.LeCmp(esNew.get(1), ast.SeqLength(esNew.get(0))())())
                       v1.decider.assume(Less(t1, SeqLength(t0)), assertExp3, assertExp3New)
                       failure combine Q(s1, SeqUpdate(t0, t1, t2), eNew, v1)}
                     else failure}
@@ -887,8 +888,8 @@ object evaluator extends EvaluationRules {
                 val failure1 = createFailure(pve dueTo SeqIndexNegative(e0, e1), v1, s1, AtLeast(t1, IntLiteral(0)), assertExpNew)
                 if (s1.retryLevel == 0 && v1.reportFurtherErrors()) {
                   v1.decider.assume(AtLeast(t1, IntLiteral(0)), assertExp, assertExpNew)
-                  val assertExp2 = Option.when(withExp)(ast.LtCmp(e1, ast.SeqLength(e0)())(e1.pos, e1.info, e1.errT))
-                  val assertExp2New = Option.when(withExp)(ast.LtCmp(esNew.get(1), ast.SeqLength(esNew.get(0))())(e1.pos, e1.info, e1.errT))
+                  val assertExp2 = Option.when(debugOn)(ast.LtCmp(e1, ast.SeqLength(e0)())(e1.pos, e1.info, e1.errT))
+                  val assertExp2New = Option.when(debugOn)(ast.LtCmp(esNew.get(1), ast.SeqLength(esNew.get(0))())(e1.pos, e1.info, e1.errT))
                   v1.decider.assert(Less(t1, SeqLength(t0))) {
                     case true =>
                       failure1 combine Q(s1, SeqUpdate(t0, t1, t2), eNew, v1)
@@ -905,7 +906,7 @@ object evaluator extends EvaluationRules {
           val tSeq =
             tEs.tail.foldLeft[SeqTerm](SeqSingleton(tEs.head))((tSeq, te) =>
               SeqAppend(tSeq, SeqSingleton(te)))
-          val debugExp = Option.when(withExp)({
+          val debugExp = Option.when(debugOn)({
             val expNew = ast.EqCmp(ast.SeqLength(ast.ExplicitSeq(esNew.get)())(), ast.IntLit(es.size)())(seq.pos, seq.info, seq.errT)
             val exp = ast.EqCmp(ast.SeqLength(seq)(), ast.IntLit(es.size)())(seq.pos, seq.info, seq.errT)
             DebugExp.createInstance(exp, expNew)
@@ -916,9 +917,9 @@ object evaluator extends EvaluationRules {
       /* Sets and multisets */
 
       case ast.EmptySet(typ) =>
-        Q(s, EmptySet(v.symbolConverter.toSort(typ)), Option.when(withExp)(e), v)
+        Q(s, EmptySet(v.symbolConverter.toSort(typ)), Option.when(debugOn)(e), v)
       case ast.EmptyMultiset(typ) =>
-        Q(s, EmptyMultiset(v.symbolConverter.toSort(typ)), Option.when(withExp)(e), v)
+        Q(s, EmptyMultiset(v.symbolConverter.toSort(typ)), Option.when(debugOn)(e), v)
 
       case ast.ExplicitSet(es) =>
         evals2(s, es, Nil, _ => pve, v)((s1, tEs, esNew, v1) => {
@@ -991,9 +992,9 @@ object evaluator extends EvaluationRules {
       /* Maps */
 
       case ast.EmptyMap(keyType, valueType) =>
-        Q(s, EmptyMap(v.symbolConverter.toSort(keyType), v.symbolConverter.toSort(valueType)), Option.when(withExp)(e), v)
+        Q(s, EmptyMap(v.symbolConverter.toSort(keyType), v.symbolConverter.toSort(valueType)), Option.when(debugOn)(e), v)
       case em: ast.ExplicitMap =>
-        eval(s, em.desugared, pve, v)((s1, t0, _, v1) => Q(s1, t0, Option.when(withExp)(em), v1))
+        eval(s, em.desugared, pve, v)((s1, t0, _, v1) => Q(s1, t0, Option.when(debugOn)(em), v1))
       case ast.MapCardinality(base) =>
         eval(s, base, pve, v)((s1, t0, baseNew, v1) => Q(s1, MapCardinality(t0), baseNew.map(ast.MapCardinality(_)(e.pos, e.info, e.errT)), v1))
       case ast.MapDomain(base) =>
@@ -1010,8 +1011,8 @@ object evaluator extends EvaluationRules {
             v1.decider.assert(SetIn(keyT, MapDomain(baseT))) {
               case true => Q(s1, MapLookup(baseT, keyT), eNew, v1)
               case false =>
-                val assertExp = Option.when(withExp)(ast.MapContains(key, base)(ml.pos, ml.info, ml.errT))
-                val assertExpNew = Option.when(withExp)(ast.MapContains(esNew.get(1), esNew.get(0))(ml.pos, ml.info, ml.errT))
+                val assertExp = Option.when(debugOn)(ast.MapContains(key, base)(ml.pos, ml.info, ml.errT))
+                val assertExpNew = Option.when(debugOn)(ast.MapContains(esNew.get(1), esNew.get(0))(ml.pos, ml.info, ml.errT))
                 val failure1 = createFailure(pve dueTo MapKeyNotContained(base, key), v1, s1, SetIn(keyT, MapDomain(baseT)), assertExpNew)
                 if (s1.retryLevel == 0 && v1.reportFurtherErrors()) {
                   v1.decider.assume(SetIn(keyT, MapDomain(baseT)), assertExp, assertExpNew)
@@ -1102,7 +1103,7 @@ object evaluator extends EvaluationRules {
             val (auxGlobals, auxNonGlobalQuants) =
               v3.decider.pcs.after(preMark).quantified(quant, tVars, tTriggers, s"$name-aux", isGlobal = false, bc)
             val auxExps =
-              Option.when(withExp)(v3.decider.pcs.after(preMark).quantifiedExp(quant, varPairs map (_._2.get), tVars, optTriggers.getOrElse(Nil), tTriggers, s"$name-aux", isGlobal = false, bc))
+              Option.when(debugOn)(v3.decider.pcs.after(preMark).quantifiedExp(quant, varPairs map (_._2.get), tVars, optTriggers.getOrElse(Nil), tTriggers, s"$name-aux", isGlobal = false, bc))
             val additionalPossibleTriggers: Map[ast.Exp, Term] =
               if (s.recordPossibleTriggers) s5.possibleTriggers else Map()
             es2AndTriggerTerms = Some((ts2, es2New, tTriggers, (auxGlobals, auxNonGlobalQuants), auxExps, additionalPossibleTriggers))
@@ -1115,10 +1116,10 @@ object evaluator extends EvaluationRules {
       case (s2, ts1, es1New1, Some((ts2, es2New1, tTriggers, (tAuxGlobal, tAux), eAuxExps, additionalPossibleTriggers))) =>
         val s3 = s.copy(possibleTriggers = s.possibleTriggers ++ additionalPossibleTriggers)
                 .preserveAfterLocalEvaluation(s2)
-        Q(s3, tVars, Option.when(withExp)(varPairs map (e => ast.LocalVarDecl(e._2.get.name, e._2.get.typ)(e._2.get.pos, e._2.get.info, e._2.get.errT))), ts1, es1New1, Some((ts2, es2New1, tTriggers, (tAuxGlobal, tAux), Option.when(withExp)((eAuxExps.get._1, eAuxExps.get._2)))), v)
+        Q(s3, tVars, Option.when(debugOn)(varPairs map (e => ast.LocalVarDecl(e._2.get.name, e._2.get.typ)(e._2.get.pos, e._2.get.info, e._2.get.errT))), ts1, es1New1, Some((ts2, es2New1, tTriggers, (tAuxGlobal, tAux), Option.when(debugOn)((eAuxExps.get._1, eAuxExps.get._2)))), v)
       case (s2, ts1, es1New1, None) =>
         val s3 = s.preserveAfterLocalEvaluation(s2)
-        Q(s3, tVars, Option.when(withExp)(varPairs map (e => ast.LocalVarDecl(e._2.get.name, e._2.get.typ)(e._2.get.pos, e._2.get.info, e._2.get.errT))), ts1, es1New1, None, v)
+        Q(s3, tVars, Option.when(debugOn)(varPairs map (e => ast.LocalVarDecl(e._2.get.name, e._2.get.typ)(e._2.get.pos, e._2.get.info, e._2.get.errT))), ts1, es1New1, None, v)
     }
   }
 
@@ -1135,7 +1136,7 @@ object evaluator extends EvaluationRules {
     joiner.join[(Term, Option[ast.Exp]), (Term, Option[ast.Exp])](s, v)((s1, v1, QB) =>
       brancher.branch(s1.copy(parallelizeBranches = false), tLhs, eLhs, v1, fromShortCircuitingAnd = fromShortCircuitingAnd)(
         (s2, v2) => eval(s2.copy(parallelizeBranches = s1.parallelizeBranches), eRhs, pve, v2)((s2, tRhs, eRhsNew, v2) => QB(s2, (tRhs, eRhsNew), v2)),
-        (s2, v2) => QB(s2.copy(parallelizeBranches = s1.parallelizeBranches), (True, Option.when(withExp)(ast.TrueLit()())), v2))
+        (s2, v2) => QB(s2.copy(parallelizeBranches = s1.parallelizeBranches), (True, Option.when(debugOn)(ast.TrueLit()())), v2))
     )(entries => {
       assert(entries.length <= 2)
       val s1 = entries.tail.foldLeft(entries.head.s)((sAcc, entry) => sAcc.merge(entry.s))
@@ -1184,7 +1185,6 @@ object evaluator extends EvaluationRules {
         s.possibleTriggers
       }
       val s4 = s3.copy(h = s.h,
-                       oldHeaps = s3.oldHeaps + (label -> s3.h),
                        partiallyConsumedHeap = s.partiallyConsumedHeap,
                        possibleTriggers = newPossibleTriggers,
                        isEvalInOld = s.isEvalInOld)
@@ -1239,7 +1239,7 @@ object evaluator extends EvaluationRules {
     v.decider.assert(tDivisor !== tZero){
       case true => Q(s, t, v)
       case false =>
-        val (notZeroExp, notZeroExpNew) = if (withExp) {
+        val (notZeroExp, notZeroExpNew) = if (debugOn) {
           (Some(ast.NeCmp(eDivisor, ast.IntLit(0)())(eDivisor.pos, eDivisor.info, eDivisor.errT)), Some(ast.NeCmp(eDivisorNew.get, ast.IntLit(0)())(eDivisor.pos, eDivisor.info, eDivisor.errT)))
         } else { (None, None) }
         val failure = createFailure(pve dueTo DivisionByZero(eDivisor), v, s, tDivisor !== tZero, notZeroExpNew)
@@ -1390,7 +1390,7 @@ object evaluator extends EvaluationRules {
 
     (r, optRemainingTriggerTerms) match {
       case (Success(), Some(remainingTriggerTerms)) =>
-        v.decider.assume(pcDelta, Option.when(withExp)(DebugExp.createInstance("pcDeltaExp", children = pcDeltaExp)), enforceAssumption = false)
+        v.decider.assume(pcDelta, Option.when(debugOn)(DebugExp.createInstance("pcDeltaExp", children = pcDeltaExp)), enforceAssumption = false)
         Q(s.copy(functionRecorder = functionRecorder), cachedTriggerTerms ++ remainingTriggerTerms, v)
       case _ =>
         for (e <- remainingTriggerExpressions)
@@ -1424,8 +1424,8 @@ object evaluator extends EvaluationRules {
 
         val joinDefEqs: Seq[(Term, Option[ast.Exp], Option[ast.Exp])] = entries map (entry =>
           (Implies(And(entry.pathConditions.branchConditions), BuiltinEquals(joinTerm, entry.data._1)),
-          Option.when(withExp)(ast.Implies(BigAnd(entry.pathConditions.branchConditionExps.map(bc => bc._1)), ast.EqCmp(joinedExp.get, entry.data._2.get)())()),
-          Option.when(withExp)(ast.Implies(BigAnd(entry.pathConditions.branchConditionExps.map(bc => bc._2.get)), ast.EqCmp(joinedExp.get, entry.data._2.get)())())))
+          Option.when(debugOn)(ast.Implies(BigAnd(entry.pathConditions.branchConditionExps.map(bc => bc._1)), ast.EqCmp(joinedExp.get, entry.data._2.get)())()),
+          Option.when(debugOn)(ast.Implies(BigAnd(entry.pathConditions.branchConditionExps.map(bc => bc._2.get)), ast.EqCmp(joinedExp.get, entry.data._2.get)())())))
 
 
         var sJoined = entries.tail.foldLeft(entries.head.s)((sAcc, entry) => sAcc.merge(entry.s))
@@ -1456,7 +1456,7 @@ object evaluator extends EvaluationRules {
     }
 
     val triggerString = exps.mkString(", ")
-    v.decider.assume(triggerAxioms, Option.when(withExp)(DebugExp.createInstance(s"Heap Triggers ($triggerString)")), enforceAssumption = false)
+    v.decider.assume(triggerAxioms, Option.when(debugOn)(DebugExp.createInstance(s"Heap Triggers ($triggerString)")), enforceAssumption = false)
     var fr = s.functionRecorder
     for (smDef <- smDefs){
       fr = fr.recordFvfAndDomain(smDef)
@@ -1530,7 +1530,7 @@ object evaluator extends EvaluationRules {
             ){case Seq(ent) =>
                 (ent.s, ent.data)
               case Seq(ent1, ent2) =>
-                val exp = Option.when(withExp)({
+                val exp = Option.when(debugOn)({
                   if (constructor == Or)
                     ast.Or(ent1.data._2.get, ent2.data._2.get)()
                   else
diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala
index 763ac1afa..7c80df619 100644
--- a/src/main/scala/rules/Executor.scala
+++ b/src/main/scala/rules/Executor.scala
@@ -92,7 +92,10 @@ object executor extends ExecutionRules {
         val (fr1, h1) = v.stateConsolidator(s).merge(s.functionRecorder, s, s.h, s.invariantContexts.head, v)
         val s1 = s.copy(functionRecorder = fr1, h = h1,
           invariantContexts = s.invariantContexts.tail)
-        s1
+        if (debugOn && s.recordIntermediateHeaps)
+          v.recordIntermediateHeap(s1).copy(intermediateHeapCause = None)
+        else
+          s1
       case _ =>
         /* No need to do anything special. See also the handling of loop heads in exec below. */
         s
@@ -244,7 +247,8 @@ object executor extends ExecutionRules {
             val gBody = Store(wvs.foldLeft(s.g.values)((map, x) => {
               val xNew = v.decider.fresh(x)
               map.updated(x, xNew)}))
-            val sBody = s.copy(g = gBody, h = v.heapSupporter.getEmptyHeap(s.program))
+            val sBody = s.copy(g = gBody, h = v.heapSupporter.getEmptyHeap(s.program),
+              intermediateHeapCause = if (debugOn) Some("nil", InhaleInv(), v.decider.pcs.duplicate()) else None)
 
             val edges = s.methodCfg.outEdges(block)
             val (outEdges, otherEdges) = edges partition(_.kind == cfg.Kind.Out)
@@ -267,7 +271,11 @@ object executor extends ExecutionRules {
                 })})
             combine executionFlowController.locally(s, v)((s0, v0) => {
                 v0.decider.prover.comment("Loop head block: Establish invariant")
-                consumes(s0, invs, false, LoopInvariantNotEstablished, v0)((sLeftover, _, v1) => {
+                val s0a = if (debugOn) {
+                  val currentLabel = v0.getDebugHeapLabel(s0).getOrElse("missingHeap")
+                  s0.copy(intermediateHeapCause = Some(currentLabel, ExhaleInv(), v.decider.pcs.duplicate()))
+                } else s0
+                consumes(s0a, invs, false, LoopInvariantNotEstablished, v0)((sLeftover, _, v1) => {
                   v1.decider.prover.comment("Loop head block: Execute statements of loop head block (in invariant state)")
                   phase1data.foldLeft(Success(): VerificationResult) {
                     case (result, _) if !result.continueVerification => result
@@ -276,12 +284,13 @@ object executor extends ExecutionRules {
                       intermediateResult combine executionFlowController.locally(s2, v1)((s3, v2) => {
                         v2.decider.declareAndRecordAsFreshFunctions(ff1 -- v2.decider.freshFunctions) /* [BRANCH-PARALLELISATION] */
                         v2.decider.declareAndRecordAsFreshMacros(fm1.filter(!v2.decider.freshMacros.contains(_)))  /* [BRANCH-PARALLELISATION] */
-                        v2.decider.assume(pcs.assumptions, Option.when(withExp)(DebugExp.createInstance("Loop invariant", pcs.assumptionExps)), false)
+                        v2.decider.assume(pcs.assumptions, Option.when(debugOn)(DebugExp.createInstance("Loop invariant", pcs.assumptionExps)), false)
                         v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract)
                         if (v2.decider.checkSmoke())
                           Success()
                         else {
-                          execs(s3, stmts, v2)((s4, v3) => {
+                          val s3a = if (debugOn) v2.recordDebugHeap(s3, "nil", InhaleInv()) else s3
+                          execs(s3a, stmts, v2)((s4, v3) => {
                             val edgeCondWelldefinedness = {
                               v1.decider.prover.comment("Loop head block: Check well-definedness of edge conditions")
                               edgeConditions.foldLeft(Success(): VerificationResult) {
@@ -294,7 +303,11 @@ object executor extends ExecutionRules {
                               }
                             }
                             v3.decider.prover.comment("Loop head block: Follow loop-internal edges")
-                            edgeCondWelldefinedness combine follows(s4, sortedEdges, WhileFailed, v3, joinPoint)(Q)})}})}})}))
+                            val s4a = if (debugOn) {
+                              val currentLabel = v3.getDebugHeapLabel(s4).getOrElse("nil")
+                              s4.copy(intermediateHeapCause = Some(currentLabel, MergeContext(), v3.decider.pcs.duplicate()))
+                            } else s4
+                            edgeCondWelldefinedness combine follows(s4a, sortedEdges, WhileFailed, v3, joinPoint)(Q)})}})}})}))
 
           case _ =>
             /* We've reached a loop head block via an edge other than an in-edge: a normal edge or
@@ -334,6 +347,8 @@ object executor extends ExecutionRules {
     val s = state.copy(h = magicWandSupporter.getExecutionHeap(state))
     val Q: (State, Verifier) => VerificationResult = (s, v) => {
       continuation(magicWandSupporter.moveToReserveHeap(s, v), v)}
+    val oldLabel = v.getDebugHeapLabel(s).getOrElse("missingHeap")
+    val oldPCS = v.decider.pcs.duplicate()
 
     /* For debugging-purposes only */
     stmt match {
@@ -353,7 +368,8 @@ object executor extends ExecutionRules {
 
       case ast.Label(name, _) =>
         val s1 = s.copy(oldHeaps = s.oldHeaps + (name -> magicWandSupporter.getEvalHeap(s)))
-        Q(s1, v)
+        val s2 = if (debugOn) v.recordDebugHeap(s, oldLabel, CreateLabel()) else s1
+        Q(s2, v)
 
       case ast.LocalVarDeclStmt(decl) =>
         val x = decl.localVar
@@ -375,22 +391,25 @@ object executor extends ExecutionRules {
         assert(!s.exhaleExt)
         val pve = AssignmentFailed(ass)
         eval(s, eRcvr, pve, v)((s1, tRcvr, eRcvrNew, v1) => {
-          eval(s1, rhs, pve, v1)((s2, tRhs, eRhsNew, v2) => {
+          val s1a = if (debugOn) s1.copy(intermediateHeapCause = Some(oldLabel, ExecStmt(ass), oldPCS)) else s1
+          eval(s1a, rhs, pve, v1)((s2, tRhs, eRhsNew, v2) => {
             val (tSnap, _) = ssaifyRhs(tRhs, rhs, eRhsNew, field.name, field.typ, v2, s2)
-            v2.heapSupporter.execFieldAssign(s2, ass, tRcvr, eRcvrNew, tSnap, eRhsNew, pve, v2)(Q)
+            v2.heapSupporter.execFieldAssign(s2, ass, tRcvr, eRcvrNew, tSnap, eRhsNew, pve, v2)((s1, v1) => {
+              val s2 = if (debugOn) v1.recordDebugHeap(s1, oldLabel, ExecStmt(ass)).copy(intermediateHeapCause = None) else s1
+              Q(s2, v1)})
           })
         })
 
       case stmt@ast.NewStmt(x, fields) =>
         val (tRcvr, eRcvrNew) = v.decider.fresh(x)
-        val debugExp = Option.when(withExp)(ast.NeCmp(x, ast.NullLit()())())
-        val debugExpSubst = Option.when(withExp)(ast.NeCmp(eRcvrNew.get, ast.NullLit()())())
+        val debugExp = Option.when(debugOn)(ast.NeCmp(x, ast.NullLit()())())
+        val debugExpSubst = Option.when(debugOn)(ast.NeCmp(eRcvrNew.get, ast.NullLit()())())
 
         v.decider.assume(tRcvr !== Null, debugExp, debugExpSubst)
 
-        val eRcvr = Option.when(withExp)(Seq(x))
+        val eRcvr = Option.when(debugOn)(Seq(x))
         val p = FullPerm
-        val pExp = Option.when(withExp)(ast.FullPerm()(stmt.pos, stmt.info, stmt.errT))
+        val pExp = Option.when(debugOn)(ast.FullPerm()(stmt.pos, stmt.info, stmt.errT))
 
         def addFieldPerms(s: State, flds: Seq[ast.Field], v: Verifier)
                          (QB: (State, Verifier) => VerificationResult): VerificationResult = {
@@ -398,7 +417,7 @@ object executor extends ExecutionRules {
             QB(s, v)
           } else {
             val fld = flds.head
-            val snap = v.decider.fresh(fld.name, v.symbolConverter.toSort(fld.typ), Option.when(withExp)(extractPTypeFromExp(x)))
+            val snap = v.decider.fresh(fld.name, v.symbolConverter.toSort(fld.typ), Option.when(debugOn)(extractPTypeFromExp(x)))
             v.heapSupporter.produceSingle(s, fld, Seq(tRcvr), eRcvr, snap, None, p, pExp, NullPartialVerificationError, false, v)((s1, v1) => {
               addFieldPerms(s1, flds.tail, v1)(QB)
             })
@@ -408,9 +427,8 @@ object executor extends ExecutionRules {
         val esNew = eRcvrNew.map(rcvr => BigAnd(viper.silicon.state.utils.computeReferenceDisjointnessesExp(s, rcvr)))
         addFieldPerms(s, fields, v)((s0, v0) => {
           val s1 = s0.copy(g = s0.g + (x, (tRcvr, eRcvrNew)))
-          val (debugHeapName, _) = v.getDebugOldLabel(s1, stmt.pos, Some(magicWandSupporter.getEvalHeap(s1)))
-          val s2 = if (withExp) s1.copy(oldHeaps = s1.oldHeaps + (debugHeapName -> magicWandSupporter.getEvalHeap(s1))) else s1
-          v0.decider.assume(ts, Option.when(withExp)(DebugExp.createInstance(Some("Reference Disjointness"), esNew, esNew, InsertionOrderedSet.empty)), enforceAssumption = false)
+          val s2 = if (debugOn) v0.recordDebugHeap(s1, oldLabel, ExecStmt(stmt)) else s1
+          v0.decider.assume(ts, Option.when(debugOn)(DebugExp.createInstance(Some("Reference Disjointness"), esNew, esNew, InsertionOrderedSet.empty)), enforceAssumption = false)
           Q(s2, v0)
         })
 
@@ -419,15 +437,21 @@ object executor extends ExecutionRules {
           /* We're done */
           Success()
         case _ =>
-          produce(s, freshSnap, a, InhaleFailed(inhale), v)((s1, v1) => {
+          val s0 = if (debugOn) s.copy(intermediateHeapCause = Some(oldLabel, ExecStmt(inhale), oldPCS)) else s
+          produce(s0, freshSnap, a, InhaleFailed(inhale), v)((s1, v1) => {
             v1.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterInhale)
-            Q(s1, v1)})
+            val s1a = if (debugOn) v1.recordDebugHeap(s1, oldLabel, ExecStmt(inhale), oldPCS).copy(intermediateHeapCause = None)
+            else s1
+            Q(s1a, v1)})
       }
 
       case exhale @ ast.Exhale(a) =>
         val pve = ExhaleFailed(exhale)
-        consume(s, a, false, pve, v)((s1, _, v1) =>
-          Q(s1, v1))
+        val s0 = if (debugOn) s.copy(intermediateHeapCause = Some(oldLabel, ExecStmt(exhale), oldPCS)) else s
+        consume(s0, a, false, pve, v)((s1, _, v1) => {
+          val s1a = if (debugOn) v1.recordDebugHeap(s1, oldLabel, ExecStmt(exhale), oldPCS).copy(intermediateHeapCause = None)
+          else s1
+          Q(s1a, v1)})
 
       case assert @ ast.Assert(a: ast.FalseLit) if !s.isInPackage =>
         /* "assert false" triggers a smoke check. If successful, we backtrack. */
@@ -435,7 +459,7 @@ object executor extends ExecutionRules {
           if (v1.decider.checkSmoke(true))
             QS(s1.copy(h = s.h), v1)
           else
-            createFailure(AssertFailed(assert) dueTo AssertionFalse(a), v1, s1, False, true, Option.when(withExp)(a))
+            createFailure(AssertFailed(assert) dueTo AssertionFalse(a), v1, s1, False, true, Option.when(debugOn)(a))
         })((_, _) => Success())
 
       case assert @ ast.Assert(a) if Verifier.config.disableSubsumption() =>
@@ -503,7 +527,11 @@ object executor extends ExecutionRules {
         val sepIdentifier = v.symbExLog.openScope(mcLog)
         val paramLog = new CommentRecord("Parameters", s, v.decider.pcs)
         val paramId = v.symbExLog.openScope(paramLog)
-        evals(s, eArgs, _ => pveCall, v)((s1, tArgs, eArgsNew, v1) => {
+        val s0 = if (debugOn)
+          s.copy(intermediateHeapCause = Some(oldLabel, ExecStmt(call), oldPCS))
+        else s
+
+        evals(s0, eArgs, _ => pveCall, v)((s1, tArgs, eArgsNew, v1) => {
           v1.symbExLog.closeScope(paramId)
           val exampleTrafo = CounterexampleTransformer({
             case ce: SiliconCounterexample => ce.withStore(s1.g)
@@ -512,44 +540,51 @@ object executor extends ExecutionRules {
           val pvePre = ErrorWrapperWithExampleTransformer(PreconditionInCallFalse(call).withReasonNodeTransformed(reasonTransformer), exampleTrafo)
           val preCondLog = new CommentRecord("Precondition", s1, v1.decider.pcs)
           val preCondId = v1.symbExLog.openScope(preCondLog)
-          val argsWithExp = if (withExp)
+          val argsWithExp = if (debugOn)
             tArgs zip (eArgsNew.get.map(Some(_)))
           else
             tArgs zip Seq.fill(tArgs.size)(None)
-          val s2 = s1.copy(g = Store(fargs.zip(argsWithExp)),
+          val s1a = s1.copy(g = Store(fargs.zip(argsWithExp)),
                            recordVisited = true)
-          consumes(s2, meth.pres, false, _ => pvePre, v1)((s3, _, v2) => {
+          consumes(s1a, meth.pres, false, _ => pvePre, v1)((s2, _, v2) => {
             v2.symbExLog.closeScope(preCondId)
-            val postCondLog = new CommentRecord("Postcondition", s3, v2.decider.pcs)
+            val postCondLog = new CommentRecord("Postcondition", s2, v2.decider.pcs)
             val postCondId = v2.symbExLog.openScope(postCondLog)
             val outs = meth.formalReturns.map(_.localVar)
             val gOuts = Store(outs.map(x => (x, v2.decider.fresh(x))).toMap)
-            val s4 = s3.copy(g = s3.g + gOuts, oldHeaps = s3.oldHeaps + (Verifier.PRE_STATE_LABEL -> magicWandSupporter.getEvalHeap(s1)))
-            produces(s4, freshSnap, meth.posts, _ => pveCallTransformed, v2)((s5, v3) => {
+            val s2a = s2.copy(g = s2.g + gOuts,
+                             oldHeaps = s2.oldHeaps + (Verifier.PRE_STATE_LABEL -> magicWandSupporter.getEvalHeap(s1)))
+            produces(s2a, freshSnap, meth.posts, _ => pveCallTransformed, v2)((s3, v3) => {
               v3.symbExLog.closeScope(postCondId)
               v3.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract)
               val gLhs = Store(lhs.zip(outs)
-                              .map(p => (p._1, s5.g.values(p._2))).toMap)
-              val s6 = s5.copy(g = s1.g + gLhs,
+                              .map(p => (p._1, s3.g.values(p._2))).toMap)
+              val s3a = s3.copy(g = s1.g + gLhs,
                                oldHeaps = s1.oldHeaps,
                                recordVisited = s1.recordVisited)
               v3.symbExLog.closeScope(sepIdentifier)
-              Q(s6, v3)})})})
+              val s3b = if (debugOn)
+                v3.recordDebugHeap(s3a, s3a.intermediateHeapCause.get._1, ExecStmt(call), s3a.intermediateHeapCause.get._3).copy(intermediateHeapCause = None)
+              else s3a
+              Q(s3b, v3)})})})
 
       case fold @ ast.Fold(pap @ ast.PredicateAccessPredicate(predAcc @ ast.PredicateAccess(eArgs, predicateName), _)) =>
         assert(s.constrainableARPs.isEmpty)
         v.decider.startDebugSubExp()
         val ePerm = pap.perm
         val pve = FoldFailed(fold)
-        evals(s, eArgs, _ => pve, v)((s1, tArgs, eArgsNew, v1) =>
+        val s0 = if (debugOn) s.copy(intermediateHeapCause = Some(oldLabel, ExecStmt(fold), oldPCS)) else s
+        evals(s0, eArgs, _ => pve, v)((s1, tArgs, eArgsNew, v1) =>
           eval(s1, ePerm, pve, v1)((s2, tPerm, ePermNew, v2) =>
-            permissionSupporter.assertPositive(s2, tPerm, if (withExp) ePermNew.get else ePerm, pve, v2)((s3, v3) => {
+            permissionSupporter.assertPositive(s2, tPerm, if (debugOn) ePermNew.get else ePerm, pve, v2)((s3, v3) => {
               val wildcards = s3.constrainableARPs -- s1.constrainableARPs
               predicateSupporter.fold(s3, predAcc, tArgs, eArgsNew, tPerm, ePermNew, wildcards, pve, v3)((s4, v4) => {
-                  v3.decider.finishDebugSubExp(s"folded ${predAcc.toString}")
-                  Q(s4, v4)
-                }
-              )})))
+                v3.decider.finishDebugSubExp(s"folded ${predAcc.toString}")
+                val s4a = if (debugOn) v4.recordDebugHeap(s4, oldLabel, ExecStmt(fold), oldPCS).copy(intermediateHeapCause = None)
+                else s4
+                Q(s4a, v4)
+              })
+            })))
 
       case unfold @ ast.Unfold(pap @ ast.PredicateAccessPredicate(pa @ ast.PredicateAccess(eArgs, predicateName), _)) =>
         assert(s.constrainableARPs.isEmpty)
@@ -557,30 +592,37 @@ object executor extends ExecutionRules {
         val ePerm = pap.perm
         val predicate = s.program.findPredicate(predicateName)
         val pve = UnfoldFailed(unfold)
-        evals(s, eArgs, _ => pve, v)((s1, tArgs, eArgsNew, v1) =>
+        val s0 = if (debugOn) s.copy(intermediateHeapCause = Some(oldLabel, ExecStmt(unfold), oldPCS)) else s
+        evals(s0, eArgs, _ => pve, v)((s1, tArgs, eArgsNew, v1) =>
           eval(s1, ePerm, pve, v1)((s2, tPerm, ePermNew, v2) => {
             val s2a = v2.heapSupporter.triggerResourceIfNeeded(s2, pa, tArgs, eArgsNew, v2)
 
-            permissionSupporter.assertPositive(s2a, tPerm, if (withExp) ePermNew.get else ePerm, pve, v2)((s3, v3) => {
+            permissionSupporter.assertPositive(s2a, tPerm, if (debugOn) ePermNew.get else ePerm, pve, v2)((s3, v3) => {
               val wildcards = s3.constrainableARPs -- s1.constrainableARPs
               predicateSupporter.unfold(s3, predicate, tArgs, eArgsNew, tPerm, ePermNew, wildcards, pve, v3, pa)(
                 (s4, v4) => {
                   v2.decider.finishDebugSubExp(s"unfolded ${pa.toString}")
-                  Q(s4, v4)
+                  val s4a = if (debugOn)
+                    v2.recordDebugHeap(s4, oldLabel, ExecStmt(unfold), oldPCS).copy(intermediateHeapCause = None)
+                  else s4
+                  Q(s4a, v4)
                 })
             })
           }))
 
       case pckg @ ast.Package(wand, proofScript) =>
         val pve = PackageFailed(pckg)
-          magicWandSupporter.packageWand(s.copy(isInPackage = true), wand, proofScript, pve, v)((s1, chWand, v1) => {
-
-            val hOps = s1.reserveHeaps.head + chWand
-            assert(s.exhaleExt || s1.reserveHeaps.length == 1)
-            val s2 =
-              if (s.exhaleExt) {
-                s1.copy(h = v1.heapSupporter.getEmptyHeap(s1.program),
-                        exhaleExt = true,
+        val s0 = if (debugOn)
+          s.copy(isInPackage = true, intermediateHeapCause = Some(oldLabel, ExecStmt(pckg), oldPCS))
+        else s.copy(isInPackage = true)
+
+        magicWandSupporter.packageWand(s0, wand, proofScript, pve, v)((s1, chWand, v1) => {
+          val hOps = s1.reserveHeaps.head + chWand
+          assert(s.exhaleExt || s1.reserveHeaps.length == 1)
+          val s2 =
+            if (s.exhaleExt) {
+              s1.copy(h = v1.heapSupporter.getEmptyHeap(s1.program),
+                      exhaleExt = true,
                         /* It is assumed, that s.reserveHeaps.head (hUsed) is not used or changed
                          * by the packageWand method. hUsed is normally used during transferring
                          * consume to store permissions that have already been consumed. The
@@ -588,27 +630,32 @@ object executor extends ExecutionRules {
                          * execution. hUsed should therefore be empty unless the package statement
                          * was triggered by heuristics during a consume operation.
                          */
-                        reserveHeaps = s.reserveHeaps.head +: hOps +: s1.reserveHeaps.tail)
-              } else {
-                /* c1.reserveHeap is expected to be [σ.h'], i.e. the remainder of σ.h */
-                s1.copy(h = hOps,
-                        exhaleExt = false,
-                        reserveHeaps = Nil)
-              }
-            assert(s2.reserveHeaps.length == s.reserveHeaps.length)
-
-            val s3 = chWand match {
-              case ch: QuantifiedMagicWandChunk =>
-                v1.heapSupporter.triggerResourceIfNeeded(s2, wand, ch.singletonArgs.get, ch.singletonArgExps, v1)
-              case _ => s2
+                      reserveHeaps = s.reserveHeaps.head +: hOps +: s1.reserveHeaps.tail)
+            } else {
+              /* c1.reserveHeap is expected to be [σ.h'], i.e. the remainder of σ.h */
+              s1.copy(h = hOps,
+                      exhaleExt = false,
+                      reserveHeaps = Nil)
             }
+          assert(s2.reserveHeaps.length == s.reserveHeaps.length)
+          val s3 = chWand match {
+            case ch: QuantifiedMagicWandChunk =>
+              v1.heapSupporter.triggerResourceIfNeeded(s2, wand, ch.singletonArgs.get, ch.singletonArgExps, v1)
+            case _ => s2
+          }
 
-            continuation(s3.copy(isInPackage = s.isInPackage), v1)
-          })
+          val s4 = if (debugOn) v1.recordDebugHeap(s3, oldLabel, ExecStmt(pckg), oldPCS).copy(intermediateHeapCause = None)
+          else s3
+          continuation(s4.copy(isInPackage = s.isInPackage), v1)
+        })
 
       case apply @ ast.Apply(e) =>
         val pve = ApplyFailed(apply)
-        magicWandSupporter.applyWand(s, e, pve, v)(Q)
+        val s0 = if (debugOn) s.copy(intermediateHeapCause = Some(oldLabel, ExecStmt(apply), oldPCS)) else s
+        magicWandSupporter.applyWand(s0, e, pve, v)((s1, v1) => {
+          val s1a = if (debugOn) v1.recordDebugHeap(s1, oldLabel, ExecStmt(apply), oldPCS).copy(intermediateHeapCause = None)
+          else s1
+          Q(s1a, v1)})
 
       case havoc: ast.Quasihavoc =>
         havocSupporter.execHavoc(havoc, v, s)(Q)
@@ -654,8 +701,8 @@ object executor extends ExecutionRules {
           *   performance; instead, it can cause an exponential blow-up in term size, as
           *   reported by Silicon issue #328.
           */
-         val t = v.decider.fresh(name, v.symbolConverter.toSort(typ), Option.when(withExp)(extractPTypeFromExp(rhsExp)))
-         val (eNew, debugExp) = if (withExp) {
+         val t = v.decider.fresh(name, v.symbolConverter.toSort(typ), Option.when(debugOn)(extractPTypeFromExp(rhsExp)))
+         val (eNew, debugExp) = if (debugOn) {
            val eRhs = rhsExp
            val eNew = ast.LocalVarWithVersion(simplifyVariableName(t.id.name), typ)(eRhs.pos, eRhs.info, eRhs.errT)
            val exp = ast.EqCmp(ast.LocalVar(name, typ)(), eRhs)(eRhs.pos, eRhs.info, eRhs.errT)
diff --git a/src/main/scala/rules/HavocSupporter.scala b/src/main/scala/rules/HavocSupporter.scala
index 8b3a1cc88..359e2c46b 100644
--- a/src/main/scala/rules/HavocSupporter.scala
+++ b/src/main/scala/rules/HavocSupporter.scala
@@ -118,7 +118,7 @@ object havocSupporter extends SymbolicExecutionRules {
         v.decider.prover.comment("Check havocall receiver injectivity")
         val notInjectiveReason = QuasihavocallNotInjective(havocall)
 
-        val injectivityDebugExp = Option.when(withExp)(DebugExp.createInstance("QP receiver injectivity check is well-defined", true))
+        val injectivityDebugExp = Option.when(debugOn)(DebugExp.createInstance("QP receiver injectivity check is well-defined", true))
         v.decider.assume(FunctionPreconditionTransformer.transform(receiverInjectivityCheck, s.program), injectivityDebugExp)
         v.decider.assert(receiverInjectivityCheck) {
           case false => createFailure(pve dueTo notInjectiveReason, v, s1, receiverInjectivityCheck, "QP receiver injective")
@@ -133,7 +133,7 @@ object havocSupporter extends SymbolicExecutionRules {
               codomainQVars = codomainQVars,
               codomainQVarExps = codomainQVarsExp,
               additionalInvArgs = Seq(), // There are no additional quantified vars
-              additionalInvArgExps = Option.when(withExp)(Seq()),
+              additionalInvArgExps = Option.when(debugOn)(Seq()),
               stateQVars = Seq(),
               userProvidedTriggers = None,
               qidPrefix = qid,
@@ -141,7 +141,7 @@ object havocSupporter extends SymbolicExecutionRules {
             )
             val comment = "Definitional axioms for havocall inverse functions"
             v.decider.prover.comment(comment)
-            v.decider.assume(inverseFunctions.definitionalAxioms, Option.when(withExp)(DebugExp.createInstance(comment, isInternal_ = true)), enforceAssumption = false)
+            v.decider.assume(inverseFunctions.definitionalAxioms, Option.when(debugOn)(DebugExp.createInstance(comment, isInternal_ = true)), enforceAssumption = false)
 
             // Call the havoc helper function, which returns a new heap, which is
             // partially havocked. Since we are executing a Havocall statement, we wrap
@@ -165,6 +165,6 @@ object havocSupporter extends SymbolicExecutionRules {
 
   // Get the variables that we must quantify over for each resource type
   private def getCodomainQVars(s: State, eRsc: ast.Resource, v: Verifier): (Seq[Var], Option[Seq[ast.LocalVarDecl]]) = {
-    (s.getFormalArgVars(eRsc, v), Option.when(withExp)(s.getFormalArgDecls(eRsc)))
+    (s.getFormalArgVars(eRsc, v), Option.when(debugOn)(s.getFormalArgDecls(eRsc)))
   }
 }
diff --git a/src/main/scala/rules/HeapSupporter.scala b/src/main/scala/rules/HeapSupporter.scala
index 649c1c629..131386525 100644
--- a/src/main/scala/rules/HeapSupporter.scala
+++ b/src/main/scala/rules/HeapSupporter.scala
@@ -191,13 +191,13 @@ class DefaultHeapSupportRules extends HeapSupportRules {
         s2,
         relevantChunks,
         Seq(`?r`),
-        Option.when(withExp)(Seq(ast.LocalVarDecl(`?r`.id.name, ast.Ref)())),
+        Option.when(debugOn)(Seq(ast.LocalVarDecl(`?r`.id.name, ast.Ref)())),
         `?r` === tRcvr,
         eRcvrNew.map(r => ast.EqCmp(ast.LocalVar(`?r`.id.name, ast.Ref)(), r)()),
         Some(Seq(tRcvr)),
         field,
         FullPerm,
-        Option.when(withExp)(ast.FullPerm()()),
+        Option.when(debugOn)(ast.FullPerm()()),
         chunkOrderHeuristics,
         v
       )
@@ -206,30 +206,28 @@ class DefaultHeapSupportRules extends HeapSupportRules {
           val h3 = Heap(remainingChunks ++ otherChunks)
           val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s3, field, Seq(tRcvr), tRhs, v)
           v.decider.prover.comment("Definitional axioms for singleton-FVF's value")
-          val debugExp = Option.when(withExp)(DebugExp.createInstance("Definitional axioms for singleton-FVF's value", isInternal_ = true))
+          val debugExp = Option.when(debugOn)(DebugExp.createInstance("Definitional axioms for singleton-FVF's value", isInternal_ = true))
           v.decider.assumeDefinition(smValueDef, debugExp)
-          val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(Seq(`?r`), Option.when(withExp)(Seq(ast.LocalVarDecl("r", ast.Ref)(ass.pos, ass.info, ass.errT))),
-            field, Seq(tRcvr), Option.when(withExp)(Seq(eRcvrNew.get)), FullPerm, Option.when(withExp)(ast.FullPerm()(ass.pos, ass.info, ass.errT)), sm, s.program)
+          val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(Seq(`?r`), Option.when(debugOn)(Seq(ast.LocalVarDecl("r", ast.Ref)(ass.pos, ass.info, ass.errT))),
+            field, Seq(tRcvr), Option.when(debugOn)(Seq(eRcvrNew.get)), FullPerm, Option.when(debugOn)(ast.FullPerm()(ass.pos, ass.info, ass.errT)), sm, s.program)
           if (s3.heapDependentTriggers.contains(field)) {
-            val debugExp2 = Option.when(withExp)(DebugExp.createInstance(s"FieldTrigger(${eRcvrNew.toString()}.${field.name})"))
+            val debugExp2 = Option.when(debugOn)(DebugExp.createInstance(s"FieldTrigger(${eRcvrNew.toString()}.${field.name})"))
             v.decider.assume(FieldTrigger(field.name, sm, tRcvr), debugExp2)
           }
           val s4 = s3.copy(h = h3 + ch)
-          val (debugHeapName, _) = v.getDebugOldLabel(s4, ass.lhs.pos, Some(magicWandSupporter.getEvalHeap(s4)))
-          val s5 = if (withExp) s4.copy(oldHeaps = s4.oldHeaps + (debugHeapName -> magicWandSupporter.getEvalHeap(s4))) else s4
+          val s5 = if (debugOn && s4.recordIntermediateHeaps) v.recordIntermediateHeap(s4) else s4
           Q(s5, v)
         case (Incomplete(_, _), s3, _) =>
           createFailure(ve, v, s3, "sufficient permission")
       }
     } else {
       val description = s"consume ${ass.pos}: $ass"
-      chunkSupporter.consume(s, s.h, field, Seq(tRcvr), eRcvrNew.map(Seq(_)), FullPerm, Option.when(withExp)(ast.FullPerm()(ass.pos, ass.info, ass.errT)), false, ve, v, description)((s3, h3, _, v3) => {
+      chunkSupporter.consume(s, s.h, field, Seq(tRcvr), eRcvrNew.map(Seq(_)), FullPerm, Option.when(debugOn)(ast.FullPerm()(ass.pos, ass.info, ass.errT)), false, ve, v, description)((s3, h3, _, v3) => {
         val id = BasicChunkIdentifier(field.name)
-        val newChunk = BasicChunk(FieldID, id, Seq(tRcvr), eRcvrNew.map(Seq(_)), tRhs, eRhsNew, FullPerm, Option.when(withExp)(ast.FullPerm()(ass.pos, ass.info, ass.errT)))
+        val newChunk = BasicChunk(FieldID, id, Seq(tRcvr), eRcvrNew.map(Seq(_)), tRhs, eRhsNew, FullPerm, Option.when(debugOn)(ast.FullPerm()(ass.pos, ass.info, ass.errT)))
         chunkSupporter.produce(s3, h3, newChunk, v3)((s4, h4, v4) => {
           val s5 = s4.copy(h = h4)
-          val (debugHeapName, _) = v4.getDebugOldLabel(s5, ass.lhs.pos, Some(magicWandSupporter.getEvalHeap(s5)))
-          val s6 = if (withExp) s5.copy(oldHeaps = s5.oldHeaps + (debugHeapName -> magicWandSupporter.getEvalHeap(s5))) else s5
+          val s6 = if (debugOn && s5.recordIntermediateHeaps) v.recordIntermediateHeap(s5) else s5
           Q(s6, v4)
         })
       })
@@ -263,7 +261,7 @@ class DefaultHeapSupportRules extends HeapSupportRules {
           if (s2.isUsedAsTrigger(res)) {
             val trigger = ResourceTriggerFunction(res, smDef.sm, tArgs, s.program)
             val argsString = eArgs.mkString(", ")
-            v.decider.assume(trigger, Option.when(withExp)({
+            v.decider.assume(trigger, Option.when(debugOn)({
               val name = res match {
                 case f: ast.Field => f.name
                 case p: ast.Predicate => p.name
@@ -275,18 +273,16 @@ class DefaultHeapSupportRules extends HeapSupportRules {
 
           val currentPermAmount = ResourcePermissionLookup(res, pmDef.pm, tArgs, s2.program)
 
-          val s3 = res match {
+          res match {
             case _: ast.Field =>
               v.decider.prover.comment(s"perm($resAcc)  ~~>  assume upper permission bound")
-              val (debugHeapName, debugLabel) = v.getDebugOldLabel(s2, resAcc.pos, Some(h))
-              val exp = Option.when(withExp)(ast.PermLeCmp(ast.DebugLabelledOld(ast.CurrentPerm(resAcc)(), debugLabel)(), ast.FullPerm()())())
+              val debugLabel = v.getDebugOldLabel(s2, resAcc.pos, Some(h))
+              val exp = Option.when(debugOn)(ast.PermLeCmp(ast.DebugLabelledOld(ast.CurrentPerm(resAcc)(), debugLabel)(), ast.FullPerm()())())
               v.decider.assume(PermAtMost(currentPermAmount, FullPerm), exp, exp.map(s2.substituteVarsInExp(_)))
-              val s3 = if (Verifier.config.enableDebugging()) s2.copy(oldHeaps = s2.oldHeaps + (debugHeapName -> h)) else s2
-              s3
-            case _ => s2
+            case _ =>
           }
 
-          (s3, currentPermAmount)
+          (s2, currentPermAmount)
         } else {
           val chs = chunkSupporter.findChunksWithID[NonQuantifiedChunk](h.values, identifier)
           val currentPermAmount =
@@ -320,10 +316,10 @@ class DefaultHeapSupportRules extends HeapSupportRules {
            * quantifier in whose body field 'fa.field' was accessed)
            * which is protected by a trigger term that we currently don't have.
            */
-          v.decider.assume(And(fvfDef.valueDefinitions), Option.when(withExp)(DebugExp.createInstance("Value definitions", isInternal_ = true)))
+          v.decider.assume(And(fvfDef.valueDefinitions), Option.when(debugOn)(DebugExp.createInstance("Value definitions", isInternal_ = true)))
           if (s.heapDependentTriggers.contains(fa.field)) {
             val trigger = FieldTrigger(fa.field.name, fvfDef.sm, tRcvr)
-            val triggerExp = Option.when(withExp)(DebugExp.createInstance(s"FieldTrigger(${eRcvr.toString()}.${fa.field.name})"))
+            val triggerExp = Option.when(debugOn)(DebugExp.createInstance(s"FieldTrigger(${eRcvr.toString()}.${fa.field.name})"))
             v.decider.assume(trigger, triggerExp)
           }
           if (s.triggerExp) {
@@ -335,7 +331,7 @@ class DefaultHeapSupportRules extends HeapSupportRules {
             val toAssert = IsPositive(totalPermissions.replace(`?r`, tRcvr))
             v.decider.assert(toAssert) {
               case false =>
-                createFailure(ve, v, s, toAssert, Option.when(withExp)(perms.IsPositive(ast.CurrentPerm(fa)())()))
+                createFailure(ve, v, s, toAssert, Option.when(debugOn)(perms.IsPositive(ast.CurrentPerm(fa)())()))
               case true =>
                 val fvfLookup = Lookup(fa.field.name, fvfDef.sm, tRcvr)
                 val fr1 = s.functionRecorder.recordSnapshot(fa, v.decider.pcs.branchConditions, fvfLookup).recordFvfAndDomain(fvfDef)
@@ -367,12 +363,12 @@ class DefaultHeapSupportRules extends HeapSupportRules {
           }
           if (s2.heapDependentTriggers.contains(fa.field)) {
             val trigger = FieldTrigger(fa.field.name, sm, tRcvr)
-            val triggerExp = Option.when(withExp)(DebugExp.createInstance(s"FieldTrigger(${eRcvr.toString()}.${fa.field.name})"))
+            val triggerExp = Option.when(debugOn)(DebugExp.createInstance(s"FieldTrigger(${eRcvr.toString()}.${fa.field.name})"))
             v.decider.assume(trigger, triggerExp)
           }
           val (permCheck, permCheckExp, s3) =
             if (s2.triggerExp) {
-              (True, Option.when(withExp)(ast.TrueLit()()), s2)
+              (True, Option.when(debugOn)(ast.TrueLit()()), s2)
             } else {
               val (s3, lhs) = tRcvr match {
                 case _: Literal | _: Var => (s2, True)
@@ -382,7 +378,7 @@ class DefaultHeapSupportRules extends HeapSupportRules {
                   val newFuncRec = s2.functionRecorder.recordFreshSnapshot(rcvrVar.applicable.asInstanceOf[Function])
                   (s2.copy(functionRecorder = newFuncRec), BuiltinEquals(rcvrVar, tRcvr))
               }
-              (Implies(lhs, IsPositive(totalPerms)), Option.when(withExp)(perms.IsPositive(ast.CurrentPerm(fa)(fa.pos, fa.info, fa.errT))(fa.pos, fa.info, fa.errT)), s3)
+              (Implies(lhs, IsPositive(totalPerms)), Option.when(debugOn)(perms.IsPositive(ast.CurrentPerm(fa)(fa.pos, fa.info, fa.errT))(fa.pos, fa.info, fa.errT)), s3)
             }
           v.decider.assert(permCheck) {
             case false =>
@@ -397,7 +393,7 @@ class DefaultHeapSupportRules extends HeapSupportRules {
       }
     } else {
       val resource = fa.res(s.program)
-      chunkSupporter.lookup(s, s.h, resource, Seq(tRcvr), Option.when(withExp)(Seq(eRcvr.get)), ve, v)((s2, h2, tSnap, v2) => {
+      chunkSupporter.lookup(s, s.h, resource, Seq(tRcvr), Option.when(debugOn)(Seq(eRcvr.get)), ve, v)((s2, h2, tSnap, v2) => {
         val fr = s2.functionRecorder.recordSnapshot(fa, v2.decider.pcs.branchConditions, tSnap)
         val s3 = s2.copy(h = h2, functionRecorder = fr)
         Q(s3, tSnap, v)
@@ -429,7 +425,7 @@ class DefaultHeapSupportRules extends HeapSupportRules {
         quantifiedChunkSupporter.summarisingSnapshotMap(
           s, resource, tFormalArgs, relevantChunks, v)
       val eArgsStr = eArgs.mkString(", ")
-      val debugExp = Option.when(withExp)(DebugExp.createInstance(Some(s"Resource trigger(${name}($eArgsStr))"), Some(resAcc),
+      val debugExp = Option.when(debugOn)(DebugExp.createInstance(Some(s"Resource trigger(${name}($eArgsStr))"), Some(resAcc),
         Some(resAcc), None, isInternal_ = true, InsertionOrderedSet.empty))
       v.decider.assume(trigger(smDef1.sm), debugExp)
       s.copy(smCache = smCache1, functionRecorder = s.functionRecorder.recordFvfAndDomain(smDef1))
@@ -454,7 +450,7 @@ class DefaultHeapSupportRules extends HeapSupportRules {
     if (useQPs) {
       val trigger = (sm: Term) => ResourceTriggerFunction(resource, sm, tArgs, s.program)
       val tFormalArgs = s.getFormalArgVars(resource, v)
-      val eFormalArgs = Option.when(withExp)(s.getFormalArgDecls(resource))
+      val eFormalArgs = Option.when(debugOn)(s.getFormalArgDecls(resource))
       quantifiedChunkSupporter.produceSingleLocation(
         s, resource, tFormalArgs, eFormalArgs, tArgs, eArgs, tSnap, tPerm, ePerm, trigger, mergeAndTrigger, v)(Q)
     } else {
@@ -473,7 +469,7 @@ class DefaultHeapSupportRules extends HeapSupportRules {
                 && !Verifier.config.disableFunctionUnfoldTrigger()) {
                 val predicate = resource.asInstanceOf[ast.Predicate]
                 val argsString = eArgs.mkString(", ")
-                val debugExp = Option.when(withExp)(DebugExp.createInstance(s"PredicateTrigger(${predicate.name}($argsString))", isInternal_ = true))
+                val debugExp = Option.when(debugOn)(DebugExp.createInstance(s"PredicateTrigger(${predicate.name}($argsString))", isInternal_ = true))
                 v2.decider.assume(App(s2.predicateData(predicate.name).triggerFunction, snap1 +: tArgs), debugExp)
               }
               Q(s2.copy(h = h2), v2)
@@ -500,7 +496,7 @@ class DefaultHeapSupportRules extends HeapSupportRules {
     val useQPs = s.isQuantifiedResource(resource)
     if (useQPs) {
       val tFormalArgs = s.getFormalArgVars(resource, v)
-      val eFormalArgs = Option.when(withExp)(s.getFormalArgDecls(resource))
+      val eFormalArgs = Option.when(debugOn)(s.getFormalArgDecls(resource))
       quantifiedChunkSupporter.consumeSingleLocation(
         s, h, tFormalArgs, eFormalArgs, tArgs, eArgs, resAcc, tPerm, ePerm, returnSnap, None, pve, v)(Q)
     } else {
@@ -671,7 +667,7 @@ class DefaultHeapSupportRules extends HeapSupportRules {
 
     val newChunks = relevantChunks.map {
       case ch: MagicWandChunk =>
-        val havockedSnap = v.decider.fresh("mwsf", sorts.MagicWandSnapFunction, Option.when(withExp)(PUnknown()))
+        val havockedSnap = v.decider.fresh("mwsf", sorts.MagicWandSnapFunction, Option.when(debugOn)(PUnknown()))
         val cond = replacementCond(lhs, ch.args, condInfo)
         val magicWandSnapshot = MagicWandSnapshot(Ite(cond, havockedSnap, ch.snap.mwsf))
         ch.withSnap(magicWandSnapshot, None)
@@ -757,7 +753,7 @@ class DefaultHeapSupportRules extends HeapSupportRules {
       )
 
       v.decider.prover.comment("axiomatized snapshot map after havoc")
-      val debugExp = Option.when(withExp)(DebugExp.createInstance("havoc new axiom", isInternal_ = true))
+      val debugExp = Option.when(debugOn)(DebugExp.createInstance("havoc new axiom", isInternal_ = true))
       v.decider.assume(newAxiom, debugExp)
 
       ch.withSnapshotMap(newSm)
@@ -805,7 +801,7 @@ class DefaultHeapSupportRules extends HeapSupportRules {
       chs.map { ch =>
         val bc = IsPositive(ch.perm.replace(ch.quantifiedVars, tArgs))
         val bcExp: ast.Exp = ast.LocalVar("chunk has non-zero permission", ast.Bool)() // TODO
-        val bcExpNew = Option.when(withExp)(ast.GeCmp(replaceVarsInExp(ch.permExp.get, ch.quantifiedVarExps.get.map(_.name), eArgs.get), ast.NoPerm()())(ch.permExp.get.pos, ch.permExp.get.info, ch.permExp.get.errT))
+        val bcExpNew = Option.when(debugOn)(ast.GeCmp(replaceVarsInExp(ch.permExp.get, ch.quantifiedVarExps.get.map(_.name), eArgs.get), ast.NoPerm()())(ch.permExp.get.pos, ch.permExp.get.info, ch.permExp.get.errT))
         val tTriggers = Seq(Trigger(ch.valueAt(tArgs)))
 
         val trig = ch match {
@@ -828,7 +824,7 @@ class DefaultHeapSupportRules extends HeapSupportRules {
 
         val lhsExp: ast.Exp = ast.LocalVar("chunk matches forperm pattern and has positive permission", ast.Bool)() // TODO
 
-        val lhsExpNew = if (withExp) {
+        val lhsExpNew = if (debugOn) {
           val argsEqualExps = (eArgs.get zip ch.argsExp.get) map (ae => ast.EqCmp(ae._1, ae._2)())
           val permExp = ch.permExp.get
           val isPositiveExpNew = ast.GeCmp(permExp, ast.NoPerm()())(permExp.pos, permExp.info, permExp.errT)
diff --git a/src/main/scala/rules/Joiner.scala b/src/main/scala/rules/Joiner.scala
index e61691995..04dc4803e 100644
--- a/src/main/scala/rules/Joiner.scala
+++ b/src/main/scala/rules/Joiner.scala
@@ -94,21 +94,21 @@ object joiner extends JoiningRules {
         val (sJoined, dataJoined) = merge(entries)
 
         var feasibleBranches: List[Term] = Nil
-        var feasibleBranchesExp: Option[List[ast.Exp]] = Option.when(withExp)(Nil)
-        var feasibleBranchesExpNew: Option[List[ast.Exp]] = Option.when(withExp)(Nil)
+        var feasibleBranchesExp: Option[List[ast.Exp]] = Option.when(debugOn)(Nil)
+        var feasibleBranchesExpNew: Option[List[ast.Exp]] = Option.when(debugOn)(Nil)
 
         entries foreach (entry => {
           val pcs = entry.pathConditions.conditionalized
-          val pcsExp = Option.when(withExp)(entry.pathConditions.conditionalizedExp)
+          val pcsExp = Option.when(debugOn)(entry.pathConditions.conditionalizedExp)
           val comment = "Joined path conditions"
           v.decider.prover.comment(comment)
-          v.decider.assume(pcs, Option.when(withExp)(DebugExp.createInstance(comment, InsertionOrderedSet(pcsExp.get))), enforceAssumption = false)
+          v.decider.assume(pcs, Option.when(debugOn)(DebugExp.createInstance(comment, InsertionOrderedSet(pcsExp.get))), enforceAssumption = false)
           feasibleBranches = And(entry.pathConditions.branchConditions) :: feasibleBranches
           feasibleBranchesExp = feasibleBranchesExp.map(fbe => BigAnd(entry.pathConditions.branchConditionExps.map(_._1)) :: fbe)
           feasibleBranchesExpNew = feasibleBranchesExpNew.map(fbe => BigAnd(entry.pathConditions.branchConditionExps.map(_._2.get)) :: fbe)
         })
         // Assume we are in a feasible branch
-        v.decider.assume(Or(feasibleBranches), Option.when(withExp)(DebugExp.createInstance(Some("Feasible Branches"), feasibleBranchesExp.map(BigOr(_)), feasibleBranchesExpNew.map(BigOr(_)), InsertionOrderedSet.empty)))
+        v.decider.assume(Or(feasibleBranches), Option.when(debugOn)(DebugExp.createInstance(Some("Feasible Branches"), feasibleBranchesExp.map(BigOr(_)), feasibleBranchesExpNew.map(BigOr(_)), InsertionOrderedSet.empty)))
         Q(sJoined, dataJoined, v)
       }
     }
diff --git a/src/main/scala/rules/MagicWandSupporter.scala b/src/main/scala/rules/MagicWandSupporter.scala
index d8d99e2d5..02d3f7375 100644
--- a/src/main/scala/rules/MagicWandSupporter.scala
+++ b/src/main/scala/rules/MagicWandSupporter.scala
@@ -94,7 +94,7 @@ object magicWandSupporter extends SymbolicExecutionRules {
                  : VerificationResult = {
     evaluateWandArguments(s, wand, pve, v)((s1, ts, esNew, v1) =>
       Q(s1, MagicWandChunk(MagicWandIdentifier(wand, s.program), s1.g.values, ts, esNew, snap, FullPerm,
-        Option.when(withExp)(ast.FullPerm()(wand.pos, wand.info, wand.errT))), v1)
+        Option.when(debugOn)(ast.FullPerm()(wand.pos, wand.info, wand.errT))), v1)
     )
   }
 
@@ -112,13 +112,13 @@ object magicWandSupporter extends SymbolicExecutionRules {
    * @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, Option.when(withExp)(PUnknown()))
+    val mwsf = v.decider.fresh("mwsf", sorts.MagicWandSnapFunction, Option.when(debugOn)(PUnknown()))
     val magicWandSnapshot = MagicWandSnapshot(mwsf)
     v.decider.assumeDefinition(Forall(
       abstractLhs,
       MWSFLookup(mwsf, abstractLhs) === rhsSnapshot,
       Trigger(MWSFLookup(mwsf, abstractLhs))
-    ), Option.when(withExp)(DebugExp.createInstance("Magic wand snapshot definition", true)))
+    ), Option.when(debugOn)(DebugExp.createInstance("Magic wand snapshot definition", true)))
     magicWandSnapshot
   }
 
@@ -181,7 +181,7 @@ object magicWandSupporter extends SymbolicExecutionRules {
               case (Some(ch1: QuantifiedBasicChunk), Some(ch2: QuantifiedBasicChunk)) => ch1.snapshotMap === ch2.snapshotMap
               case _ => True
             }
-            v.decider.assume(tEq, Option.when(withExp)(DebugExp.createInstance("Snapshots", isInternal_ = true)))
+            v.decider.assume(tEq, Option.when(debugOn)(DebugExp.createInstance("Snapshots", isInternal_ = true)))
 
             /* In the future it might be worth to recheck whether the permissions needed, in the case of
              * success being an instance of Incomplete, are zero.
@@ -319,23 +319,23 @@ object magicWandSupporter extends SymbolicExecutionRules {
         // to the HeapSupporter.
         val (s3, ch, tPcs, ePcs, v3 ) = if (s2.qpMagicWands.contains(MagicWandIdentifier(wand, s2.program))) {
           val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ), false))
-          val formalVarExps = Option.when(withExp)(bodyVars.indices.toList.map(i => ast.LocalVarDecl(s"x$i", bodyVars(i).typ)()))
+          val formalVarExps = Option.when(debugOn)(bodyVars.indices.toList.map(i => ast.LocalVarDecl(s"x$i", bodyVars(i).typ)()))
           val snapshotTerm = Combine(freshSnapRoot, snapRhs)
           val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s2, wand, tArgs, snapshotTerm, v2)
           v2.decider.prover.comment("Definitional axioms for singleton-SM's value")
-          val debugExp = Option.when(withExp)(DebugExp.createInstance("Definitional axioms for singleton-SM's value", true))
+          val debugExp = Option.when(debugOn)(DebugExp.createInstance("Definitional axioms for singleton-SM's value", true))
           v2.decider.assumeDefinition(smValueDef, debugExp)
           val ch = quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalVars, formalVarExps, wand, tArgs,
-            eArgsNew, FullPerm, Option.when(withExp)(ast.FullPerm()()), sm, s.program)
+            eArgsNew, FullPerm, Option.when(debugOn)(ast.FullPerm()()), sm, s.program)
           val conservedPcs = s2.conservedPcs.head :+ v2.decider.pcs.after(preMark).definitionsOnly
-          (s2, ch, conservedPcs.flatMap(_.conditionalized), Option.when(withExp)(conservedPcs.flatMap(_.conditionalizedExp)), v2)
+          (s2, ch, conservedPcs.flatMap(_.conditionalized), Option.when(debugOn)(conservedPcs.flatMap(_.conditionalizedExp)), v2)
         } else {
           val ch = MagicWandChunk(MagicWandIdentifier(wand, s.program), s2.g.values, tArgs, eArgsNew, wandSnapshot, FullPerm,
-            Option.when(withExp)(ast.FullPerm()(wand.pos, wand.info, wand.errT)))
+            Option.when(debugOn)(ast.FullPerm()(wand.pos, wand.info, wand.errT)))
           val conservedPcs = s2.conservedPcs.head :+ v2.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(pcs => pcs.conditionalized).partition(_.contains(freshSnapRoot))
-          val pcsWithoutExp = Option.when(withExp)(filterDebugExpsWithoutSnapshot(conservedPcs.flatMap(pcs => pcs.conditionalizedExp), freshSnapRoot))
+          val pcsWithoutExp = Option.when(debugOn)(filterDebugExpsWithoutSnapshot(conservedPcs.flatMap(pcs => pcs.conditionalizedExp), 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,
@@ -346,7 +346,7 @@ object magicWandSupporter extends SymbolicExecutionRules {
             }),
             Trigger(MWSFLookup(wandSnapshot.mwsf, freshSnapRoot)),
           )
-          (s2, ch, pcsQuantified +: pcsWithoutFreshSnapRoot, Option.when(withExp)(DebugExp.createInstance("MWSF definition path conditions", pcsQuantified, true) +: pcsWithoutExp.get), v2)
+          (s2, ch, pcsQuantified +: pcsWithoutFreshSnapRoot, Option.when(debugOn)(DebugExp.createInstance("MWSF definition path conditions", pcsQuantified, true) +: pcsWithoutExp.get), v2)
         }
         appendToResults(s3, ch, v3.decider.pcs.after(preMark), (tPcs, ePcs), v3)
         Success()
@@ -428,7 +428,7 @@ object magicWandSupporter extends SymbolicExecutionRules {
         // We execute the continuation Q in a new scope with all branch conditions and all conserved path conditions.
         executionFlowController.locally(s1, v)((s2, v1) => {
           val exp = viper.silicon.utils.ast.BigAnd(branchConditionsExp.map(_._1))
-          val expNew = Option.when(withExp)(viper.silicon.utils.ast.BigAnd(branchConditionsExp.map(_._2.get)))
+          val expNew = Option.when(debugOn)(viper.silicon.utils.ast.BigAnd(branchConditionsExp.map(_._2.get)))
           // Set the branch conditions
           v1.decider.setCurrentBranchCondition(And(branchConditions), (exp, expNew))
 
@@ -478,7 +478,7 @@ object magicWandSupporter extends SymbolicExecutionRules {
           case SortWrapper(snapshot: MagicWandSnapshot, _) => snapshot.applyToMWSF(snapLhs.get)
           // Fallback solution for quantified magic wands
           case predicateLookup: PredicateLookup =>
-            v2.decider.assume(snapLhs.get === First(snapWand.get), Option.when(withExp)(DebugExp.createInstance("Magic wand snapshot", true)))
+            v2.decider.assume(snapLhs.get === First(snapWand.get), Option.when(debugOn)(DebugExp.createInstance("Magic wand snapshot", true)))
             Second(predicateLookup)
           case _ => snapWand.get
         }
diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala
index 1aa582efd..3e7ace62a 100644
--- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala
+++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala
@@ -45,12 +45,12 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
       /* Cache miss */
     }
     var permissionSum: Term = NoPerm
-    var permissionSumExp: Option[ast.Exp] = Option.when(withExp)(ast.NoPerm()())
+    var permissionSumExp: Option[ast.Exp] = Option.when(debugOn)(ast.NoPerm()())
     relevantChunks.foreach(ch => {
       val argumentEqualities =
         And(ch.args.zip(args).map { case (t1, t2) => t1 === t2 })
       val argumentEqualitiesExp =
-        Option.when(withExp)(BigAnd(ch.argsExp.get.zip(argsExp.get).map { case (e1, e2) => ast.EqCmp(e1, e2)() }))
+        Option.when(debugOn)(BigAnd(ch.argsExp.get.zip(argsExp.get).map { case (e1, e2) => ast.EqCmp(e1, e2)() }))
 
       permissionSum =
         PermPlus(permissionSum, Ite(argumentEqualities, ch.perm, NoPerm))
@@ -172,7 +172,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
     }
 
     val (s1, taggedSnap, snapDefs, permSum, permSumExp) = summariseOnly(s, relevantChunks, resource, args, argsExp, knownValue, v)
-    v.decider.assumeDefinition(And(snapDefs), Option.when(withExp)(DebugExp.createInstance("Snapshot", true)))
+    v.decider.assumeDefinition(And(snapDefs), Option.when(debugOn)(DebugExp.createInstance("Snapshot", true)))
     //    v.decider.assume(PermAtMost(permSum, FullPerm())) /* Done in StateConsolidator instead */
 
     val s2 =
@@ -205,7 +205,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
     if (relevantChunks.isEmpty) {
       if (v.decider.checkSmoke(true)) {
         if (s.isInPackage) {
-          val snap = v.decider.fresh(v.snapshotSupporter.optimalSnapshotSort(resource, s, v), Option.when(withExp)(PUnknown()))
+          val snap = v.decider.fresh(v.snapshotSupporter.optimalSnapshotSort(resource, s, v), Option.when(debugOn)(PUnknown()))
           Q(s, snap, v)
         } else {
           Success() // TODO: Mark branch as dead?
@@ -380,7 +380,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
         newChunks foreach { ch =>
           val resource = Resources.resourceDescriptions(ch.resourceID)
           val pathCond = interpreter.buildPathConditionsForChunk(ch, resource.instanceProperties(s.mayAssumeUpperBounds))
-          pathCond.foreach(p => v.decider.assume(p._1, Option.when(withExp)(DebugExp.createInstance(p._2, p._2))))
+          pathCond.foreach(p => v.decider.assume(p._1, Option.when(debugOn)(DebugExp.createInstance(p._2, p._2))))
         }
         val newHeap = Heap(allChunks)
 
@@ -438,9 +438,9 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
     v.decider.startDebugSubExp()
 
     var totalPermSum: Term = NoPerm
-    var totalPermSumExp: Option[ast.Exp] = Option.when(withExp)(ast.NoPerm()())
+    var totalPermSumExp: Option[ast.Exp] = Option.when(debugOn)(ast.NoPerm()())
     var totalPermTaken: Term = NoPerm
-    var totalPermTakenExp: Option[ast.Exp] = Option.when(withExp)(ast.NoPerm()())
+    var totalPermTakenExp: Option[ast.Exp] = Option.when(debugOn)(ast.NoPerm()())
     var newFr = s.functionRecorder
 
 
@@ -468,7 +468,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
             ast.Implies(ast.Not(eqExp.get)(), ast.EqCmp(permTakenExp.get, ast.NoPerm()())())(pe.pos, pe.info, pe.errT))))
 
 
-        v.decider.assume(constraint, Option.when(withExp)(DebugExp.createInstance(constraintExp, constraintExp)))
+        v.decider.assume(constraint, Option.when(debugOn)(DebugExp.createInstance(constraintExp, constraintExp)))
 
         newFr = newFr.recordPathSymbol(permTaken.applicable.asInstanceOf[Function]).recordConstraint(constraint)
 
@@ -493,7 +493,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
     v.decider.assert(Implies(PermLess(NoPerm, perms), totalPermTaken !== NoPerm)) {
       case true =>
         val constraintExp = permsExp.map(pe => ast.EqCmp(pe, totalPermTakenExp.get)())
-        v.decider.assume(perms === totalPermTaken, Option.when(withExp)(DebugExp.createInstance(constraintExp, constraintExp)))
+        v.decider.assume(perms === totalPermTaken, Option.when(debugOn)(DebugExp.createInstance(constraintExp, constraintExp)))
         if (returnSnap) {
           summarise(s1, relevantChunks.toSeq, resource, args, argsExp, None, v)((s2, snap, _, _, v1) =>
             Q(s2, updatedChunks, Some(snap), v1))
@@ -529,7 +529,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
           val eq = freeReceiver === chunk.args.head /* For field chunks, the receiver is the only argument */
           PermPlus(permSum, Ite(eq, chunk.perm, NoPerm))
         }
-      val permissionSumExp = Option.when(withExp)(relevantChunks.foldLeft(ast.NoPerm()(): ast.Exp) { case (permSumExp, chunk) =>
+      val permissionSumExp = Option.when(debugOn)(relevantChunks.foldLeft(ast.NoPerm()(): ast.Exp) { case (permSumExp, chunk) =>
         val eq = ast.EqCmp(freeReceiverExp, chunk.argsExp.get.head)() /* For field chunks, the receiver is the only argument */
         ast.PermAdd(permSumExp, ast.CondExp(eq, chunk.permExp.get, ast.NoPerm()())())()
       })
diff --git a/src/main/scala/rules/PermissionSupporter.scala b/src/main/scala/rules/PermissionSupporter.scala
index 58c386fe9..8bd0b118a 100644
--- a/src/main/scala/rules/PermissionSupporter.scala
+++ b/src/main/scala/rules/PermissionSupporter.scala
@@ -42,7 +42,7 @@ object permissionSupporter extends SymbolicExecutionRules {
       case _ =>
         v.decider.assert(perms.IsPositive(tPerm)) {
           case true => Q(s, v)
-          case false => createFailure(pve dueTo NonPositivePermission(ePerm), v, s, perms.IsPositive(tPerm), Option.when(withExp)(perms.IsPositive(ePerm)()))
+          case false => createFailure(pve dueTo NonPositivePermission(ePerm), v, s, perms.IsPositive(tPerm), Option.when(debugOn)(perms.IsPositive(ePerm)()))
         }
     }
   }
diff --git a/src/main/scala/rules/PredicateSupporter.scala b/src/main/scala/rules/PredicateSupporter.scala
index 65ff902e9..1086b6672 100644
--- a/src/main/scala/rules/PredicateSupporter.scala
+++ b/src/main/scala/rules/PredicateSupporter.scala
@@ -67,7 +67,7 @@ object predicateSupporter extends PredicateSupportRules {
 
     val predicate = pa.loc(s.program)
     val body = predicate.body.get /* Only non-abstract predicates can be unfolded */
-    val tArgsWithE = if (withExp)
+    val tArgsWithE = if (debugOn)
       tArgs zip eArgs.get.map(Some(_))
     else
       tArgs zip Seq.fill(tArgs.length)(None)
@@ -75,17 +75,20 @@ object predicateSupporter extends PredicateSupportRules {
     val s1 = s.copy(g = gIns,
                     smDomainNeeded = true)
               .scalePermissionFactor(tPerm, ePerm)
+
     consume(s1, body, true, pve, v)((s1a, snap, v1) => {
       if (!Verifier.config.disableFunctionUnfoldTrigger()) {
         val predTrigger = App(s1a.predicateData(predicate.name).triggerFunction,
           snap.get.convert(terms.sorts.Snap) +: tArgs)
         val eArgsString = eArgs.mkString(", ")
-        v1.decider.assume(predTrigger, Option.when(withExp)(DebugExp.createInstance(s"PredicateTrigger(${predicate.name}($eArgsString))")))
+        v1.decider.assume(predTrigger, Option.when(debugOn)(DebugExp.createInstance(s"PredicateTrigger(${predicate.name}($eArgsString))")))
       }
       val s2 = s1a.copy(g = s.g,
                         smDomainNeeded = s.smDomainNeeded,
                         permissionScalingFactor = s.permissionScalingFactor,
                         permissionScalingFactorExp = s.permissionScalingFactorExp).setConstrainable(constrainableWildcards, false)
+      lazy val oldHeap = magicWandSupporter.getEvalHeap(s2)
+      lazy val oldPCS = v1.decider.pcs.duplicate()
 
       v1.heapSupporter.produceSingle(s2, predicate, tArgs, eArgs, snap.get.convert(s2.predicateSnapMap(predicate.name)), None, tPerm, ePerm, pve, true, v1)((s3, v3) => {
         val s4 = v3.heapSupporter.triggerResourceIfNeeded(s3, pa, tArgs, eArgs, v3)
@@ -99,7 +102,7 @@ object predicateSupporter extends PredicateSupportRules {
             : VerificationResult = {
     tree match {
       case PredicateLeafNode(h, assumptions) =>
-        val debugExp = Option.when(withExp)(DebugExp.createInstance("Assumption from unfolded predicate body"))
+        val debugExp = Option.when(debugOn)(DebugExp.createInstance("Assumption from unfolded predicate body"))
         v.decider.assume(assumptions.map(a => (a.replace(toReplace), debugExp)).toSeq)
         val substChunks = h.values.map(_.substitute(toReplace).asInstanceOf[GeneralChunk].permScale(s.permissionScalingFactor, s.permissionScalingFactorExp))
 
@@ -190,13 +193,15 @@ object predicateSupporter extends PredicateSupportRules {
             (Q: (State, Verifier) => VerificationResult)
             : VerificationResult = {
 
-    val tArgsWithE = if (withExp)
+    val tArgsWithE = if (debugOn)
       tArgs zip eArgs.get.map(Some(_))
     else
       tArgs zip Seq.fill(tArgs.length)(None)
     val gIns = s.g + Store(predicate.formalArgs map (_.localVar) zip tArgsWithE)
     val body = predicate.body.get /* Only non-abstract predicates can be unfolded */
     val s1 = s.scalePermissionFactor(tPerm, ePerm)
+    lazy val oldHeap = magicWandSupporter.getEvalHeap(s)
+    lazy val oldPCS = v.decider.pcs.duplicate()
 
     v.heapSupporter.consumeSingle(s1, s1.h, pa, tArgs, eArgs, tPerm, ePerm, true, pve, v)((s2, h2, snap, v1) => {
       val s3 = s2.copy(g = gIns, h = h2)
@@ -210,7 +215,7 @@ object predicateSupporter extends PredicateSupportRules {
               App(s4.predicateData(predicate.name).triggerFunction,
                 snap.get.convert(terms.sorts.Snap) +: tArgs)
             val eargs = eArgs.mkString(", ")
-            v4.decider.assume(predicateTrigger, Option.when(withExp)(DebugExp.createInstance(s"PredicateTrigger(${predicate.name}($eargs))")))
+            v4.decider.assume(predicateTrigger, Option.when(debugOn)(DebugExp.createInstance(s"PredicateTrigger(${predicate.name}($eargs))")))
           }
           Q(s4.copy(g = s.g,
             permissionScalingFactor = s.permissionScalingFactor,
@@ -225,7 +230,7 @@ object predicateSupporter extends PredicateSupportRules {
               App(s4.predicateData(predicate.name).triggerFunction,
                 snap.get.convert(terms.sorts.Snap) +: tArgs)
             val eargs = eArgs.mkString(", ")
-            v2.decider.assume(predicateTrigger, Option.when(withExp)(DebugExp.createInstance(s"PredicateTrigger(${predicate.name}($eargs))")))
+            v2.decider.assume(predicateTrigger, Option.when(debugOn)(DebugExp.createInstance(s"PredicateTrigger(${predicate.name}($eargs))")))
           }
           Q(s4.copy(g = s.g,
             permissionScalingFactor = s.permissionScalingFactor,
diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala
index 2c6f072a9..a178fea3b 100644
--- a/src/main/scala/rules/Producer.scala
+++ b/src/main/scala/rules/Producer.scala
@@ -227,7 +227,7 @@ object producer extends ProductionRules {
                 QB(s3, null, v3)
               }),
               (s2, v2) => {
-                v2.decider.assume(sf(sorts.Snap, v2) === Unit, Option.when(withExp)(DebugExp.createInstance("Empty snapshot", true)))
+                v2.decider.assume(sf(sorts.Snap, v2) === Unit, Option.when(debugOn)(DebugExp.createInstance("Empty snapshot", true)))
                 /* TODO: Avoid creating a fresh var (by invoking) `sf` that is not used
                  * otherwise. In order words, only make this assumption if `sf` has
                  * already been used, e.g. in a snapshot equality such as `s0 == (s1, s2)`.
@@ -258,7 +258,7 @@ object producer extends ProductionRules {
               Q(s3, v3)
             }),
             (s2, v2) => {
-                v2.decider.assume(sf(sorts.Snap, v2) === Unit, Option.when(withExp)(DebugExp.createInstance("Empty snapshot", true)))
+                v2.decider.assume(sf(sorts.Snap, v2) === Unit, Option.when(debugOn)(DebugExp.createInstance("Empty snapshot", true)))
                   /* TODO: Avoid creating a fresh var (by invoking) `sf` that is not used
                    * otherwise. In order words, only make this assumption if `sf` has
                    * already been used, e.g. in a snapshot equality such as `s0 == (s1, s2)`.
@@ -330,7 +330,8 @@ object producer extends ProductionRules {
               else
                 WildcardSimplifyingPermTimes(tPerm, s2.permissionScalingFactor)
               val gainExp = ePermNew.map(p => ast.PermMul(p, s2.permissionScalingFactorExp.get)(p.pos, p.info, p.errT))
-              v2.heapSupporter.produceSingle(s2, resource, tArgs, eArgsNew, snap, None, gain, gainExp, pve, true, v2)(Q)
+              v2.heapSupporter.produceSingle(s2, resource, tArgs, eArgsNew, snap, None, gain, gainExp, pve, true, v2)((s3, v3) =>
+                Q(s3, v3))
             })))
 
 
@@ -339,7 +340,7 @@ object producer extends ProductionRules {
         val resAcc = accPred.loc
         val eArgs = resAcc.args(s.program)
         val tFormalArgs = s.getFormalArgVars(resource, v)
-        val eFormalArgs = Option.when(withExp)(s.getFormalArgDecls(resource))
+        val eFormalArgs = Option.when(debugOn)(s.getFormalArgDecls(resource))
         val ePerm = accPred.perm
         val qid =
           accPred match {
@@ -359,10 +360,11 @@ object producer extends ProductionRules {
             val s1a = s1.copy(constrainableARPs = s.constrainableARPs)
             v1.heapSupporter.produceQuantified(s1a, sf, forall, resource, qvars, qvarExps, tFormalArgs, eFormalArgs, qid, optTrigger, tTriggers, auxGlobals, auxNonGlobals,
               auxExps.map(_._1), auxExps.map(_._2), tCond, eCondNew.map(_.head), tArgs, permArgs.map(_.tail), tPerm, permArgs.map(_.head), pve, NegativePermission(ePerm),
-              QPAssertionNotInjective(resAcc), v1)((s2, v2) => {
+              QPAssertionNotInjective(resAcc), v1)((s2, v2) =>
               Q(s2.copy(functionRecorder = s2.functionRecorder.leaveQuantifiedExp(qpa)), v2)
-            })
-          case (s1, _, _, _, _, None, v1) => Q(s1.copy(constrainableARPs = s.constrainableARPs), v1)
+            )
+          case (s1, _, _, _, _, None, v1) =>
+            Q(s1.copy(constrainableARPs = s.constrainableARPs), v1)
         }
 
       case _: ast.InhaleExhaleExp =>
@@ -371,9 +373,9 @@ object producer extends ProductionRules {
       /* Any regular expressions, i.e. boolean and arithmetic. */
       case _ =>
         v.decider.assume(sf(sorts.Snap, v) === Unit,
-          Option.when(withExp)(DebugExp.createInstance("Empty snapshot", true))) /* TODO: See comment for case ast.Implies above */
+          Option.when(debugOn)(DebugExp.createInstance("Empty snapshot", true))) /* TODO: See comment for case ast.Implies above */
         eval(s, a, pve, v)((s1, t, aNew, v1) => {
-          v1.decider.assume(t, Option.when(withExp)(a), aNew)
+          v1.decider.assume(t, Option.when(debugOn)(a), aNew)
           Q(s1, v1)})
     }
 
diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala
index b1a12e07e..60fa12299 100644
--- a/src/main/scala/rules/QuantifiedChunkSupport.scala
+++ b/src/main/scala/rules/QuantifiedChunkSupport.scala
@@ -510,7 +510,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       case _: ast.Field =>
         (codomainQVars.head, optSmDomainDefinitionCondition, (ch: QuantifiedBasicChunk) => IsPositive(ch.perm))
       case _ =>
-        val qvar = v.decider.fresh("s", sorts.Snap, Option.when(withExp)(PUnknown())) /* Quantified snapshot s */
+        val qvar = v.decider.fresh("s", sorts.Snap, Option.when(debugOn)(PUnknown())) /* Quantified snapshot s */
 
         // Create a replacement map for rewriting e(r_1, r_2, ...) to e(first(s), second(s), ...),
         // including necessary sort wrapper applications
@@ -648,13 +648,13 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
 
     Verifier.config.mapCache(s.pmCache.get(resource, relevantChunks)) match {
       case Some(pmDef) =>
-        v.decider.assume(pmDef.valueDefinitions, Option.when(withExp)(DebugExp.createInstance("value definitions", isInternal_ = true)), enforceAssumption = false)
+        v.decider.assume(pmDef.valueDefinitions, Option.when(debugOn)(DebugExp.createInstance("value definitions", isInternal_ = true)), enforceAssumption = false)
         (pmDef, s.pmCache)
       case _ =>
         val (pm, valueDef) =
           quantifiedChunkSupporter.summarisePerm(s, relevantChunks, formalQVars, resource, smDef, v)
         val pmDef = PermMapDefinition(resource, pm, valueDef)
-        v.decider.assume(valueDef, Option.when(withExp)(DebugExp.createInstance("value definitions", isInternal_ = true)), enforceAssumption = false)
+        v.decider.assume(valueDef, Option.when(debugOn)(DebugExp.createInstance("value definitions", isInternal_ = true)), enforceAssumption = false)
         (pmDef, s.pmCache + ((resource, relevantChunks) -> pmDef))
     }
   }
@@ -695,7 +695,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
           case None =>
             val comment = "Definitional axioms for snapshot map domain"
             v.decider.prover.comment(comment)
-            v.decider.assume(smDef.domainDefinitions, Option.when(withExp)(DebugExp.createInstance(comment, isInternal_ = true)), enforceAssumption = false)
+            v.decider.assume(smDef.domainDefinitions, Option.when(debugOn)(DebugExp.createInstance(comment, isInternal_ = true)), enforceAssumption = false)
           case Some(_instantiations) =>
             // TODO: Avoid pattern matching on resource
             val instantiations = resource match {
@@ -707,7 +707,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
             v.decider.prover.comment(comment)
             // TODO: Avoid cast to Quantification
             v.decider.assume(smDef.domainDefinitions.map(_.asInstanceOf[Quantification].instantiate(instantiations)),
-              Option.when(withExp)(DebugExp.createInstance(comment, isInternal_ = true)), enforceAssumption = false)
+              Option.when(debugOn)(DebugExp.createInstance(comment, isInternal_ = true)), enforceAssumption = false)
         }
       }
 
@@ -715,7 +715,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
         case None =>
           val comment = "Definitional axioms for snapshot map values"
           v.decider.prover.comment(comment)
-          v.decider.assume(smDef.valueDefinitions, Option.when(withExp)(DebugExp.createInstance(comment, isInternal_ = true)), enforceAssumption = false)
+          v.decider.assume(smDef.valueDefinitions, Option.when(debugOn)(DebugExp.createInstance(comment, isInternal_ = true)), enforceAssumption = false)
         case Some(_instantiations) =>
           // TODO: Avoid pattern matching on resource
           val instantiations = resource match {
@@ -727,7 +727,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
           v.decider.prover.comment(comment)
           // TODO: Avoid cast to Quantification
           v.decider.assume(smDef.valueDefinitions.map(_.asInstanceOf[Quantification].instantiate(instantiations)),
-            Option.when(withExp)(DebugExp.createInstance(comment, true)), enforceAssumption = false)
+            Option.when(debugOn)(DebugExp.createInstance(comment, true)), enforceAssumption = false)
       }
     }
 
@@ -854,7 +854,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
         codomainQVarExps     = formalQVarExps,
         sm                   = tSnap,
         additionalInvArgs    = s.relevantQuantifiedVariables(tArgs).map(_._1),
-        additionalInvArgExps = Option.when(withExp)(s.relevantQuantifiedVariables(tArgs).map(_._2.get)),
+        additionalInvArgExps = Option.when(debugOn)(s.relevantQuantifiedVariables(tArgs).map(_._2.get)),
         stateQVars           = s.quantifiedVariables.map(_._1).filter(qvar => (tArgs ++ Seq(tCond)).exists(_.contains(qvar))),
         userProvidedTriggers = optTrigger.map(_ => tTriggers),
         qidPrefix            = qid,
@@ -904,7 +904,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
 
     val commentGlobals = "Nested auxiliary terms: globals"
     v.decider.prover.comment(commentGlobals)
-    v.decider.assume(auxGlobals, Option.when(withExp)(DebugExp.createInstance(description=commentGlobals, children=auxGlobalsExp.get)),
+    v.decider.assume(auxGlobals, Option.when(debugOn)(DebugExp.createInstance(description=commentGlobals, children=auxGlobalsExp.get)),
       enforceAssumption = false)
 
     val commentNonGlobals = "Nested auxiliary terms: non-globals"
@@ -913,7 +913,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       auxNonGlobals.map(_.copy(
         vars = effectiveTriggersQVars,
         triggers = effectiveTriggers)),
-      Option.when(withExp)(DebugExp.createInstance(description=commentNonGlobals, children=auxNonGlobalsExp.get)), enforceAssumption = false)
+      Option.when(debugOn)(DebugExp.createInstance(description=commentNonGlobals, children=auxNonGlobalsExp.get)), enforceAssumption = false)
 
     val nonNegImplication = Implies(tCond, perms.IsNonNegative(tPerm))
     val nonNegImplicationExp = eCond.map(c => ast.Implies(c, ast.PermGeCmp(ePerm.get, ast.NoPerm()())())(c.pos, c.info, c.errT))
@@ -950,8 +950,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
             v.decider.prover.comment(comment)
             val definitionalAxiomMark = v.decider.setPathConditionMark()
             v.decider.assume(inv.definitionalAxioms.map(a => FunctionPreconditionTransformer.transform(a, s.program)),
-              Option.when(withExp)(DebugExp.createInstance(comment, isInternal_ = true)), enforceAssumption = false)
-            v.decider.assume(inv.definitionalAxioms, Option.when(withExp)(DebugExp.createInstance(comment, isInternal_ = true)), enforceAssumption = false)
+              Option.when(debugOn)(DebugExp.createInstance(comment, isInternal_ = true)), enforceAssumption = false)
+            v.decider.assume(inv.definitionalAxioms, Option.when(debugOn)(DebugExp.createInstance(comment, isInternal_ = true)), enforceAssumption = false)
             val conservedPcs =
               if (s.recordPcs) (s.conservedPcs.head :+ v.decider.pcs.after(definitionalAxiomMark)) +: s.conservedPcs.tail
               else s.conservedPcs
@@ -998,7 +998,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
               val qvarsToInv = inv.qvarsToInversesOf(codomainVars)
               val condOfInv = tCond.replace(qvarsToInv)
               v.decider.assume(Forall(codomainVars, Implies(condOfInv, trigger), Trigger(inv.inversesOf(codomainVars))),
-                Option.when(withExp)(DebugExp.createInstance("Inverse Trigger", true)))
+                Option.when(debugOn)(DebugExp.createInstance("Inverse Trigger", true)))
               val newFuncRec = fr1.recordFvfAndDomain(smDef1)
               (smCache1, newFuncRec)
             } else {
@@ -1038,7 +1038,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
     val comment = "Definitional axioms for singleton-SM's value"
     v.decider.prover.comment(comment)
     val definitionalAxiomMark = v.decider.setPathConditionMark()
-    v.decider.assumeDefinition(smValueDef, Option.when(withExp)(DebugExp.createInstance(comment, true)))
+    v.decider.assumeDefinition(smValueDef, Option.when(debugOn)(DebugExp.createInstance(comment, true)))
     val conservedPcs =
       if (s.recordPcs) (s.conservedPcs.head :+ v.decider.pcs.after(definitionalAxiomMark)) +: s.conservedPcs.tail
       else s.conservedPcs
@@ -1050,7 +1050,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       val interpreter = new NonQuantifiedPropertyInterpreter(h1.values, v)
       val resourceDescription = Resources.resourceDescriptions(ch.resourceID)
       val pcs = interpreter.buildPathConditionsForChunk(ch, resourceDescription.instanceProperties(s.mayAssumeUpperBounds))
-      pcs.foreach(p => v.decider.assume(p._1, Option.when(withExp)(DebugExp.createInstance(p._2, p._2))))
+      pcs.foreach(p => v.decider.assume(p._1, Option.when(debugOn)(DebugExp.createInstance(p._2, p._2))))
 
       val smCache1 = if (s.isUsedAsTrigger(resource)) {
         val (relevantChunks, _) =
@@ -1058,7 +1058,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
         val (smDef1, smCache1) =
           quantifiedChunkSupporter.summarisingSnapshotMap(
             s, resource, formalQVars, relevantChunks, v)
-        v.decider.assume(resourceTriggerFactory(smDef1.sm), Option.when(withExp)(DebugExp.createInstance("Resource Trigger", true)))
+        v.decider.assume(resourceTriggerFactory(smDef1.sm), Option.when(debugOn)(DebugExp.createInstance("Resource Trigger", true)))
         smCache1
       } else {
         s.smCache
@@ -1115,7 +1115,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
         formalQVars,
         formalQVarsExp,
         s.relevantQuantifiedVariables(tArgs ++ Seq(tCond)).map(_._1),
-        Option.when(withExp)(s.relevantQuantifiedVariables(tArgs).map(_._2.get)),
+        Option.when(debugOn)(s.relevantQuantifiedVariables(tArgs).map(_._2.get)),
         s.quantifiedVariables.map(_._1).filter(qvar => (tArgs ++ Seq(tCond)).exists(_.contains(qvar))),
         optTrigger.map(_ => tTriggers),
         qid,
@@ -1137,7 +1137,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
 
     val comment = "Nested auxiliary terms: globals"
     v.decider.prover.comment(comment)
-    v.decider.assume(auxGlobals, Option.when(withExp)(DebugExp.createInstance(description=comment, children=auxGlobalsExp.get)), enforceAssumption = false)
+    v.decider.assume(auxGlobals, Option.when(debugOn)(DebugExp.createInstance(description=comment, children=auxGlobalsExp.get)), enforceAssumption = false)
 
     val comment2 = "Nested auxiliary terms: non-globals"
     v.decider.prover.comment(comment2)
@@ -1147,10 +1147,10 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
         v.decider.assume(
           auxNonGlobals.map(_.copy(
             vars = effectiveTriggersQVars,
-            triggers = effectiveTriggers)), Option.when(withExp)(DebugExp.createInstance(description=comment2, children=auxNonGlobalsExp.get)), enforceAssumption = false)
+            triggers = effectiveTriggers)), Option.when(debugOn)(DebugExp.createInstance(description=comment2, children=auxNonGlobalsExp.get)), enforceAssumption = false)
       case Some(_) =>
         /* Explicit triggers were provided. */
-        v.decider.assume(auxNonGlobals, Option.when(withExp)(DebugExp.createInstance(description=comment2, children=auxNonGlobalsExp.get)), enforceAssumption = false)
+        v.decider.assume(auxNonGlobals, Option.when(debugOn)(DebugExp.createInstance(description=comment2, children=auxNonGlobalsExp.get)), enforceAssumption = false)
     }
 
     val nonNegImplication = Implies(tCond, perms.IsNonNegative(tPerm))
@@ -1208,8 +1208,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
             v.decider.prover.comment("Definitional axioms for inverse functions")
 
             v.decider.assume(inverseFunctions.definitionalAxioms.map(a => FunctionPreconditionTransformer.transform(a, s.program)),
-              Option.when(withExp)(DebugExp.createInstance("Inverse Function Axioms", isInternal_ = true)), enforceAssumption = false)
-            v.decider.assume(inverseFunctions.definitionalAxioms, Option.when(withExp)(DebugExp.createInstance("Inverse function axiom", isInternal_ = true)), enforceAssumption = false)
+              Option.when(debugOn)(DebugExp.createInstance("Inverse Function Axioms", isInternal_ = true)), enforceAssumption = false)
+            v.decider.assume(inverseFunctions.definitionalAxioms, Option.when(debugOn)(DebugExp.createInstance("Inverse function axiom", isInternal_ = true)), enforceAssumption = false)
 
             if (s.isUsedAsTrigger(resource)){
               v.decider.assume(
@@ -1217,7 +1217,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                   formalQVars,
                   Implies(condOfInvOfLoc, ResourceTriggerFunction(resource, smDef1.get.sm, formalQVars, s.program)),
                   Trigger(inverseFunctions.inversesOf(formalQVars)))),
-                Option.when(withExp)(DebugExp.createInstance("Inverse Function", isInternal_ = true)), enforceAssumption = false)
+                Option.when(debugOn)(DebugExp.createInstance("Inverse Function", isInternal_ = true)), enforceAssumption = false)
             }
 
 
@@ -1273,14 +1273,14 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                   formalQVarsExp,
                   smDef2.sm,
                   s3.relevantQuantifiedVariables(tArgs).map(_._1),
-                  Option.when(withExp)(s3.relevantQuantifiedVariables(tArgs).map(_._2.get)),
+                  Option.when(debugOn)(s3.relevantQuantifiedVariables(tArgs).map(_._2.get)),
                   s.quantifiedVariables.map(_._1).filter(qvar => (tArgs ++ Seq(tCond)).exists(_.contains(qvar))),
                   optTrigger.map(_ => tTriggers),
                   qid,
                   v2,
                   s.program
                 )
-                val debugExp = Option.when(withExp)(DebugExp.createInstance("Inverse functions for quantified permission", true))
+                val debugExp = Option.when(debugOn)(DebugExp.createInstance("Inverse functions for quantified permission", true))
                 v.decider.assume(FunctionPreconditionTransformer.transform(inverseFunctions.axiomInvertiblesOfInverses, s3.program), debugExp)
                 v.decider.assume(inverseFunctions.axiomInvertiblesOfInverses, debugExp)
                 val substitutedAxiomInversesOfInvertibles = inverseFunctions.axiomInversesOfInvertibles.replace(formalQVars, tArgs)
@@ -1486,7 +1486,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                           : ConsumptionResult = {
 
     var permsAvailable: Term = NoPerm
-    var permsAvailableExp: Option[ast.Exp] = Option.when(withExp)(ast.NoPerm()())
+    var permsAvailableExp: Option[ast.Exp] = Option.when(debugOn)(ast.NoPerm()())
 
 
     for (ch <- candidates) {
@@ -1547,7 +1547,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
     var remainingChunks = Vector.empty[QuantifiedBasicChunk]
     var permsNeeded = perms
     var permsNeededExp = permsExp
-    var success: ConsumptionResult = Incomplete(permsNeeded, Option.when(withExp)(ast.TrueLit()()))
+    var success: ConsumptionResult = Incomplete(permsNeeded, Option.when(debugOn)(ast.TrueLit()()))
 
     v.decider.prover.comment("Precomputing data for removing quantified permissions")
 
@@ -1684,7 +1684,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
             Nil,
             s"qp.srp${v.counter(this).next()}")
 
-        val forallExp = Option.when(withExp)(ast.Forall(codomainQVarsExp.get, Seq(), ast.Implies(
+        val forallExp = Option.when(debugOn)(ast.Forall(codomainQVarsExp.get, Seq(), ast.Implies(
           ast.NeCmp(ithChunk.permExp.get, ast.NoPerm()())(),
           ast.PermLtCmp(conditionalizedPermsExp.get, ithChunk.permExp.get)())())())
 
@@ -2003,7 +2003,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
               val result = v.decider.check(And(equalityCond, equalityTerm), Verifier.config.checkTimeout())
               if (result) {
                 // Learn the equality
-                val debugExp = Option.when(withExp)(DebugExp.createInstance("Chunks alias", true))
+                val debugExp = Option.when(debugOn)(DebugExp.createInstance("Chunks alias", true))
                 v.decider.assume(equalityTerm, debugExp)
               }
               result
@@ -2033,7 +2033,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
               val result = v.decider.check(equalityTerm, Verifier.config.checkTimeout())
               if (result) {
                 // Learn the equality
-                val debugExp = Option.when(withExp)(DebugExp.createInstance("Chunks alias", true))
+                val debugExp = Option.when(debugOn)(DebugExp.createInstance("Chunks alias", true))
                 v.decider.assume(equalityTerm, debugExp)
               }
               result
diff --git a/src/main/scala/rules/StateConsolidator.scala b/src/main/scala/rules/StateConsolidator.scala
index 663282d3c..42dfafd33 100644
--- a/src/main/scala/rules/StateConsolidator.scala
+++ b/src/main/scala/rules/StateConsolidator.scala
@@ -80,7 +80,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol
 
           val (_functionRecorder, _mergedChunks, _, snapEqs) = singleMerge(functionRecorder, destChunks, newChunks, s.functionRecorderQuantifiedVariables().map(_._1), v)
 
-          snapEqs foreach (t => v.decider.assume(t, Option.when(withExp)(DebugExp.createInstance("Snapshot Equations", true))))
+          snapEqs foreach (t => v.decider.assume(t, Option.when(debugOn)(DebugExp.createInstance("Snapshot Equations", true))))
 
           functionRecorder = _functionRecorder
           mergedChunks = _mergedChunks
@@ -98,12 +98,12 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol
         mergedChunks.filter(_.isInstanceOf[BasicChunk]) foreach { case ch: BasicChunk =>
           val resource = Resources.resourceDescriptions(ch.resourceID)
           val pathCond = interpreter.buildPathConditionsForChunk(ch, resource.instanceProperties(s.mayAssumeUpperBounds))
-          pathCond.foreach(p => v.decider.assume(p._1, Option.when(withExp)(DebugExp.createInstance(p._2, p._2))))
+          pathCond.foreach(p => v.decider.assume(p._1, Option.when(debugOn)(DebugExp.createInstance(p._2, p._2))))
         }
 
         Resources.resourceDescriptions foreach { case (id, desc) =>
           val pathCond = interpreter.buildPathConditionsForResource(id, desc.delayedProperties(s.mayAssumeUpperBounds))
-          pathCond.foreach(p => v.decider.assume(p._1, Option.when(withExp)(DebugExp.createInstance(p._2, p._2))))
+          pathCond.foreach(p => v.decider.assume(p._1, Option.when(debugOn)(DebugExp.createInstance(p._2, p._2))))
         }
 
         v.symbExLog.closeScope(sepIdentifier)
@@ -114,9 +114,22 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol
                     h = mergedHeaps.head,
                     reserveHeaps = mergedHeaps.tail)
 
-    val s2 = assumeUpperPermissionBoundForQPFields(s1, v)
-
-    s2
+    val s2 = if (debugOn) {
+      val s1a = if (s1.recordIntermediateHeaps) v.recordIntermediateHeap(s1) else s1
+      val currentLabel = v.getDebugHeapLabel(s1a).getOrElse("preConsolidateHeapMissing")
+      s1a.copy(intermediateHeapCause = Some(currentLabel, StateConsolidation(), v.decider.pcs.duplicate()))
+    } else s1
+
+    val s3 = assumeUpperPermissionBoundForQPFields(s2, v)
+
+    if (debugOn){
+      if (s1.recordIntermediateHeaps) {
+        // update the old intermediateCause
+        val newParent = v.getDebugHeapLabel(s3).getOrElse("postConsolidateHeapMissing")
+        val newInterCause = Some(newParent, s1.intermediateHeapCause.get._2, v.decider.pcs.duplicate())
+        s3.copy(intermediateHeapCause = newInterCause)
+      } else s3.copy(intermediateHeapCause = None)
+    } else s3
   }
 
   def consolidateOptionally(s: State, v: Verifier): State =
@@ -132,13 +145,13 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol
     val sepIdentifier = v.symbExLog.openScope(mergeLog)
     val (fr2, mergedChunks, newlyAddedChunks, snapEqs) = singleMerge(fr1, h.values.toSeq, newH.values.toSeq, s.functionRecorderQuantifiedVariables().map(_._1), v)
 
-    v.decider.assume(snapEqs, Option.when(withExp)(DebugExp.createInstance("Snapshot", isInternal_ = true)), enforceAssumption = false)
+    v.decider.assume(snapEqs, Option.when(debugOn)(DebugExp.createInstance("Snapshot", isInternal_ = true)), enforceAssumption = false)
 
     val interpreter = new NonQuantifiedPropertyInterpreter(mergedChunks, v)
     newlyAddedChunks.filter(_.isInstanceOf[BasicChunk]) foreach { case ch: BasicChunk =>
       val resource = Resources.resourceDescriptions(ch.resourceID)
       val pathCond = interpreter.buildPathConditionsForChunk(ch, resource.instanceProperties(s.mayAssumeUpperBounds))
-      pathCond.foreach(p => v.decider.assume(p._1, Option.when(withExp)(DebugExp.createInstance(p._2, p._2))))
+      pathCond.foreach(p => v.decider.assume(p._1, Option.when(debugOn)(DebugExp.createInstance(p._2, p._2))))
     }
 
     v.symbExLog.closeScope(sepIdentifier)
@@ -277,10 +290,11 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol
           val currentPermAmount = PermLookup(field.name, pmDef.pm, receiver)
           v.decider.prover.comment(s"Assume upper permission bound for field ${field.name}")
 
-          val debugExp = if (withExp) {
-            val (debugHeapName, debugLabel) = v.getDebugOldLabel(sf, ast.NoPosition)
-            sf = sf.copy(oldHeaps = sf.oldHeaps + (debugHeapName -> sf.h))
-            val permExp = ast.DebugLabelledOld(ast.CurrentPerm(ast.FieldAccess(receiverExp.localVar, field)())(ast.NoPosition, ast.NoInfo, ast.NoTrafos), debugLabel)()
+          val debugExp = if (debugOn) {
+            sf = if (sf.recordIntermediateHeaps) v.recordIntermediateHeap(sf)
+            else v.recordDebugHeap(sf, v.getDebugHeapLabel(sf).get, StateConsolidation())
+            val permExp = ast.DebugLabelledOld(ast.CurrentPerm(ast.FieldAccess(receiverExp.localVar, field)())(ast.NoPosition, ast.NoInfo, ast.NoTrafos),
+              v.getDebugOldLabel(sf, ast.NoPosition))()
             val exp = ast.Forall(Seq(receiverExp), Seq(), ast.PermLeCmp(permExp, ast.FullPerm()())())()
             Some(DebugExp.createInstance(exp, exp))
           } else { None }
@@ -295,10 +309,11 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol
            */
           for (chunk <- fieldChunks) {
             if (chunk.singletonRcvr.isDefined){
-              val debugExp = if (withExp) {
-                val (debugHeapName, debugLabel) = v.getDebugOldLabel(sf, ast.NoPosition)
-                val permExp = ast.DebugLabelledOld(ast.CurrentPerm(ast.FieldAccess(chunk.singletonRcvrExp.get, field)())(), debugLabel)()
-                sf = sf.copy(oldHeaps = sf.oldHeaps + (debugHeapName -> sf.h))
+              val debugExp = if (debugOn) {
+                val permExp = ast.DebugLabelledOld(ast.CurrentPerm(ast.FieldAccess(chunk.singletonRcvrExp.get, field)())(),
+                  v.getDebugOldLabel(sf, ast.NoPosition))()
+                sf = if (sf.recordIntermediateHeaps) v.recordIntermediateHeap(sf)
+                else v.recordDebugHeap(sf, v.getDebugHeapLabel(sf).get, StateConsolidation())
                 val exp = ast.PermLeCmp(permExp, ast.FullPerm()())()
                 Some(DebugExp.createInstance(exp, exp))
               } else { None }
@@ -308,12 +323,12 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol
               val triggers = chunkReceivers.map(r => Trigger(r)).toSeq
               val currentPermAmount = PermLookup(field.name, pmDef.pm, chunk.quantifiedVars.head)
               v.decider.prover.comment(s"Assume upper permission bound for field ${field.name}")
-              val debugExp = if (withExp) {
+              val debugExp = if (debugOn) {
                 val chunkReceiverExp = chunk.quantifiedVarExps.get.head.localVar
                 var permExp: ast.Exp = ast.CurrentPerm(ast.FieldAccess(chunkReceiverExp, field)())(chunkReceiverExp.pos, chunkReceiverExp.info, chunkReceiverExp.errT)
-                val (debugHeapName, debugLabel) = v.getDebugOldLabel(sf, ast.NoPosition)
-                sf = sf.copy(oldHeaps = sf.oldHeaps + (debugHeapName -> sf.h))
-                permExp = ast.DebugLabelledOld(permExp, debugLabel)()
+                sf = if (sf.recordIntermediateHeaps) v.recordIntermediateHeap(sf)
+                else v.recordDebugHeap(sf, v.getDebugHeapLabel(sf).get, StateConsolidation())
+                permExp = ast.DebugLabelledOld(permExp, v.getDebugOldLabel(sf, ast.NoPosition))()
                 val exp = ast.Forall(chunk.quantifiedVarExps.get, Seq(), ast.PermLeCmp(permExp, ast.FullPerm()())())()
                 Some(DebugExp.createInstance(exp, exp))
               } else { None }
diff --git a/src/main/scala/rules/SymbolicExecutionRules.scala b/src/main/scala/rules/SymbolicExecutionRules.scala
index 66b8c2fb1..386087153 100644
--- a/src/main/scala/rules/SymbolicExecutionRules.scala
+++ b/src/main/scala/rules/SymbolicExecutionRules.scala
@@ -17,30 +17,30 @@ import viper.silver.verifier.errors.ErrorWrapperWithExampleTransformer
 import viper.silver.verifier.{Counterexample, CounterexampleTransformer, VerificationError}
 
 trait SymbolicExecutionRules {
-  lazy val withExp = Verifier.config.enableDebugging()
+  lazy val debugOn: Boolean = Verifier.config.enableDebugging()
 
   protected def createFailure(ve: VerificationError, v: Verifier, s: State, failedAssert: Term, failedAssertDescription: String, generateNewModel: Boolean): Failure = {
-    createFailure(ve, v, s, failedAssert, Option.when(withExp)(DebugExp.createInstance(failedAssertDescription)), generateNewModel)
+    createFailure(ve, v, s, failedAssert, Option.when(debugOn)(DebugExp.createInstance(failedAssertDescription)), generateNewModel)
   }
 
   protected def createFailure(ve: VerificationError, v: Verifier, s: State, failedAssert: Term, failedAssertDescription: String): Failure = {
-    createFailure(ve, v, s, failedAssert, Option.when(withExp)(DebugExp.createInstance(failedAssertDescription)), false)
+    createFailure(ve, v, s, failedAssert, Option.when(debugOn)(DebugExp.createInstance(failedAssertDescription)), false)
   }
 
   protected def createFailure(ve: VerificationError, v: Verifier, s: State, missingTermDescription: String): Failure = {
-    createFailure(ve, v, s, False, Option.when(withExp)(DebugExp.createInstance(s"Asserted term for '$missingTermDescription' not available, substituting false.")), false)
+    createFailure(ve, v, s, False, Option.when(debugOn)(DebugExp.createInstance(s"Asserted term for '$missingTermDescription' not available, substituting false.")), false)
   }
 
   protected def createFailure(ve: VerificationError, v: Verifier, s: State, missingTermDescription: String, generateNewModel: Boolean): Failure = {
-    createFailure(ve, v, s, False, Option.when(withExp)(DebugExp.createInstance(s"Asserted term for '$missingTermDescription' not available, substituting false.")), generateNewModel)
+    createFailure(ve, v, s, False, Option.when(debugOn)(DebugExp.createInstance(s"Asserted term for '$missingTermDescription' not available, substituting false.")), generateNewModel)
   }
 
   protected def createFailure(ve: VerificationError, v: Verifier, s: State, failedAssert: Term, failedAssertExp: Option[ast.Exp]): Failure = {
-    createFailure(ve, v, s, failedAssert, Option.when(withExp)(DebugExp.createInstance(failedAssertExp, failedAssertExp)), false)
+    createFailure(ve, v, s, failedAssert, Option.when(debugOn)(DebugExp.createInstance(failedAssertExp, failedAssertExp)), false)
   }
 
   protected def createFailure(ve: VerificationError, v: Verifier, s: State, failedAssert: Term, generateNewModel: Boolean, failedAssertExp: Option[ast.Exp]): Failure = {
-    createFailure(ve, v, s, failedAssert, Option.when(withExp)(DebugExp.createInstance(failedAssertExp, failedAssertExp)), generateNewModel)
+    createFailure(ve, v, s, failedAssert, Option.when(debugOn)(DebugExp.createInstance(failedAssertExp, failedAssertExp)), generateNewModel)
   }
 
   protected def createFailure(ve: VerificationError, v: Verifier, s: State, failedAssert: Term, failedAssertExp: Option[DebugExp], generateNewModel: Boolean): Failure = {
diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala
index 22043c79a..cad7c4037 100644
--- a/src/main/scala/state/State.scala
+++ b/src/main/scala/state/State.scala
@@ -12,9 +12,9 @@ import viper.silver.ast
 import viper.silver.cfg.silver.SilverCfg
 import viper.silicon.common.Mergeable
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
-import viper.silicon.decider.RecordedPathConditions
+import viper.silicon.decider.{PathConditionStack, RecordedPathConditions}
 import viper.silicon.interfaces.state.GeneralChunk
-import viper.silicon.state.State.OldHeaps
+import viper.silicon.state.State.{DebugOldHeaps, OldHeaps}
 import viper.silicon.state.terms.{Term, Var}
 import viper.silicon.interfaces.state.Chunk
 import viper.silicon.state.terms.predef.`?r`
@@ -33,6 +33,9 @@ final case class State(g: Store = Store(),
                        predicateData: Map[String, PredicateData],
                        functionData: Map[String, FunctionData],
                        oldHeaps: OldHeaps = Map.empty,
+                       debugOldHeaps: DebugOldHeaps = Map.empty,
+                       // (parentLabel, cause, oldPCS) if an operation might cause intermediate heaps
+                       intermediateHeapCause: Option[(String, HeapCause, PathConditionStack)] = None,
 
                        parallelizeBranches: Boolean = false,
 
@@ -132,6 +135,8 @@ final case class State(g: Store = Store(),
 
   val isLastRetry: Boolean = retryLevel == 0
 
+  val recordIntermediateHeaps: Boolean = intermediateHeapCause.isDefined
+
   def incCycleCounter(m: ast.Predicate) =
     if (recordVisited) copy(visited = m :: visited)
     else this
@@ -189,8 +194,26 @@ final case class State(g: Store = Store(),
   override val toString = s"${this.getClass.getSimpleName}(...)"
 }
 
+sealed trait HeapCause
+case class InhalePre() extends HeapCause
+case class ExhalePost() extends HeapCause
+case class InhaleInv() extends HeapCause
+case class ExhaleInv() extends HeapCause
+case class MergeContext() extends HeapCause
+case class CreateLabel() extends HeapCause
+case class StateConsolidation() extends HeapCause
+case class ExecStmt(stmt: ast.Stmt) extends HeapCause
+case class EvalExp(exp: ast.Exp) extends HeapCause
+
+case class DebugHeap(heap: Heap,
+                     parentLabel: String,
+                     cause: HeapCause,
+                     intermediateCause: Option[ast.Exp],
+                     branchConds: Seq[(ast.Exp, Term)])
+
 object State {
   type OldHeaps = Map[String, Heap]
+  type DebugOldHeaps = Map[String, DebugHeap]
   val OldHeaps = Map
 
   def merge(s1: State, s2: State): State = {
@@ -200,6 +223,8 @@ object State {
                  predicateData,
                  functionData,
                  oldHeaps1,
+                 debugOldHeaps1,
+                 intermediateHeapCause1,
                  parallelizeBranches1,
                  recordVisited1, visited1,
                  methodCfg1, invariantContexts1,
@@ -225,6 +250,8 @@ object State {
                      `program`, `member`,
                      `predicateData`, `functionData`,
                      oldHeaps2,
+                     debugOldHeaps2,
+                     intermediateHeapCause2,
                      `parallelizeBranches1`,
                      `recordVisited1`, `visited1`,
                      `methodCfg1`, `invariantContexts1`,
@@ -245,6 +272,8 @@ object State {
                      moreCompleteExhale2, `moreJoins`) =>
 
             val oldHeaps3 = oldHeaps1 ++ oldHeaps2
+            val debugOldHeaps3 = debugOldHeaps1 ++ debugOldHeaps2
+            val intermediateHeapCause3 = if (intermediateHeapCause1 == intermediateHeapCause2) intermediateHeapCause1 else None
             val functionRecorder3 = functionRecorder1.merge(functionRecorder2)
             val triggerExp3 = triggerExp1 && triggerExp2
             val possibleTriggers3 = possibleTriggers1 ++ possibleTriggers2
@@ -263,6 +292,8 @@ object State {
               .map({ case (pcs1, pcs2) => (pcs1 ++ pcs2).distinct })
 
             s1.copy(oldHeaps = oldHeaps3,
+                    debugOldHeaps = debugOldHeaps3,
+                    intermediateHeapCause = intermediateHeapCause3,
                     functionRecorder = functionRecorder3,
                     possibleTriggers = possibleTriggers3,
                     triggerExp = triggerExp3,
@@ -275,6 +306,7 @@ object State {
                     conservedPcs = conservedPcs3)
 
           case _ =>
+            println(s1.possibleTriggers.toString() + s2.possibleTriggers.toString())
             val err = new StringBuilder()
             for (ix <- 0 until s1.productArity) {
               val e1 = s1.productElement(ix)
@@ -358,6 +390,8 @@ object State {
       case State(g1, h1, program, member,
       predicateData, functionData,
       oldHeaps1,
+      debugOldHeaps1,
+      intermediateHeapCause1,
       parallelizeBranches1,
       recordVisited1, visited1,
       methodCfg1, invariantContexts1,
@@ -382,6 +416,8 @@ object State {
           case State(g2, h2, `program`, `member`,
           `predicateData`, `functionData`,
           oldHeaps2,
+          debugOldHeaps2,
+          intermediateHeapCause2,
           `parallelizeBranches1`,
           `recordVisited1`, `visited1`,
           `methodCfg1`, invariantContexts2,
@@ -401,6 +437,8 @@ object State {
           `predicateSnapMap1`, `predicateFormalVarMap1`, `retryLevel`, `useHeapTriggers`,
           moreCompleteExhale2, `moreJoins`) =>
 
+            val debugOldHeaps3 = debugOldHeaps1 ++ debugOldHeaps2
+            val intermediateHeapCause3 = if (intermediateHeapCause1 == intermediateHeapCause2) intermediateHeapCause1 else None
             val functionRecorder3 = functionRecorder1.merge(functionRecorder2)
             val triggerExp3 = triggerExp1 && triggerExp2
             val possibleTriggers3 = possibleTriggers1 ++ possibleTriggers2
@@ -483,6 +521,8 @@ object State {
                              g = g3,
                              h = h3,
                              oldHeaps = oldHeaps3,
+                             debugOldHeaps = debugOldHeaps3,
+                             intermediateHeapCause = intermediateHeapCause3,
                              partiallyConsumedHeap = partiallyConsumedHeap3,
                              smDomainNeeded = smDomainNeeded3,
                              invariantContexts = invariantContexts3,
diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala
index 71a2eb44a..041a70a4f 100644
--- a/src/main/scala/supporters/MethodSupporter.scala
+++ b/src/main/scala/supporters/MethodSupporter.scala
@@ -13,12 +13,13 @@ import viper.silver.verifier.errors._
 import viper.silicon.interfaces._
 import viper.silicon.decider.Decider
 import viper.silicon.logger.records.data.WellformednessCheckRecord
-import viper.silicon.rules.{consumer, executionFlowController, executor, producer}
-import viper.silicon.state.{State, Store}
+import viper.silicon.rules.{consumer, executionFlowController, executor, magicWandSupporter, producer}
+import viper.silicon.state.{DebugHeap, ExhalePost, InhalePre, State, Store}
 import viper.silicon.state.State.OldHeaps
 import viper.silicon.verifier.{Verifier, VerifierComponent}
 import viper.silicon.utils.freshSnap
 import viper.silicon.Map
+import viper.silver.ast.MethodCall
 
 /* TODO: Consider changing the DefaultMethodVerificationUnitProvider into a SymbolicExecutionRule */
 
@@ -68,7 +69,11 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif
       val s = sInit.copy(g = g,
                          h = v.heapSupporter.getEmptyHeap(sInit.program),
                          oldHeaps = OldHeaps(),
+                         debugOldHeaps = Map(),
                          methodCfg = body)
+      val s0 = if (producer.debugOn)
+        s.copy(intermediateHeapCause = Some("nil", InhalePre(), decider.pcs.duplicate()))
+      else s
 
       if (Verifier.config.printMethodCFGs()) {
         viper.silicon.common.io.toFile(
@@ -81,11 +86,16 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif
         /* Combined the well-formedness check and the execution of the body, which are two separate
          * rules in Smans' paper.
          */
-        executionFlowController.locally(s, v)((s1, v1) => {
+        executionFlowController.locally(s0, v)((s1, v1) => {
           produces(s1, freshSnap, pres, ContractNotWellformed, v1)((s2, v2) => {
             v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract)
             val s2a = s2.copy(oldHeaps = s2.oldHeaps + (Verifier.PRE_STATE_LABEL -> s2.h))
-            (  executionFlowController.locally(s2a, v2)((s3, v3) => {
+            val s2b = if (producer.debugOn) {
+              val branchConds = v2.decider.pcs.branchConditionExps.map(bc => bc._1).zip(v2.decider.pcs.branchConditions)
+              val initDebugHeap = DebugHeap(magicWandSupporter.getEvalHeap(s2), "nil", InhalePre(), None, branchConds)
+              s2a.copy(debugOldHeaps = s2a.debugOldHeaps + (Verifier.PRE_STATE_LABEL -> initDebugHeap))
+            } else s2a
+            (  executionFlowController.locally(s2b, v2)((s3, v3) => {
                   val s4 = s3.copy(h = v3.heapSupporter.getEmptyHeap(s3.program))
                   val impLog = new WellformednessCheckRecord(posts, s, v.decider.pcs)
                   val sepIdentifier = symbExLog.openScope(impLog)
@@ -93,10 +103,14 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif
                     symbExLog.closeScope(sepIdentifier)
                     Success()})})
             && {
-               executionFlowController.locally(s2a, v2)((s3, v3) =>  {
-                  exec(s3, body, v3)((s4, v4) =>
-                    consumes(s4, posts, false, postViolated, v4)((_, _, _) =>
-                      Success()))}) }  )})})
+               executionFlowController.locally(s2b, v2)((s3, v3) =>  {
+                  exec(s3, body, v3)((s4, v4) => {
+                    val currentLabel = v4.getDebugHeapLabel(s4).getOrElse("finalHeapMissing")
+                    val s4a = if (producer.debugOn)
+                      s4.copy(intermediateHeapCause = Some(currentLabel, ExhalePost(), v4.decider.pcs.duplicate()))
+                    else s4
+                    consumes(s4a, posts, false, postViolated, v4)((_, _, _) =>
+                      Success())})}) }  )})})
 
       v.decider.resetProverOptions()
 
diff --git a/src/main/scala/supporters/QuantifierSupporter.scala b/src/main/scala/supporters/QuantifierSupporter.scala
index 024a6bd68..bcff77dee 100644
--- a/src/main/scala/supporters/QuantifierSupporter.scala
+++ b/src/main/scala/supporters/QuantifierSupporter.scala
@@ -89,7 +89,7 @@ class DefaultQuantifierSupporter(triggerGenerator: TriggerGenerator) extends Qua
       .distinct
       // : Seq[(Trigger, Seq[Term])]
       // Map all heap dependencies to fresh variables
-      .map({ case (ts, deps) => (ts, deps.map(t => (t, fresh("proj", t.sort, Option.when(evaluator.withExp)(PUnknown())))).toMap)})
+      .map({ case (ts, deps) => (ts, deps.map(t => (t, fresh("proj", t.sort, Option.when(evaluator.debugOn)(PUnknown())))).toMap)})
       // : Seq[(Trigger, Map[Term, Var])]
       // For each trigger, create a new quantifier where all heap dependencies are replaced with the new variables
       .map({ case (ts, m) =>
diff --git a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala
index 3cc1c934a..4d9a87657 100644
--- a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala
+++ b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala
@@ -21,7 +21,7 @@ import viper.silicon.state.terms._
 import viper.silicon.state.terms.predef.`?s`
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
 import viper.silicon.decider.Decider
-import viper.silicon.rules.{consumer, evaluator, executionFlowController, producer}
+import viper.silicon.rules.{consumer, evaluator, executionFlowController, magicWandSupporter, producer}
 import viper.silicon.supporters.{AnnotationSupporter, PredicateData}
 import viper.silicon.utils.ast.{BigAnd, simplifyVariableName}
 import viper.silicon.verifier.{Verifier, VerifierComponent}
@@ -175,7 +175,8 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver
       val data = functionData(function.name)
       val s = sInit.copy(functionRecorder = ActualFunctionRecorder(Left(data)),
         conservingSnapshotGeneration = true,
-        assertReadAccessOnly = !Verifier.config.respectFunctionPrePermAmounts())
+        assertReadAccessOnly = !Verifier.config.respectFunctionPrePermAmounts(),
+        intermediateHeapCause = if (evaluator.debugOn) Some("nil", InhalePre(), decider.pcs.duplicate()) else None)
 
       /* Phase 1: Check well-definedness of the specifications */
       checkSpecificationWelldefinedness(s, function) match {
@@ -221,7 +222,7 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver
       val pres = function.pres
       val posts = function.posts
       val argsStore = data.formalArgs map {
-        case (localVar, t) => (localVar, (t, Option.when(evaluator.withExp)(LocalVarWithVersion(simplifyVariableName(t.id.name), localVar.typ)(localVar.pos, localVar.info, localVar.errT))))
+        case (localVar, t) => (localVar, (t, Option.when(evaluator.debugOn)(LocalVarWithVersion(simplifyVariableName(t.id.name), localVar.typ)(localVar.pos, localVar.info, localVar.errT))))
       }
       val g = Store(argsStore + (function.result -> (data.formalResult, data.valFormalResultExp)))
       val s = sInit.copy(g = g, h = v.heapSupporter.getEmptyHeap(sInit.program), oldHeaps = OldHeaps())
@@ -234,7 +235,7 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver
         produces(s0, toSf(`?s`), pres, ContractNotWellformed, v)((s1, _) => {
           val relevantPathConditionStack = decider.pcs.after(preMark)
           phase1Data :+= Phase1Data(s1, relevantPathConditionStack.branchConditions, relevantPathConditionStack.branchConditionExps,
-            relevantPathConditionStack.assumptions, Option.when(evaluator.withExp)(relevantPathConditionStack.assumptionExps))
+            relevantPathConditionStack.assumptions, Option.when(evaluator.debugOn)(relevantPathConditionStack.assumptionExps))
           // The postcondition must be produced with a fresh snapshot (different from `?s`) because
           // the postcondition's snapshot structure is most likely different than that of the
           // precondition
@@ -260,7 +261,7 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver
       val postconditionViolated = (offendingNode: ast.Exp) => PostconditionViolated(offendingNode, function)
 
       var recorders: Seq[FunctionRecorder] = Vector.empty
-      val wExp = evaluator.withExp
+      val wExp = evaluator.debugOn
 
       val result = phase1data.foldLeft(Success(): VerificationResult) {
         case (fatalResult: FatalResult, _) => fatalResult
@@ -276,8 +277,13 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver
                 Some(DebugExp.createInstance(e, eNew))
               } else { None }
               decider.assume(BuiltinEquals(data.formalResult, tBody), debugExp)
-              consumes(s2, posts, false, postconditionViolated, v)((s3, _, _) => {
-                recorders :+= s3.functionRecorder
+              val s3 = if (wExp) {
+                val initDebugHeap = DebugHeap(magicWandSupporter.getEvalHeap(s2), "nil", InhalePre(), None, Seq())
+                val s2a = s2.copy(debugOldHeaps = s2.debugOldHeaps + (Verifier.PRE_STATE_LABEL -> initDebugHeap))
+                s2a.copy(intermediateHeapCause = Some(Verifier.PRE_STATE_LABEL, ExhalePost(), decider.pcs.duplicate()))
+              } else s2
+              consumes(s3, posts, false, postconditionViolated, v)((s4, _, _) => {
+                recorders :+= s4.functionRecorder
                 Success()})})})}
 
       data.advancePhase(recorders)
diff --git a/src/main/scala/verifier/Verifier.scala b/src/main/scala/verifier/Verifier.scala
index d012082f7..835ec7870 100644
--- a/src/main/scala/verifier/Verifier.scala
+++ b/src/main/scala/verifier/Verifier.scala
@@ -7,14 +7,15 @@
 package viper.silicon.verifier
 
 import com.typesafe.scalalogging.Logger
-import viper.silicon.decider.Decider
+import viper.silicon.decider.{Decider, PathConditionStack}
 import viper.silicon.reporting.StateFormatter
-import viper.silicon.state.terms.{AxiomRewriter, TriggerGenerator}
-import viper.silicon.rules.{HeapSupportRules, StateConsolidationRules, defaultHeapSupporter}
-import viper.silicon.state.{Heap, IdentifierFactory, State, SymbolConverter}
+import viper.silicon.state.terms.{AxiomRewriter, Term, TriggerGenerator}
+import viper.silicon.rules.{HeapSupportRules, StateConsolidationRules, defaultHeapSupporter, magicWandSupporter}
+import viper.silicon.state.{DebugHeap, EvalExp, ExecStmt, Heap, HeapCause, IdentifierFactory, State, SymbolConverter}
 import viper.silicon.supporters.{QuantifierSupporter, SnapshotSupporter}
 import viper.silicon.utils.Counter
 import viper.silicon.Config
+import viper.silicon.interfaces.state.Chunk
 import viper.silicon.logger.MemberSymbExLogger
 import viper.silver.ast
 import viper.silver.reporter.Reporter
@@ -46,7 +47,7 @@ trait Verifier {
 
   val errorsReportedSoFar = new AtomicInteger(0);
 
-  var debugHeapCounter = new AtomicInteger(0);
+  private val debugHeapCounter = new AtomicInteger(0);
 
   def reportFurtherErrors(): Boolean = (Verifier.config.numberOfErrorsToReport() > errorsReportedSoFar.get()
     || Verifier.config.numberOfErrorsToReport() == 0);
@@ -59,23 +60,83 @@ trait Verifier {
     * @param h the heap to consider, if not the heap from state s
     * @return a pair containing the label of the given heap, and the label of the current expression in the given heap
     */
-  def getDebugOldLabel(s: State, pos: ast.Position, h: Option[Heap] = None): (String, String) = {
+  def getDebugOldLabel(s: State, pos: ast.Position, h: Option[Heap] = None): String = {
     val posString = pos match {
       case column: ast.HasLineColumn => s"l:${column.line}.${column.column}"
       case _ => s"l:unknown"
     }
+    val heapLabel = getDebugHeapLabel(s, h).getOrElse("unrecordedHeap")
+    s"$heapLabel#$posString"
+  }
+
+  def getDebugHeapLabel(s: State, h: Option[Heap] = None): Option[String] = {
     val heap = h match {
       case Some(heap) => heap
-      case None => s.h
+      case None => magicWandSupporter.getEvalHeap(s)
     }
-    val equalHeaps = s.oldHeaps.filter(h => h._1.startsWith("debug@") && h._2.equals(heap)).keys
-    if (equalHeaps.nonEmpty){
-      (equalHeaps.head, s"${equalHeaps.head}#$posString")
-    } else {
-      val counter = debugHeapCounter.getAndIncrement()
-      (s"debug@$counter", s"debug@$counter#$posString")
+
+    def equalChunks(h1: Heap, h2: Heap): Boolean = {
+      implicit def chunkOrd: Ordering[Chunk] = Ordering.by(_.toString)
+      h1.values.toList.sorted == h2.values.toList.sorted
+    }
+
+    val equalHeaps = s.debugOldHeaps.filter(dh => equalChunks(dh._2.heap, heap)).keys
+    equalHeaps.headOption
+  }
+
+  private def getOrMakeHeapLabel(s: State, h: Option[Heap] = None): String = {
+    getDebugHeapLabel(s, h) match {
+      case Some(label) => label
+      case None =>
+        val counter = debugHeapCounter.getAndIncrement()
+        s"debug@$counter"
+    }
+  }
+
+  def recordDebugHeap(s: State, parentLabel: String, cause: HeapCause): State = {
+    recordDebugHeap(s, magicWandSupporter.getEvalHeap(s), parentLabel, cause, None, None)
+  }
+
+  def recordDebugHeap(s: State, parentLabel: String, cause: HeapCause, oldPCS: PathConditionStack): State = {
+    recordDebugHeap(s, magicWandSupporter.getEvalHeap(s), parentLabel, cause, None, Some(oldPCS))
+  }
+
+  def recordDebugHeap(s: State, heap: Heap, parentLabel: String,
+                      cause: HeapCause,
+                      intermediateCause: Option[ast.Exp],
+                      oldPCS: Option[PathConditionStack]): State = {
+    val heapLabel = getOrMakeHeapLabel(s, Some(heap))
+    if (s.debugOldHeaps.contains(heapLabel))
+      s // Don't overwrite parents if we return to a heap
+    else {
+      val newBranchConds = oldPCS match {
+        case None => Seq()
+        case Some(pcs) =>
+          def zipConds(pcs2: PathConditionStack): Seq[(ast.Exp, Term)] =
+            pcs2.branchConditionExps.map(bc => bc._1).zip(pcs2.branchConditions)
+          val currentBranchConds = zipConds(decider.pcs)
+          val oldBranchConds = zipConds(pcs)
+          currentBranchConds.filterNot(oldBranchConds.contains(_))
+      }
+      val debugHeap = DebugHeap(heap, parentLabel, cause, intermediateCause, newBranchConds)
+      s.copy(debugOldHeaps = s.debugOldHeaps + (heapLabel -> debugHeap))
     }
   }
+
+  def recordIntermediateHeap(s: State): State = recordIntermediateHeap(s, None)
+
+  def recordIntermediateHeap(s: State, intermediateCause: ast.Exp): State =
+    recordIntermediateHeap(s, Some(intermediateCause))
+
+  // Expects intermediateHeapCause to be defined
+  def recordIntermediateHeap(s: State, intermediateCause: Option[ast.Exp]): State = {
+    assert(s.recordIntermediateHeaps, "recordIntermediateHeap requires s.intermediateHeapCause to be defined.")
+    val (parentLabel, originalCause, oldPCS) = s.intermediateHeapCause.get
+    val s2 = recordDebugHeap(s, magicWandSupporter.getEvalHeap(s), parentLabel,
+      originalCause, intermediateCause, Some(oldPCS))
+    val currentLabel = getOrMakeHeapLabel(s2)
+    s2.copy(intermediateHeapCause = Some(currentLabel, originalCause, decider.pcs.duplicate()))
+  }
 }
 
 object Verifier {