diff --git a/silver b/silver
index d09e011fa..88dc6f913 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit d09e011fa313860d76316805c9c301c4540e5c6e
+Subproject commit 88dc6f913ba7ceb835c8ba973d8995f198683611
diff --git a/src/main/scala/debugger/DebugParser.scala b/src/main/scala/debugger/DebugParser.scala
new file mode 100644
index 000000000..5ab5f5c4f
--- /dev/null
+++ b/src/main/scala/debugger/DebugParser.scala
@@ -0,0 +1,59 @@
+package debugger
+
+import fastparse._
+import viper.silver.ast._
+import viper.silver.parser._
+
+import scala.collection.mutable
+class DebugParser extends FastParser {
+
+  def versionedIdentifier[$: P]: P[Unit] = CharIn("A-Z", "a-z", "$_") ~~ CharIn("0-9", "A-Z", "a-z", "$_").repX ~~ CharIn("@") ~~ CharIn("0-9") ~~ CharIn("0-9").repX
+
+  def versionedIdent[$: P]: P[String] = versionedIdentifier.!.opaque("versionedIdentifier")
+
+  def versionedidnuse[$: P]: P[PVersionedIdnUse] = FP(versionedIdent).map { case (pos, id) =>
+    val parts = id.split("@")
+    PVersionedIdnUse(name = parts(0), version = parts(1))(pos)
+  }
+
+  def debugOldLabel[$: P]: P[String] = (StringIn("line") ~~ CharIn("@") ~~ CharIn("0-9", "A-Z", "a-z", "$_.").repX).!.opaque("debugOldLabel")
+
+  def debugOldLabelUse[$: P]: P[PVersionedIdnUse] = FP(debugOldLabel).map { case (pos, id) =>
+    val parts = id.split("@")
+    PVersionedIdnUse(name = parts(0), version = parts(1))(pos)
+  }
+
+  def debugOld[$: P]: P[PExp] = P(StringIn("old") ~ FP("[" ~ debugOldLabelUse ~ "](" ~ exp ~ ")").map {
+    case (pos, (a, b)) => PDebugLabelledOld(a, b)(pos)
+  })
+
+  override def atom(implicit ctx: P[_]): P[PExp] = // TODO ake:
+    P(ParserExtension.newExpAtStart(ctx) | versionedidnuse
+    | debugOld
+    | annotatedAtom
+    | integer | booltrue | boolfalse | nul | old
+    | result | unExp | typedFuncApp
+    | "(" ~ exp ~ ")" | accessPred | inhaleExhale | perm | let | quant | forperm | unfolding | applying
+    | setTypedEmpty | explicitSetNonEmpty | multiSetTypedEmpty | explicitMultisetNonEmpty | seqTypedEmpty
+    | size | explicitSeqNonEmpty | seqRange
+    | mapTypedEmpty | explicitMapNonEmpty | mapDomain | mapRange
+    | newExp | funcApp | idnuse | ParserExtension.newExpAtEnd(ctx))
+}
+
+
+class DebugTranslator(p: PProgram, override val members: mutable.Map[String, Node]) extends Translator(p) {
+
+  override protected def expInternal(pexp: PExp, pos: PExp, info: Info): Exp = {
+    pexp match {
+      case pviu@PVersionedIdnUse(_, _, _) =>
+        pexp.typ match {
+          case null => sys.error("should not occur in type-checked program")
+          case _ => LocalVarWithVersion(pviu.versionedName, ttyp(pexp.typ))(pos, info)
+        }
+      case PDebugLabelledOld(lbl, e) =>
+        DebugLabelledOld(exp(e), lbl.versionedName)(pos, info)
+      case _ => super.expInternal(pexp, pos, info)
+    }
+  }
+
+}
diff --git a/src/main/scala/debugger/DebugTypechecker.scala b/src/main/scala/debugger/DebugTypechecker.scala
index b00fe2280..9525f775f 100644
--- a/src/main/scala/debugger/DebugTypechecker.scala
+++ b/src/main/scala/debugger/DebugTypechecker.scala
@@ -1,14 +1,37 @@
 package debugger
 
-import viper.silver.parser.{NameAnalyser, PProgram, Resolver, TypeChecker}
+import viper.silver.FastMessaging
+import viper.silver.parser._
 
+import scala.reflect.ClassTag
 
-class DebugResolver(override val p: PProgram) extends Resolver(p){
-  override val typechecker: TypeChecker = new DebugTypeChecker(names)
 
+class DebugResolver(override val p: PProgram, names: NameAnalyser) extends Resolver(p){
+  override val typechecker: DebugTypeChecker = new DebugTypeChecker(names)
 }
 
 class DebugTypeChecker(override val names: NameAnalyser) extends TypeChecker(names) {
+  var debugVariableTypes: Map[String, PType] = Map.empty
 
+  override def checkInternal(exp: PExp): Unit = {
+        exp match {
+          case pviu: PVersionedIdnUse =>
+            acceptAndCheckTypedEntityWithVersion[PAnyVarDecl, Nothing](Seq(pviu), "expected variable identifier with version")
+          case _ => super.checkInternal(exp)
+        }
+  }
+
+  def acceptAndCheckTypedEntityWithVersion[T1: ClassTag, T2: ClassTag]
+  (idnUses: Seq[PVersionedIdnUse], errorMessage: => String): Unit = {
+
+    idnUses.foreach { use =>
+      val decl1 = debugVariableTypes.get(use.versionedName)
+
+      decl1 match {
+        case Some(value) => use.typ = value
+        case None => messages ++= FastMessaging.message(use, errorMessage)
+      }
+    }
+  }
 
 }
diff --git a/src/main/scala/debugger/SiliconDebugger.scala b/src/main/scala/debugger/SiliconDebugger.scala
index e0503611c..45af269f4 100644
--- a/src/main/scala/debugger/SiliconDebugger.scala
+++ b/src/main/scala/debugger/SiliconDebugger.scala
@@ -12,8 +12,8 @@ import viper.silver.ast
 import viper.silver.ast._
 import viper.silver.parser._
 import viper.silver.reporter.{NoopReporter, Reporter}
-import viper.silver.verifier.{ErrorReason, PartialVerificationError}
 import viper.silver.verifier.errors.ContractNotWellformed
+import viper.silver.verifier.{ErrorReason, PartialVerificationError}
 
 import scala.io.StdIn.readLine
 import scala.language.postfixOps
@@ -26,7 +26,9 @@ case class ProofObligation(s: State,
                            assertion: Term,
                            eAssertion: ast.Exp,
                            printConfig: DebugExpPrintConfiguration,
-                           originalErrorReason: ErrorReason
+                           originalErrorReason: ErrorReason,
+                           resolver: DebugResolver,
+                           translator: DebugTranslator
                           ){
 
   def removeAssumptions(ids: Seq[Int]): ProofObligation = {
@@ -144,7 +146,8 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
       Some(ProofObligation(failureContext.state.get, failureContext.verifier.get, failureContext.proverDecls,
         failureContext.branchConditions, failureContext.assumptions,
         False /* TODO */ , failureContext.failedAssertion.getOrElse(ast.TrueLit()()),
-        new DebugExpPrintConfiguration, currResult.message.reason))
+        new DebugExpPrintConfiguration, currResult.message.reason,
+        new DebugResolver(this.pprogram, this.resolver.names), new DebugTranslator(this.pprogram, translator.getMembers())))
     }else{
       None
     }
@@ -161,12 +164,12 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
       failedPExp = failedPExp.get.parent
     }
     if(failedPExp.isDefined){
-      resolver.typechecker.curMember = failedPExp.get.asInstanceOf[PScope]
+      obl.resolver.typechecker.curMember = failedPExp.get.asInstanceOf[PScope]
     }else{
       println("Could not determine the scope for typechecking.")
     }
 
-    resolver.typechecker.debugVariableTypes =
+    obl.resolver.typechecker.debugVariableTypes =
       obl.v.decider.debugVariableTypes map { case (str, t) => (simplifyVariableName(str), typeToPType(t)) }
   }
 
@@ -236,7 +239,7 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
     if (userInput.isEmpty || userInput.equalsIgnoreCase("s") || userInput.equalsIgnoreCase("skip")) {
       obl
     } else {
-      val assumptionE = translateStringToExp(userInput)
+      val assumptionE = translateStringToExp(userInput, obl)
       val (_, _, _, resV) = evalAssumption(assumptionE, obl, obl.v)
       obl.copy(assumptionsExp = resV.decider.pcs.assumptionExps, v = resV)
     }
@@ -248,7 +251,7 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
     if (userInput.equalsIgnoreCase("s") || userInput.equalsIgnoreCase("skip")) {
       obl
     } else {
-      val assumptionE = translateStringToExp(userInput)
+      val assumptionE = translateStringToExp(userInput, obl)
       var resT: Term = null
       var resE: ast.Exp = null
       var resV: Verifier = null
@@ -269,10 +272,10 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
     }
   }
 
-  private def translateStringToExp(str: String): ast.Exp ={
+  private def translateStringToExp(str: String, obl: ProofObligation): ast.Exp ={
     def parseToPExp(): PExp = {
       try {
-        val fp = new FastParser()
+        val fp = new DebugParser()
         fp._line_offset = Seq(0, str.length + 1).toArray
         val parsedExp = fastparse.parse(str, fp.exp(_))
         parsedExp.get.value
@@ -284,7 +287,7 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
 
     def typecheckPExp(pexp: PExp): Unit = {
       try {
-        resolver.typechecker.check(pexp, PPrimitiv("Bool")())
+        obl.resolver.typechecker.check(pexp, PPrimitiv("Bool")())
       } catch {
         case e: Throwable => println(s"Error while typechecking $str: ${e.getMessage}")
           throw e
@@ -293,7 +296,7 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
 
     def translatePExp(pexp: PExp): ast.Exp = {
       try {
-        translator.exp(pexp)
+        obl.translator.exp(pexp)
       } catch {
         case e: Throwable => println(s"Error while translating $str: ${e.getMessage}")
           throw e
diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala
index d10d88b3e..e35483be4 100644
--- a/src/main/scala/rules/Evaluator.scala
+++ b/src/main/scala/rules/Evaluator.scala
@@ -1078,7 +1078,7 @@ object evaluator extends EvaluationRules {
         case _: ast.SetType => evalBinOp(s, e0, e1, SetIn, pve, v)((s1, t, e0New, e1New, v1)
           => Q(s1, t, ast.AnySetContains(e0New, e1New)(e.pos, e.info, e.errT), v1))
         case _: ast.MultisetType => evalBinOp(s, e0, e1, (t0, t1) => MultisetCount(t1, t0), pve, v)((s1, t, e0New, e1New, v1)
-          => Q(s1, t, ast.AnySetContains(e0New, e1New)(e.pos, e.info, e.errT), v1)) // TODO ake: multiset COUNT
+          => Q(s1, t, ast.AnySetContains(e0New, e1New)(e.pos, e.info, e.errT), v1))
         case _ => sys.error("Expected a (multi)set-typed expression but found %s (%s) of sort %s"
                             .format(e, e.getClass.getName, e.typ))
       }