diff --git a/silver b/silver
index ab75f0825..d6d3a540e 160000
--- a/silver
+++ b/silver
@@ -1 +1 @@
-Subproject commit ab75f08250897dc45841bee354cca1e84384d8e5
+Subproject commit d6d3a540eb7fff3cd98c1351d056da6ce7bfa6a3
diff --git a/src/main/resources/z3config.smt2 b/src/main/resources/z3config.smt2
index e76604147..945d5a6b7 100644
--- a/src/main/resources/z3config.smt2
+++ b/src/main/resources/z3config.smt2
@@ -25,6 +25,7 @@
 (set-option :smt.qi.eager_threshold 100)
 (set-option :smt.arith.solver 2)
 (set-option :model.v2 true)
+(set-option :model.partial true)
 
 ; We want unlimited multipatterns
 (set-option :smt.qi.max_multi_patterns 1000)
diff --git a/src/main/scala/reporting/Converter.scala b/src/main/scala/reporting/Converter.scala
index ed437f989..5ea3df3ed 100644
--- a/src/main/scala/reporting/Converter.scala
+++ b/src/main/scala/reporting/Converter.scala
@@ -251,12 +251,20 @@ object Converter {
     }
   }
 
-  def evaluateTerm(term: Term, model: Model): ExtractedModelEntry = {
+  /**
+    * Evaluates a Silicon term against the given SMT model. `env` binds (quantified) variables to
+    * already-evaluated values, which is used e.g. to evaluate a quantified chunk's permission and
+    * value terms for a concrete receiver. This is the single term-evaluation facility used by the
+    * counterexample machinery; it handles snapshots, function applications, boolean connectives,
+    * comparisons, collection membership, and permission arithmetic.
+    */
+  def evaluateTerm(term: Term, model: Model, env: Map[Var, ExtractedModelEntry] = Map.empty): ExtractedModelEntry = {
     term match {
       case Unit              => UnprocessedModelEntry(ConstantEntry(snapUnitId))
       case IntLiteral(x)     => LitIntEntry(x)
       case t: BooleanLiteral => LitBoolEntry(t.value)
       case Null              => VarEntry(model.entries(nullRefId).toString, sorts.Ref)
+      case v: Var if env.contains(v) => env(v)
       case Var(_, sort, _) =>
         val key: String = term.toString
         val entry: Option[ModelEntry] = model.entries.get(key)
@@ -277,7 +285,7 @@ object Converter {
         }
         val toSort = app.resultSort
         val argEntries: Seq[ExtractedModelEntry] = args
-          .map(t => evaluateTerm(t, model))
+          .map(t => evaluateTerm(t, model, env))
 
         val argsFinal = argEntries.map {
           case UnprocessedModelEntry(entry) => entry
@@ -286,13 +294,13 @@ object Converter {
         getFunctionValue(model, fname, argsFinal, toSort)
 
       case Combine(p0, p1) =>
-        val p0Eval = evaluateTerm(p0, model).asValueEntry
-        val p1Eval = evaluateTerm(p1, model).asValueEntry
+        val p0Eval = evaluateTerm(p0, model, env).asValueEntry
+        val p1Eval = evaluateTerm(p1, model, env).asValueEntry
         val entry = ApplicationEntry("$Snap.combine", Seq(p0Eval, p1Eval))
         UnprocessedModelEntry(entry)
 
       case First(p) =>
-        val sub = evaluateTerm(p, model)
+        val sub = evaluateTerm(p, model, env)
         sub match {
           case UnprocessedModelEntry(ApplicationEntry(name, args)) =>
             if (name == "$Snap.combine") {
@@ -305,7 +313,7 @@ object Converter {
         }
 
       case Second(p) =>
-        val sub = evaluateTerm(p, model)
+        val sub = evaluateTerm(p, model, env)
         sub match {
           case UnprocessedModelEntry(ApplicationEntry(name, args)) =>
             if (name == "$Snap.combine") {
@@ -318,7 +326,7 @@ object Converter {
         }
 
       case SortWrapper(t, to) =>
-        val sub = evaluateTerm(t, model)
+        val sub = evaluateTerm(t, model, env)
         val fromSortName: String = termconverter.convert(t.sort)
         val toSortName: String = termconverter.convert(to)
         val fname = s"$$SortWrappers.${fromSortName}To$toSortName"
@@ -334,14 +342,133 @@ object Converter {
       case PredicateLookup(predname, psf, args) =>
         val lookupFuncName: String = s"$$PSF.lookup_$predname"
         val snap = toSnapTree.apply(args)
-        val snapVal = evaluateTerm(snap, model).asValueEntry
-        val psfVal = evaluateTerm(psf, model).asValueEntry
+        val snapVal = evaluateTerm(snap, model, env).asValueEntry
+        val psfVal = evaluateTerm(psf, model, env).asValueEntry
         val arg = Seq(psfVal, snapVal)
         getFunctionValue(model, lookupFuncName, arg, sorts.Snap)
+
+      case l: Lookup =>
+        val toSort = l.fvf.sort match {
+          case fvfSort: sorts.FieldValueFunction => fvfSort.codomainSort
+          case _ => sorts.Snap
+        }
+        val fvfVal = evaluateTerm(l.fvf, model, env).asValueEntry
+        val atVal = evaluateTerm(l.at, model, env).asValueEntry
+        getFunctionValue(model, s"$$FVF.lookup_${l.field}", Seq(fvfVal, atVal), toSort)
+
+      case SeqLength(s) =>
+        getFunctionValue(model, "Seq_length", Seq(evaluateTerm(s, model, env).asValueEntry), sorts.Int)
+
+      case SetIn(e, s) =>
+        getFunctionValue(model, "Set_in", Seq(evaluateTerm(e, model, env).asValueEntry, evaluateTerm(s, model, env).asValueEntry), sorts.Bool)
+
+      case Ite(cond, thn, els) =>
+        evaluateTerm(cond, model, env) match {
+          case LitBoolEntry(true)  => evaluateTerm(thn, model, env)
+          case LitBoolEntry(false) => evaluateTerm(els, model, env)
+          case _                   => OtherEntry(term.toString, "condition not evaluable")
+        }
+
+      case Not(t0) =>
+        evaluateTerm(t0, model, env) match {
+          case LitBoolEntry(b) => LitBoolEntry(!b)
+          case _               => OtherEntry(term.toString, "not evaluable")
+        }
+      case And(ts) =>
+        val rs = ts.map(t0 => evaluateTerm(t0, model, env))
+        if (rs.exists { case LitBoolEntry(false) => true; case _ => false }) LitBoolEntry(false)
+        else if (rs.forall { case LitBoolEntry(true) => true; case _ => false }) LitBoolEntry(true)
+        else OtherEntry(term.toString, "not evaluable")
+      case Or(ts) =>
+        val rs = ts.map(t0 => evaluateTerm(t0, model, env))
+        if (rs.exists { case LitBoolEntry(true) => true; case _ => false }) LitBoolEntry(true)
+        else if (rs.forall { case LitBoolEntry(false) => true; case _ => false }) LitBoolEntry(false)
+        else OtherEntry(term.toString, "not evaluable")
+
+      case AtMost(t0, t1)  => intComparison(t0, t1, model, env)(_ <= _)
+      case AtLeast(t0, t1) => intComparison(t0, t1, model, env)(_ >= _)
+      case Less(t0, t1)    => intComparison(t0, t1, model, env)(_ < _)
+      case t: Greater      => intComparison(t.p0, t.p1, model, env)(_ > _)
+      case BuiltinEquals(t0, t1) =>
+        val e0 = evaluateTerm(t0, model, env)
+        val e1 = evaluateTerm(t1, model, env)
+        (e0, e1) match {
+          case (_: OtherEntry, _) | (_, _: OtherEntry) => OtherEntry(term.toString, "not evaluable")
+          case _                                       => LitBoolEntry(e0.toString == e1.toString)
+        }
+
+      case NoPerm                 => LitPermEntry(Rational.zero)
+      case FullPerm               => LitPermEntry(Rational.one)
+      case FractionPermLiteral(r) => LitPermEntry(Rational(r.numerator, r.denominator))
+      case FractionPerm(t0, t1) =>
+        (evaluateTerm(t0, model, env), evaluateTerm(t1, model, env)) match {
+          case (LitIntEntry(n), LitIntEntry(d)) if d != 0 => LitPermEntry(Rational(n, d))
+          case _                                          => OtherEntry(term.toString, "not evaluable")
+        }
+      case PermPlus(t0, t1)  => permArithmetic(t0, t1, model, env)(_ + _)
+      case PermMinus(t0, t1) => permArithmetic(t0, t1, model, env)(_ - _)
+      case PermTimes(t0, t1) => permArithmetic(t0, t1, model, env)(_ * _)
+      case PermMin(t0, t1)   => permArithmetic(t0, t1, model, env)((a, b) => if (a < b) a else b)
+
+      // Integer arithmetic. Div/Mod follow the SMT-LIB `div`/`mod` (Euclidean) semantics that
+      // Silicon translates them to, so the results agree with the solver's model.
+      case t: Plus  => intArithmetic(t.p0, t.p1, model, env)(_ + _)
+      case t: Minus => intArithmetic(t.p0, t.p1, model, env)(_ - _)
+      case t: Times => intArithmetic(t.p0, t.p1, model, env)(_ * _)
+      case t: Div   => intDivMod(t.p0, t.p1, model, env)(euclideanDiv)
+      case t: Mod   => intDivMod(t.p0, t.p1, model, env)(euclideanMod)
+
+      // Multiset containment: `e in ms` is the count of `e` in `ms`.
+      case t: MultisetCount =>
+        getFunctionValue(model, "Multiset_count",
+          Seq(evaluateTerm(t.p0, model, env).asValueEntry, evaluateTerm(t.p1, model, env).asValueEntry), sorts.Int)
+
+      // Map operations. `r in domain(m)` desugars to SetIn(r, MapDomain(m)), so evaluating the
+      // domain to its set value lets the existing SetIn case take over.
+      case t: MapDomain =>
+        getFunctionValue(model, "Map_domain", Seq(evaluateTerm(t.p, model, env).asValueEntry), t.sort)
+      case t: MapLookup =>
+        getFunctionValue(model, "Map_apply",
+          Seq(evaluateTerm(t.base, model, env).asValueEntry, evaluateTerm(t.key, model, env).asValueEntry), t.sort)
+      case t: MapCardinality =>
+        getFunctionValue(model, "Map_card", Seq(evaluateTerm(t.p, model, env).asValueEntry), sorts.Int)
+
       case _ => OtherEntry(term.toString, "unhandled")
     }
   }
 
+  private def euclideanMod(a: BigInt, b: BigInt): BigInt = { val r = a % b; if (r < 0) r + b.abs else r }
+  private def euclideanDiv(a: BigInt, b: BigInt): BigInt = (a - euclideanMod(a, b)) / b
+
+  private def intArithmetic(t0: Term, t1: Term, model: Model, env: Map[Var, ExtractedModelEntry])
+                           (op: (BigInt, BigInt) => BigInt): ExtractedModelEntry =
+    (evaluateTerm(t0, model, env), evaluateTerm(t1, model, env)) match {
+      case (LitIntEntry(a), LitIntEntry(b)) => LitIntEntry(op(a, b))
+      case _                                => OtherEntry(s"integer arithmetic on $t0 and $t1", "not evaluable")
+    }
+
+  private def intDivMod(t0: Term, t1: Term, model: Model, env: Map[Var, ExtractedModelEntry])
+                       (op: (BigInt, BigInt) => BigInt): ExtractedModelEntry =
+    (evaluateTerm(t0, model, env), evaluateTerm(t1, model, env)) match {
+      case (LitIntEntry(_), LitIntEntry(b)) if b == 0 => OtherEntry(s"division of $t0 by zero", "not evaluable")
+      case (LitIntEntry(a), LitIntEntry(b))           => LitIntEntry(op(a, b))
+      case _                                          => OtherEntry(s"division of $t0 by $t1", "not evaluable")
+    }
+
+  private def intComparison(t0: Term, t1: Term, model: Model, env: Map[Var, ExtractedModelEntry])
+                           (op: (BigInt, BigInt) => Boolean): ExtractedModelEntry =
+    (evaluateTerm(t0, model, env), evaluateTerm(t1, model, env)) match {
+      case (LitIntEntry(a), LitIntEntry(b)) => LitBoolEntry(op(a, b))
+      case _                                => OtherEntry(s"comparison of $t0 and $t1", "not evaluable")
+    }
+
+  private def permArithmetic(t0: Term, t1: Term, model: Model, env: Map[Var, ExtractedModelEntry])
+                            (op: (Rational, Rational) => Rational): ExtractedModelEntry =
+    (evaluateTerm(t0, model, env), evaluateTerm(t1, model, env)) match {
+      case (LitPermEntry(a), LitPermEntry(b)) => LitPermEntry(op(a, b))
+      case _                                  => OtherEntry(s"permission arithmetic on $t0 and $t1", "not evaluable")
+    }
+
   def extractHeap(h: Iterable[Chunk], model: Model): ExtractedHeap = {
     var entries: Vector[HeapEntry] = Vector()
     h foreach {
diff --git a/src/main/scala/reporting/SiliconResolvedCounterexample.scala b/src/main/scala/reporting/SiliconResolvedCounterexample.scala
new file mode 100644
index 000000000..9165962a2
--- /dev/null
+++ b/src/main/scala/reporting/SiliconResolvedCounterexample.scala
@@ -0,0 +1,1157 @@
+package viper.silicon.reporting
+
+import viper.silver.verifier.{ApplicationEntry, ConstantEntry, MapEntry, Model, ValueEntry}
+import viper.silver.ast.{CondExp, Exp, FieldAccessPredicate, LocalVar, Member, NeCmp, Predicate, Program, Resource, Type}
+import viper.silver.ast
+
+import scala.util.Try
+import viper.silicon.{Map, state => st}
+import viper.silicon.interfaces.state.Chunk
+import viper.silicon.resources.{FieldID, PredicateID}
+import viper.silicon.state.{BasicChunk, DefaultSymbolConverter, SimpleIdentifier, State, Store, SymbolConverter}
+import viper.silicon.state.terms._
+import viper.silicon.state._
+import viper.silicon.decider.TermToSMTLib2Converter
+import viper.silicon.interfaces.decider.TermConverter
+import viper.silicon.interfaces.SiliconCounterexample
+import viper.silicon.reporting.Converter.evaluateTerm
+import viper.silver.verifier._
+import viper.silver.verifier.Rational
+
+/**
+  * Transforms a counterexample returned by Boogie back to a Viper counterexample. The programmer can choose between an
+  * "intermediate" CE or an "extended" CE.
+  */
+
+/**
+  * CounterexampleGenerator class used for generating an "extended" CE.
+  */
+case class SiliconResolvedCounterexample(model: Model,
+                                         internalStore: Store,
+                                         heap: Iterable[Chunk],
+                                         oldHeaps: State.OldHeaps,
+                                         program: ast.Program) extends SiliconCounterexample with ResolvedCounterexample {
+  val rawCE = SiliconRawCounterexample(model, internalStore, heap, oldHeaps, program)
+
+  val (ceStore, refOcc) = SiliconResolvedCounterexample.detStore(internalStore, rawCE.basicVariables, rawCE.allCollections)
+  val nameTranslationMap = SiliconResolvedCounterexample.detTranslationMap(rawCE.basicVariables, rawCE.allCollections, refOcc)
+  val ceHeaps = rawCE.allRawHeaps.reverse.map(bh => (bh._1, SiliconResolvedCounterexample.detHeap(bh._2, program, rawCE.allCollections, nameTranslationMap, model)))
+
+  val domainEntries = SiliconResolvedCounterexample.detTranslatedDomains(rawCE.domainEntries, nameTranslationMap)
+  val functionEntries =  SiliconResolvedCounterexample.detTranslatedFunctions(rawCE.nonDomainFunctions, nameTranslationMap)
+
+  override def toString: String = {
+    var finalString = "      Resolved Counterexample: \n"
+    finalString += "   Store: \n"
+    if (!ceStore.storeEntries.isEmpty)
+      finalString += ceStore.storeEntries.map(x => x.toString).mkString("", "\n", "\n")
+    if (!ceHeaps.filter(y => !y._2.heapEntries.isEmpty).isEmpty)
+      finalString += ceHeaps.filter(y => !y._2.heapEntries.isEmpty).map(x => "   " + x._1 + " Heap: \n" + x._2.toString).mkString("")
+    if (domainsAndFunctions.nonEmpty) {
+      finalString += "   Domains: \n"
+      finalString += domainsAndFunctions.map(x => x.toString).mkString("", "\n", "\n")
+    }
+    finalString
+  }
+
+  override def withStore(s: Store): SiliconCounterexample = {
+    SiliconResolvedCounterexample(model, s, heap, oldHeaps, program)
+  }
+}
+
+/**
+  * CounterexampleGenerator class used for generating an "intermediate" CE.
+  */
+case class SiliconRawCounterexample(model: Model,
+                                             internalStore: Store,
+                                             heap: Iterable[Chunk],
+                                             oldHeaps: State.OldHeaps,
+                                             program: ast.Program) extends SiliconCounterexample with RawCounterexample {
+  val basicVariables: Seq[CEVariable] = SiliconRawCounterexample.detBasicVariables(model, internalStore)
+  val allSequences: Seq[CECollection] = SiliconRawCounterexample.detSequences(model)
+  val allSets: Seq[CECollection] = SiliconRawCounterexample.detSets(model)
+  val allMultisets: Seq[CECollection] = SiliconRawCounterexample.detMultisets(model)
+  val allMaps: Seq[CECollection] = SiliconRawCounterexample.detMaps(model)
+  var allRawHeaps: Seq[(String, RawHeap)] = Seq(("current", RawHeap(SiliconRawCounterexample.detHeap(model, heap, program.predicatesByName))))
+  oldHeaps.foreach {case (n, h) => allRawHeaps +:= ((n, RawHeap(SiliconRawCounterexample.detHeap(model, h.values, program.predicatesByName))))}
+
+  def rawHeaps: Seq[(String, RawHeap)] = allRawHeaps
+  val domainEntries: Seq[BasicDomainEntry] = SiliconRawCounterexample.getAllDomains(model, program)
+  val nonDomainFunctions: Seq[BasicFunctionEntry] = SiliconRawCounterexample.getAllFunctions(model, program)
+
+  override def toString: String = {
+    var finalString = "      Raw Counterexample: \n"
+    finalString ++= "   Local Information:\n"
+    if (!basicVariables.isEmpty)
+      finalString += basicVariables.map(x => x.toString).mkString("", "\n", "\n")
+    if (!allCollections.isEmpty)
+      finalString += allCollections.map(x => x.toString).mkString("", "\n", "\n")
+    if (!allRawHeaps.filter(y => !y._2.rawHeapEntries.isEmpty).isEmpty)
+      finalString += allRawHeaps.filter(y => !y._2.rawHeapEntries.isEmpty).map(x => "   " + x._1 + " Heap: \n" + x._2.toString).mkString("", "\n", "\n")
+    if (!domainEntries.isEmpty || !nonDomainFunctions.isEmpty)
+      finalString ++= "   Domains:\n"
+    if (!domainEntries.isEmpty)
+      finalString += domainEntries.map(x => x.toString).mkString("", "\n", "\n")
+    if (!nonDomainFunctions.isEmpty)
+      finalString += nonDomainFunctions.map(x => x.toString).mkString("", "\n", "\n")
+    finalString
+  }
+
+  override def withStore(s: Store): SiliconCounterexample = {
+    SiliconResolvedCounterexample(model, s, heap, oldHeaps, program).rawCE
+  }
+}
+
+object SiliconRawCounterexample {
+
+  /**
+    * Determines the local variables and their value.
+    */
+  def detBasicVariables(model: Model, store: Store): Seq[CEVariable] = {
+    var res = Seq[CEVariable]()
+    for ((k, (v, _)) <- store.values) {
+      if (v.toString.contains('@')) {
+        model.entries.get(v.toString) match {
+          case Some(x) =>
+            var varTyp: Option[Type] = None
+            if (k.isInstanceOf[LocalVar]) {
+              varTyp = Some(k.asInstanceOf[LocalVar].typ)
+            }
+            if (x.isInstanceOf[ConstantEntry]) {
+              res +:= CEVariable(k.name, CounterexampleValue.literal(x.toString, varTyp), varTyp)
+            } else if (x.isInstanceOf[ApplicationEntry]) {
+              res +:= CEVariable(k.name, CounterexampleValue.literal(x.toString, varTyp), varTyp)
+            } else {
+              println(s"Couldn't find a ConstantEntry or ApplicationEntry for the Variable: ${k.name}")
+            }
+          case None => //
+        }
+      } else {
+        var varTyp: Option[Type] = None
+        if (k.isInstanceOf[LocalVar]) {
+          varTyp = Some(k.asInstanceOf[LocalVar].typ)
+        }
+        res +:= CEVariable(k.name, CounterexampleValue.literal(v.toString, varTyp), varTyp)
+      }
+    }
+    if (model.entries.contains("$Ref.null")) {
+      val nullRef = model.entries.get("$Ref.null").get
+      if (nullRef.isInstanceOf[ConstantEntry]) {
+        res +:= CEVariable("null", CounterexampleValue.literal(nullRef.toString, Some(ast.Ref)), Some(ast.Ref))
+      }
+    }
+    res
+  }
+
+  /**
+    * Defines every sequence that can be extracted in the model. The entries of the sequences still consist of identifiers
+    * and are not assigned to their actual value. Additionally, not every sequence in the output set will be mentioned
+    * in the "extended" CE as only sequences that are used in the method containing the verification error will be mentioned there.
+    */
+  def detSequences(model: Model): Seq[CECollection] = {
+    var res = Map[String, Seq[String]]()
+    var tempMap = Map[(String, Seq[String]), String]()
+    for ((opName, opValues) <- model.entries) {
+      if (opName == "Seq_length") {
+        if (opValues.isInstanceOf[MapEntry]) {
+          for ((k, v) <- opValues.asInstanceOf[MapEntry].options) {
+            res += (k(0).toString -> Seq.fill(v.toString.toInt)("#undefined"))
+          }
+        }
+      } else if (opName == "Seq_empty") {
+        if (opValues.isInstanceOf[MapEntry]) {
+          for ((k, v) <- opValues.asInstanceOf[MapEntry].options) {
+            res += (v.toString -> Seq())
+          }
+        }
+      } else if (opName != "Seq_singleton" && opName != "Seq_range" && opName.startsWith("Seq_")) {
+        if (opValues.isInstanceOf[MapEntry]) {
+          for ((k, v) <- opValues.asInstanceOf[MapEntry].options) {
+            tempMap += ((opName, k.map(x => x.toString)) -> v.toString)
+          }
+        }
+      }
+    }
+    for ((opName, opValues) <- model.entries) {
+      if (opName == "Seq_singleton") {
+        if (opValues.isInstanceOf[MapEntry]) {
+          for ((k, v) <- opValues.asInstanceOf[MapEntry].options) {
+            res += (v.toString -> Seq(k(0).toString))
+          }
+        }
+      }
+      if (opName == "Seq_range") {
+        if (opValues.isInstanceOf[MapEntry]) {
+          for ((k, v) <- opValues.asInstanceOf[MapEntry].options) {
+            if (k(0).isInstanceOf[ConstantEntry] && k(1).isInstanceOf[ConstantEntry]) {
+              res += (v.toString -> Seq.range(k(0).toString.toInt, k(1).toString.toInt).map(x => x.toString))
+            }
+          }
+        }
+      }
+    }
+    var found = true
+    while (found) {
+      found = false
+      for (((opName, k), v) <- tempMap) {
+        if (opName == "Seq_append") {
+          (res.get(k(0)), res.get(k(1))) match {
+            case (Some(x), Some(y)) =>
+              if (!res.contains(v)) {
+                res += (v -> (x ++ y))
+                tempMap -= ((opName, k))
+                found = true
+              }
+            case (_, _) => //
+          }
+        } else if (opName == "Seq_take") {
+          res.get(k(0)) match {
+            case Some(x) =>
+              if (!k(1).startsWith("(")) {
+                res += (v -> x.take(k(1).toInt))
+              }
+              tempMap -= ((opName, k))
+              found = true
+            case _ => //
+          }
+        } else if (opName == "Seq_drop") {
+          res.get(k(0)) match {
+            case Some(x) =>
+              if (!k(1).startsWith("(")) {
+                res += (v -> x.drop(k(1).toInt))
+              }
+              tempMap -= ((opName, k))
+              found = true
+            case _ => //
+          }
+        } else if (opName == "Seq_index") {
+          res.get(k(0)) match {
+            case Some(x) =>
+              if (!k(1).startsWith("(") && (k(1).toInt < x.length)) {
+                res += (k(0) -> x.updated(k(1).toInt, v))
+              }
+              tempMap -= ((opName, k))
+              found = true
+            case _ => //
+          }
+        } else if (opName == "Seq_update") {
+          res.get(k(0)) match {
+            case Some(x) =>
+              if (!k(1).startsWith("(")) {
+                res += (v -> x.updated(k(1).toInt, k(2)))
+              }
+              tempMap -= ((opName, k))
+              found = true
+            case _ => //
+          }
+        }
+      }
+    }
+    var ans = Seq[CECollection]()
+    res.foreach {
+      case (n, s) =>
+        val elemTyp: Option[Type] = detASTTypeFromString(n.replaceAll(".*?<(.*)>.*", "$1"))
+        val elems = s.map(e => CounterexampleValue.literal(e, elemTyp))
+        val value = if (elems.isEmpty) ast.EmptySeq(elemTyp.getOrElse(ast.InternalType))() else ast.ExplicitSeq(elems)()
+        ans +:= CECollection(n, value)
+    }
+    ans
+  }
+
+  /**
+    * Defines every set that can be extracted in the model. The entries of the sets still consist of identifiers
+    * and are not assigned to their actual value. Additionally, not every set in the output set will be mentioned
+    * in the "extended" CE as only sets that are used in the method containing the verification error will be mentioned there.
+    */
+  def detSets(model: Model): Seq[CECollection] = {
+    var res = Map[String, Set[String]]()
+    for ((opName, opValues) <- model.entries) {
+      if (opName == "Set_empty") {
+        if (opValues.isInstanceOf[MapEntry]) {
+          for ((k, v) <- opValues.asInstanceOf[MapEntry].options) {
+            res += (v.toString -> Set())
+          }
+        } else if (opValues.isInstanceOf[ConstantEntry] && opValues.asInstanceOf[ConstantEntry].value != "false" && opValues.asInstanceOf[ConstantEntry].value != "true") {
+          res += (opValues.asInstanceOf[ConstantEntry].value -> Set())
+        }
+      }
+      if (opName == "Set_singleton") {
+        if (opValues.isInstanceOf[MapEntry]) {
+          for ((k, v) <- opValues.asInstanceOf[MapEntry].options) {
+            res += (v.toString -> Set(k(0).toString))
+          }
+        }
+      }
+      if (opName == "Set_card") {
+        if (opValues.isInstanceOf[MapEntry]) {
+          for ((k, v) <- opValues.asInstanceOf[MapEntry].options) {
+            if (v.toString.startsWith("0")) {
+              res += (k(0).toString -> Set())
+            }
+          }
+        }
+      }
+    }
+    var tempMap = Map[(String, Seq[String]), String]()
+    for ((opName, opValues) <- model.entries) {
+      if (opName == "Set_unionone" || opName == "Set_in") {
+        if (opValues.isInstanceOf[MapEntry]) {
+          for ((k, v) <- opValues.asInstanceOf[MapEntry].options) {
+            tempMap += ((opName, k.map(x => x.toString)) -> v.toString)
+          }
+        }
+      }
+    }
+    while (!tempMap.isEmpty) {
+      for (((opName, k), v) <- tempMap) {
+        if (opName == "Set_unionone") {
+          res.get(k(0)) match {
+            case Some(x) =>
+              res += (v -> x.union(Set(k(1))))
+              tempMap -= ((opName, k))
+            case None => //
+          }
+        } else if (opName == "Set_in") {
+          res.get(k(1)) match {
+            case Some(x) =>
+              if (v.toBoolean) {
+                res += (k(1) -> x.union(Set(k(0))))
+              }
+            case None =>
+              if (v.toBoolean) {
+                res += (k(1) -> Set(k(0)))
+              }
+          }
+          tempMap -= ((opName, k))
+        }
+      }
+    }
+    for ((opName, opValues) <- model.entries) {
+      if (opName == "Set_union" || opName == "Set_difference" || opName == "Set_intersection") {
+        if (opValues.isInstanceOf[MapEntry]) {
+          for ((k, v) <- opValues.asInstanceOf[MapEntry].options) {
+            tempMap += ((opName, k.map(x => x.toString)) -> v.toString)
+          }
+        }
+      }
+    }
+    while (!tempMap.isEmpty) {
+      for (((opName, k), v) <- tempMap) {
+        val firstSet = res.get(k(0))
+        val secondSet = res.get(k(1))
+        if (firstSet.isDefined && secondSet.isDefined) {
+          if (opName == "Set_union") {
+            res += (v -> firstSet.get.union(secondSet.get))
+            tempMap -= ((opName, k))
+          } else if (opName == "Set_intersection") {
+            res += (v -> firstSet.get.intersect(secondSet.get))
+            tempMap -= ((opName, k))
+          } else if (opName == "Set_difference") {
+            res += (v -> firstSet.get.diff(secondSet.get))
+            tempMap -= ((opName, k))
+          }
+        }
+      }
+    }
+    var ans = Seq[CECollection]()
+    res.foreach {
+      case (n, s) =>
+        val elemTyp: Option[Type] = detASTTypeFromString(n.replaceAll(".*?<(.*)>.*", "$1"))
+        val elems = s.filter(_ != "#undefined").toSeq.map(e => CounterexampleValue.literal(e, elemTyp))
+        val value = if (elems.isEmpty) ast.EmptySet(elemTyp.getOrElse(ast.InternalType))() else ast.ExplicitSet(elems)()
+        ans +:= CECollection(n, value)
+    }
+    ans
+  }
+
+  /**
+    * Defines every multiset that can be extracted in the model. The entries of the multisets still consist of identifiers
+    * and are not assigned to their actual value. Additionally, not every multiset in the output set will be mentioned
+    * in the "extended" CE as only multisets that are used in the method containing the verification error will be mentioned there.
+    */
+  def detMultisets(model: Model): Seq[CECollection] = {
+    var res = Map[String, scala.collection.immutable.Map[String, Int]]()
+    for ((opName, opValues) <- model.entries) {
+      if (opName == "Multiset_empty") {
+        if (opValues.isInstanceOf[MapEntry]) {
+          for ((_, v) <- opValues.asInstanceOf[MapEntry].options) {
+            res += (v.toString -> Map[String, Int]())
+          }
+        } else if (opValues.isInstanceOf[ConstantEntry] && opValues.asInstanceOf[ConstantEntry].value != "false" && opValues.asInstanceOf[ConstantEntry].value != "true") {
+          res += (opValues.asInstanceOf[ConstantEntry].value -> Map[String, Int]())
+        }
+      }
+      if (opName == "Multiset_singleton") {
+        if (opValues.isInstanceOf[MapEntry]) {
+          for ((k, v) <- opValues.asInstanceOf[MapEntry].options) {
+            res += (v.toString -> Map(k(0).toString -> 1))
+          }
+        }
+      }
+      if (opName == "Multiset_count") {
+        if (opValues.isInstanceOf[MapEntry]) {
+          for ((k, v) <- opValues.asInstanceOf[MapEntry].options) {
+            if (!v.toString.startsWith("0")) {
+              res += (k(0).toString -> res.getOrElse(k(0).toString, scala.collection.immutable.Map.empty).updated(k(1).toString, v.toString.toInt))
+            }
+          }
+        }
+      }
+      if (opName == "Multiset_card") {
+        if (opValues.isInstanceOf[MapEntry]) {
+          for ((k, v) <- opValues.asInstanceOf[MapEntry].options) {
+            if (v.toString.startsWith("0")) {
+              res += (k(0).toString -> Map[String, Int]())
+            }
+          }
+        }
+      }
+    }
+    var tempMap = Map[(String, Seq[String]), String]()
+    for ((opName, opValues) <- model.entries) {
+      if (opName == "Multiset_unionone") {
+        if (opValues.isInstanceOf[MapEntry]) {
+          for ((k, v) <- opValues.asInstanceOf[MapEntry].options) {
+            tempMap += ((opName, k.map(x => x.toString)) -> v.toString)
+          }
+        }
+      }
+    }
+    while (!tempMap.isEmpty) {
+      for (((opName, k), v) <- tempMap) {
+        res.get(k(0)) match {
+          case Some(x) =>
+            res += (v -> x.updated(k(1), x.getOrElse(k(1), 0) + 1))
+            tempMap -= ((opName, k))
+          case None => //
+        }
+      }
+    }
+    for ((opName, opValues) <- model.entries) {
+      if (opName == "Multiset_union" || opName == "Multiset_difference" || opName == "Multiset_intersection") {
+        if (opValues.isInstanceOf[MapEntry]) {
+          for ((k, v) <- opValues.asInstanceOf[MapEntry].options) {
+            tempMap += ((opName, k.map(x => x.toString)) -> v.toString)
+          }
+        }
+      }
+    }
+    while (!tempMap.isEmpty) {
+      for (((opName, k), v) <- tempMap) {
+        val firstMultiset = res.get(k(0))
+        val secondMultiset = res.get(k(1))
+        if ((firstMultiset != None) && (secondMultiset != None)) {
+          if (opName == "Multiset_union") {
+            res += (v -> (firstMultiset.get.keySet ++ secondMultiset.get.keySet).map { key =>
+              (key -> (firstMultiset.get.getOrElse(key, 0) + secondMultiset.get.getOrElse(key, 0)))
+            }.toMap)
+            tempMap -= ((opName, k))
+          } else if (opName == "Multiset_intersection") {
+            res += (v -> (firstMultiset.get.keySet & secondMultiset.get.keySet).map { key =>
+              key -> Math.min(firstMultiset.get.get(key).get, secondMultiset.get.get(key).get)
+            }.toMap)
+            tempMap -= ((opName, k))
+          } else if (opName == "Multiset_difference") {
+            res += (v -> (firstMultiset.get.map { case (key, count) =>
+              key -> (count - secondMultiset.get.getOrElse(key, 0))
+            }.filter(_._2 > 0) ++ secondMultiset.get.filter { case (key, _) =>
+              !firstMultiset.get.contains(key)
+            }))
+            tempMap -= ((opName, k))
+          }
+        }
+      }
+    }
+    var ans = Seq[CECollection]()
+    res.foreach {
+      case (n, s) =>
+        val elemTyp: Option[Type] = detASTTypeFromString(n.replaceAll(".*?<(.*)>.*", "$1"))
+        val elems = s.toSeq.flatMap { case (e, count) => Seq.fill(count)(CounterexampleValue.literal(e, elemTyp)) }
+        val value = if (elems.isEmpty) ast.EmptyMultiset(elemTyp.getOrElse(ast.InternalType))() else ast.ExplicitMultiset(elems)()
+        ans +:= CECollection(n, value)
+    }
+    ans
+  }
+
+  /**
+    * Reconstructs map values from the model, analogously to [[detSets]]. A map is built up from the
+    * empty map `Map_empty()` by a chain of updates `Map_update(m, k, v)`, each of which adds (or
+    * overwrites) the binding k -> v. The key/value types are taken from the map sort name when
+    * available (e.g. `Map<Int~_Int>`), otherwise the key/value literals are inferred.
+    */
+  def detMaps(model: Model): Seq[CECollection] = {
+    var res = Map[String, scala.collection.immutable.Map[String, String]]()
+    // Seed empty maps: Map_empty is the empty map for some key/value sort, and any map whose
+    // cardinality is zero is empty as well.
+    for ((opName, opValues) <- model.entries) {
+      if (opName == "Map_empty") {
+        opValues match {
+          case me: MapEntry => for ((_, v) <- me.options) res += (v.toString -> scala.collection.immutable.Map.empty)
+          case ce: ConstantEntry if ce.value != "false" && ce.value != "true" => res += (ce.value -> scala.collection.immutable.Map.empty)
+          case _ =>
+        }
+      }
+      if (opName == "Map_card") {
+        opValues match {
+          case me: MapEntry => for ((k, v) <- me.options) if (v.toString.startsWith("0")) res += (k(0).toString -> scala.collection.immutable.Map.empty)
+          case _ =>
+        }
+      }
+    }
+    // Collect the update facts Map_update(base, key, value) = result.
+    var tempMap = Map[Seq[String], String]()
+    for ((opName, opValues) <- model.entries) {
+      if (opName == "Map_update") {
+        opValues match {
+          case me: MapEntry => for ((k, v) <- me.options) tempMap += (k.map(x => x.toString) -> v.toString)
+          case _ =>
+        }
+      }
+    }
+    // Apply updates to a fixpoint: a result map becomes known as soon as its base map is known.
+    var progress = true
+    while (tempMap.nonEmpty && progress) {
+      progress = false
+      for ((k, v) <- tempMap) {
+        res.get(k(0)) match {
+          case Some(base) =>
+            res += (v -> base.updated(k(1), k(2)))
+            tempMap -= k
+            progress = true
+          case None => //
+        }
+      }
+    }
+    // Maps that are not built from an update chain (e.g. a bare parameter constrained only via
+    // `m[k] == v` / `k in domain(m)`) have no entry above. Reconstruct them the way partial sets are
+    // recovered from membership: the domain `Map_domain(m)` is a set whose members come from `Set_in`
+    // facts, and for each such key `Map_apply(m, k)` gives the value. Only keys that are both in the
+    // domain and have a known value are shown (analogous to a set only listing its known members).
+    val mapDomain = model.entries.get("Map_domain") match {
+      case Some(me: MapEntry) => me.options.collect { case (k, v) if k.nonEmpty => (k(0).toString, v.toString) }
+      case _ => Map.empty[String, String]
+    }
+    if (mapDomain.nonEmpty) {
+      val setMembers = model.entries.get("Set_in") match {
+        case Some(me: MapEntry) =>
+          me.options.toSeq.collect { case (k, v) if v.toString == "true" && k.length >= 2 => (k(1).toString, k(0).toString) }
+            .groupMap(_._1)(_._2).view.mapValues(_.toSet).toMap
+        case _ => Map.empty[String, Set[String]]
+      }
+      val mapApply = model.entries.get("Map_apply") match {
+        case Some(me: MapEntry) => me.options.collect { case (k, v) if k.length >= 2 => ((k(0).toString, k(1).toString), v.toString) }
+        case _ => Map.empty[(String, String), String]
+      }
+      for ((mapId, domainSetId) <- mapDomain if !res.contains(mapId)) {
+        val entries = setMembers.getOrElse(domainSetId, Set.empty).flatMap(key =>
+          mapApply.get((mapId, key)).map(value => key -> value)).toMap
+        res += (mapId -> entries)
+      }
+    }
+    var ans = Seq[CECollection]()
+    res.foreach {
+      case (n, m) =>
+        val (keyTyp, valueTyp) = detMapTypesFromString(n.replaceAll(".*?<(.*)>.*", "$1"))
+        val maplets: Seq[ast.Exp] = m.toSeq.map { case (k, v) =>
+          ast.Maplet(CounterexampleValue.literal(k, keyTyp), CounterexampleValue.literal(v, valueTyp))()
+        }
+        val value = if (maplets.isEmpty) ast.EmptyMap(keyTyp.getOrElse(ast.InternalType), valueTyp.getOrElse(ast.InternalType))()
+                    else ast.ExplicitMap(maplets)()
+        ans +:= CECollection(n, value)
+    }
+    ans
+  }
+
+  /**
+    * Splits the inner part of a map sort name (e.g. `Int~_Int`) into its key and value types at the
+    * top-level `~_` separator, ignoring `~_` that occurs inside nested type arguments. Returns
+    * (None, None) when the types cannot be determined (e.g. Boogie value ids that carry no type).
+    */
+  def detMapTypesFromString(inner: String): (Option[Type], Option[Type]) = {
+    var depth = 0
+    var i = 0
+    while (i + 1 < inner.length) {
+      inner(i) match {
+        case '<' | '[' => depth += 1
+        case '>' | ']' => depth -= 1
+        case '~' if depth == 0 && inner(i + 1) == '_' =>
+          return (detASTTypeFromString(inner.substring(0, i)), detASTTypeFromString(inner.substring(i + 2)))
+        case _ =>
+      }
+      i += 1
+    }
+    (None, None)
+  }
+
+  /**
+    * Translates a string identifier to an actual AST Viper Type.
+    */
+  def detASTTypeFromString(typ: String): Option[Type] = {
+    typ match {
+      case "Int" => Some(ast.Int)
+      case "Bool" => Some(ast.Bool)
+      case "Perm" => Some(ast.Perm)
+      case "Ref" => Some(ast.Ref)
+      case _ => None
+    }
+  }
+
+  /**
+    * Transforms the Heap Chunks to their Viper heap types.
+    */
+  def detHeap(model: Model, h: Iterable[Chunk], predByName: scala.collection.immutable.Map[String, Predicate]): Set[RawHeapEntry] = {
+    var heap = Set[RawHeapEntry]()
+    // Quantified field permissions are computed per receiver and summed across all quantified
+    // field chunks for the same (receiver, field) location, so that e.g. two separate quantified
+    // permissions covering the same location report their combined permission amount.
+    val qpFields = scala.collection.mutable.LinkedHashMap[(String, String), (Rational, String)]()
+    // Quantified predicate permissions are likewise computed per argument tuple and summed across
+    // all quantified predicate chunks for the same (predicate, arguments) instance.
+    val qpPreds = scala.collection.mutable.LinkedHashMap[(String, Seq[String]), Rational]()
+    h foreach {
+      case c@BasicChunk(FieldID, _, _, _, _, _, _, _) =>
+        heap += detField(model, c)
+      case c@BasicChunk(PredicateID, _, _, _, _, _, _, _) =>
+        heap += detPredicate(model, c, predByName)
+      case c@BasicChunk(id, _, _, _, _, _, _, _) =>
+        println("This Basic Chunk couldn't be matched as a CE heap entry!")
+      case c: st.QuantifiedFieldChunk =>
+        for ((recv, value, perm) <- detQPFieldEntries(c, model)) {
+          val key = (recv, c.id.name)
+          val prev = qpFields.get(key)
+          val summedPerm = prev.map(_._1).getOrElse(Rational.zero) + perm
+          val knownValue = prev.map(_._2).filter(_ != "#undefined").getOrElse(value)
+          qpFields(key) = (summedPerm, knownValue)
+        }
+      case c: st.QuantifiedPredicateChunk =>
+        for ((args, perm) <- detQPPredEntries(c, model)) {
+          val key = (c.id.name, args)
+          qpPreds(key) = qpPreds.get(key).getOrElse(Rational.zero) + perm
+        }
+      case c@MagicWandChunk(_, _, _, _, _, _, _) =>
+        heap += detMagicWand(model, c)
+      case _ => //println("This case is not supported in detHeap")
+    }
+    for (((recv, field), (perm, value)) <- qpFields) {
+      heap += RawHeapEntry(Seq(recv), Seq(field), value, Some(perm), QPFieldType, None)
+    }
+    for (((predName, args), perm) <- qpPreds) {
+      heap += RawHeapEntry(Seq(predName), args, "#undefined", Some(perm), QPPredicateType, None)
+    }
+    heap
+  }
+
+  /**
+    * Extracts, for a single quantified field chunk, the concrete (receiver, value, permission)
+    * triples it contributes to the counterexample. Candidate receivers are the argument values for
+    * which the SMT model instantiated the chunk's inverse/image functions; for each such receiver
+    * `r` the chunk's permission term is evaluated with the quantified variable bound to `r`.
+    */
+  def detQPFieldEntries(c: st.QuantifiedFieldChunk, model: Model): Seq[(String, String, Rational)] = {
+    val qvar = c.quantifiedVars.head
+    // Candidate receivers are the argument values for which the model instantiated the chunk's
+    // inverse/image functions (the receiver is the last argument of each such application).
+    val invImgNames = c.invs.toSeq.flatMap(i => (i.inverses ++ i.images).map(_.id.toString))
+    var receivers: Set[String] = invImgNames.flatMap { fn =>
+      model.entries.get(fn) match {
+        case Some(MapEntry(m, _)) => m.keys.flatMap(_.lastOption).map(_.toString)
+        case _ => Seq.empty[String]
+      }
+    }.toSet
+    if (receivers.isEmpty) {
+      c.singletonRcvr.map(t => evaluateTerm(t, model).asValueEntry.toString).foreach(r => receivers += r)
+    }
+    receivers.toSeq.flatMap { r =>
+      val env = Map[Var, ExtractedModelEntry](qvar -> UnprocessedModelEntry(ConstantEntry(r)))
+      evaluateTerm(c.perm, model, env) match {
+        case LitPermEntry(p) =>
+          // LitPermEntry uses viper.silver.utility.Common.Rational; counterexamples use viper.silver.verifier.Rational.
+          val perm = Rational(p.numerator, p.denominator)
+          if (perm > Rational.zero) {
+            val value = evaluateTerm(c.valueAt(qvar), model, env) match {
+              case _: OtherEntry => "#undefined"
+              case e => e.toString
+            }
+            Some((r, value, perm))
+          } else None
+        case _ => None
+      }
+    }
+  }
+
+  /**
+    * Extracts, for a single quantified predicate chunk, the (arguments, permission) pairs it
+    * contributes. Candidate argument tuples are the keys for which the model instantiated the
+    * chunk's inverse/image functions; for each tuple the chunk's permission term is evaluated with
+    * the quantified variables bound to the tuple's values.
+    */
+  def detQPPredEntries(c: st.QuantifiedPredicateChunk, model: Model): Seq[(Seq[String], Rational)] = {
+    val qvars = c.quantifiedVars
+    val invImgNames = c.invs.toSeq.flatMap(i => (i.inverses ++ i.images).map(_.id.toString))
+    var argTuples: Set[Seq[String]] = invImgNames.flatMap { fn =>
+      model.entries.get(fn) match {
+        case Some(MapEntry(m, _)) => m.keys.map(_.map(_.toString))
+        case _ => Seq.empty[Seq[String]]
+      }
+    }.toSet
+    if (argTuples.isEmpty) {
+      c.singletonArguments.map(_.map(t => evaluateTerm(t, model).asValueEntry.toString)).foreach(t => argTuples += t)
+    }
+    argTuples.toSeq.flatMap { tuple =>
+      if (tuple.length < qvars.length) None
+      else {
+        val env = Map[Var, ExtractedModelEntry](qvars.zip(tuple).map { case (qv, v) => qv -> UnprocessedModelEntry(ConstantEntry(v)) }: _*)
+        evaluateTerm(c.perm, model, env) match {
+          case LitPermEntry(p) =>
+            val perm = Rational(p.numerator, p.denominator)
+            if (perm > Rational.zero) Some((tuple.take(qvars.length), perm)) else None
+          case _ => None
+        }
+      }
+    }
+  }
+
+  def detField(model: Model, chunk: BasicChunk): RawHeapEntry = {
+    val recvVar = evaluateTerm(chunk.args(0), model).toString
+    val fieldName = chunk.id.name
+    val value = evaluateTerm(chunk.snap, model).toString
+    val perm = evalPerm(chunk.perm, model)
+    RawHeapEntry(Seq(recvVar), Seq(fieldName), value, perm, FieldType, None)
+  }
+
+  def detPredicate(model: Model, chunk: BasicChunk, predByName: scala.collection.immutable.Map[String, Predicate]): RawHeapEntry = {
+    val predName = chunk.id.name
+    val references = chunk.args.map(x => evaluateTerm(x, model))
+    var snap: Seq[ModelEntry] = Seq()
+    if (chunk.snap.isInstanceOf[First] || chunk.snap.isInstanceOf[Second] || chunk.snap.isInstanceOf[Var] || chunk.snap.isInstanceOf[Combine]) {
+      snap = evalSnap(chunk.snap, model: Model)
+    }
+    val astPred = predByName.get(predName)
+    val insidePredicateMap = evalInsidePredicate(snap, astPred)
+    val perm = evalPerm(chunk.perm, model)
+    RawHeapEntry(Seq(predName), references.map(x => x.toString), chunk.snap.toString, perm, PredicateType, Some(insidePredicateMap))
+  }
+
+  /**
+    * Evaluate the snapshot of a predicate.
+    */
+  def evalInsidePredicate(snap: Seq[ModelEntry], astPred: Option[Predicate]): scala.collection.immutable.Map[Exp, ModelEntry] = {
+    var ans = scala.collection.immutable.Map[Exp, ModelEntry]()
+    if (astPred.isDefined && !astPred.get.isAbstract) {
+      val predBody = astPred.get.body.get
+      val insPred = snapToBody(predBody, snap)
+      if (snap.length == 0 || (snap.length == 1 && (snap(0).toString.startsWith("$Snap") || snap(0).toString.startsWith("($Snap")))) {
+        ans = scala.collection.immutable.Map[Exp, ModelEntry]()
+      } else {
+        var assignedPredBody = scala.collection.immutable.Map[Exp, ModelEntry]()
+        for ((exp, value) <- insPred) {
+          if (value.toString.startsWith("$Snap") || value.toString.startsWith("($Snap")) {
+            assignedPredBody += evalBody(exp, UnspecifiedEntry, assignedPredBody)
+          } else {
+            assignedPredBody += evalBody(exp, value, assignedPredBody)
+          }
+        }
+        ans = assignedPredBody
+      }
+    }
+    ans
+  }
+
+  /**
+    * Compare the snapshot of a predicate to its actual body (accessed through its ast node).
+    */
+  def evalBody(exp: Exp, value: ModelEntry, lookup: scala.collection.immutable.Map[Exp, ModelEntry]): (Exp, ModelEntry) = {
+    exp match {
+      case FieldAccessPredicate(predAcc, _) => (predAcc, value)
+      case CondExp(cond, thn, els) =>
+        if (evalExp(cond, lookup)) {
+          evalBody(thn, value, lookup)
+        } else {
+          evalBody(els, value, lookup)
+        }
+      case ast.Implies(left, right) =>
+        if (evalExp(left, lookup)) {
+          evalBody(right, value, lookup)
+        } else {
+          (left, ConstantEntry("False"))
+        }
+      case _ => (exp, value)
+    }
+  }
+
+  def evalExp(exp: Exp, lookup: scala.collection.immutable.Map[Exp, ModelEntry]): Boolean = exp match {
+    case NeCmp(left, right) => !(lookup.getOrElse(left, ConstantEntry(left.toString)).toString.equalsIgnoreCase(lookup.getOrElse(right, ConstantEntry(right.toString)).toString))
+    case ast.EqCmp(left, right) => (lookup.getOrElse(left, ConstantEntry(left.toString)).toString.equalsIgnoreCase(lookup.getOrElse(right, ConstantEntry(right.toString)).toString))
+    case _ => false
+  }
+
+  def snapToBody(body: Exp, snap: Seq[ModelEntry]): Seq[(Exp, ModelEntry)] = {
+    if (snap.length == 0) {
+      Seq()
+    } else if (snap.length == 1) {
+      Seq((body, snap(0)))
+    } else {
+      if (body.subExps.length == 2) {
+        Seq((body.subExps(0), snap(0))) ++ snapToBody(body.subExps(1), snap.tail)
+      } else {
+        Seq()
+      }
+    }
+  }
+
+  def evalSnap(term: Term, model: Model): Seq[ModelEntry] = term match {
+    case First(t) =>
+      val subSnap = evalSnap(t, model)
+      if (subSnap(0).isInstanceOf[ApplicationEntry]) {
+        Seq(subSnap(0).asInstanceOf[ApplicationEntry].arguments(0))
+      } else {
+        Seq(UnspecifiedEntry)
+      }
+    case Second(t) =>
+      val subSnap = evalSnap(t, model)
+      if (subSnap(0).isInstanceOf[ApplicationEntry]) {
+        Seq(subSnap(0).asInstanceOf[ApplicationEntry].arguments(1))
+      } else {
+        Seq(UnspecifiedEntry)
+      }
+    case Combine(t1, t2) => evalSnap(t1, model) ++ evalSnap(t2, model)
+    case Var(id, _, _) => Seq(model.entries.getOrElse(id.name, UnspecifiedEntry))
+    case SortWrapper(t, s) => Seq(ConstantEntry(t.toString))
+    case _ => Seq(UnspecifiedEntry)
+  }
+
+  def detMagicWand(model: Model, chunk: MagicWandChunk): RawHeapEntry = {
+    val name = chunk.id.toString
+    var args = Seq[String]()
+    for (x <- chunk.args) {
+      val tempArg = evaluateTerm(x, model)
+      var arg = tempArg.toString
+      if (tempArg.isInstanceOf[OtherEntry]) {
+        if (evalTermToModelEntry(x, model).isDefined) {
+          arg = evalTermToModelEntry(x, model).get.toString
+        } else if (evalPerm(x, model).isDefined) {
+          arg = evalPerm(x, model).get.toString
+        } else {
+          arg = x.toString
+        }
+      }
+      args ++= Seq(arg)
+    }
+    val perm = evalPerm(chunk.perm, model)
+    RawHeapEntry(Seq(name), args, "#undefined", perm, MagicWandType, None)
+  }
+
+  /**
+    * Evaluates a permission-sorted term to a rational by delegating to the shared term evaluator
+    * ([[Converter.evaluateTerm]]).
+    */
+  def evalPerm(value: Term, model: Model): Option[Rational] = evaluateTerm(value, model) match {
+    case LitPermEntry(r) => Some(Rational(r.numerator, r.denominator))
+    case _ => None
+  }
+
+  /**
+    * Evaluates a Term to a value of the counterexample from the SMT solver.
+    */
+  def evalTermToModelEntry(value: Term, model: Model): Option[ModelEntry] = {
+    value match {
+      case v: Var =>
+        if (v.id.name.contains("@")) {
+          model.entries.get(v.id.name)
+        } else {
+          Some(ConstantEntry(v.id.name))
+        }
+      case a: App =>
+        if (model.entries.get(a.applicable.id.toString).isDefined && model.entries.get(a.applicable.id.toString).get.isInstanceOf[MapEntry]) {
+          val tempMap = model.entries.get(a.applicable.id.toString).get.asInstanceOf[MapEntry].options
+          tempMap.get(a.args.map(t => ConstantEntry(t.toString)))
+        } else {
+          None
+        }
+      case SeqLength(t) =>
+        val seqName = model.entries.get(t.toString)
+        val tempMap = model.entries.get("Seq_length")
+        if (seqName.isDefined && tempMap.isDefined && tempMap.get.isInstanceOf[MapEntry]) {
+          tempMap.get.asInstanceOf[MapEntry].options.get(Seq(ConstantEntry(seqName.get.toString)))
+        } else {
+          None
+        }
+      case IntLiteral(t) => Some(ConstantEntry(t.intValue.toString))
+      case SeqTake(t0, t1) =>
+        if (evalTermToModelEntry(t0, model).isDefined) {
+          Some(ConstantEntry(evalTermToModelEntry(t0, model).toString ++ " at idx " ++ t1.toString))
+        } else {
+          None
+        }
+      case SeqAt(t0, t1) => None
+      case _ => None
+    }
+  }
+
+  lazy val termconverter: TermConverter[String, String, String] = {
+    val conv = new TermToSMTLib2Converter()
+    conv.start()
+    conv
+  }
+  lazy val symbolConverter: SymbolConverter = new DefaultSymbolConverter
+  lazy val snapUnitId: String = termconverter.convert(Unit)
+  lazy val nullRefId: String = termconverter.convert(Null)
+
+  /**
+    * Extracts domains from a program. Only the ones that are used in the program... no generics.
+    * It also extracts all instances (translates the generics to concrete values).
+    */
+  def getAllDomains(model: Model, program: ast.Program): Seq[BasicDomainEntry] = {
+    val domains = program.collect {
+      case a: ast.Domain => a
+    }
+    val concreteDomains = program.collect { // find all definitive type instances
+      case ast.DomainType(n, map) => (n, map)
+      case d: ast.DomainFuncApp => (d.domainName, d.typVarMap) // sometimes we use a function without having an actual member of this...
+
+    }.filterNot(x => x._2.values.toSeq.exists(y => y.isInstanceOf[ast.TypeVar])).toSet // make sure we have all possible mappings without duplicates
+
+    val doms: Seq[(ast.Domain, scala.collection.immutable.Map[ast.TypeVar, Type])] = domains.flatMap(x =>
+      if (x.typVars == Nil) {
+        Seq((x, Map.empty[ast.TypeVar, ast.Type]))
+      } else {
+        concreteDomains.filter(_._1 == x.name).map(y => (x, y._2))
+      }).toSeq
+    var domainEntries = Seq[BasicDomainEntry]()
+    for ((dom, typeMap) <- doms) {
+      val types = try {
+        dom.typVars.map(typeMap)
+      } catch {
+        case _: Throwable => Seq()
+      }
+      val translatedFunctions = dom.functions.map(y => detFunction(model, y, typeMap, program, false))
+      domainEntries +:= BasicDomainEntry(dom.name, types, translatedFunctions)
+    }
+    domainEntries
+  }
+
+  /**
+    * Extract all the functions occuring inside of a domain.
+    */
+  def getAllFunctions(model: Model, program: ast.Program): Seq[BasicFunctionEntry] = {
+    val funcs = program.collect {
+      case f: ast.Function => f
+    }
+    funcs.map(x => detFunction(model, x, Map.empty, program, true)).toSeq
+  }
+
+  /**
+    * Determine all the inputs and outputs combinations of a function occruing the counterexample model.
+    */
+  def detFunction(model: Model, func: ast.FuncLike, genmap: scala.collection.immutable.Map[ast.TypeVar, ast.Type], program: ast.Program, hd: Boolean): BasicFunctionEntry = {
+    def toSort(typ: ast.Type): Either[Throwable, Sort] = Try(symbolConverter.toSort(typ)).toEither
+    def toSortWithSubstitutions(typ: ast.Type, typeErrorMsg: String): Either[String, Sort] = {
+      toSort(typ)
+        .left
+        .flatMap(_ => typ match {
+          case x: ast.GenericType => toSort(x.substitute(genmap)).left.map(_ => typeErrorMsg)
+          case t: ast.TypeVar => toSort(genmap.apply(t)).left.map(_ => typeErrorMsg)
+          case _ => Left("type not resolvable")
+        })
+    }
+    val fname = func.name
+    val resTyp: ast.Type = func.typ
+    val argTyp: Seq[ast.Type] = func.formalArgs.map(x => x.typ)
+    val keys = model.entries.keys
+    var (argSortErrors, argSort) = func.formalArgs
+      .map(x => toSortWithSubstitutions(x.typ, s"typeError in arg type ${x.typ}"))
+      .partitionMap(identity)
+    if (argSortErrors.nonEmpty) {
+      return BasicFunctionEntry("ERROR", argTyp, resTyp, Map.empty, s"$fname ${argSortErrors.head}")
+    }
+    val resSort = toSortWithSubstitutions(resTyp, s"typeError in return type $resTyp")
+      .fold(err => {
+        return BasicFunctionEntry("ERROR", argTyp, resTyp, Map.empty, s"$fname $err")
+      }, identity)
+    val smtfunc = func match {
+      case t: ast.Function => symbolConverter.toFunction(t).id
+      case t@ast.BackendFunc(_, _, _, _) => symbolConverter.toFunction(t, program).id
+      case t: ast.DomainFunc => symbolConverter.toFunction(t, argSort :+ resSort, program).id
+    }
+    val kek = smtfunc.toString
+      .replace("[", "<")
+      .replace("]", ">")
+      .replace(", ", "~_")
+    val modelfname = try {
+      (keys.filter(_.contains(fname + "%limited")) ++ keys.filter(_ == fname) ++ keys.filter(_ == kek)).head
+    } catch {
+      case _: Throwable => return BasicFunctionEntry("ERROR", argTyp, resTyp, Map.empty, s"$fname model function not found")
+    }
+    var heapStateList = Map[ValueEntry, String]()
+    var heapStateCounter = 0
+    def getTranslatedEntry(x: ValueEntry) : String = {
+      if (x.toString.startsWith("$")) {
+        if (heapStateList.contains(x)) {
+          heapStateList.get(x).get
+        } else {
+          val heapStateName = "Heap@" + heapStateCounter.toString
+          heapStateCounter += 1
+          heapStateList += (x -> heapStateName)
+          heapStateName
+        }
+      } else {
+        x.toString
+      }
+    }
+    model.entries.get(modelfname) match {
+      case Some(MapEntry(m, els)) =>
+        var options = Map[Seq[String], String]()
+        if (hd) {
+          for ((k, v) <- m) {
+            val temp = k.tail.map(x => heapStateList.getOrElse(x, x.toString))
+            options += (Seq(getTranslatedEntry(k.head)) ++ temp -> v.toString)
+          }
+        } else {
+          for ((k, v) <- m) {
+            val temp: Seq[String] = k.map(x => heapStateList.getOrElse(x, x.toString))
+            options += (temp -> v.toString)
+          }
+        }
+        BasicFunctionEntry(fname, argTyp, resTyp, options, els.toString)
+      case Some(ConstantEntry(t)) => BasicFunctionEntry(fname, argTyp, resTyp, Map.empty, t)
+      case Some(ApplicationEntry(n, args)) => BasicFunctionEntry(fname, argTyp, resTyp, Map.empty, ApplicationEntry(n, args).toString)
+      case Some(x) => BasicFunctionEntry(fname, argTyp, resTyp, Map.empty, x.toString)
+      case None => BasicFunctionEntry(fname, argTyp, resTyp, Map.empty, "#undefined")
+    }
+  }
+}
+
+object SiliconResolvedCounterexample {
+  /**
+    * Combine a local variable with its ast node.
+    */
+  def detStore(store: Store, variables: Seq[CEVariable], collections: Seq[CECollection]): (StoreCounterexample, Map[String, (String, Int)])  = {
+    var refOccurences = Map[String, (String, Int)]()
+    var ans = Seq[StoreEntry]()
+    for ((k, _) <- store.values) {
+      for (vari <- variables) {
+        if (k.name == vari.name) {
+          if (k.typ == ast.Ref) {
+            if (refOccurences.get(vari.value.toString).isDefined) {
+              val (n, i) = refOccurences.get(vari.value.toString).get
+              if (n != k.name) {
+                refOccurences += (vari.value.toString -> (k.name, i + 1))
+              }
+            } else {
+              refOccurences += (vari.value.toString -> (k.name, 1))
+            }
+          }
+          var found = false
+          for (coll <- collections) {
+            if (vari.value.toString == coll.id) {
+              ans +:= StoreEntry(k, coll.value)
+              found = true
+            }
+          }
+          if (!found) {
+            ans +:= StoreEntry(k, vari.value)
+          }
+        }
+      }
+    }
+    (StoreCounterexample(ans), refOccurences)
+  }
+
+  /**
+    * Match the collection type for the "extended" CE.
+    */
+  def detTranslationMap(variables: Seq[CEVariable], collections: Seq[CECollection], fields: Map[String, (String, Int)]): Map[String, String] = {
+    var namesTranslation = Map[String, String]()
+    for (vari <- variables) {
+      collections.find(_.id == vari.value.toString) match {
+        case Some(coll) =>
+          val suffix = vari.typ match {
+            case Some(_: ast.SeqType) => " (Seq)"
+            case Some(_: ast.SetType) => " (Set)"
+            case Some(_: ast.MultisetType) => " (MultiSet)"
+            case _ => ""
+          }
+          namesTranslation += (coll.id -> (vari.name + suffix))
+        case None => //
+      }
+    }
+    for ((k, v) <- fields) {
+      if (v._2 == 1) {
+        namesTranslation += (k -> v._1)
+      }
+    }
+    namesTranslation
+  }
+
+  def replace(expression: Exp, repl: scala.collection.immutable.Map[Exp, Exp]): Exp = {
+    repl.get(expression) match {
+      case Some(replacement) => replacement
+      case None =>
+        if (expression.subExps.isEmpty) {
+          expression
+        } else {
+          expression
+          //expression.subExps.map(x => replace(x, repl))
+        }
+    }
+  }
+
+  /**
+    * Match heap resources to their ast node and translate all identifiers (for fields and references)
+    */
+  def detHeap(basicHeap: RawHeap, program: Program, collections: Seq[CECollection], translNames: Map[String, String], model: Model): HeapCounterexample = {
+    var ans = Seq[(Resource, ResolvedHeapEntry)]()
+    for (bhe <- basicHeap.rawHeapEntries) {
+      bhe.het match {
+        case FieldType | QPFieldType =>
+          for ((fn, fv) <- program.fieldsByName) {
+            if (fn == bhe.field.head) {
+              collections.find(_.id == bhe.valueID) match {
+                case Some(coll) =>
+                  ans +:= (fv, FieldResolvedEntry(bhe.reference.head, bhe.field.head, coll.value, bhe.perm, fv.typ, bhe.het))
+                case None =>
+                  ans +:= (fv, FieldResolvedEntry(bhe.reference.head, bhe.field.head, CounterexampleValue.literal(bhe.valueID, Some(fv.typ)), bhe.perm, fv.typ, bhe.het))
+              }
+            }
+          }
+        case PredicateType | QPPredicateType =>
+          for ((pn, pv) <- program.predicatesByName) {
+            if (pn == bhe.reference.head) {
+              val argExps = bhe.field.zip(pv.formalArgs).map { case (v, fa) => CounterexampleValue.literal(v, Some(fa.typ)) }
+              var translatedArgs: Option[scala.collection.immutable.Map[Exp, ModelEntry]] = bhe.insidePredicate
+              if (bhe.insidePredicate.isDefined) {
+                translatedArgs = Some(bhe.insidePredicate.get.map{case (k,v) => (k, ConstantEntry(translNames.getOrElse(v.toString, model.entries.getOrElse(v.toString, v).toString)))})
+              }
+              ans +:= (pv, PredResolvedEntry(bhe.reference.head, argExps, bhe.perm, translatedArgs, bhe.het))
+            }
+          }
+        case MagicWandType | QPMagicWandType =>
+          val argValues: Seq[String] = bhe.field.map(x => translNames.getOrElse(x, x))
+          for ((mw, idx) <- program.magicWandStructures.zipWithIndex) {
+            val wandName = "wand@" ++ idx.toString
+            if (bhe.reference(0) == wandName) {
+              ans +:= (mw, WandResolvedEntry.fromStructure(wandName, mw, argValues, bhe.perm, bhe.het, program))
+            }
+          }
+        case _ => println("This type of heap entry could not be matched correctly!")
+      }
+    }
+    HeapCounterexample(ans)
+  }
+
+  def detTranslatedDomains(domEntries: Seq[BasicDomainEntry], namesMap: Map[String, String]): Seq[BasicDomainEntry] = {
+    domEntries.map(de => BasicDomainEntry(de.name, de.types, detTranslatedFunctions(de.functions, namesMap)))
+  }
+
+  def detTranslatedFunctions(funEntries: Seq[BasicFunctionEntry], namesMap: Map[String, String]): Seq[BasicFunctionEntry] = {
+    funEntries.map(bf => detNameTranslationOfFunction(bf, namesMap))
+  }
+
+  def detNameTranslationOfFunction(fun: BasicFunctionEntry, namesMap: Map[String, String]): BasicFunctionEntry = {
+    val translatedFun = fun.options.map { case (in, out) =>
+      (in.map(intName => namesMap.getOrElse(intName, intName)), namesMap.getOrElse(out, out))
+    }
+    val translatedEls = namesMap.getOrElse(fun.default, fun.default)
+    BasicFunctionEntry(fun.fname, fun.argtypes, fun.returnType, translatedFun, translatedEls)
+  }
+}
\ No newline at end of file
diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala
index 6d20c6909..a0b388f05 100644
--- a/src/main/scala/rules/QuantifiedChunkSupport.scala
+++ b/src/main/scala/rules/QuantifiedChunkSupport.scala
@@ -1568,7 +1568,10 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
       // converting to a Z3 term.
       // During function verification, we should not define macros, since they could contain resullt, which is not
       // defined elsewhere.
-      val declareMacro = s.functionRecorder == NoopFunctionRecorder // && !Verifier.config.useFlyweight
+      // Inline pTaken (instead of defining a macro) when a counterexample is requested, so that the
+      // chunk's permission term contains proper permission arithmetic the counterexample machinery
+      // can evaluate, rather than an opaque macro application.
+      val declareMacro = s.functionRecorder == NoopFunctionRecorder && Verifier.config.counterexample.toOption.isEmpty // && !Verifier.config.useFlyweight
 
       val permsProvided = ch.perm
       val permsProvidedExp = ch.permExp
diff --git a/src/main/scala/rules/SymbolicExecutionRules.scala b/src/main/scala/rules/SymbolicExecutionRules.scala
index 34655667d..2387311e2 100644
--- a/src/main/scala/rules/SymbolicExecutionRules.scala
+++ b/src/main/scala/rules/SymbolicExecutionRules.scala
@@ -8,11 +8,12 @@ package viper.silicon.rules
 
 import viper.silicon.debugger.DebugExp
 import viper.silicon.interfaces.{Failure, SiliconDebuggingFailureContext, SiliconFailureContext, SiliconMappedCounterexample, SiliconNativeCounterexample, SiliconVariableCounterexample}
+import viper.silicon.reporting.SiliconResolvedCounterexample
 import viper.silicon.state.State
 import viper.silicon.state.terms.{False, Term}
 import viper.silicon.verifier.Verifier
+import viper.silver.frontend.{ResolvedModel, RawModel, MappedModel, NativeModel, VariablesModel}
 import viper.silver.ast
-import viper.silver.frontend.{MappedModel, NativeModel, VariablesModel}
 import viper.silver.verifier.errors.ErrorWrapperWithExampleTransformer
 import viper.silver.verifier.{Counterexample, CounterexampleTransformer, VerificationError}
 import viper.silver.reporter.BlockFailureMessage
@@ -82,6 +83,8 @@ trait SymbolicExecutionRules {
             SiliconVariableCounterexample(s.g, nativeModel)
           case MappedModel =>
             SiliconMappedCounterexample(s.g, s.h.values, s.oldHeaps, nativeModel, s.program)
+          case RawModel => SiliconResolvedCounterexample(nativeModel, s.g, s.h.values, s.oldHeaps, s.program).rawCE
+          case ResolvedModel => SiliconResolvedCounterexample(nativeModel, s.g, s.h.values, s.oldHeaps, s.program)
         }
         val finalCE = ceTrafo match {
           case Some(trafo) => trafo.f(ce)
diff --git a/src/test/resources/counterexamples/cyclic-ref.vpr b/src/test/resources/counterexamples/cyclic-ref.vpr
deleted file mode 100644
index d7d0ef13e..000000000
--- a/src/test/resources/counterexamples/cyclic-ref.vpr
+++ /dev/null
@@ -1,13 +0,0 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
-field next: Ref
-
-method foo(a: Ref, b: Ref)
-  requires acc(a.next) && acc(b.next)
-{
-  a.next := b
-  b.next := a
-  //:: ExpectedCounterexample(assert.failed:assertion.false, (a.next.next == a, b == b.next.next))
-  assert(false)
-}
diff --git a/src/test/resources/counterexamples/functions.vpr b/src/test/resources/counterexamples/functions.vpr
deleted file mode 100644
index 7cff7b254..000000000
--- a/src/test/resources/counterexamples/functions.vpr
+++ /dev/null
@@ -1,16 +0,0 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
-function foo(z: Int): Int
-{
-  42
-}
-
-method bar()
-  requires foo(3) == 42
-{
-  var x: Int := 5
-  var y: Int := foo(x)
-  //:: ExpectedCounterexample(assert.failed:assertion.false, (x == 5, y == 42))
-  assert(false)
-}
diff --git a/src/test/resources/counterexamples/lseg.vpr b/src/test/resources/counterexamples/lseg.vpr
deleted file mode 100644
index 3efc72126..000000000
--- a/src/test/resources/counterexamples/lseg.vpr
+++ /dev/null
@@ -1,27 +0,0 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
-field elem : Int
-field next : Ref
-
-predicate lseg(first: Ref, last: Ref, values: Seq[Int])
-{
-  first != last ==>
-    acc(first.elem) && acc(first.next) &&
-    0 < |values| &&
-    first.elem == values[0] &&
-    lseg(first.next, last, values[1..])
-}
-
-method removeFirst(first: Ref, last: Ref, values: Seq[Int]) returns  (value: Int, second: Ref)
-  requires lseg(first, last, values)
-  requires first != last
-  ensures  lseg(second, last, values[1..])
-  // we have insufficient field permissions when second is equal to last:
-  //:: ExpectedCounterexample(not.wellformed:insufficient.permission, (second == last))
-  ensures  value != unfolding lseg(second, last, values[1..]) in second.elem
-{
-  unfold lseg(first, last, values)
-  value := first.elem
-  second := first.next
-}
diff --git a/src/test/resources/counterexamples/method-call.vpr b/src/test/resources/counterexamples/method-call.vpr
deleted file mode 100644
index c4a197b01..000000000
--- a/src/test/resources/counterexamples/method-call.vpr
+++ /dev/null
@@ -1,19 +0,0 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
-field f: Int
-
-method client(a: Ref)
-  requires acc(a.f)
-{
-  //:: ExpectedCounterexample(call.precondition:assertion.false, (a.f == 5))
-  set(a, 5)
-  a.f := 6
-}
-
-method set(x: Ref, i: Int)
-  requires acc(x.f) && x.f != i
-  ensures  acc(x.f) && x.f == i
-{
-  x.f := i
-}
diff --git a/src/test/resources/counterexamples/negative.vpr b/src/test/resources/counterexamples/negative.vpr
deleted file mode 100644
index 036b8599b..000000000
--- a/src/test/resources/counterexamples/negative.vpr
+++ /dev/null
@@ -1,10 +0,0 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
-method fun(x:Int)
-  requires x == 42
-{
-  var y: Int := -x
-  //:: ExpectedCounterexample(assert.failed:assertion.false, (x == 42, y == -42))
-  assert(false)
-}
diff --git a/src/test/resources/counterexamples/permissions.vpr b/src/test/resources/counterexamples/permissions.vpr
deleted file mode 100644
index 0a46448af..000000000
--- a/src/test/resources/counterexamples/permissions.vpr
+++ /dev/null
@@ -1,11 +0,0 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
-field f: Int
-
-method foo(x: Ref, y: Ref)
-  requires acc(x.f, 1/2) && acc(y.f, 1/2)
-{
-  //:: ExpectedCounterexample(assignment.failed:insufficient.permission, (acc(x.f, 1/2)))
-  x.f := y.f * 2 + 2
-}
diff --git a/src/test/resources/counterexamples/predicate.vpr b/src/test/resources/counterexamples/predicate.vpr
deleted file mode 100644
index 6d5df8aef..000000000
--- a/src/test/resources/counterexamples/predicate.vpr
+++ /dev/null
@@ -1,27 +0,0 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
-field x: Int
-field y: Int
-
-predicate StructA(this: Ref) {
-  acc(this.x) && acc(this.y)
-}
-
-predicate StructB(this: Ref) {
-  acc(this.x) && acc(this.y)
-}
-
-method foo(a: Ref, b: Ref)
-  requires StructA(a)
-  requires StructB(b)
-  //:: ExpectedCounterexample(postcondition.violated:assertion.false, (a.x == 3))
-  ensures  acc(a.x) && a.x == 42
-{
-  unfold StructA(a)
-  unfold StructB(b)
-  a.x := 3
-  a.y := 4
-  b.x := 5
-  b.y := 6
-}
diff --git a/src/test/resources/counterexamples/ref-sequence.vpr b/src/test/resources/counterexamples/ref-sequence.vpr
deleted file mode 100644
index 858a38372..000000000
--- a/src/test/resources/counterexamples/ref-sequence.vpr
+++ /dev/null
@@ -1,12 +0,0 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
-field seq: Seq[Int]
-
-method foo(x: Ref) returns (value: Int)
-  requires acc(x.seq) && |x.seq| > 1
-  //:: ExpectedCounterexample(postcondition.violated:assertion.false, (x.seq[1] == 42))
-  ensures  value != 42
-{
-  value := x.seq[1]
-}
diff --git a/src/test/resources/counterexamples/sequence.vpr b/src/test/resources/counterexamples/sequence.vpr
deleted file mode 100644
index 2f9770447..000000000
--- a/src/test/resources/counterexamples/sequence.vpr
+++ /dev/null
@@ -1,14 +0,0 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
-method update(values: Seq[Int]) returns (updatedValues: Seq[Int])
-  requires |values| > 3
-  ensures  |values| == |updatedValues|
-  ensures  updatedValues[0] != updatedValues[1]
-  //:: ExpectedCounterexample(postcondition.violated:assertion.false, (updatedValues[1] == 42, updatedValues[2] == 42))
-  ensures  updatedValues[1] != updatedValues[2]
-{
-  updatedValues := values[0 := 0]
-  updatedValues := updatedValues[1 := 42]
-  updatedValues := updatedValues[2 := 42]
-}
diff --git a/src/test/resources/counterexamples/simple-refs-rec.vpr b/src/test/resources/counterexamples/simple-refs-rec.vpr
deleted file mode 100644
index 81082fab8..000000000
--- a/src/test/resources/counterexamples/simple-refs-rec.vpr
+++ /dev/null
@@ -1,27 +0,0 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
-field left: Int
-field right: Int
-field next: Ref
-field valid: Bool
-
-method simple(x: Ref, y: Ref, z: Ref, r: Int) returns (n: Int)
-  requires acc(x.left) && acc(x.right)
-  requires acc(y.left) && acc(y.right)
-  requires acc(z.next) && acc(z.next.right)
-  requires acc(x.valid) && x.valid
-  requires r == 155
-  requires y.left == 3 && y.right == 4
-  requires x.left == 42 && x.right > 52
-  requires z.next.right == 12
-  //:: ExpectedCounterexample(postcondition.violated:assertion.false, (n == 42))
-  ensures  n == 1
-{
-  n := x.left
-  var b: Bool := false
-  var s: Int := 99
-  label ret
-  x.left := 101
-  x.right := 201
-}
diff --git a/src/test/resources/counterexamples/simple-refs.vpr b/src/test/resources/counterexamples/simple-refs.vpr
deleted file mode 100644
index e098b63f4..000000000
--- a/src/test/resources/counterexamples/simple-refs.vpr
+++ /dev/null
@@ -1,21 +0,0 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
-field left: Int
-field right: Int
-
-method simple(x: Ref, y: Ref) returns (n:Int)
-  requires acc(x.left) && acc(x.right)
-  requires acc(y.left) && acc(y.right)
-  requires y.left == 3 && y.right == 4
-  requires x.left == 42 && x.right > 52
-  ensures  acc(x.left) && acc(x.right)
-  ensures  acc(y.left) && acc(y.right)
-  //:: ExpectedCounterexample(postcondition.violated:assertion.false, (x.left == 84))
-  ensures  x.left == 42
-{
-  n := x.left
-  label ret
-  x.left := x.left * 2
-  x.right := 201
-}
diff --git a/src/test/scala/GeneralCounterexampleTests.scala b/src/test/scala/GeneralCounterexampleTests.scala
new file mode 100644
index 000000000..9ebc60498
--- /dev/null
+++ b/src/test/scala/GeneralCounterexampleTests.scala
@@ -0,0 +1,26 @@
+// 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
+
+import viper.silicon.Silicon
+import viper.silver.testing.{CounterexampleTestInput, DefaultAnnotatedTestInput}
+
+import java.nio.file.Path
+
+class GeneralCounterexampleTests extends SiliconTests {
+  override val testDirectories: Seq[String] = Seq("counterexample_mapped", "counterexample_general")
+
+  override def configureVerifiersFromConfigMap(configMap: Map[String, Any]): Unit = {
+    val args = Silicon.optionsFromScalaTestConfigMap(prefixSpecificConfigMap(configMap).getOrElse("silicon", Map()))
+    val additionalArgs = Seq("--counterexample", "resolved")
+
+    silicon.parseCommandLine(args ++ additionalArgs :+ Silicon.dummyInputFilename)
+  }
+
+  override def buildTestInput(file: Path, prefix: String): DefaultAnnotatedTestInput =
+    CounterexampleTestInput(file, prefix)
+}
diff --git a/src/test/scala/CounterexampleTests.scala b/src/test/scala/MappedCounterexampleTests.scala
similarity index 93%
rename from src/test/scala/CounterexampleTests.scala
rename to src/test/scala/MappedCounterexampleTests.scala
index 5db30a8e6..aad2f650a 100644
--- a/src/test/scala/CounterexampleTests.scala
+++ b/src/test/scala/MappedCounterexampleTests.scala
@@ -17,8 +17,8 @@ import viper.silver.verifier.{FailureContext, VerificationError}
 
 import java.nio.file.Path
 
-class CounterexampleTests extends SiliconTests {
-  override val testDirectories: Seq[String] = Seq("counterexamples")
+class MappedCounterexampleTests extends SiliconTests {
+  override val testDirectories: Seq[String] = Seq("counterexample_mapped")
 
   override def configureVerifiersFromConfigMap(configMap: Map[String, Any]): Unit = {
     val args = Silicon.optionsFromScalaTestConfigMap(prefixSpecificConfigMap(configMap).getOrElse("silicon", Map()))
@@ -53,7 +53,7 @@ class CounterexampleTests extends SiliconTests {
     override val outputIdPattern: String = "([^:]*)(:([^,]*))?"
 
     private def isExpectedCounterexample(annotation: String, file: Path, lineNr: Int): Option[TestAnnotation] = {
-      def parseExpectedCounterexample(id: OutputAnnotationId, expectedCounterexampleString: String): Option[ExpectedCounterexampleAnnotation] = {
+      def parseExpectedCounterexample(id: OutputAnnotationId, expectedCounterexampleString: String): Option[ExpectedMappedCounterexampleAnnotation] = {
         // in order to reuse as much of the existing Viper parser as possible, we have to initialize the `_file` and `_line_offset` fields:
         val fp = new FastParser()
         fp._file = file.toAbsolutePath
@@ -68,7 +68,7 @@ class CounterexampleTests extends SiliconTests {
         val cParser = new CounterexampleParser(fp)
         // now parsing is actually possible:
         fastparse.parse(expectedCounterexampleString, cParser.expectedCounterexample(_)) match {
-          case Parsed.Success(expectedCounterexample, _) => Some(ExpectedCounterexampleAnnotation(id, file, lineNr, expectedCounterexample))
+          case Parsed.Success(expectedCounterexample, _) => Some(ExpectedMappedCounterexampleAnnotation(id, file, lineNr, expectedCounterexample))
           case Parsed.Failure(_, _, extra) =>
             println(s"Parsing expected counterexample failed in file $file: ${extra.trace().longAggregateMsg}")
             None
@@ -88,7 +88,7 @@ class CounterexampleTests extends SiliconTests {
 }
 
 /** represents an expected output (identified by `id`) with an associated (possibly partial) counterexample model */
-case class ExpectedCounterexampleAnnotation(id: OutputAnnotationId, file: Path, forLineNr: Int, expectedCounterexample: ExpectedCounterexample) extends CustomAnnotation {
+case class ExpectedMappedCounterexampleAnnotation(id: OutputAnnotationId, file: Path, forLineNr: Int, expectedCounterexample: ExpectedCounterexample) extends CustomAnnotation {
   override def matches(actual: AbstractOutput): Boolean =
     id.matches(actual.fullId) && actual.isSameLine(file, forLineNr) && containsModel(actual)
 
@@ -164,5 +164,5 @@ case class ExpectedCounterexampleAnnotation(id: OutputAnnotationId, file: Path,
 
   override def notFoundError: TestError = TestCustomError(s"Expected the following counterexample on line $forLineNr: $expectedCounterexample")
 
-  override def withForLineNr(line: Int = forLineNr): ExpectedCounterexampleAnnotation = ExpectedCounterexampleAnnotation(id, file, line, expectedCounterexample)
+  override def withForLineNr(line: Int = forLineNr): ExpectedMappedCounterexampleAnnotation = ExpectedMappedCounterexampleAnnotation(id, file, line, expectedCounterexample)
 }