diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala
index 95934e2c5..e7ea13004 100644
--- a/src/main/scala/Config.scala
+++ b/src/main/scala/Config.scala
@@ -193,6 +193,13 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
+  val enableSimplifiedUnfolds: ScallopOption[Boolean] = opt[Boolean]("enableSimplifiedUnfolds",
+    descr = (  "Enable an optimization that reuses the results of verifying a predicate to simplify the process "
+             + "of unfolding it (via an unfold statement or an unfolding expression)."),
+    default = Some(false),
+    noshort = true
+  )
+
   val logLevel: ScallopOption[String] = opt[String]("logLevel",
     descr = "One of the log levels ALL, TRACE, DEBUG, INFO, WARN, ERROR, OFF",
     default = None,
diff --git a/src/main/scala/interfaces/Preamble.scala b/src/main/scala/interfaces/Preamble.scala
index 66a7ba7b9..8e3401770 100644
--- a/src/main/scala/interfaces/Preamble.scala
+++ b/src/main/scala/interfaces/Preamble.scala
@@ -29,10 +29,8 @@ trait PreambleContributor[+SO, +SY, +AX] extends StatefulComponent {
   def sortsAfterAnalysis: Iterable[SO]
   def declareSortsAfterAnalysis(sink: ProverLike): Unit
 
-  def symbolsAfterAnalysis: Iterable[SY]
   def declareSymbolsAfterAnalysis(sink: ProverLike): Unit
 
-  def axiomsAfterAnalysis: Iterable[AX]
   def emitAxiomsAfterAnalysis(sink: ProverLike): Unit
 }
 
diff --git a/src/main/scala/interfaces/state/Chunks.scala b/src/main/scala/interfaces/state/Chunks.scala
index bb1a2b9e2..9eb103064 100644
--- a/src/main/scala/interfaces/state/Chunks.scala
+++ b/src/main/scala/interfaces/state/Chunks.scala
@@ -6,12 +6,14 @@
 
 package viper.silicon.interfaces.state
 
+import viper.silicon
 import viper.silicon.resources.ResourceID
 import viper.silicon.state.terms.{Term, Var}
 import viper.silver.ast
 
-trait Chunk
-
+trait Chunk {
+  def substitute(terms: silicon.Map[Term, Term]): Chunk
+}
 trait ChunkIdentifer
 
 trait GeneralChunk extends Chunk {
@@ -22,6 +24,8 @@ trait GeneralChunk extends Chunk {
   def permMinus(perm: Term, permExp: Option[ast.Exp]): GeneralChunk
   def permPlus(perm: Term, permExp: Option[ast.Exp]): GeneralChunk
 
+  def permScale(perm: Term, permExp: Option[ast.Exp]): GeneralChunk
+
   val permExp: Option[ast.Exp]
 }
 
diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala
index d15f1b882..e09d1581e 100644
--- a/src/main/scala/rules/Consumer.scala
+++ b/src/main/scala/rules/Consumer.scala
@@ -383,7 +383,7 @@ object consumer extends ConsumptionRules {
               val debugExp = Option.when(withExp)(DebugExp.createInstance(s"Field Trigger: ${eRcvrNew.get.toString}.${field.name}"))
               v2.decider.assume(FieldTrigger(field.name, smDef1.sm, tRcvr), debugExp)
               //            v2.decider.assume(PermAtMost(tPerm, FullPerm()))
-              s2.copy(smCache = smCache1)
+              s2.copy(smCache = smCache1, functionRecorder = s2.functionRecorder.recordFvfAndDomain(smDef1))
             } else {
               s2
             }
@@ -427,7 +427,7 @@ object consumer extends ConsumptionRules {
                   s2, predicate, s2.predicateFormalVarMap(predicate), relevantChunks, v2)
               val debugExp = Option.when(withExp)(DebugExp.createInstance(s"PredicateTrigger(${predicate.name}(${eArgsNew.mkString(", ")}))", isInternal_ = true))
               v2.decider.assume(PredicateTrigger(predicate.name, smDef1.sm, tArgs), debugExp)
-              s2.copy(smCache = smCache1)
+              s2.copy(smCache = smCache1, functionRecorder = s2.functionRecorder.recordFvfAndDomain(smDef1))
             } else {
               s2
             }
@@ -497,7 +497,7 @@ object consumer extends ConsumptionRules {
             val predName = MagicWandIdentifier(wand, s.program).toString
             val debugExp = Option.when(withExp)(DebugExp.createInstance(s"PredicateTrigger($predName($argsString))", isInternal_ = true))
             v1.decider.assume(PredicateTrigger(predName, smDef1.sm, tArgs), debugExp)
-            s1.copy(smCache = smCache1)
+            s1.copy(smCache = smCache1, functionRecorder = s1.functionRecorder.recordFvfAndDomain(smDef1))
           } else {
             s1
           }
diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala
index be3f27ab4..0f80e0e93 100644
--- a/src/main/scala/rules/Evaluator.scala
+++ b/src/main/scala/rules/Evaluator.scala
@@ -6,6 +6,7 @@
 
 package viper.silicon.rules
 
+import viper.silicon
 import viper.silicon.debugger.DebugExp
 import viper.silicon.Config.JoinMode
 import viper.silver.ast
@@ -316,7 +317,7 @@ object evaluator extends EvaluationRules {
                     val smLookup = Lookup(fa.field.name, smDef1.sm, tRcvr)
                     val fr2 =
                       s2.functionRecorder.recordSnapshot(fa, v1.decider.pcs.branchConditions, smLookup)
-                        .recordFvfAndDomain(smDef1)
+                        .recordFvfAndDomain(smDef1).recordPermMap(pmDef1)
                     val s3 = s2.copy(functionRecorder = fr2)
                     Q(s3, smLookup, newFa, v1)
                 }
@@ -578,7 +579,8 @@ object evaluator extends EvaluationRules {
                       quantifiedChunkSupporter.summarisingPermissionMap(
                         s1, wand, formalVars, relevantChunks, null, v1)
 
-                    (s1.copy(pmCache = pmCache), pmDef)
+                    val newFr = s1.functionRecorder.recordPermMap(pmDef)
+                    (s1.copy(pmCache = pmCache, functionRecorder = newFr), pmDef)
                   }
                   (s2, PredicatePermLookup(identifier.toString, pmDef.pm, args))
 
@@ -594,8 +596,8 @@ object evaluator extends EvaluationRules {
                     val (pmDef, pmCache) =
                       quantifiedChunkSupporter.summarisingPermissionMap(
                         s1, field, Seq(`?r`), relevantChunks, null, v1)
-
-                    (s1.copy(pmCache = pmCache), pmDef)
+                    val newFr = s1.functionRecorder.recordPermMap(pmDef)
+                    (s1.copy(pmCache = pmCache, functionRecorder = newFr), pmDef)
                   }
                   val currentPermAmount = PermLookup(field.name, pmDef.pm, args.head)
                   v1.decider.prover.comment(s"perm($resacc)  ~~>  assume upper permission bound")
@@ -1029,16 +1031,33 @@ object evaluator extends EvaluationRules {
                       val argsPairs: List[(Term, Option[ast.Exp])] = if (withExp) 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)
-                      produce(s7a, toSf(snap.get), body, pve, v4)((s8, v5) => {
-                        val s9 = s8.copy(g = s7.g,
-                                         functionRecorder = s8.functionRecorder.changeDepthBy(-1),
-                                         recordVisited = s3.recordVisited,
-                                         permissionScalingFactor = s6.permissionScalingFactor,
-                                         permissionScalingFactorExp = s6.permissionScalingFactorExp,
-                                         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))})})
+
+                      if (s7a.predicateData(predicate).predContents.isDefined) {
+                        val toReplace: silicon.Map[Term, Term] = silicon.Map.from(s7a.predicateData(predicate).params.get.zip(Seq(snap.get) ++ tArgs))
+                        predicateSupporter.producePredicateContents(s7a, s7a.predicateData(predicate).predContents.get, toReplace, v4, true)((s8, v5) => {
+                          val s9 = s8.copy(g = s7.g,
+                            functionRecorder = s8.functionRecorder.changeDepthBy(-1),
+                            recordVisited = s3.recordVisited,
+                            permissionScalingFactor = s6.permissionScalingFactor,
+                            permissionScalingFactorExp = s6.permissionScalingFactorExp,
+                            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))
+                        })
+                      } else {
+                        produce(s7a, toSf(snap.get), body, pve, v4)((s8, v5) => {
+                          val s9 = s8.copy(g = s7.g,
+                                           functionRecorder = s8.functionRecorder.changeDepthBy(-1),
+                                           recordVisited = s3.recordVisited,
+                                           permissionScalingFactor = s6.permissionScalingFactor,
+                                           permissionScalingFactorExp = s6.permissionScalingFactorExp,
+                                           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))})
+                      }
+                    })
                   })(join(eIn.typ, "joined_unfolding", s2.relevantQuantifiedVariables.map(_._1),
                     Option.when(withExp)(s2.relevantQuantifiedVariables.map(_._2.get)), v2))((s12, r12, v7)
                     => {
@@ -1049,7 +1068,8 @@ object evaluator extends EvaluationRules {
                   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))
-          Q(s, unknownValue, Option.when(withExp)(ast.LocalVarWithVersion("unknownValue", eIn.typ)(eIn.pos, eIn.info, eIn.errT)), v)
+          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)
         }
 
       case ast.Applying(wand, eIn) =>
diff --git a/src/main/scala/rules/PredicateSupporter.scala b/src/main/scala/rules/PredicateSupporter.scala
index 7a0f814c1..09ce9d112 100644
--- a/src/main/scala/rules/PredicateSupporter.scala
+++ b/src/main/scala/rules/PredicateSupporter.scala
@@ -6,12 +6,17 @@
 
 package viper.silicon.rules
 
+import viper.silicon
+import viper.silicon.Config.JoinMode
 import viper.silicon.debugger.DebugExp
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
 import viper.silicon.interfaces.VerificationResult
-import viper.silicon.resources.PredicateID
+import viper.silicon.interfaces.state.{ChunkIdentifer, GeneralChunk, NonQuantifiedChunk}
+import viper.silicon.resources.{FieldID, PredicateID}
 import viper.silicon.state._
 import viper.silicon.state.terms._
+import viper.silicon.state.terms.predef.`?r`
+import viper.silicon.supporters.{PredicateBranchNode, PredicateLeafNode, PredicateContentsTree}
 import viper.silicon.utils.toSf
 import viper.silicon.verifier.Verifier
 import viper.silver.ast
@@ -124,6 +129,89 @@ object predicateSupporter extends PredicateSupportRules {
     })
   }
 
+  def producePredicateContents(s: State, tree: PredicateContentsTree, toReplace: silicon.Map[Term, Term], v: Verifier, isUnfolding: Boolean = false)
+                              (Q: (State, Verifier) => VerificationResult)
+            : VerificationResult = {
+    tree match {
+      case PredicateLeafNode(h, assumptions) =>
+        val debugExp = Option.when(withExp)(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))
+
+        val quantifiedResourceIdentifiers: Set[ChunkIdentifer] = s.qpPredicates.map(p => BasicChunkIdentifier(p.name)) ++ s.qpFields.map(f => BasicChunkIdentifier(f.name)) ++ s.qpMagicWands
+
+        var newFr = s.functionRecorder
+        val substChunksOptQps = substChunks.map(c => {
+          if (quantifiedResourceIdentifiers.contains(c.id) && c.isInstanceOf[NonQuantifiedChunk]) {
+            c match {
+              case bc: BasicChunk =>
+                val resource = bc.resourceID match {
+                  case FieldID => s.program.findField(bc.id.name)
+                  case _ => s.program.findPredicate(bc.id.name)
+                }
+                val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s, resource, bc.args, bc.snap, v)
+                v.decider.assumeDefinition(smValueDef, None)
+                val codQvars = bc.resourceID match {
+                  case FieldID => Seq(`?r`)
+                  case _ => s.predicateFormalVarMap(resource.asInstanceOf[ast.Predicate])
+                }
+                newFr = newFr.recordFvfAndDomain(SnapshotMapDefinition(resource, sm, Seq(smValueDef), Seq()))
+                quantifiedChunkSupporter.createSingletonQuantifiedChunk(codQvars, None, resource, bc.args, None, bc.perm, None, sm, s.program)
+              case mwc: MagicWandChunk =>
+                val wand = mwc.id.ghostFreeWand
+                val bodyVars = wand.subexpressionsToEvaluate(s.program)
+                val codQvars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ), false))
+                val (sm, smValueDef) = quantifiedChunkSupporter.singletonSnapshotMap(s, wand, mwc.args, mwc.snap, v)
+                v.decider.assumeDefinition(smValueDef, None)
+                newFr = newFr.recordFvfAndDomain(SnapshotMapDefinition(wand, sm, Seq(smValueDef), Seq()))
+                quantifiedChunkSupporter.createSingletonQuantifiedChunk(codQvars, None, wand, mwc.args, None, mwc.perm, None, sm, s.program)
+            }
+          } else {
+            c
+          }
+        })
+        val substHeap = Heap(substChunksOptQps)
+        val (fr1, h1) = v.stateConsolidator(s).merge(newFr, s, s.h, substHeap, v)
+        val s1 = s.copy(h = h1, functionRecorder = fr1)
+
+        Q(s1, v)
+      case PredicateBranchNode(cond, condExp, left, right) =>
+        val substCond = cond.replace(toReplace)
+
+        if (!isUnfolding && s.moreJoins.id >= JoinMode.Impure.id) {
+          joiner.join[scala.Null, scala.Null](s, v, resetState = false)((s1, v1, QB) => {
+            brancher.branch(s1, substCond, condExp, v1)(
+              (s2, v2) => {
+                producePredicateContents(s2, left, toReplace, v2, isUnfolding)((s3, v3) => QB(s3, null, v3))
+              },
+              (s2, v2) => {
+                producePredicateContents(s2, right, toReplace, v2, isUnfolding)((s3, v3) => QB(s3, null, v3))
+              }
+            )
+          }) (entries => {
+            val s2 = entries match {
+              case Seq(entry) => // One branch is dead
+                entry.s
+              case Seq(entry1, entry2) => // Both branches are alive
+                entry1.pathConditionAwareMergeWithoutConsolidation(entry2, v)
+              case _ =>
+                sys.error(s"Unexpected join data entries: $entries")
+            }
+            (s2, null)
+          }) ((sp, _, vp) => Q(sp, vp))
+        } else {
+          brancher.branch(s, substCond, condExp, v)(
+            (s1, v1) => {
+              producePredicateContents(s1, left, toReplace, v1, isUnfolding)(Q)
+            },
+            (s2, v2) => {
+              producePredicateContents(s2, right, toReplace, v2, isUnfolding)(Q)
+            }
+          )
+        }
+    }
+  }
+
   def unfold(s: State,
              predicate: ast.Predicate,
              tArgs: List[Term],
@@ -163,19 +251,39 @@ object predicateSupporter extends PredicateSupportRules {
       )((s2, h2, snap, v1) => {
         val s3 = s2.copy(g = gIns, h = h2)
                    .setConstrainable(constrainableWildcards, false)
-        produce(s3, toSf(snap.get), body, pve, v1)((s4, v2) => {
-          v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterUnfold)
-          if (!Verifier.config.disableFunctionUnfoldTrigger()) {
-            val predicateTrigger =
-              App(s4.predicateData(predicate).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))")))
-          }
-          Q(s4.copy(g = s.g,
-                    permissionScalingFactor = s.permissionScalingFactor,
-                    permissionScalingFactorExp = s.permissionScalingFactorExp),
-            v2)})
+        if (s3.predicateData(predicate).predContents.isDefined) {
+          val toReplace: silicon.Map[Term, Term] = silicon.Map.from(s3.predicateData(predicate).params.get.zip(Seq(snap.get) ++ tArgs))
+          producePredicateContents(s3, s3.predicateData(predicate).predContents.get, toReplace, v1, false)((s4, v4) => {
+            v4.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterUnfold)
+            if (!Verifier.config.disableFunctionUnfoldTrigger()) {
+              val predicateTrigger =
+                App(s4.predicateData(predicate).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))")))
+            }
+            Q(s4.copy(g = s.g,
+              permissionScalingFactor = s.permissionScalingFactor,
+              permissionScalingFactorExp = s.permissionScalingFactorExp),
+              v4)
+          })
+        } else {
+          produce(s3, toSf(snap.get), body, pve, v1)((s4, v2) => {
+            v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterUnfold)
+            if (!Verifier.config.disableFunctionUnfoldTrigger()) {
+              val predicateTrigger =
+                App(s4.predicateData(predicate).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))")))
+            }
+            Q(s4.copy(g = s.g,
+              permissionScalingFactor = s.permissionScalingFactor,
+              permissionScalingFactorExp = s.permissionScalingFactorExp),
+              v2)
+          })
+        }
+
       })
     } else {
       val ve = pve dueTo InsufficientPermission(pa)
@@ -183,31 +291,35 @@ object predicateSupporter extends PredicateSupportRules {
       chunkSupporter.consume(s1, s1.h, predicate, tArgs, eArgs, s1.permissionScalingFactor, s1.permissionScalingFactorExp, true, ve, v, description)((s2, h1, snap, v1) => {
         val s3 = s2.copy(g = gIns, h = h1)
                    .setConstrainable(constrainableWildcards, false)
-        produce(s3, toSf(snap.get), body, pve, v1)((s4, v2) => {
-          v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterUnfold)
-          if (!Verifier.config.disableFunctionUnfoldTrigger()) {
-            val predicateTrigger =
-              App(s4.predicateData(predicate).triggerFunction, snap.get +: tArgs)
-            val eargs = eArgs.mkString(", ")
-            v2.decider.assume(predicateTrigger, Option.when(withExp)(DebugExp.createInstance(s"PredicateTrigger(${pa.predicateName}($eargs))")))
-          }
-          val s5 = s4.copy(g = s.g,
-                           permissionScalingFactor = s.permissionScalingFactor,
-                           permissionScalingFactorExp = s.permissionScalingFactorExp)
-          Q(s5, v2)})})
+        if (s3.predicateData(predicate).predContents.isDefined) {
+          val toReplace: silicon.Map[Term, Term] = silicon.Map.from(s3.predicateData(predicate).params.get.zip(Seq(snap.get) ++ tArgs))
+          producePredicateContents(s3, s3.predicateData(predicate).predContents.get, toReplace, v1, false)((s4, v4) => {
+            v4.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterUnfold)
+            if (!Verifier.config.disableFunctionUnfoldTrigger()) {
+              val predicateTrigger =
+                App(s4.predicateData(predicate).triggerFunction, snap.get +: tArgs)
+              val eargs = eArgs.mkString(", ")
+              v4.decider.assume(predicateTrigger, Option.when(withExp)(DebugExp.createInstance(s"PredicateTrigger(${pa.predicateName}($eargs))")))
+            }
+            val s5 = s4.copy(g = s.g,
+              permissionScalingFactor = s.permissionScalingFactor,
+              permissionScalingFactorExp = s.permissionScalingFactorExp)
+            Q(s5, v4)
+          })
+        } else {
+          produce(s3, toSf(snap.get), body, pve, v1)((s4, v2) => {
+            v2.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterUnfold)
+            if (!Verifier.config.disableFunctionUnfoldTrigger()) {
+              val predicateTrigger =
+                App(s4.predicateData(predicate).triggerFunction, snap.get +: tArgs)
+              val eargs = eArgs.mkString(", ")
+              v2.decider.assume(predicateTrigger, Option.when(withExp)(DebugExp.createInstance(s"PredicateTrigger(${pa.predicateName}($eargs))")))
+            }
+            val s5 = s4.copy(g = s.g,
+                             permissionScalingFactor = s.permissionScalingFactor,
+                             permissionScalingFactorExp = s.permissionScalingFactorExp)
+            Q(s5, v2)})}
+      })
     }
   }
-
-/* NOTE: Possible alternative to storing the permission scaling factor in the context
- *       or passing it to produce/consume as an explicit argument.
- *       Carbon uses Permissions.multiplyExpByPerm as well (but does not extend the
- *       store).
- */
-//    private def scale(γ: ST, body: ast.Exp, perm: Term) = {
-//      /* TODO: Ensure that variable name does not clash with any Silver identifier already in use */
-//      val scaleFactorVar = ast.LocalVar(identifierFactory.fresh("p'unf").name)(ast.Perm)
-//      val scaledBody = ast.utility.Permissions.multiplyExpByPerm(body, scaleFactorVar)
-//
-//      (γ + (scaleFactorVar -> perm), scaledBody)
-//    }
 }
diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala
index 2932f0598..e9a200903 100644
--- a/src/main/scala/rules/QuantifiedChunkSupport.scala
+++ b/src/main/scala/rules/QuantifiedChunkSupport.scala
@@ -6,6 +6,7 @@
 
 package viper.silicon.rules
 
+import viper.silicon
 import viper.silicon.debugger.DebugExp
 import viper.silicon.Map
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
@@ -35,7 +36,7 @@ import scala.reflect.ClassTag
 case class InverseFunctions(condition: Term,
                             invertibles: Seq[Term],
                             invertibleExps: Option[Seq[ast.Exp]],
-                            additionalArguments: Vector[Var],
+                            additionalArguments: Vector[Term],
                             axiomInversesOfInvertibles: Quantification,
                             axiomInvertiblesOfInverses: Quantification,
                             qvarExps: Option[Seq[ast.LocalVarDecl]],
@@ -79,6 +80,14 @@ case class InverseFunctions(condition: Term,
          |$linePrefix  axiomInvertiblesOfInverses
          |$linePrefix    ${axiomInvertiblesOfInverses.stringRepresentationWithTriggers}
        """.stripMargin
+
+  def substitute(terms: silicon.Map[Term, Term]) = copy(
+    condition = condition.replace(terms),
+    invertibles = invertibles.map(_.replace(terms)),
+    additionalArguments = additionalArguments.map(_.replace(terms)),
+    axiomInversesOfInvertibles = axiomInversesOfInvertibles.replace(terms).asInstanceOf[Quantification],
+    axiomInvertiblesOfInverses = axiomInvertiblesOfInverses.replace(terms).asInstanceOf[Quantification]
+  )
 }
 
 case class SnapshotMapDefinition(resource: ast.Resource,
@@ -637,12 +646,12 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
   }
 
   def summarisingPermissionMap(s: State,
-                             resource: ast.Resource,
-                             formalQVars: Seq[Var],
-                             relevantChunks: Seq[QuantifiedBasicChunk],
-                             smDef: SnapshotMapDefinition,
-                             v: Verifier)
-                            : (PermMapDefinition, PmCache) = {
+                               resource: ast.Resource,
+                               formalQVars: Seq[Var],
+                               relevantChunks: Seq[QuantifiedBasicChunk],
+                               smDef: SnapshotMapDefinition,
+                               v: Verifier)
+                              : (PermMapDefinition, PmCache) = {
 
     Verifier.config.mapCache(s.pmCache.get(resource, relevantChunks)) match {
       case Some(pmDef) =>
@@ -774,7 +783,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       quantifiedChunkSupporter.summarisingPermissionMap(
         s1, resource, codomainQVars, relevantChunks, smDef, v)
 
-    val s2 = s1.copy(pmCache = pmCache)
+    val s2 = s1.copy(pmCache = pmCache, functionRecorder = s1.functionRecorder.recordFvfAndDomain(smDef).recordPermMap(pmDef))
 
     (s2, smDef, pmDef)
   }
@@ -980,7 +989,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
               case wand: ast.MagicWand => MagicWandIdentifier(wand, s.program)
               case r => r
             }
-            val smCache1 = if (s.heapDependentTriggers.contains(resourceIdentifier)){
+            val (smCache1, fr2) = if (s.heapDependentTriggers.contains(resourceIdentifier)){
               // TODO: Why not formalQVars? Used as codomainVars, see above.
               val codomainVars =
                 resource match {
@@ -1001,13 +1010,14 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
               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)))
-              smCache1
+              val newFuncRec = fr1.recordFvfAndDomain(smDef1)
+              (smCache1, newFuncRec)
             } else {
-              s.smCache
+              (s.smCache, fr1)
             }
             val s1 =
               s.copy(h = h1,
-                     functionRecorder = fr1.recordFieldInv(inv),
+                     functionRecorder = fr2.recordFieldInv(inv),
                      conservedPcs = conservedPcs,
                      smCache = smCache1)
             Q(s1, v)
@@ -1325,8 +1335,12 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
                       else None
                     val (smDef2, smCache2) = quantifiedChunkSupporter.summarisingSnapshotMap(
                       s2, resource, formalQVars, relevantChunks, v, optSmDomainDefinitionCondition2)
-                    val fr3 = s2.functionRecorder.recordFvfAndDomain(smDef2)
+                    var fr3 = s2.functionRecorder.recordFvfAndDomain(smDef2)
                       .recordFieldInv(inverseFunctions)
+                    fr3 = smDef1 match {
+                      case None => fr3
+                      case Some(smDef) => fr3.recordFvfAndDomain(smDef)
+                    }
                     val s3 = s2.copy(functionRecorder = fr3,
                       partiallyConsumedHeap = Some(h3),
                       constrainableARPs = s.constrainableARPs,
@@ -1959,11 +1973,15 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
   override def findChunk(chunks: Iterable[Chunk], chunk: QuantifiedChunk, v: Verifier): Option[QuantifiedChunk] = {
     val lr = chunk match {
       case qfc: QuantifiedFieldChunk if qfc.invs.isDefined =>
-        Left(qfc.invs.get.invertibles, qfc.quantifiedVars, qfc.condition)
+        val qvarsAndInverses = qfc.invs.get.qvarsToInverses.map(qvi => (qvi._1, App(qvi._2, qfc.invs.get.additionalArguments.toSeq ++ qfc.quantifiedVars)))
+        val invertiblesReplaced = qfc.invs.get.invertibles.map(_.replace(qvarsAndInverses))
+        Left(invertiblesReplaced, qfc.quantifiedVars, qfc.condition)
       case qfc: QuantifiedFieldChunk if qfc.singletonArguments.isDefined =>
         Right(qfc.singletonArguments.get, qfc.condition)
       case qpc: QuantifiedPredicateChunk if qpc.invs.isDefined =>
-        Left(qpc.invs.get.invertibles, qpc.quantifiedVars, qpc.condition)
+        val qvarsAndInverses = qpc.invs.get.qvarsToInverses.map(qvi => (qvi._1, App(qvi._2, qpc.invs.get.additionalArguments.toSeq ++ qpc.quantifiedVars)))
+        val invertiblesReplaced = qpc.invs.get.invertibles.map(_.replace(qvarsAndInverses))
+        Left(invertiblesReplaced, qpc.quantifiedVars, qpc.condition)
       case qpc: QuantifiedPredicateChunk if qpc.singletonArguments.isDefined =>
         Right(qpc.singletonArguments.get, qpc.condition)
       case _ => return None
@@ -2007,9 +2025,13 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
     relevantChunks.find { ch =>
       val chunkInfo = ch match {
         case qfc: QuantifiedFieldChunk if qfc.invs.isDefined =>
-          Some(qfc.invs.get.invertibles, qfc.quantifiedVars, qfc.condition)
+          val qvarsAndInverses = qfc.invs.get.qvarsToInverses.map(qvi => (qvi._1, App(qvi._2, qfc.invs.get.additionalArguments.toSeq ++ qfc.quantifiedVars)))
+          val invertiblesReplaced = qfc.invs.get.invertibles.map(_.replace(qvarsAndInverses))
+          Some(invertiblesReplaced, qfc.quantifiedVars, qfc.condition)
         case qpc: QuantifiedPredicateChunk if qpc.invs.isDefined =>
-          Some(qpc.invs.get.invertibles, qpc.quantifiedVars, qpc.condition)
+          val qvarsAndInverses = qpc.invs.get.qvarsToInverses.map(qvi => (qvi._1, App(qvi._2, qpc.invs.get.additionalArguments.toSeq ++ qpc.quantifiedVars)))
+          val invertiblesReplaced = qpc.invs.get.invertibles.map(_.replace(qvarsAndInverses))
+          Some(invertiblesReplaced, qpc.quantifiedVars, qpc.condition)
         case _ => None
       }
       chunkInfo match {
diff --git a/src/main/scala/state/Chunks.scala b/src/main/scala/state/Chunks.scala
index 638be4288..a4942f237 100644
--- a/src/main/scala/state/Chunks.scala
+++ b/src/main/scala/state/Chunks.scala
@@ -6,6 +6,7 @@
 
 package viper.silicon.state
 
+import viper.silicon
 import viper.silver.ast
 import viper.silicon.interfaces.state._
 import viper.silicon.resources._
@@ -50,6 +51,9 @@ case class BasicChunk(resourceID: BaseID,
     withPerm(PermMinus(perm, newPerm), newPermExp.map(npe => ast.PermSub(permExp.get, npe)()))
   override def permPlus(newPerm: Term, newPermExp: Option[ast.Exp]) =
     withPerm(PermPlus(perm, newPerm), newPermExp.map(npe => ast.PermAdd(permExp.get, npe)()))
+
+  override def permScale(newPerm: Term, newPermExp: Option[ast.Exp]) =
+    withPerm(PermTimes(perm, newPerm), permExp.map(pe => ast.PermMul(pe, newPermExp.get)()))
   override def withPerm(newPerm: Term, newPermExp: Option[ast.Exp]) = BasicChunk(resourceID, id, args, argsExp, snap, snapExp, newPerm, newPermExp)
   override def withSnap(newSnap: Term, newSnapExp: Option[ast.Exp]) = BasicChunk(resourceID, id, args, argsExp, newSnap, newSnapExp, perm, permExp)
 
@@ -57,6 +61,10 @@ case class BasicChunk(resourceID: BaseID,
     case FieldID => s"${args.head}.$id -> $snap # $perm"
     case PredicateID => s"$id($snap; ${args.mkString(",")}) # $perm"
   }
+
+  override def substitute(terms: silicon.Map[Term, Term]) = {
+    copy(args = args.map(_.replace(terms)), snap = snap.replace(terms), perm = perm.replace(terms))
+  }
 }
 
 sealed trait QuantifiedBasicChunk extends QuantifiedChunk {
@@ -118,10 +126,17 @@ case class QuantifiedFieldChunk(id: BasicChunkIdentifier,
     withPerm(PermMinus(permValue, newPerm), newPermExp.map(npe => ast.PermSub(permValueExp.get, npe)()))
   override def permPlus(newPerm: Term, newPermExp: Option[ast.Exp]) =
     withPerm(PermPlus(permValue, newPerm), newPermExp.map(npe => ast.PermAdd(permValueExp.get, npe)()))
+
+  override def permScale(newPerm: Term, newPermExp: Option[ast.Exp]) =
+    withPerm(PermTimes(perm, newPerm), permExp.map(pe => ast.PermMul(pe, newPermExp.get)()))
   override def withSnapshotMap(newFvf: Term) =
     QuantifiedFieldChunk(id, newFvf, condition, conditionExp, permValue, permValueExp, invs, singletonRcvr, singletonRcvrExp, hints)
 
   override lazy val toString = s"${terms.Forall} ${`?r`} :: ${`?r`}.$id -> $fvf # $perm"
+
+  override def substitute(terms: silicon.Map[Term, Term]): Chunk =
+    copy(fvf = fvf.replace(terms), condition = condition.replace(terms), permValue = permValue.replace(terms),
+      singletonRcvr = singletonRcvr.map(_.replace(terms)), hints = hints.map(_.replace(terms)), invs = invs.map(_.substitute(terms)))
 }
 
 case class QuantifiedPredicateChunk(id: BasicChunkIdentifier,
@@ -159,10 +174,17 @@ case class QuantifiedPredicateChunk(id: BasicChunkIdentifier,
     withPerm(PermMinus(permValue, newPerm), newPermExp.map(npe => ast.PermSub(permValueExp.get, npe)()))
   override def permPlus(newPerm: Term, newPermExp: Option[ast.Exp]) =
     withPerm(PermPlus(permValue, newPerm), newPermExp.map(npe => ast.PermAdd(permValueExp.get, npe)()))
+
+  override def permScale(newPerm: Term, newPermExp: Option[ast.Exp]) =
+    withPerm(PermTimes(perm, newPerm), permExp.map(pe => ast.PermMul(pe, newPermExp.get)()))
   override def withSnapshotMap(newPsf: Term) =
     QuantifiedPredicateChunk(id, quantifiedVars, quantifiedVarExps, newPsf, condition, conditionExp, permValue, permValueExp, invs, singletonArgs, singletonArgExps, hints)
 
   override lazy val toString = s"${terms.Forall} ${quantifiedVars.mkString(",")} :: $id(${quantifiedVars.mkString(",")}) -> $psf # $perm"
+
+  override def substitute(terms: silicon.Map[Term, Term]): Chunk =
+    copy(psf = psf.replace(terms), condition = condition.replace(terms), permValue = permValue.replace(terms),
+      singletonArgs = singletonArgs.map(_.map(_.replace(terms))), hints = hints.map(_.replace(terms)), invs = invs.map(_.substitute(terms)))
 }
 
 case class QuantifiedMagicWandChunk(id: MagicWandIdentifier,
@@ -194,12 +216,19 @@ case class QuantifiedMagicWandChunk(id: MagicWandIdentifier,
     withPerm(PermMinus(perm, newPerm), newPermExp.map(npe => ast.PermSub(permExp.get, npe)()))
   override def permPlus(newPerm: Term, newPermExp: Option[ast.Exp]) =
     withPerm(PermPlus(perm, newPerm), newPermExp.map(npe => ast.PermAdd(permExp.get, npe)()))
+
+  override def permScale(newPerm: Term, newPermExp: Option[ast.Exp]) =
+    withPerm(PermTimes(perm, newPerm), permExp.map(pe => ast.PermMul(pe, newPermExp.get)()))
   def withPerm(newPerm: Term, newPermExp: Option[ast.Exp]) =
     QuantifiedMagicWandChunk(id, quantifiedVars, quantifiedVarExps, wsf, newPerm, newPermExp, invs, singletonArgs, singletonArgExps, hints)
   override def withSnapshotMap(newWsf: Term) =
     QuantifiedMagicWandChunk(id, quantifiedVars, quantifiedVarExps, newWsf, perm, permExp, invs, singletonArgs, singletonArgExps, hints)
 
   override lazy val toString = s"${terms.Forall} ${quantifiedVars.mkString(",")} :: $id(${quantifiedVars.mkString(",")}) -> $wsf # $perm"
+
+  override def substitute(terms: silicon.Map[Term, Term]): Chunk =
+    copy(wsf = wsf.replace(terms), perm = perm.replace(terms), singletonArgs = singletonArgs.map(_.map(_.replace(terms))),
+      hints = hints.map(_.replace(terms)), invs = invs.map(_.substitute(terms)))
 }
 
 case class MagicWandIdentifier(ghostFreeWand: ast.MagicWand)(override val hashCode: Int) extends ChunkIdentifer {
@@ -238,6 +267,9 @@ case class MagicWandChunk(id: MagicWandIdentifier,
     withPerm(PermMinus(perm, newPerm), newPermExp.map(npe => ast.PermSub(permExp.get, npe)()))
   override def permPlus(newPerm: Term, newPermExp: Option[ast.Exp]) =
     withPerm(PermPlus(perm, newPerm), newPermExp.map(npe => ast.PermAdd(permExp.get, npe)()))
+
+  override def permScale(newPerm: Term, newPermExp: Option[ast.Exp]) =
+    withPerm(PermTimes(perm, newPerm), permExp.map(pe => ast.PermMul(pe, newPermExp.get)()))
   override def withPerm(newPerm: Term, newPermExp: Option[ast.Exp]) = MagicWandChunk(id, bindings, args, argsExp, snap, newPerm, newPermExp)
 
   override def withSnap(newSnap: Term, newSnapExp: Option[ast.Exp]) = {
@@ -255,4 +287,8 @@ case class MagicWandChunk(id: MagicWandIdentifier,
     }
     s"wand@$pos[$snap; ${args.mkString(", ")}]"
   }
+
+  override def substitute(terms: silicon.Map[Term, Term]) = {
+    copy(args = args.map(_.replace(terms)), snap = snap.replace(terms).asInstanceOf[MagicWandSnapshot], perm = perm.replace(terms))
+  }
 }
diff --git a/src/main/scala/state/State.scala b/src/main/scala/state/State.scala
index 3256ff451..e6632523f 100644
--- a/src/main/scala/state/State.scala
+++ b/src/main/scala/state/State.scala
@@ -130,7 +130,7 @@ final case class State(g: Store = Store(),
     State.preserveAfterLocalEvaluation(this, post)
 
   def functionRecorderQuantifiedVariables(): Seq[(Var, Option[ast.AbstractLocalVar])] =
-    functionRecorder.data.fold(Seq.empty[(Var, Option[ast.AbstractLocalVar])])(d => d.arguments.zip(d.argumentExps))
+    functionRecorder.arguments.fold(Seq.empty[(Var, Option[ast.AbstractLocalVar])])(d => d)
 
   def relevantQuantifiedVariables(filterPredicate: Var => Boolean): Seq[(Var, Option[ast.AbstractLocalVar])] = (
        functionRecorderQuantifiedVariables()
diff --git a/src/main/scala/state/Utils.scala b/src/main/scala/state/Utils.scala
index d624db648..eaf7b3ff7 100644
--- a/src/main/scala/state/Utils.scala
+++ b/src/main/scala/state/Utils.scala
@@ -148,7 +148,7 @@ package object utils {
     def goTriggers(trigger: Trigger) = Trigger(trigger.p map go)
 
     def recurse(term: Term): Term = term match {
-      case _: Var | _: Function | _: Literal | _: MagicWandChunkTerm | _: Distinct => term
+      case _: Var | _: Function | _: Literal | _: MagicWandChunkTerm | _: Distinct | _: AppHint => term
 
       case Quantification(quantifier, variables, body, triggers, name, isGlobal, weight) =>
         Quantification(quantifier, variables map go, go(body), triggers map goTriggers, name, isGlobal, weight)
diff --git a/src/main/scala/supporters/MagicWandSnapFunctionsContributor.scala b/src/main/scala/supporters/MagicWandSnapFunctionsContributor.scala
index c2b925c6a..df2f79037 100644
--- a/src/main/scala/supporters/MagicWandSnapFunctionsContributor.scala
+++ b/src/main/scala/supporters/MagicWandSnapFunctionsContributor.scala
@@ -54,17 +54,10 @@ class MagicWandSnapFunctionsContributor(preambleReader: PreambleReader[String, S
     sortsAfterAnalysis foreach (s => sink.declare(SortDecl(s)))
   }
 
-  /** Symbols to add to the preamble of the SMT proof script. */
-  override def symbolsAfterAnalysis: Iterable[String] =
-    extractPreambleLines(collectedFunctionDecls)
-
   /** Add all symbols needed to the preamble using `sink`. */
   override def declareSymbolsAfterAnalysis(sink: ProverLike): Unit =
     emitPreambleLines(sink, collectedFunctionDecls)
 
-  /** Axioms to add to the preamble of the SMT proof script. Currently, there are none. */
-  override def axiomsAfterAnalysis: Iterable[String] = Seq.empty
-
   /** Add all axioms needed to the preamble using `sink`. Currently, there are none. */
   override def emitAxiomsAfterAnalysis(sink: ProverLike): Unit = {}
 
diff --git a/src/main/scala/supporters/PredicateVerificationUnit.scala b/src/main/scala/supporters/PredicateVerificationUnit.scala
index 388c54709..4252cba14 100644
--- a/src/main/scala/supporters/PredicateVerificationUnit.scala
+++ b/src/main/scala/supporters/PredicateVerificationUnit.scala
@@ -7,6 +7,8 @@
 package viper.silicon.supporters
 
 import com.typesafe.scalalogging.Logger
+import viper.silicon.common.collections.immutable.InsertionOrderedSet
+import viper.silicon.debugger.DebugExp
 import viper.silver.ast
 import viper.silver.ast.Program
 import viper.silver.components.StatefulComponent
@@ -19,24 +21,35 @@ import viper.silicon.state.State.OldHeaps
 import viper.silicon.state.terms._
 import viper.silicon.interfaces._
 import viper.silicon.rules.executionFlowController
+import viper.silicon.supporters.functions.{ActualFunctionRecorder, FunctionRecorder, FunctionRecorderHandler, NoopFunctionRecorder}
 import viper.silicon.verifier.{Verifier, VerifierComponent}
-import viper.silicon.utils.freshSnap
+import viper.silicon.utils.{freshSnap, toSf}
 
 class PredicateData(predicate: ast.Predicate)
                    /* Note: Holding a reference to a fixed symbol converter (instead of going
                     *       through a verifier) is only safe if the converter is effectively
                     *       independent of the verifiers.
                     */
-                   (private val symbolConvert: SymbolConverter) {
+                   (private val symbolConvert: SymbolConverter) extends FunctionRecorderHandler {
+
+  var predContents: Option[PredicateContentsTree] = None
+  var params: Option[Seq[Var]] = None
 
   val argumentSorts = predicate.formalArgs map (fm => symbolConvert.toSort(fm.typ))
 
   val triggerFunction =
     Fun(Identifier(s"${predicate.name}%trigger"), sorts.Snap +: argumentSorts, sorts.Bool)
+
 }
 
+trait PredicateContentsTree
+
+case class PredicateBranchNode(cond: Term, condExp: (ast.Exp, Option[ast.Exp]), left: PredicateContentsTree, right: PredicateContentsTree) extends PredicateContentsTree
+
+case class PredicateLeafNode(heap: Heap, assumptions: InsertionOrderedSet[Term]) extends PredicateContentsTree
+
 trait PredicateVerificationUnit
-    extends VerifyingPreambleContributor[Sort, Fun, Term, ast.Predicate] {
+    extends VerifyingPreambleContributor[Sort, Decl, Term, ast.Predicate] {
 
   def data: Map[ast.Predicate, PredicateData]
 }
@@ -87,11 +100,24 @@ trait DefaultPredicateVerificationUnitProvider extends VerifierComponent { v: Ve
       openSymbExLogger(predicate)
 
       val ins = predicate.formalArgs.map(_.localVar)
-      val s = sInit.copy(g = Store(ins.map(x => (x, decider.fresh(x)))),
+      val snap = freshSnap(sorts.Snap, v)
+      val argVars = ins.map(x => (x, decider.fresh(x)))
+      var funcRecorder: FunctionRecorder = if (!Verifier.config.enableSimplifiedUnfolds()) {
+        NoopFunctionRecorder
+      } else {
+        ActualFunctionRecorder(Right((predicate, Seq(snap) ++ argVars.map(_._2._1))))
+      }
+
+      val s = sInit.copy(g = Store(argVars),
                          h = Heap(),
-                         oldHeaps = OldHeaps())
+                         oldHeaps = OldHeaps(),
+                         functionRecorder = funcRecorder)
+
       val err = PredicateNotWellformed(predicate)
 
+      var branchResults: Seq[(Seq[Term], Seq[(ast.Exp, Option[ast.Exp])], Heap, InsertionOrderedSet[Term])] = Seq()
+
+
       val result = predicate.body match {
         case None =>
           Success()
@@ -99,25 +125,82 @@ trait DefaultPredicateVerificationUnitProvider extends VerifierComponent { v: Ve
           /*    locallyXXX {
                 magicWandSupporter.checkWandsAreSelfFraming(σ.γ, σ.h, predicate, c)}
           &&*/  executionFlowController.locally(s, v)((s1, _) => {
-                  produce(s1, freshSnap, body, err, v)((_, _) =>
-                    Success())})
+                  produce(s1, toSf(snap), body, err, v)((s2, v2) => {
+                    val branchConds = v2.decider.pcs.branchConditions.reverse
+                    val branchCondExps = v2.decider.pcs.branchConditionExps.reverse
+                    assert(branchConds.length == branchCondExps.length)
+                    val heap = s2.h
+                    val assumptions = v2.decider.pcs.assumptions
+                    branchResults = branchResults :+
+                      (branchConds, branchCondExps, heap, assumptions)
+                    funcRecorder = funcRecorder.merge(s2.functionRecorder)
+                    Success()
+                  })})
       }
 
+      val overallResult = if (predicate.body.isDefined && !result.isFatal && Verifier.config.enableSimplifiedUnfolds())
+        Some(makePredTree(branchResults)) else None
+
+      this.predicateData(predicate).predContents = overallResult
+      this.predicateData(predicate).params = Some(Seq(snap) ++ argVars.map(_._2._1))
+      this.predicateData(predicate).addRecorders(Seq(funcRecorder))
+
       symbExLog.closeMemberScope()
       Seq(result)
     }
 
+    def makePredTree(branches: Seq[(Seq[Term], Seq[(ast.Exp, Option[ast.Exp])], Heap, InsertionOrderedSet[Term])]): PredicateContentsTree = {
+      if (branches.head._1.isEmpty) {
+        assert(branches.length == 1)
+        PredicateLeafNode(branches.head._3, branches.head._4)
+      } else {
+        val branchCond = branches.head._1.head
+        val branchCondExp = branches.head._2.head
+        val (trueBranches, falseBranches) = branches.partition(_._1.head == branchCond)
+        if (trueBranches.nonEmpty && falseBranches.nonEmpty) {
+          val trueTree = makePredTree(trueBranches.map(brnchs => (brnchs._1.tail, brnchs._2.tail, brnchs._3, brnchs._4)))
+          val falseTree = makePredTree(falseBranches.map(brnchs => (brnchs._1.tail, brnchs._2.tail, brnchs._3, brnchs._4)))
+          PredicateBranchNode(branchCond, branchCondExp, trueTree, falseTree)
+        } else if (trueBranches.nonEmpty) {
+          makePredTree(trueBranches.map(brnchs => (brnchs._1.tail, brnchs._2.tail, brnchs._3, brnchs._4)))
+        } else {
+          assert(falseBranches.nonEmpty)
+          makePredTree(falseBranches.map(brnchs => (brnchs._1.tail, brnchs._2.tail, brnchs._3, brnchs._4)))
+        }
+      }
+    }
+
     /* Predicate supporter generates no sorts */
     val sortsAfterVerification: Iterable[Sort] = Seq.empty
     def declareSortsAfterVerification(sink: ProverLike): Unit = ()
 
-    /* Predicate supporter does not generate additional symbols during verification */
-    val symbolsAfterVerification: Iterable[Fun] = Seq.empty
-    def declareSymbolsAfterVerification(sink: ProverLike): Unit = ()
+    val symbolsAfterVerification: Iterable[Decl] =
+      generateFunctionSymbolsAfterVerification collect { case Right(f) => f }
+
+    def declareSymbolsAfterVerification(sink: ProverLike): Unit = {
+      generateFunctionSymbolsAfterVerification foreach {
+        case Left(comment) => sink.comment(comment)
+        case Right(decl) => sink.declare(decl)
+      }
+    }
+
+    private def generateFunctionSymbolsAfterVerification: Iterable[Either[String, Decl]] = {
+      // TODO: It can currently happen that a pTaken macro (see QuantifiedChunkSupporter, def removePermissions)
+      //       is recorded as a fresh macro before a snapshot map that is used in the macro definition (body)
+      //       is recorded, which will yield a Z3 syntax error (undeclared symbol). To work around this,
+      //       macros are declared last. This work-around shouldn't be necessary, though.
+      val (macroDecls, otherDecls) =
+      predicateData.values.flatMap(_.getFreshSymbolsAcrossAllPhases).partition(_.isInstanceOf[MacroDecl])
+
+      Seq(Left("Declaring symbols related to program functions (from verification)")) ++
+        otherDecls.map(Right(_)) ++
+        macroDecls.map(Right(_))
+    }
 
     /* Predicate supporter generates no axioms */
     val axiomsAfterVerification: Iterable[Term] = Seq.empty
-    def emitAxiomsAfterVerification(sink: ProverLike): Unit = ()
+    def emitAxiomsAfterVerification(sink: ProverLike): Unit = {
+    }
 
     /* Lifetime */
 
diff --git a/src/main/scala/supporters/functions/FunctionData.scala b/src/main/scala/supporters/functions/FunctionData.scala
index 786156fcf..7293e99a1 100644
--- a/src/main/scala/supporters/functions/FunctionData.scala
+++ b/src/main/scala/supporters/functions/FunctionData.scala
@@ -13,7 +13,7 @@ import viper.silver.ast
 import viper.silver.ast.utility.Functions
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
 import viper.silicon.interfaces.FatalResult
-import viper.silicon.rules.{InverseFunctions, SnapshotMapDefinition, functionSupporter}
+import viper.silicon.rules.{InverseFunctions, PermMapDefinition, SnapshotMapDefinition, functionSupporter}
 import viper.silicon.state.terms._
 import viper.silicon.state.terms.predef._
 import viper.silicon.state.{Identifier, IdentifierFactory, SymbolConverter}
@@ -25,11 +25,66 @@ import viper.silver.ast.LocalVarWithVersion
 import viper.silver.parser.PUnknown
 import viper.silver.reporter.Reporter
 
-/* TODO: Refactor FunctionData!
- *       Separate computations from "storing" the final results and sharing
- *       them with other components. Computations should probably be moved to the
- *       FunctionVerificationUnit.
- */
+trait FunctionRecorderHandler {
+
+  protected[functions] var locToSnap: Map[(ast.LocationAccess, Seq[ExpContext]), Term] = Map.empty
+  protected[functions] var fappToSnap: Map[(ast.FuncApp, Seq[ExpContext]), Term] = Map.empty
+  protected[this] var freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition] = InsertionOrderedSet.empty
+  protected[this] var freshPermMaps: InsertionOrderedSet[PermMapDefinition] = InsertionOrderedSet.empty
+  protected[this] var freshFieldInvs: InsertionOrderedSet[InverseFunctions] = InsertionOrderedSet.empty
+  protected[this] var freshConstrainedVars: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet.empty
+  protected[this] var freshConstraints: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
+  protected[this] var freshSnapshots: InsertionOrderedSet[Function] = InsertionOrderedSet.empty
+  protected[this] var freshPathSymbols: InsertionOrderedSet[Function] = InsertionOrderedSet.empty
+  protected[this] var freshMacros: InsertionOrderedSet[MacroDecl] = InsertionOrderedSet.empty
+  protected[this] var freshSymbolsAcrossAllPhases: InsertionOrderedSet[Decl] = InsertionOrderedSet.empty
+
+  private[functions] def getFreshFieldInvs: InsertionOrderedSet[InverseFunctions] = freshFieldInvs
+
+  private[functions] def getFreshConstrainedVars: InsertionOrderedSet[Var] = freshConstrainedVars.map(_._1)
+
+  def getFreshSymbolsAcrossAllPhases: InsertionOrderedSet[Decl] = freshSymbolsAcrossAllPhases
+
+  def addRecorders(recorders: Seq[FunctionRecorder]): Unit = {
+    val mergedFunctionRecorder: FunctionRecorder =
+      if (recorders.isEmpty)
+        NoopFunctionRecorder
+      else
+        recorders.tail.foldLeft(recorders.head)((summaryRec, nextRec) => summaryRec.merge(nextRec))
+
+    locToSnap = mergedFunctionRecorder.locToSnap
+    fappToSnap = mergedFunctionRecorder.fappToSnap
+    freshFvfsAndDomains = mergedFunctionRecorder.freshFvfsAndDomains
+    freshPermMaps = mergedFunctionRecorder.freshPermMaps
+    freshFieldInvs = mergedFunctionRecorder.freshFieldInvs
+    freshConstrainedVars = mergedFunctionRecorder.freshConstrainedVars
+    freshConstraints = mergedFunctionRecorder.freshConstraints
+    freshSnapshots = mergedFunctionRecorder.freshSnapshots
+    freshPathSymbols = mergedFunctionRecorder.freshPathSymbols
+    freshMacros = mergedFunctionRecorder.freshMacros
+
+    freshSymbolsAcrossAllPhases ++= freshPathSymbols map FunctionDecl
+    freshSymbolsAcrossAllPhases ++= freshConstrainedVars.map(pair => FunctionDecl(pair._1))
+    freshSymbolsAcrossAllPhases ++= freshSnapshots map FunctionDecl
+    freshSymbolsAcrossAllPhases ++= freshFieldInvs.flatMap(i => (i.inverses ++ i.images) map FunctionDecl)
+    freshSymbolsAcrossAllPhases ++= freshMacros
+
+    freshSymbolsAcrossAllPhases ++= freshFvfsAndDomains map (fvfDef =>
+      fvfDef.sm match {
+        case x: Var => ConstDecl(x)
+        case App(f: Function, _) => FunctionDecl(f)
+        case other => sys.error(s"Unexpected SM $other of type ${other.getClass.getSimpleName}")
+      })
+    freshSymbolsAcrossAllPhases ++= freshPermMaps map (pmDef =>
+      pmDef.pm match {
+        case x: Var => ConstDecl(x)
+        case App(f: Function, _) => FunctionDecl(f)
+        case other => sys.error(s"Unexpected permission map $other of type ${other.getClass.getSimpleName}")
+      })
+  }
+
+}
+
 class FunctionData(val programFunction: ast.Function,
                    val height: Int,
                    val quantifiedFields: InsertionOrderedSet[ast.Field],
@@ -45,9 +100,7 @@ class FunctionData(val programFunction: ast.Function,
                    predicateData: ast.Predicate => PredicateData,
                    @unused config: Config,
                    @unused reporter: Reporter)
-    extends LazyLogging {
-
-  private[this] var phase = 0
+    extends LazyLogging with FunctionRecorderHandler {
 
   /*
    * Properties computed from the constructor arguments
@@ -100,62 +153,24 @@ class FunctionData(val programFunction: ast.Function,
    */
 
   private[functions] var verificationFailures: Seq[FatalResult] = Vector.empty
-  private[functions] var locToSnap: Map[(ast.LocationAccess, Seq[ExpContext]), Term] = Map.empty
-  private[functions] var fappToSnap: Map[(ast.FuncApp, Seq[ExpContext]), Term] = Map.empty
-  private[this] var freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition] = InsertionOrderedSet.empty
-  private[this] var freshFieldInvs: InsertionOrderedSet[InverseFunctions] = InsertionOrderedSet.empty
-  private[this] var freshConstrainedVars: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet.empty
-  private[this] var freshConstraints: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
-  private[this] var freshSnapshots: InsertionOrderedSet[Function] = InsertionOrderedSet.empty
-  private[this] var freshPathSymbols: InsertionOrderedSet[Function] = InsertionOrderedSet.empty
-  private[this] var freshMacros: InsertionOrderedSet[MacroDecl] = InsertionOrderedSet.empty
-  private[this] var freshSymbolsAcrossAllPhases: InsertionOrderedSet[Decl] = InsertionOrderedSet.empty
 
-  private[functions] def getFreshFieldInvs: InsertionOrderedSet[InverseFunctions] = freshFieldInvs
-  private[functions] def getFreshConstrainedVars: InsertionOrderedSet[Var] = freshConstrainedVars.map(_._1)
-  private[functions] def getFreshSymbolsAcrossAllPhases: InsertionOrderedSet[Decl] = freshSymbolsAcrossAllPhases
+  private[this] var phase = 0
 
   private[functions] def advancePhase(recorders: Seq[FunctionRecorder]): Unit = {
     assert(0 <= phase && phase <= 1, s"Cannot advance from phase $phase")
 
-    val mergedFunctionRecorder: FunctionRecorder =
-      if (recorders.isEmpty)
-        NoopFunctionRecorder
-      else
-        recorders.tail.foldLeft(recorders.head)((summaryRec, nextRec) => summaryRec.merge(nextRec))
-
-    locToSnap = mergedFunctionRecorder.locToSnap
-    fappToSnap = mergedFunctionRecorder.fappToSnap
-    freshFvfsAndDomains = mergedFunctionRecorder.freshFvfsAndDomains
-    freshFieldInvs = mergedFunctionRecorder.freshFieldInvs
-    freshConstrainedVars = mergedFunctionRecorder.freshConstrainedVars
-    freshConstraints = mergedFunctionRecorder.freshConstraints
-    freshSnapshots = mergedFunctionRecorder.freshSnapshots
-    freshPathSymbols = mergedFunctionRecorder.freshPathSymbols
-    freshMacros = mergedFunctionRecorder.freshMacros
-
-    freshSymbolsAcrossAllPhases ++= freshPathSymbols map FunctionDecl
-    freshSymbolsAcrossAllPhases ++= freshConstrainedVars.map(pair => FunctionDecl(pair._1))
-    freshSymbolsAcrossAllPhases ++= freshSnapshots map FunctionDecl
-    freshSymbolsAcrossAllPhases ++= freshFieldInvs.flatMap(i => (i.inverses ++ i.images) map FunctionDecl)
-    freshSymbolsAcrossAllPhases ++= freshMacros
-
-    freshSymbolsAcrossAllPhases ++= freshFvfsAndDomains map (fvfDef =>
-      fvfDef.sm match {
-        case x: Var => ConstDecl(x)
-        case App(f: Function, _) => FunctionDecl(f)
-        case other => sys.error(s"Unexpected SM $other of type ${other.getClass.getSimpleName}")
-      })
-
+    addRecorders(recorders)
     phase += 1
   }
 
+
   private def generateNestedDefinitionalAxioms: InsertionOrderedSet[Term] = {
     val freshSymbols: Set[Identifier] = freshSymbolsAcrossAllPhases.map(_.id)
 
     val nested = (
          freshFieldInvs.flatMap(_.definitionalAxioms)
       ++ freshFvfsAndDomains.flatMap (fvfDef => fvfDef.domainDefinitions ++ fvfDef.valueDefinitions)
+      ++ freshPermMaps.flatMap (pmDef => pmDef.valueDefinitions)
       ++ freshConstrainedVars.map(_._2)
       ++ freshConstraints)
 
diff --git a/src/main/scala/supporters/functions/FunctionRecorder.scala b/src/main/scala/supporters/functions/FunctionRecorder.scala
index 0991dbc4b..03d89b2ba 100644
--- a/src/main/scala/supporters/functions/FunctionRecorder.scala
+++ b/src/main/scala/supporters/functions/FunctionRecorder.scala
@@ -9,21 +9,23 @@ package viper.silicon.supporters.functions
 import viper.silver.ast
 import viper.silicon.common.Mergeable
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
-import viper.silicon.rules.{InverseFunctions, SnapshotMapDefinition}
+import viper.silicon.rules.{InverseFunctions, PermMapDefinition, SnapshotMapDefinition}
 import viper.silicon.{Map, Stack}
 import viper.silicon.state.terms._
+import viper.silver.ast.AbstractLocalVar
 
 // TODO: FunctionRecorder records Function, Var, etc., which are later on turned into corresponding
 //       declarations (e.g. FunctionDecl), see FunctionData's field freshSymbolsAcrossAllPhases.
 //       Only macros are already recorded as MacroDecls — this should be the case for Functions,
 //       etc. as well.
 trait FunctionRecorder extends Mergeable[FunctionRecorder] {
-  def data: Option[FunctionData]
+  def arguments: Option[Seq[(Var, Option[ast.AbstractLocalVar])]]
   private[functions] def locToSnaps: Map[(ast.LocationAccess, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]]
   def locToSnap: Map[(ast.LocationAccess, Seq[ExpContext]), Term]
   private[functions] def fappToSnaps: Map[(ast.FuncApp, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]]
   def fappToSnap: Map[(ast.FuncApp, Seq[ExpContext]), Term]
   def freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition]
+  def freshPermMaps: InsertionOrderedSet[PermMapDefinition]
   def freshFieldInvs: InsertionOrderedSet[InverseFunctions]
   def freshConstrainedVars: InsertionOrderedSet[(Var, Term)]
   def freshConstraints: InsertionOrderedSet[Term]
@@ -33,6 +35,7 @@ trait FunctionRecorder extends Mergeable[FunctionRecorder] {
   def recordSnapshot(loc: ast.LocationAccess, guards: Stack[Term], snap: Term): FunctionRecorder
   def recordSnapshot(fapp: ast.FuncApp, guards: Stack[Term], snap: Term): FunctionRecorder
   def recordFvfAndDomain(fvfDef: SnapshotMapDefinition): FunctionRecorder
+  def recordPermMap(pmDef: PermMapDefinition): FunctionRecorder
   def recordFieldInv(inv: InverseFunctions): FunctionRecorder
   def recordConstrainedVar(v: Var, constraint: Term): FunctionRecorder
   def recordConstraint(constraint: Term): FunctionRecorder
@@ -47,14 +50,16 @@ trait FunctionRecorder extends Mergeable[FunctionRecorder] {
   def leaveQuantifiedExp(q: ast.QuantifiedExp): FunctionRecorder
 }
 
+
 trait ExpContext
 case class LetContext(l: ast.Let) extends ExpContext
 case class QuantifierContext(q: ast.QuantifiedExp) extends ExpContext
 
-case class ActualFunctionRecorder(private val _data: FunctionData,
+case class ActualFunctionRecorder(private val _data: Either[FunctionData, (ast.Predicate, Seq[Var])],
                                   private[functions] val locToSnaps: Map[(ast.LocationAccess, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]] = Map(),
                                   private[functions] val fappToSnaps: Map[(ast.FuncApp, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]] = Map(),
                                   freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition] = InsertionOrderedSet(),
+                                  freshPermMaps: InsertionOrderedSet[PermMapDefinition] = InsertionOrderedSet(),
                                   freshFieldInvs: InsertionOrderedSet[InverseFunctions] = InsertionOrderedSet(),
                                   freshConstrainedVars: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet(),
                                   freshConstraints: InsertionOrderedSet[Term] = InsertionOrderedSet(),
@@ -99,7 +104,10 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
    * unfolding's in-clause, which, as argued before, are not part of f.
    */
 
-  val data = Some(_data)
+  override def arguments: Option[Stack[(Var, Option[AbstractLocalVar])]] = _data match {
+    case Left(fd) => Some(fd.arguments.zip(fd.argumentExps))
+    case Right((_, args)) => Some(args.map((_, None)))
+  }
 
   private def exprToSnap[E <: ast.Exp]
                         (recordings: Map[(E, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]])
@@ -194,6 +202,10 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
     if (depth <= 2) copy(freshFvfsAndDomains = freshFvfsAndDomains + fvfDef)
     else this
 
+  def recordPermMap(pmDef: PermMapDefinition): ActualFunctionRecorder =
+    if (depth <= 2) copy(freshPermMaps = freshPermMaps + pmDef)
+    else this
+
   def recordFieldInv(inv: InverseFunctions): ActualFunctionRecorder =
     if (depth <= 2) copy(freshFieldInvs = freshFieldInvs + inv)
     else this
@@ -207,7 +219,7 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
     else this
 
   def recordFreshSnapshot(snap: Function): ActualFunctionRecorder =
-    if (depth <= 1) copy(freshSnapshots = freshSnapshots + snap)
+    if (depth <= 3) copy(freshSnapshots = freshSnapshots + snap)
     else this
 
   def recordPathSymbol(symbol: Function): ActualFunctionRecorder =
@@ -249,7 +261,6 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
     if (depth > 1) return this
 
     assert(other.getClass == this.getClass)
-    assert(other.asInstanceOf[ActualFunctionRecorder]._data eq this._data)
 
     var lts = locToSnaps
     var fts = fappToSnaps
@@ -269,6 +280,7 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
     }
 
     val fvfs = freshFvfsAndDomains ++ other.freshFvfsAndDomains
+    val pmDefs = freshPermMaps ++ other.freshPermMaps
     val fieldInvs = freshFieldInvs ++ other.freshFieldInvs
     val arps = freshConstrainedVars ++ other.freshConstrainedVars
     val constraints = freshConstraints ++ other.freshConstraints
@@ -279,6 +291,7 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
     copy(locToSnaps = lts,
          fappToSnaps = fts,
          freshFvfsAndDomains = fvfs,
+         freshPermMaps = pmDefs,
          freshFieldInvs = fieldInvs,
          freshConstrainedVars = arps,
          freshConstraints = constraints,
@@ -303,12 +316,14 @@ case class ActualFunctionRecorder(private val _data: FunctionData,
 }
 
 case object NoopFunctionRecorder extends FunctionRecorder {
-  val data: Option[FunctionData] = None
+  def arguments: Option[Seq[(viper.silicon.state.terms.Var, Option[viper.silver.ast.AbstractLocalVar])]] = None
   private[functions] val fappToSnaps: Map[(ast.FuncApp, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]] = Map.empty
   val fappToSnap: Map[(ast.FuncApp, Seq[ExpContext]), Term] = Map.empty
   private[functions] val locToSnaps: Map[(ast.LocationAccess, Seq[ExpContext]), InsertionOrderedSet[(Stack[Term], Term)]] = Map.empty
   val locToSnap: Map[(ast.LocationAccess, Seq[ExpContext]), Term] = Map.empty
+
   val freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition] = InsertionOrderedSet.empty
+  val freshPermMaps: InsertionOrderedSet[PermMapDefinition] = InsertionOrderedSet.empty
   val freshFieldInvs: InsertionOrderedSet[InverseFunctions] = InsertionOrderedSet.empty
   val freshConstrainedVars: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet.empty
   val freshConstraints: InsertionOrderedSet[Term] = InsertionOrderedSet.empty
@@ -325,6 +340,7 @@ case object NoopFunctionRecorder extends FunctionRecorder {
 
   def recordSnapshot(loc: ast.LocationAccess, guards: Stack[Term], snap: Term): NoopFunctionRecorder.type = this
   def recordFvfAndDomain(fvfDef: SnapshotMapDefinition): NoopFunctionRecorder.type = this
+  def recordPermMap(pmDef: PermMapDefinition): NoopFunctionRecorder.type = this
   def recordFieldInv(inv: InverseFunctions): NoopFunctionRecorder.type = this
   def recordSnapshot(fapp: ast.FuncApp, guards: Stack[Term], snap: Term): NoopFunctionRecorder.type = this
   def recordConstrainedVar(arp: Var, constraint: Term): NoopFunctionRecorder.type = this
diff --git a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala
index b877b511f..f964754c6 100644
--- a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala
+++ b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala
@@ -168,7 +168,7 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver
 
     private def handleFunction(sInit: State, function: ast.Function): VerificationResult = {
       val data = functionData(function)
-      val s = sInit.copy(functionRecorder = ActualFunctionRecorder(data),
+      val s = sInit.copy(functionRecorder = ActualFunctionRecorder(Left(data)),
         conservingSnapshotGeneration = true,
         assertReadAccessOnly = !Verifier.config.respectFunctionPrePermAmounts())
 
diff --git a/src/test/resources/symbExLogTests/symbLogTest_ImpureBranching.vpr.elog b/src/test/resources/symbExLogTests/symbLogTest_ImpureBranching.vpr.elog
index 85ac9cda9..9590b5c8e 100644
--- a/src/test/resources/symbExLogTests/symbLogTest_ImpureBranching.vpr.elog
+++ b/src/test/resources/symbExLogTests/symbLogTest_ImpureBranching.vpr.elog
@@ -1,7 +1,7 @@
 predicate P
-  Branch b@0@00:
+  Branch b@1@00:
     comment: Reachable
-  Branch !(b@0@00):
+  Branch !(b@1@00):
     comment: Reachable
 
 method test1
diff --git a/src/test/resources/symbExLogTests/symbLogTest_linkedListMinimal.vpr.elog b/src/test/resources/symbExLogTests/symbLogTest_linkedListMinimal.vpr.elog
index 5cb0de266..3f84459a8 100644
--- a/src/test/resources/symbExLogTests/symbLogTest_linkedListMinimal.vpr.elog
+++ b/src/test/resources/symbExLogTests/symbLogTest_linkedListMinimal.vpr.elog
@@ -1,37 +1,37 @@
 predicate lseg
-  Branch this@0@00 != end@1@00:
+  Branch this@1@00 != end@2@00:
     comment: Reachable
     Join
-      Branch First:(Second:($t@2@00)) != end@1@00:
+      Branch First:(Second:($t@0@00)) != end@2@00:
         comment: Reachable
         Join
-          Branch First:(Second:(First:(Second:(Second:($t@2@00))))) != end@1@00:
+          Branch First:(Second:(First:(Second:(Second:($t@0@00))))) != end@2@00:
             comment: Reachable
             Join
-              Branch First:(Second:(First:(Second:(Second:($t@2@00))))) != end@1@00:
+              Branch First:(Second:(First:(Second:(Second:($t@0@00))))) != end@2@00:
                 comment: Reachable
-              Branch First:(Second:(First:(Second:(Second:($t@2@00))))) == end@1@00:
+              Branch First:(Second:(First:(Second:(Second:($t@0@00))))) == end@2@00:
                 comment: Unreachable
-          Branch First:(Second:(First:(Second:(Second:($t@2@00))))) == end@1@00:
+          Branch First:(Second:(First:(Second:(Second:($t@0@00))))) == end@2@00:
             comment: Reachable
             Join
-              Branch First:(Second:(First:(Second:(Second:($t@2@00))))) != end@1@00:
+              Branch First:(Second:(First:(Second:(Second:($t@0@00))))) != end@2@00:
                 comment: Unreachable
-              Branch First:(Second:(First:(Second:(Second:($t@2@00))))) == end@1@00:
+              Branch First:(Second:(First:(Second:(Second:($t@0@00))))) == end@2@00:
                 comment: Reachable
         Join
-          Branch First:(Second:($t@2@00)) != end@1@00:
+          Branch First:(Second:($t@0@00)) != end@2@00:
             comment: Reachable
-          Branch First:(Second:($t@2@00)) == end@1@00:
+          Branch First:(Second:($t@0@00)) == end@2@00:
             comment: Unreachable
-      Branch First:(Second:($t@2@00)) == end@1@00:
+      Branch First:(Second:($t@0@00)) == end@2@00:
         comment: Reachable
         Join
-          Branch First:(Second:($t@2@00)) != end@1@00:
+          Branch First:(Second:($t@0@00)) != end@2@00:
             comment: Unreachable
-          Branch First:(Second:($t@2@00)) == end@1@00:
+          Branch First:(Second:($t@0@00)) == end@2@00:
             comment: Reachable
-  Branch this@0@00 == end@1@00:
+  Branch this@1@00 == end@2@00:
     comment: Reachable
 
 predicate List
@@ -43,58 +43,6 @@ method insert
   execute unfold acc(lseg(this.head, null), write)
     Branch First:($t@6@01) != Null:
       comment: Reachable
-      Join
-        Branch First:(Second:(Second:($t@6@01))) != Null:
-          comment: Reachable
-          Join
-            Branch First:(Second:(First:(Second:(Second:(Second:($t@6@01)))))) != Null:
-              comment: Reachable
-              Join
-                Branch First:(Second:(First:(Second:(Second:(Second:($t@6@01)))))) != Null:
-                  comment: Reachable
-                Branch First:(Second:(First:(Second:(Second:(Second:($t@6@01)))))) == Null:
-                  comment: Unreachable
-            Branch First:(Second:(First:(Second:(Second:(Second:($t@6@01)))))) == Null:
-              comment: Reachable
-              Join
-                Branch First:(Second:(First:(Second:(Second:(Second:($t@6@01)))))) != Null:
-                  comment: Unreachable
-                Branch First:(Second:(First:(Second:(Second:(Second:($t@6@01)))))) == Null:
-                  comment: Reachable
-          Join
-            Branch First:(Second:(Second:($t@6@01))) != Null:
-              comment: Reachable
-            Branch First:(Second:(Second:($t@6@01))) == Null:
-              comment: Unreachable
-        Branch First:(Second:(Second:($t@6@01))) == Null:
-          comment: Reachable
-          Join
-            Branch First:(Second:(Second:($t@6@01))) != Null:
-              comment: Unreachable
-            Branch First:(Second:(Second:($t@6@01))) == Null:
-              comment: Reachable
-      Branch 1:
-        comment: Reachable
-        Join
-          Branch First:($t@6@01) == Null:
-            comment: Reachable
-          Branch First:($t@6@01) != Null:
-            comment: Reachable
-        Branch !(First:($t@6@01) == Null || elem@4@01 <= First:(Second:($t@6@01))):
-          comment: Reachable
-        Branch First:($t@6@01) == Null || elem@4@01 <= First:(Second:($t@6@01)):
-          comment: Reachable
-      Branch 2:
-        comment: Reachable
-        Join
-          Branch First:($t@6@01) == Null:
-            comment: Reachable
-          Branch First:($t@6@01) != Null:
-            comment: Reachable
-        Branch First:($t@6@01) == Null || elem@4@01 <= First:(Second:($t@6@01)):
-          comment: Reachable
-        Branch !(First:($t@6@01) == Null || elem@4@01 <= First:(Second:($t@6@01))):
-          comment: Reachable
     Branch First:($t@6@01) == Null:
       comment: Reachable
       Branch 1:
diff --git a/src/test/resources/symbExLogTests/symbLogTest_minimal.vpr.elog b/src/test/resources/symbExLogTests/symbLogTest_minimal.vpr.elog
index 0f0cd18d4..dc2dba656 100644
--- a/src/test/resources/symbExLogTests/symbLogTest_minimal.vpr.elog
+++ b/src/test/resources/symbExLogTests/symbLogTest_minimal.vpr.elog
@@ -1,7 +1,7 @@
 predicate P4
-  Branch b@0@00:
+  Branch b@1@00:
     comment: Reachable
-  Branch !(b@0@00):
+  Branch !(b@1@00):
     comment: Reachable
 
 method topOfStackInIgnoredSepSetCheck
diff --git a/src/test/scala/SiliconTestsSimplifiedUnfold.scala b/src/test/scala/SiliconTestsSimplifiedUnfold.scala
new file mode 100644
index 000000000..d516e0324
--- /dev/null
+++ b/src/test/scala/SiliconTestsSimplifiedUnfold.scala
@@ -0,0 +1,16 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2025 ETH Zurich.
+
+package viper.silicon.tests
+
+class SiliconTestsSimplifiedUnfold extends SiliconTests {
+  override val testDirectories: Seq[String] = Seq("all/predicates")
+
+  override val commandLineArguments: Seq[String] = Seq(
+    "--timeout", "300" /* seconds */,
+    "--enableSimplifiedUnfolds"
+  )
+}