diff --git a/src/main/scala/Utils.scala b/src/main/scala/Utils.scala
index 48aeaf8e0..0c29c4258 100644
--- a/src/main/scala/Utils.scala
+++ b/src/main/scala/Utils.scala
@@ -137,7 +137,8 @@ package object utils {
       exps.zip(terms).filter(t => t._2 != True).map(e => e._1)
     }
 
-    def buildIteExp(condTerm: Term, ifTerm: Term, elseTerm: Term, condExp: silver.ast.Exp, ifExp: silver.ast.Exp, elseExp: silver.ast.Exp): silver.ast.Exp ={
+    // TODO ake: find a better way to do this
+    def buildIteExp(condTerm: Term, ifTerm: Term, elseTerm: Term, condExp: silver.ast.Exp, ifExp: silver.ast.Exp, elseExp: silver.ast.Exp, typ: silver.ast.Type): silver.ast.Exp ={
       val iteTerm = Ite(condTerm, ifTerm, elseTerm)
       if(iteTerm.equals(ifTerm)){
         ifExp
@@ -148,11 +149,12 @@ package object utils {
       } else if (iteTerm.equals(Not(condTerm))) {
         silver.ast.Not(condExp)()
       }else{
-        silver.ast.And(silver.ast.Implies(condExp, ifExp)(), silver.ast.Implies(silver.ast.Not(condExp)(), elseExp)())()
+        silver.ast.FuncApp("Ite", Seq(condExp, ifExp, elseExp))(condExp.pos, condExp.info, typ, condExp.errT)
+//        silver.ast.And(silver.ast.Implies(condExp, ifExp)(), silver.ast.Implies(silver.ast.Not(condExp)(), elseExp)())() TODO ake: remove
       }
     }
 
-    def buildImpliesExp(assmptTerm: Term, rhsTerm: Term, assmptExp: silver.ast.Exp, rhsExp: silver.ast.Exp): silver.ast.Exp= {
+     def buildImpliesExp(assmptTerm: Term, rhsTerm: Term, assmptExp: silver.ast.Exp, rhsExp: silver.ast.Exp): silver.ast.Exp= {
       val implTerm = Implies(assmptTerm, rhsTerm)
       if (implTerm.equals(True)) {
         silver.ast.TrueLit()()
diff --git a/src/main/scala/decider/DebugExp.scala b/src/main/scala/decider/DebugExp.scala
index 1d57633ef..739e5e3c7 100644
--- a/src/main/scala/decider/DebugExp.scala
+++ b/src/main/scala/decider/DebugExp.scala
@@ -11,6 +11,7 @@ import viper.silicon.state.terms.Term
 import viper.silver.ast
 
 import scala.annotation.unused
+import scala.math
 class DebugExp(str : Option[String],
                @unused exp : Option[ast.Exp],
                substitutedExp : Option[ast.Exp],
@@ -42,7 +43,7 @@ class DebugExp(str : Option[String],
   }
 
   def this(exp : ast.Exp, substitutedExp : ast.Exp) = {
-    this(None, Some(exp), Some(exp), InsertionOrderedSet.empty)
+    this(None, Some(exp), Some(substitutedExp), InsertionOrderedSet.empty)
   }
 
   def withTerms(newTerms : InsertionOrderedSet[Term]): DebugExp = {
@@ -53,17 +54,38 @@ class DebugExp(str : Option[String],
     terms
   }
 
+  def isInternal(): Boolean = isInternal
+
   @unused
   def termsToString: String = {
     terms.map(t => t.toString.replaceAll("@.. ", " ")).mkString(" && ")
   }
 
   override def toString: String = {
-    if(str.isDefined){
-      if(children.isEmpty) str.get
-      else str.get + ": " + children.mkString(" && ")
-    }else{
-      substitutedExp.get.toString() + (if(isImplicationLHS && children.nonEmpty) " ==> (" + children.mkString(" && ") + ")" else "")
+    toString(printInternals = true, 5)
+  }
+
+  def childrenToString(printInternals: Boolean, printChildrenDepth: Int): String = {
+    val nonInternalChildren = children.filter(de => printInternals || !de.isInternal())
+    if (nonInternalChildren.isEmpty || printChildrenDepth <= 0) ""
+    else {
+      "(" + nonInternalChildren.tail.foldLeft[String](nonInternalChildren.head.toString(printInternals, printChildrenDepth - 1))((s, de) => s + " && " + de.toString(printInternals, printChildrenDepth - 1)) + ")"
+    }
+  }
+
+  def toString(printInternals: Boolean, printChildrenDepth: Int): String = {
+    if(isInternal && !printInternals){
+      return ""
+    }
+    if (str.isDefined) {
+      val mainStr = str.get + (if (substitutedExp.isDefined) "(" + substitutedExp.get.toString() + ")" else "")
+      if (children.isEmpty || printChildrenDepth <= 0) mainStr
+      else "(" + mainStr + ": " + childrenToString(printInternals, printChildrenDepth) + ")"
+    } else {
+      if (isImplicationLHS && children.nonEmpty) {
+        "(" + substitutedExp.get.toString() + " ==> " + childrenToString(printInternals, math.max(printChildrenDepth, 1)) + ")"
+      }
+      substitutedExp.get.toString()
     }
   }
 
diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala
index 3d0eefe7a..c825af2e2 100644
--- a/src/main/scala/decider/Decider.scala
+++ b/src/main/scala/decider/Decider.scala
@@ -212,8 +212,8 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
         }
         case None => {
           pathConditions.setCurrentBranchCondition(t, None)
-          assume(t, new DebugExp("unknown branch condition"))
-        } // TODO ake
+          assume(t, new DebugExp("unknown branch condition")) // TODO ake: branch conditions
+        }
       }
     }
 
diff --git a/src/main/scala/interfaces/Verification.scala b/src/main/scala/interfaces/Verification.scala
index 2081b9c8b..2c2564468 100644
--- a/src/main/scala/interfaces/Verification.scala
+++ b/src/main/scala/interfaces/Verification.scala
@@ -144,7 +144,8 @@ case class SiliconFailureContext(branchConditions: Seq[ast.Exp],
 
   lazy val assumptionsString: String = {
     if(assumptions.nonEmpty){
-      s"\n\nassumptions: ${assumptions.mkString(" && ")}"
+      val nonInternalAssumptions = assumptions.filter(de => !de.isInternal())
+      s"\n\nassumptions:\n${nonInternalAssumptions.tail.foldLeft[String](nonInternalAssumptions.head.toString(printInternals = false, 5))((s, de) => s + " && " + de.toString(printInternals = false, 5)) + ")"}"
     }else{
       ""
     }
@@ -152,7 +153,7 @@ case class SiliconFailureContext(branchConditions: Seq[ast.Exp],
 
   lazy val failedAssertionString: String ={
     if(failedAssertion.isDefined){
-      s"Failed Assertion:\n\t\t${failedAssertion.get.toString()}"
+      s"\n\nFailed Assertion:\n\t\t${failedAssertion.get.toString()}"
     }else{
       ""
     }
diff --git a/src/main/scala/resources/NonQuantifiedPropertyInterpreter.scala b/src/main/scala/resources/NonQuantifiedPropertyInterpreter.scala
index 1333ca663..2cc3d2337 100644
--- a/src/main/scala/resources/NonQuantifiedPropertyInterpreter.scala
+++ b/src/main/scala/resources/NonQuantifiedPropertyInterpreter.scala
@@ -83,7 +83,7 @@ class NonQuantifiedPropertyInterpreter(heap: Iterable[Chunk], verifier: Verifier
 
   override protected def buildValueAccess(chunkPlaceholder: ChunkPlaceholder, info: Info) = {
     info.pm(chunkPlaceholder) match {
-      case c: NonQuantifiedChunk => new Pair(c.snap, ast.TrueLit()())
+      case c: NonQuantifiedChunk => new Pair(c.snap, ast.LocalVar("buildValueAccess not implemented", ast.Int)()) // TODO ake: permission
       // TODO: remove once singleton quantified chunks are not used anymore
       case c: QuantifiedBasicChunk => new Pair(c.valueAt(c.singletonArguments.get), ast.TrueLit()()) // TODO ake: qp
     }
diff --git a/src/main/scala/rules/ChunkSupporter.scala b/src/main/scala/rules/ChunkSupporter.scala
index 8acad3cde..c7544d73d 100644
--- a/src/main/scala/rules/ChunkSupporter.scala
+++ b/src/main/scala/rules/ChunkSupporter.scala
@@ -178,7 +178,8 @@ object chunkSupporter extends ChunkSupportRules {
           (ConsumptionResult(PermMinus(perms, toTake), ast.PermSub(permsExp, toTakeExp)(permsExp.pos, permsExp.info, permsExp.errT), v, 0), s, newHeap, takenChunk)
         } else {
           if (v.decider.check(ch.perm !== NoPerm, Verifier.config.checkTimeout())) {
-            v.decider.assume(PermLess(perms, ch.perm), new DebugExp("Perm Less"))
+            val debugExp = ast.PermLtCmp(permsExp, ch.permExp)(permsExp.pos, permsExp.info, permsExp.errT)
+            v.decider.assume(PermLess(perms, ch.perm), new DebugExp(debugExp, s.substituteVarsInExp(debugExp)))
             val newChunk = ch.withPerm(PermMinus(ch.perm, perms), ast.PermSub(ch.permExp, permsExp)(permsExp.pos, permsExp.info, permsExp.errT))
             val takenChunk = ch.withPerm(perms, permsExp)
             val newHeap = h - ch + newChunk
@@ -203,7 +204,7 @@ object chunkSupporter extends ChunkSupportRules {
 
     // Try to merge the chunk into the heap by finding an alias.
     // In any case, property assumptions are added after the merge step.
-    val (fr1, h1) = v.stateConsolidator.merge(s.functionRecorder, h, ch, v)
+    val (fr1, h1) = v.stateConsolidator.merge(s.functionRecorder, s, h, ch, v)
     Q(s.copy(functionRecorder = fr1), h1, v)
   }
 
diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala
index 09ec5ed8a..dce3ef38b 100644
--- a/src/main/scala/rules/Consumer.scala
+++ b/src/main/scala/rules/Consumer.scala
@@ -364,8 +364,8 @@ object consumer extends ConsumptionRules {
               val (smDef1, smCache1) =
                 quantifiedChunkSupporter.summarisingSnapshotMap(
                   s2, predicate, s2.predicateFormalVarMap(predicate), relevantChunks, v2)
-              val argsString = eArgs.map(e => s2.substituteVarsInExp(e)).mkString(", ")
-              val debugExp = new DebugExp(s"Predicate Trigger: ${predicate.name}($argsString)")
+              val argsString = eArgs.map(s2.substituteVarsInExp).mkString(", ")
+              val debugExp = new DebugExp(s"PredicateTrigger(${predicate.name}($argsString))")
               v2.decider.assume(PredicateTrigger(predicate.name, smDef1.sm, tArgs), debugExp)
               s2.copy(smCache = smCache1)
             } else {
@@ -422,9 +422,9 @@ object consumer extends ConsumptionRules {
             val (smDef1, smCache1) =
               quantifiedChunkSupporter.summarisingSnapshotMap(
                 s1, wand, formalVars, relevantChunks, v1)
-            val argsString = bodyVars.map(e => s1.substituteVarsInExp(e)).mkString(", ")
+            val argsString = bodyVars.map(s1.substituteVarsInExp).mkString(", ")
             val predName = MagicWandIdentifier(wand, s.program).toString
-            val debugExp = new DebugExp(s"Predicate Trigger: $predName($argsString)")
+            val debugExp = new DebugExp(s"PredicateTrigger($predName($argsString))")
             v1.decider.assume(PredicateTrigger(predName, smDef1.sm, tArgs), debugExp)
             s1.copy(smCache = smCache1)
           } else {
diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala
index c70ccd64d..881db2350 100644
--- a/src/main/scala/rules/Evaluator.scala
+++ b/src/main/scala/rules/Evaluator.scala
@@ -173,7 +173,7 @@ object evaluator extends EvaluationRules {
 
       case _: ast.WildcardPerm =>
         val (tVar, tConstraints) = v.decider.freshARP()
-        v.decider.assume(tConstraints, new DebugExp(s"WildcardPerm Access: ${tConstraints.toString}")) // TODO ake: wildcard
+        v.decider.assume(tConstraints, new DebugExp(s"wildcard == ${tVar.toString}", true))
         /* TODO: Only record wildcards in State.constrainableARPs that are used in exhale
          *       position. Currently, wildcards used in inhale position (only) may not be removed
          *       from State.constrainableARPs (potentially inefficient, but should be sound).
@@ -462,8 +462,8 @@ object evaluator extends EvaluationRules {
                   val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v1.symbolConverter.toSort(bodyVars(i).typ)))
                   val (s2, pmDef) = if (s1.heapDependentTriggers.contains(MagicWandIdentifier(wand, s1.program))) {
                     val (s2, smDef, pmDef) = quantifiedChunkSupporter.heapSummarisingMaps(s1, wand, formalVars, relevantChunks, v1)
-                    val argsString = bodyVars.map(e => s2.substituteVarsInExp(e)).mkString(", ")
-                    val debugExp = new DebugExp(s"Predicate Trigger: ${identifier.toString}($argsString)")
+                    val argsString = bodyVars.map(s2.substituteVarsInExp).mkString(", ")
+                    val debugExp = new DebugExp(s"PredicateTrigger(${identifier.toString}($argsString))")
                     v1.decider.assume(PredicateTrigger(identifier.toString, smDef.sm, args), debugExp)
                     (s2, pmDef)
                   } else {
@@ -504,8 +504,8 @@ object evaluator extends EvaluationRules {
                       s1, predicate, s1.predicateFormalVarMap(predicate), relevantChunks, v1)
                   if (s2.heapDependentTriggers.contains(predicate)){
                     val trigger = PredicateTrigger(predicate.name, smDef.sm, args)
-                    val argsString = predicate.formalArgs.mkString(", ") // TODO ake: substitution
-                    val debugExp = new DebugExp(s"Predicate Trigger: ${predicate.name}($argsString)")
+                    val argsString = predicate.formalArgs.map(e => s2.substituteVarsInExp(e.localVar)).mkString(", ")
+                    val debugExp = new DebugExp(s"PredicateTrigger(${predicate.name}($argsString))")
                     v1.decider.assume(trigger, debugExp)
                   }
                   (s2, PredicatePermLookup(identifier.toString, pmDef.pm, args))
@@ -830,8 +830,8 @@ object evaluator extends EvaluationRules {
                          * (see 'predicateTriggers' in FunctionData.scala).
                          */
                       if (!Verifier.config.disableFunctionUnfoldTrigger()) {
-                        val eArgsString = eArgs.mkString(", ")
-                        val debugExp = new DebugExp(s"Predicate Trigger ${predicate.name}($eArgsString)")
+                        val eArgsString = eArgs.map(s.substituteVarsInExp).mkString(", ")
+                        val debugExp = new DebugExp(s"PredicateTrigger(${predicate.name}($eArgsString))")
                         v4.decider.assume(App(s.predicateData(predicate).triggerFunction, snap.convert(terms.sorts.Snap) +: tArgs), debugExp)
                       }
                       val body = predicate.body.get /* Only non-abstract predicates can be unfolded */
@@ -1433,7 +1433,7 @@ object evaluator extends EvaluationRules {
         var sJoined = entries.tail.foldLeft(entries.head.s)((sAcc, entry) =>sAcc.merge(entry.s))
         sJoined = sJoined.copy(functionRecorder = sJoined.functionRecorder.recordPathSymbol(joinSymbol))
 
-        v.decider.assume(joinDefEqs, new DebugExp("Join")) // TODO ake
+        v.decider.assume(joinDefEqs, new DebugExp("Join")) // TODO ake: join
 
         (sJoined, joinTerm)
     }
diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala
index b085a526c..e9de73c01 100644
--- a/src/main/scala/rules/Executor.scala
+++ b/src/main/scala/rules/Executor.scala
@@ -81,7 +81,7 @@ object executor extends ExecutionRules {
   def handleOutEdge(s: State, edge: SilverEdge, v: Verifier): State = {
     edge.kind match {
       case cfg.Kind.Out =>
-        val (fr1, h1) = v.stateConsolidator.merge(s.functionRecorder, s.h, s.invariantContexts.head, v)
+        val (fr1, h1) = v.stateConsolidator.merge(s.functionRecorder, s, s.h, s.invariantContexts.head, v)
         val s1 = s.copy(functionRecorder = fr1, h = h1,
           invariantContexts = s.invariantContexts.tail)
         s1
@@ -540,8 +540,8 @@ object executor extends ExecutionRules {
               val (smDef1, smCache1) =
                 quantifiedChunkSupporter.summarisingSnapshotMap(
                   s2, predicate, s2.predicateFormalVarMap(predicate), relevantChunks, v2)
-              val eArgsStr = eArgs.map(e => s2.substituteVarsInExp(e)).mkString(", ")
-              val debugExp = new DebugExp(Some(s"Predicate Trigger ${predicate.name}($eArgsStr)"), Some(pa), Some(s2.substituteVarsInExp(pa)), InsertionOrderedSet.empty)
+              val eArgsStr = eArgs.map(s2.substituteVarsInExp).mkString(", ")
+              val debugExp = new DebugExp(Some(s"PredicateTrigger(${predicate.name}($eArgsStr))"), Some(pa), Some(s2.substituteVarsInExp(pa)), InsertionOrderedSet.empty)
               v2.decider.assume(PredicateTrigger(predicate.name, smDef1.sm, tArgs), debugExp)
               smCache1
             } else {
diff --git a/src/main/scala/rules/MagicWandSupporter.scala b/src/main/scala/rules/MagicWandSupporter.scala
index 82e8fe100..f8db84ff1 100644
--- a/src/main/scala/rules/MagicWandSupporter.scala
+++ b/src/main/scala/rules/MagicWandSupporter.scala
@@ -438,7 +438,7 @@ object magicWandSupporter extends SymbolicExecutionRules {
       val s3 = s2.copy(conservedPcs = conservedPcs +: s2.conservedPcs.tail, reserveHeaps = s.reserveHeaps.head +: hs2)
 
       val usedChunks = chs2.flatten
-      val (fr4, hUsed) = v2.stateConsolidator.merge(s3.functionRecorder, s2.reserveHeaps.head, Heap(usedChunks), v2)
+      val (fr4, hUsed) = v2.stateConsolidator.merge(s3.functionRecorder, s3, s2.reserveHeaps.head, Heap(usedChunks), v2)
 
       val s4 = s3.copy(functionRecorder = fr4, reserveHeaps = hUsed +: s3.reserveHeaps.tail)
 
@@ -483,7 +483,7 @@ object magicWandSupporter extends SymbolicExecutionRules {
        * is consumed from hOps and permissions for the predicate are added to the state's
        * heap. After a statement is executed those permissions are transferred to hOps.
        */
-      val (fr, hOpsJoinUsed) = v.stateConsolidator.merge(newState.functionRecorder, newState.reserveHeaps(1), newState.h, v)
+      val (fr, hOpsJoinUsed) = v.stateConsolidator.merge(newState.functionRecorder, newState, newState.reserveHeaps(1), newState.h, v)
       newState.copy(functionRecorder = fr, h = Heap(),
           reserveHeaps = Heap() +: hOpsJoinUsed +: newState.reserveHeaps.drop(2))
     } else newState
diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala
index 4b8063377..6076d36dc 100644
--- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala
+++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala
@@ -117,7 +117,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
     }
     val (s1, taggedSnap, snapDefs, permSum) = summariseOnly(s, relevantChunks, resource, args, v)
 
-    v.decider.assume(And(snapDefs), new DebugExp("Snapshot", true))
+    v.decider.assume(And(snapDefs), new DebugExp("Snapshot", true)) // TODO ake: hier bekommt man assumption wie z.B. n.val == 2
 //    v.decider.assume(PermAtMost(permSum, FullPerm())) /* Done in StateConsolidator instead */
 
     val s2 =
@@ -263,11 +263,11 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
               // that already exists.
               // During function verification, we should not define macros, since they could contain resullt, which is not
               // defined elsewhere.
-              val iteExp = buildIteExp(eq, PermMin(ch.perm, pNeeded), NoPerm, eqExp, buildMinExp(Seq(ch.permExp, pNeededExp), ast.Perm), ast.NoPerm()(permsExp.pos, permsExp.info, permsExp.errT))
+              val iteExp = buildIteExp(eq, PermMin(ch.perm, pNeeded), NoPerm, eqExp, buildMinExp(Seq(ch.permExp, pNeededExp), ast.Perm), ast.NoPerm()(permsExp.pos, permsExp.info, permsExp.errT), ast.Perm)
               (Ite(eq, PermMin(ch.perm, pNeeded), NoPerm), iteExp)
             } else {
               val pTakenBody = Ite(eq, PermMin(ch.perm, pNeeded), NoPerm)
-              val pTakenExp = buildIteExp(eq, PermMin(ch.perm, pNeeded), NoPerm, eqExp, buildMinExp(Seq(ch.permExp, pNeededExp), ast.Perm), ast.NoPerm()())
+              val pTakenExp = buildIteExp(eq, PermMin(ch.perm, pNeeded), NoPerm, eqExp, buildMinExp(Seq(ch.permExp, pNeededExp), ast.Perm), ast.NoPerm()(), ast.Perm)
               val pTakenArgs = additionalArgs
               val pTakenDecl = v.decider.freshMacro("mce_pTaken", pTakenArgs, pTakenBody)
               val pTakenMacro = Macro(pTakenDecl.id, pTakenDecl.args.map(_.sort), pTakenDecl.body.sort)
@@ -278,7 +278,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
             }
 
             pSum = PermPlus(pSum, Ite(eq, ch.perm, NoPerm))
-            pSumExp = ast.PermAdd(pSumExp, buildIteExp(eq, ch.perm, NoPerm, eqExp, ch.permExp, ast.NoPerm()()))()
+            pSumExp = ast.PermAdd(pSumExp, buildIteExp(eq, ch.perm, NoPerm, eqExp, ch.permExp, ast.NoPerm()(), ast.Perm))()
 
             val newChunk = ch.withPerm(PermMinus(ch.perm, pTaken), ast.PermSub(ch.permExp, pTakenExp)(permsExp.pos, permsExp.info, permsExp.errT))
             pNeeded = PermMinus(pNeeded, pTaken)
@@ -301,7 +301,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
         newChunks foreach { ch =>
           val resource = Resources.resourceDescriptions(ch.resourceID)
           val pathCond = interpreter.buildPathConditionsForChunk(ch, resource.instanceProperties)
-          pathCond.foreach(p => v.decider.assume(p.getFirst, new DebugExp(p.getSecond, p.getSecond)))
+          pathCond.foreach(p => v.decider.assume(p.getFirst, new DebugExp(p.getSecond, s.substituteVarsInExp(p.getSecond))))
         }
         val newHeap = Heap(allChunks)
 
@@ -354,10 +354,10 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
         val eq = And(eqCmps)
         val eqExp = BigAnd(removeKnownToBeTrueExp(ch.argsExp.zip(argsExp).map{ case (t1, t2) => ast.EqCmp(t1, t2)(permsExp.pos, permsExp.info, permsExp.errT) }.toList, eqCmps.toList))
         val permTaken = v.decider.fresh("p", sorts.Perm)
-        val permTakenExp = ast.LocalVar(permTaken.id.name, ast.Perm)(permsExp.pos, permsExp.info, permsExp.errT)
+        val permTakenExp = ast.LocalVar(permTaken.id.name.substring(0, permTaken.id.name.lastIndexOf("@")), ast.Perm)(permsExp.pos, permsExp.info, permsExp.errT)
 
         totalPermSum = PermPlus(totalPermSum, Ite(eq, ch.perm, NoPerm))
-        totalPermSumExp = ast.PermAdd(totalPermSumExp, buildIteExp(eq, ch.perm, NoPerm, eqExp, ch.permExp, ast.NoPerm()()))(permsExp.pos, permsExp.info, permsExp.errT)
+        totalPermSumExp = ast.PermAdd(totalPermSumExp, buildIteExp(eq, ch.perm, NoPerm, eqExp, ch.permExp, ast.NoPerm()(), ast.Perm))(permsExp.pos, permsExp.info, permsExp.errT)
         totalPermTaken = PermPlus(totalPermTaken, permTaken)
         totalPermTakenExp = ast.PermAdd(totalPermTakenExp, permTakenExp)(permsExp.pos, permsExp.info, permsExp.errT)
 
diff --git a/src/main/scala/rules/PredicateSupporter.scala b/src/main/scala/rules/PredicateSupporter.scala
index 05346ee1b..ad706f515 100644
--- a/src/main/scala/rules/PredicateSupporter.scala
+++ b/src/main/scala/rules/PredicateSupporter.scala
@@ -70,8 +70,8 @@ object predicateSupporter extends PredicateSupportRules {
       if (!Verifier.config.disableFunctionUnfoldTrigger()) {
         val predTrigger = App(s1a.predicateData(predicate).triggerFunction,
           snap.convert(terms.sorts.Snap) +: tArgs)
-        val eArgsString = eArgs.mkString(", ")
-        v1.decider.assume(predTrigger, new DebugExp(s"Predicate Trigger: ${predicate.name}($eArgsString)"))
+        val eArgsString = eArgs.map(s1a.substituteVarsInExp).mkString(", ")
+        v1.decider.assume(predTrigger, new DebugExp(s"PredicateTrigger(${predicate.name}($eArgsString))"))
       }
       val s2 = s1a.setConstrainable(constrainableWildcards, false)
       if (s2.qpPredicates.contains(predicate)) {
@@ -93,8 +93,8 @@ object predicateSupporter extends PredicateSupportRules {
           val (smDef1, smCache1) =
             quantifiedChunkSupporter.summarisingSnapshotMap(
               s2, predicate, s2.predicateFormalVarMap(predicate), relevantChunks, v1)
-          val eArgsString = eArgs.mkString(", ")
-          v1.decider.assume(PredicateTrigger(predicate.name, smDef1.sm, tArgs), new DebugExp(s"Predicate Trigger: ${predicate.name}($eArgsString)"))
+          val eArgsString = eArgs.map(s2.substituteVarsInExp).mkString(", ")
+          v1.decider.assume(PredicateTrigger(predicate.name, smDef1.sm, tArgs), new DebugExp(s"PredicateTrigger(${predicate.name}($eArgsString))"))
           smCache1
         } else {
           s2.smCache
@@ -156,8 +156,8 @@ object predicateSupporter extends PredicateSupportRules {
             val predicateTrigger =
               App(s4.predicateData(predicate).triggerFunction,
                 snap.convert(terms.sorts.Snap) +: tArgs)
-            val eargs = eArgs.map(e => s2.substituteVarsInExp(e)).mkString(", ")
-            v2.decider.assume(predicateTrigger, new DebugExp(s"Predicate Trigger ${predicate.name}($eargs)"))
+            val eargs = eArgs.map(s2.substituteVarsInExp).mkString(", ")
+            v2.decider.assume(predicateTrigger, new DebugExp(s"PredicateTrigger(${predicate.name}($eargs))"))
           }
           Q(s4.copy(g = s.g,
                     permissionScalingFactor = s.permissionScalingFactor,
@@ -176,7 +176,7 @@ object predicateSupporter extends PredicateSupportRules {
             val predicateTrigger =
               App(s4.predicateData(predicate).triggerFunction, snap +: tArgs)
             val eargs = eArgs.map(e => s2.substituteVarsInExp(e)).mkString(", ")
-            v2.decider.assume(predicateTrigger, new DebugExp(s"Predicate Trigger ${pa.predicateName}($eargs)"))
+            v2.decider.assume(predicateTrigger, new DebugExp(s"PredicateTrigger(${pa.predicateName}($eargs))"))
           }
           val s5 = 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 60d0b6d03..4c21b4741 100644
--- a/src/main/scala/rules/Producer.scala
+++ b/src/main/scala/rules/Producer.scala
@@ -292,8 +292,8 @@ object producer extends ProductionRules {
                 chunkSupporter.produce(s2, s2.h, ch, v2)((s3, h3, v3) => {
                   if (Verifier.config.enablePredicateTriggersOnInhale() && s3.functionRecorder == NoopFunctionRecorder
                     && !Verifier.config.disableFunctionUnfoldTrigger()) {
-                    val argsString = eArgs.map(e => s2.substituteVarsInExp(e)).mkString(", ")
-                    val debugExp = new DebugExp(s"Predicate Trigger ${predicate.name}($argsString)")
+                    val argsString = eArgs.map(s2.substituteVarsInExp).mkString(", ")
+                    val debugExp = new DebugExp(s"PredicateTrigger(${predicate.name}($argsString))")
                     v3.decider.assume(App(s3.predicateData(predicate).triggerFunction, snap1 +: tArgs), debugExp)
                   }
                   Q(s3.copy(h = h3), v3)})
@@ -321,8 +321,8 @@ object producer extends ProductionRules {
             val (smDef1, smCache1) =
               quantifiedChunkSupporter.summarisingSnapshotMap(
                 s1, wand, formalVars, relevantChunks, v1)
-            val argsStr = bodyVars.map(e => s1.substituteVarsInExp(e)).mkString(", ")
-            val debugExp = new DebugExp(s"Predicate Trigger ${ch.id.toString}($argsStr)")
+            val argsStr = bodyVars.map(s1.substituteVarsInExp).mkString(", ")
+            val debugExp = new DebugExp(s"PredicateTrigger(${ch.id.toString}($argsStr))")
             v1.decider.assume(PredicateTrigger(ch.id.toString, smDef1.sm, args), debugExp)
             smCache1
           } else {
diff --git a/src/main/scala/rules/StateConsolidator.scala b/src/main/scala/rules/StateConsolidator.scala
index 201e9a4c7..dcaf78234 100644
--- a/src/main/scala/rules/StateConsolidator.scala
+++ b/src/main/scala/rules/StateConsolidator.scala
@@ -25,8 +25,8 @@ import scala.annotation.unused
 trait StateConsolidationRules extends SymbolicExecutionRules {
   def consolidate(s: State, v: Verifier): State
   def consolidateIfRetrying(s: State, v: Verifier): State
-  def merge(fr: FunctionRecorder, h: Heap, newH: Heap, v: Verifier): (FunctionRecorder, Heap)
-  def merge(fr: FunctionRecorder, h: Heap, ch: NonQuantifiedChunk, v: Verifier): (FunctionRecorder, Heap)
+  def merge(fr: FunctionRecorder, s: State, h: Heap, newH: Heap, v: Verifier): (FunctionRecorder, Heap)
+  def merge(fr: FunctionRecorder, s: State, h: Heap, ch: NonQuantifiedChunk, v: Verifier): (FunctionRecorder, Heap)
 
   protected def assumeUpperPermissionBoundForQPFields(s: State, v: Verifier): State
   protected def assumeUpperPermissionBoundForQPFields(s: State, heaps: Seq[Heap], v: Verifier): State
@@ -41,10 +41,10 @@ class MinimalStateConsolidator extends StateConsolidationRules {
   def consolidate(s: State, @unused v: Verifier): State = s
   def consolidateIfRetrying(s: State, @unused v: Verifier): State = s
 
-  def merge(fr: FunctionRecorder, h: Heap, newH: Heap, v: Verifier): (FunctionRecorder, Heap) =
+  def merge(fr: FunctionRecorder, s: State, h: Heap, newH: Heap, v: Verifier): (FunctionRecorder, Heap) =
     (fr, Heap(h.values ++ newH.values))
 
-  def merge(fr: FunctionRecorder, h: Heap, ch: NonQuantifiedChunk, v: Verifier): (FunctionRecorder, Heap) =
+  def merge(fr: FunctionRecorder, s: State, h: Heap, ch: NonQuantifiedChunk, v: Verifier): (FunctionRecorder, Heap) =
     (fr, h + ch)
 
   protected def assumeUpperPermissionBoundForQPFields(s: State, @unused v: Verifier): State = s
@@ -125,11 +125,11 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol
     if (s.retrying) consolidate(s, v)
     else s
 
-  def merge(fr: FunctionRecorder, h: Heap, ch: NonQuantifiedChunk, v: Verifier): (FunctionRecorder, Heap) = {
-    merge(fr, h, Heap(Seq(ch)), v)
+  def merge(fr: FunctionRecorder, s: State, h: Heap, ch: NonQuantifiedChunk, v: Verifier): (FunctionRecorder, Heap) = {
+    merge(fr, s, h, Heap(Seq(ch)), v)
   }
 
-  def merge(fr1: FunctionRecorder, h: Heap, newH: Heap, v: Verifier): (FunctionRecorder, Heap) = {
+  def merge(fr1: FunctionRecorder, s: State, h: Heap, newH: Heap, v: Verifier): (FunctionRecorder, Heap) = {
     val mergeLog = new CommentRecord("Merge", null, v.decider.pcs)
     val sepIdentifier = v.symbExLog.openScope(mergeLog)
     val (nonQuantifiedChunks, otherChunks) = partition(h)
@@ -142,7 +142,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol
     newlyAddedChunks foreach { ch =>
       val resource = Resources.resourceDescriptions(ch.resourceID)
       val pathCond = interpreter.buildPathConditionsForChunk(ch, resource.instanceProperties)
-      pathCond.foreach(p => v.decider.assume(p.getFirst, new DebugExp(p.getSecond, p.getSecond))) // TODO ake: substitution?
+      pathCond.foreach(p => v.decider.assume(p.getFirst, new DebugExp(p.getSecond, s.substituteVarsInExp(p.getSecond))))
     }
 
     v.symbExLog.closeScope(sepIdentifier)
@@ -313,10 +313,10 @@ class RetryingStateConsolidator(config: Config) extends DefaultStateConsolidator
   *   - Merging heaps and assuming QP permission bounds is equivalent to [[MinimalStateConsolidator]]
   */
 class MinimalRetryingStateConsolidator(config: Config) extends RetryingStateConsolidator(config) {
-  override def merge(fr: FunctionRecorder, h: Heap, newH: Heap, v: Verifier): (FunctionRecorder, Heap) =
+  override def merge(fr: FunctionRecorder, s: State, h: Heap, newH: Heap, v: Verifier): (FunctionRecorder, Heap) =
     (fr, Heap(h.values ++ newH.values))
 
-  override def merge(fr: FunctionRecorder, h: Heap, ch: NonQuantifiedChunk, v: Verifier): (FunctionRecorder, Heap) =
+  override def merge(fr: FunctionRecorder, s: State, h: Heap, ch: NonQuantifiedChunk, v: Verifier): (FunctionRecorder, Heap) =
     (fr, h + ch)
 
   override protected def assumeUpperPermissionBoundForQPFields(s: State, @unused v: Verifier): State = s
diff --git a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala
index e9abdf49e..ddb6a43c0 100644
--- a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala
+++ b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala
@@ -251,8 +251,7 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver
             decider.assume(pcsPre, new DebugExp(s"precondition ${function.name}($argsName)", InsertionOrderedSet(preExp)))
             v.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract)
             eval(s1, body, FunctionNotWellformed(function), v)((s2, tBody, _) => {
-              val resultName = data.formalResult.toString
-              val e = ast.EqCmp(ast.LocalVar(resultName.substring(0, resultName.lastIndexOf("@")), function.typ)(), function.body.get)()
+              val e = ast.EqCmp(ast.Result(function.typ)(), function.body.get)(function.pos, function.info, function.errT)
               decider.assume(data.formalResult === tBody, new DebugExp(e, s2.substituteVarsInExp(e)))
               consumes(s2, posts, postconditionViolated, v)((s3, _, _) => {
                 recorders :+= s3.functionRecorder