Fixing old in triggers

src/main/scala/rules/Evaluator.scala

@@ -1093,11 +1093,32 @@ object evaluator extends EvaluationRules {
     val h = s.oldHeaps(label)
     val s1 = s.copy(h = h, partiallyConsumedHeap = None)
     val s2 = v.stateConsolidator.consolidateIfRetrying(s1, v)
+    val possibleTriggersBefore: Map[ast.Exp, Term] = if (s.recordPossibleTriggers) s.possibleTriggers else Map.empty
 
     eval(s2, e, pve, v)((s3, t, v1) => {
+      val newPossibleTriggers = if (s.recordPossibleTriggers) {
+        // For all new possible trigger expressions e and translated term t,
+        // make sure we remember t as the term for old[label](e) instead.
+        val addedOrChangedPairs = s3.possibleTriggers.filter(t =>
+          !possibleTriggersBefore.contains(t._1) || possibleTriggersBefore(t._1) != t._2)
+
+        def wrapInOld(e: ast.Exp) = {
+          if (label == "old") {
+            ast.Old(e)(e.pos, e.info, e.errT)
+          } else {
+            ast.LabelledOld(e, label)(e.pos, e.info, e.errT)
+          }
+        }
+
+        val oldPairs = addedOrChangedPairs.map(t => wrapInOld(t._1) -> t._2)
+        s.possibleTriggers ++ oldPairs
+      } else {
+        s.possibleTriggers
+      }
       val s4 = s3.copy(h = s.h,
                        oldHeaps = s3.oldHeaps + (label -> s3.h),
-                       partiallyConsumedHeap = s.partiallyConsumedHeap)
+                       partiallyConsumedHeap = s.partiallyConsumedHeap,
+                       possibleTriggers = newPossibleTriggers)
       Q(s4, t, v1)})
   }
 
@@ -1239,9 +1260,6 @@ object evaluator extends EvaluationRules {
 
     val (cachedTriggerTerms, remainingTriggerExpressions) =
       exps.map {
-        case ast.Old(e) => e /* TODO: What about heap-dependent functions under old in triggers? */
-        case e => e
-      }.map {
         case fapp: ast.FuncApp =>
           /** Heap-dependent functions that are used as tTriggerSets should be used
             * in the limited version, because it allows for more instantiations.
@@ -1259,7 +1277,18 @@ object evaluator extends EvaluationRules {
             }
 
           (cachedTrigger, if (cachedTrigger.isDefined) None else Some(fapp))
+        case o@ast.Old(fapp: ast.FuncApp) =>
+          val cachedTrigger =
+            s.possibleTriggers.get(o) map {
+              case app@App(fun: HeapDepFun, _) =>
+                app.copy(applicable = functionSupporter.limitedVersion(fun))
+              case app: App =>
+                app
+              case other =>
+                sys.error(s"Expected $fapp to map to a function application, but found $other")
+            }
 
+          (cachedTrigger, if (cachedTrigger.isDefined) None else Some(o))
         case pt @ (_: ast.PossibleTrigger | _: ast.FieldAccess) =>
           val cachedTrigger = s.possibleTriggers.get(pt)