From 5ee32cfcab73a453f8895ded10a0d1abbed4b903 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Mon, 17 Jun 2024 16:33:58 +0200
Subject: [PATCH 1/9] Add tests for recent Silicon changes

---
 .../all/annotation/annotationProverArgs.vpr   | 30 +++++++++++++++++++
 .../resources/all/issues/silicon/0851.vpr     | 25 ++++++++++++++++
 2 files changed, 55 insertions(+)
 create mode 100644 src/test/resources/all/annotation/annotationProverArgs.vpr
 create mode 100644 src/test/resources/all/issues/silicon/0851.vpr

diff --git a/src/test/resources/all/annotation/annotationProverArgs.vpr b/src/test/resources/all/annotation/annotationProverArgs.vpr
new file mode 100644
index 000000000..1f197a37c
--- /dev/null
+++ b/src/test/resources/all/annotation/annotationProverArgs.vpr
@@ -0,0 +1,30 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+// The errors marked in this file are expected only due to the proverArgs annotation, since the properties actually
+// hold, but Z3 should not be able to prove that due to the non-linear arithmetic setting.
+// We use UnexpectedOutput annotations to mark that they're not actual errors, and that Carbon should not report them.
+
+method m1(i: Int, i2: Int)
+    requires i >= 0
+    requires i2 >= 0
+{
+    assert i * i2 >= 0
+}
+
+@proverArgs("smt.arith.nl=false")
+method m2(i: Int, i2: Int)
+    requires i >= 0
+    requires i2 >= 0
+{
+    //:: UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/000/)
+    assert i * i2 >= 0
+}
+
+@proverArgs("smt.arith.nl=true")
+method m3(i: Int, i2: Int)
+    requires i >= 0
+    requires i2 >= 0
+{
+    assert i * i2 >= 0
+}
diff --git a/src/test/resources/all/issues/silicon/0851.vpr b/src/test/resources/all/issues/silicon/0851.vpr
new file mode 100644
index 000000000..50b28e31f
--- /dev/null
+++ b/src/test/resources/all/issues/silicon/0851.vpr
@@ -0,0 +1,25 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field v: Int
+
+field r: Ref
+
+field l: Ref
+
+function fun01(x: Ref, b1: Bool, b2: Bool): Int
+  requires acc(x.v, 1 / 3)
+  requires acc(x.v, (b1 ? 1 / 3 : none))
+  requires acc(x.v, (b2 ? 1 / 3 : none))
+{
+  x.v
+}
+
+method test01(x: Ref, b1: Bool, b2: Bool)
+  requires acc(x.v, write)
+{
+  x.v := 4
+  assert fun01(x, b2, b1) == 4
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert false
+}
\ No newline at end of file

From 2dd7e138400c29e347a17a91540d0bd8303ac065 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Mon, 1 Jul 2024 16:24:42 +0200
Subject: [PATCH 2/9] General counterexample definition by Raoul

---
 src/main/scala/viper/silver/ast/Expression.scala            | 6 ++++--
 .../scala/viper/silver/frontend/SilFrontEndConfig.scala     | 4 ++++
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala
index 090d05228..c02122444 100644
--- a/src/main/scala/viper/silver/ast/Expression.scala
+++ b/src/main/scala/viper/silver/ast/Expression.scala
@@ -162,7 +162,7 @@ case class MagicWand(left: Exp, right: Exp)(val pos: Position = NoPosition, val
     collectedExpressions
   }
 
-  def structure(p: Program): MagicWandStructure = {
+  def structure(p: Program, uniqueNames: Boolean = false): MagicWandStructure = {
     /* High-level idea: take the input wand (`this`) and perform a sequence of
      * substitutions that transform the wand into a canonical form suitable for
      * checking whether or not a given state provides a particular wand.
@@ -207,10 +207,12 @@ case class MagicWand(left: Exp, right: Exp)(val pos: Position = NoPosition, val
         decl.copy(name(decl.typ, bindings(decl.name)))(decl.pos, decl.info, decl.errT))
     }
 
+    var uniqueNameIndex = -1
     val structure = StrategyBuilder.Context[Node, Bindings](
       {
         case (exp: Exp, c) if subexpressionsToEvaluate.contains(exp) =>
-          (LocalVar(exp.typ.toString(),exp.typ)(), c)
+          val varName = exp.typ.toString() + (if (uniqueNames) s"${uniqueNameIndex += 1; uniqueNameIndex}" else "")
+          (LocalVar(varName, exp.typ)(), c)
 
         case (quant: QuantifiedExp, context) =>
           /* NOTE: This case, i.e. the transformation case, is reached before the
diff --git a/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala b/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala
index 69820bc6c..08ee4c1af 100644
--- a/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala
+++ b/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala
@@ -114,6 +114,8 @@ abstract class SilFrontendConfig(args: Seq[String], private var projectName: Str
     case "native" => NativeModel
     case "variables" => VariablesModel
     case "mapped" => MappedModel
+    case "extended" => ExtendedModel
+    case "intermediate" => IntermediateModel
     case i => throw new IllegalArgumentException(s"Unsupported counterexample model provided. Expected 'native', 'variables' or 'mapped' but got $i")
   }))
 
@@ -196,3 +198,5 @@ trait CounterexampleModel
 case object NativeModel extends CounterexampleModel
 case object VariablesModel extends CounterexampleModel
 case object MappedModel extends CounterexampleModel
+case object IntermediateModel extends CounterexampleModel
+case object ExtendedModel extends CounterexampleModel

From 1528fbe98a197de4e542a3d1140f54686d7c1a86 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Mon, 1 Jul 2024 16:26:19 +0200
Subject: [PATCH 3/9] General counterexample definition by Raoul

---
 .../silver/verifier/Counterexample.scala      | 191 ++++++++++++++++++
 1 file changed, 191 insertions(+)
 create mode 100644 src/main/scala/viper/silver/verifier/Counterexample.scala

diff --git a/src/main/scala/viper/silver/verifier/Counterexample.scala b/src/main/scala/viper/silver/verifier/Counterexample.scala
new file mode 100644
index 000000000..f71be4199
--- /dev/null
+++ b/src/main/scala/viper/silver/verifier/Counterexample.scala
@@ -0,0 +1,191 @@
+package viper.silver.verifier
+import viper.silver.ast
+import viper.silver.ast.{AbstractLocalVar, Exp, Type, Resource}
+
+/**
+  * Classes used for to build "intermediate" and "extended" counterexamples.
+  */
+
+case class StoreCounterexample(storeEntries: Seq[StoreEntry]) {
+  override lazy val toString = storeEntries.map(x => x.toString).mkString("", "\n", "\n")
+}
+
+case class StoreEntry(id: AbstractLocalVar, entry: CEValue) {
+  override lazy val toString = {
+    entry match {
+      case CEVariable(_, _, _) => s"Variable Name: ${id.name}, Value: ${entry.value.toString}, Type: ${id.typ.toString}"
+      case CESequence(name, length, entries, sequence, memberTypes) => s"Collection variable \"${id.name}\" of type ${id.typ.toString} with ${length} entries:${entries.map { case (k, v) => s"\n $v at index ${k.toString()}" }.mkString}"
+      case CESet(name, length, entries, sequence, memberTypes) => s"Collection variable \"${id.name}\" of type ${id.typ.toString} with ${length} entries:${entries.map { case (k, true) => s"\n $k" }.mkString}"
+      case CEMultiset(name, length, entries, memberTypes) => s"Collection variable \"${id.name}\" of type ${id.typ.toString} with ${length} entries:${entries.foreach { case (k, v) => s"\n ${v.toString} at index $k" }}"
+    }
+  }
+}
+
+case class HeapCounterexample(heapEntries: Seq[(Resource, FinalHeapEntry)]) {
+  var finalString = ""
+  var containsQP = false
+  heapEntries.foreach { case (re,he) => if (he.entryType == QPFieldType || he.entryType == QPPredicateType || he.entryType == QPMagicWandType) containsQP = true}
+  if (containsQP)
+    finalString ++= "The heap contains Quantified Permissions. Thus, we might own some perm which are not presented in the Counterexample.\n"
+  heapEntries.foreach { se => finalString ++= se._2.toString ++ "\n" }
+  override lazy val toString = finalString
+}
+
+sealed trait FinalHeapEntry {
+  val entryType : HeapEntryType
+}
+
+case class FieldFinalEntry(ref: String, field: String, entry: CEValue, perm: Option[Rational], typ: Type, het: HeapEntryType) extends FinalHeapEntry {
+  val entryType = het
+  override lazy val toString = s"Field Entry: $ref.$field --> (Value: ${entry.value.toString}, Type: ${typ}, Perm: ${perm.getOrElse("#undefined").toString})"
+}
+
+case class PredFinalEntry(name: String, args: Seq[String], perm: Option[Rational], insidePredicate: Option[scala.collection.immutable.Map[Exp, ModelEntry]], het: HeapEntryType) extends FinalHeapEntry {
+  val entryType = het
+  override lazy val toString = s"Predicate Entry: $name(${args.mkString("", ", ", ")")} --> (Perm: ${perm.getOrElse("#undefined").toString}) ${if (insidePredicate.isDefined && !insidePredicate.get.isEmpty) insidePredicate.get.toSeq.map(x => s"${x._1} --> ${x._2}")mkString("{\n   ", "\n   ", "\n}") else ""}"
+}
+
+case class WandFinalEntry(name: String, left: Exp, right: Exp, args: Map[String, String], perm: Option[Rational], het: HeapEntryType) extends FinalHeapEntry {
+  val entryType = het
+  override lazy val toString = s"Magic Wand Entry: $name --> (Left: ${left.toString}, Right: ${right.toString}, Perm: ${perm.getOrElse("#undefined").toString})"
+}
+
+sealed trait CEValue {
+  val id : String
+  val value : Any
+  val valueType : Option[ast.Type]
+}
+
+case class CEVariable(name: String, entryValue: ModelEntry, typ: Option[Type]) extends CEValue {
+  val id = name
+  val value = entryValue
+  val valueType = typ
+  override lazy val toString = s"Variable Name: ${name}, Value: ${value.toString}, Type: ${typ.getOrElse("None").toString}"
+}
+
+case class CESequence(name: String, length: BigInt, entries: Map[BigInt, String], sequence: Seq[String], memberTypes: Option[Type]) extends CEValue {
+  val id = name
+  val value = sequence
+  val valueType = memberTypes
+  val size = length
+  val inside = entries
+  override lazy val toString = {
+    var finalString = s"$name with size ${size.toString()} with entries:"
+    for ((k,v) <- inside)
+      finalString ++= s"\n $v at index ${k.toString()}"
+    finalString
+  }
+}
+
+case class CESet(name: String, cardinality: BigInt, containment: Map[String, Boolean], set: Set[String], memberTypes: Option[Type]) extends CEValue {
+  val id = name
+  val value = set
+  val valueType = memberTypes
+  val size = cardinality
+  val inside = containment
+  override lazy val toString = s"Set $name of size ${size.toString()} with entries: ${inside.filter(x => x._2).map(x => x._1).mkString("{", ", ", "}")}"
+}
+
+case class CEMultiset(name: String, cardinality: BigInt, containment: scala.collection.immutable.Map[String, Int], memberTypes: Option[Type]) extends CEValue {
+  val id = name
+  val value = containment
+  val valueType = memberTypes
+  val size = cardinality
+  override lazy val toString = {
+    var finalString = s"Multiset $name of size ${size.toString()} with entries:"
+    for ((k, v) <- containment)
+      finalString ++= s"\n $k occurs ${v.toString} time"
+    finalString
+  }
+}
+
+case class BasicHeap(basicHeapEntries: Set[BasicHeapEntry]) {
+  override lazy val toString = basicHeapEntries.map(x => x.toString).mkString("", "\n", "")
+}
+
+case class BasicHeapEntry(reference: Seq[String], field: Seq[String], valueID: String, perm: Option[Rational], het: HeapEntryType, insidePredicate: Option[scala.collection.immutable.Map[Exp, ModelEntry]]) {
+  override lazy val toString = {
+    het match {
+      case PredicateType =>
+        println(insidePredicate.get.toString())
+        s"Heap entry: ${reference.mkString("(", ", ", ")")} + ${field.mkString("(", ", ", ")")} --> (Permission: ${perm.getOrElse("None")}) ${if (insidePredicate.isDefined && !insidePredicate.get.isEmpty) insidePredicate.get.toSeq.map(x => s"${x._1} --> ${x._2}")mkString("{\n   ", "\n   ", "\n}") else ""}"
+      case _ => s"Heap entry: ${reference.mkString("(", ", ", ")")} + ${field.mkString("(", ", ", ")")} --> (Value: $valueID, Permission: ${perm.getOrElse("None")})"
+    }
+  }
+}
+
+case class BasicDomainEntry(name: String, types: Seq[ast.Type], functions: Seq[BasicFunction]) {
+  override def toString: String = s"domain $valueName{\n ${functions.map(_.toString()).mkString("\n")}\n}"
+  val valueName: String = s"$name${printTypes()}"
+  private def printTypes(): String =
+    if (types.isEmpty) ""
+    else types.map(printType).mkString("[", ", ", "]")
+  private def printType(t: ast.Type): String = t match {
+    case ast.TypeVar(x) => x
+    case _ => t.toString()
+  }
+}
+
+
+case class BasicFunction(fname: String, argtypes: Seq[ast.Type], returnType: ast.Type, options: Map[Seq[String], String], default: String) {
+  override def toString: String = {
+    if (options.nonEmpty)
+      s"$fname${argtypes.mkString("(", ",", ")")}:${returnType}{\n" + options.map(o => "    " + o._1.mkString(" ") + " -> " + o._2).mkString("\n") + "\n    else -> " + default + "\n}"
+    else
+      s"$fname{\n    " + default + "\n}"
+  }
+}
+
+sealed trait HeapEntryType
+case object FieldType extends HeapEntryType
+case object PredicateType extends HeapEntryType
+case object QPFieldType extends HeapEntryType
+case object QPPredicateType extends HeapEntryType
+case object MagicWandType extends HeapEntryType
+case object QPMagicWandType extends HeapEntryType
+
+/*
+  Helper class for permissions
+ */
+
+final class Rational(n: BigInt, d: BigInt) extends Ordered[Rational] {
+  require(d != 0, "Denominator of Rational must not be 0.")
+
+  private val g = n.gcd(d)
+  val numerator: BigInt = n / g * d.signum
+  val denominator: BigInt = d.abs / g
+
+  def +(that: Rational): Rational = {
+    val newNum = this.numerator * that.denominator + that.numerator * this.denominator
+    val newDen = this.denominator * that.denominator
+    Rational(newNum, newDen)
+  }
+  def -(that: Rational): Rational = this + (-that)
+  def unary_- = Rational(-numerator, denominator)
+  def abs = Rational(numerator.abs, denominator)
+  def signum = Rational(numerator.signum, 1)
+
+  def *(that: Rational): Rational = Rational(this.numerator * that.numerator, this.denominator * that.denominator)
+  def /(that: Rational): Rational = this * that.inverse
+  def inverse = Rational(denominator, numerator)
+
+  def compare(that: Rational) = (this.numerator * that.denominator - that.numerator * this.denominator).signum
+
+  override def equals(obj: Any) = obj match {
+    case that: Rational => this.numerator == that.numerator && this.denominator == that.denominator
+    case _ => false
+  }
+
+  override def hashCode(): Int = viper.silver.utility.Common.generateHashCode(n, d)
+
+  override lazy val toString = s"$numerator/$denominator"
+}
+
+object Rational extends ((BigInt, BigInt) => Rational) {
+  val zero = Rational(0, 1)
+  val one = Rational(1, 1)
+
+  def apply(numer: BigInt, denom: BigInt) = new Rational(numer, denom)
+
+  def unapply(r: Rational) = Some(r.numerator, r.denominator)
+}
\ No newline at end of file

From 469ec669130fdfe731b5870d8ad2a5c0321dd6b6 Mon Sep 17 00:00:00 2001
From: marcoeilers <eilers.marco@googlemail.com>
Date: Fri, 29 Aug 2025 17:33:33 +0200
Subject: [PATCH 4/9] Added a convenience method

---
 .../scala/viper/silver/verifier/Counterexample.scala     | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/main/scala/viper/silver/verifier/Counterexample.scala b/src/main/scala/viper/silver/verifier/Counterexample.scala
index f71be4199..5567ab39e 100644
--- a/src/main/scala/viper/silver/verifier/Counterexample.scala
+++ b/src/main/scala/viper/silver/verifier/Counterexample.scala
@@ -8,6 +8,7 @@ import viper.silver.ast.{AbstractLocalVar, Exp, Type, Resource}
 
 case class StoreCounterexample(storeEntries: Seq[StoreEntry]) {
   override lazy val toString = storeEntries.map(x => x.toString).mkString("", "\n", "\n")
+  lazy val asMap: Map[String, CEValue] = storeEntries.map(se => (se.id.name, se.entry)).toMap
 }
 
 case class StoreEntry(id: AbstractLocalVar, entry: CEValue) {
@@ -56,6 +57,14 @@ sealed trait CEValue {
   val valueType : Option[ast.Type]
 }
 
+object CEValueOnly {
+  def apply(value: ModelEntry, typ: Option[ast.Type]): CEValue = CEVariable("#undefined", value, typ)
+  def unapply(ce: CEValue): Option[(ModelEntry, Option[ast.Type])] = ce match {
+    case CEVariable(_, entryValue, typ) => Some((entryValue, typ))
+    case _ => None
+  }
+}
+
 case class CEVariable(name: String, entryValue: ModelEntry, typ: Option[Type]) extends CEValue {
   val id = name
   val value = entryValue

From d15460f9bc3e8b94a9d86cb266e736cc7dcb72e1 Mon Sep 17 00:00:00 2001
From: marcoeilers <eilers.marco@googlemail.com>
Date: Fri, 29 Aug 2025 17:40:28 +0200
Subject: [PATCH 5/9] Moving test files from Silicon

---
 .../resources/counterexamples/cyclic-ref.vpr  | 13 +++++++++
 .../resources/counterexamples/functions.vpr   | 16 +++++++++++
 src/test/resources/counterexamples/lseg.vpr   | 27 +++++++++++++++++++
 .../resources/counterexamples/method-call.vpr | 19 +++++++++++++
 .../resources/counterexamples/negative.vpr    | 10 +++++++
 .../resources/counterexamples/permissions.vpr | 11 ++++++++
 .../resources/counterexamples/predicate.vpr   | 27 +++++++++++++++++++
 .../counterexamples/ref-sequence.vpr          | 12 +++++++++
 .../resources/counterexamples/sequence.vpr    | 14 ++++++++++
 .../counterexamples/simple-refs-rec.vpr       | 27 +++++++++++++++++++
 .../resources/counterexamples/simple-refs.vpr | 21 +++++++++++++++
 11 files changed, 197 insertions(+)
 create mode 100644 src/test/resources/counterexamples/cyclic-ref.vpr
 create mode 100644 src/test/resources/counterexamples/functions.vpr
 create mode 100644 src/test/resources/counterexamples/lseg.vpr
 create mode 100644 src/test/resources/counterexamples/method-call.vpr
 create mode 100644 src/test/resources/counterexamples/negative.vpr
 create mode 100644 src/test/resources/counterexamples/permissions.vpr
 create mode 100644 src/test/resources/counterexamples/predicate.vpr
 create mode 100644 src/test/resources/counterexamples/ref-sequence.vpr
 create mode 100644 src/test/resources/counterexamples/sequence.vpr
 create mode 100644 src/test/resources/counterexamples/simple-refs-rec.vpr
 create mode 100644 src/test/resources/counterexamples/simple-refs.vpr

diff --git a/src/test/resources/counterexamples/cyclic-ref.vpr b/src/test/resources/counterexamples/cyclic-ref.vpr
new file mode 100644
index 000000000..d7d0ef13e
--- /dev/null
+++ b/src/test/resources/counterexamples/cyclic-ref.vpr
@@ -0,0 +1,13 @@
+// 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
new file mode 100644
index 000000000..7cff7b254
--- /dev/null
+++ b/src/test/resources/counterexamples/functions.vpr
@@ -0,0 +1,16 @@
+// 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
new file mode 100644
index 000000000..3efc72126
--- /dev/null
+++ b/src/test/resources/counterexamples/lseg.vpr
@@ -0,0 +1,27 @@
+// 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
new file mode 100644
index 000000000..c4a197b01
--- /dev/null
+++ b/src/test/resources/counterexamples/method-call.vpr
@@ -0,0 +1,19 @@
+// 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
new file mode 100644
index 000000000..036b8599b
--- /dev/null
+++ b/src/test/resources/counterexamples/negative.vpr
@@ -0,0 +1,10 @@
+// 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
new file mode 100644
index 000000000..0a46448af
--- /dev/null
+++ b/src/test/resources/counterexamples/permissions.vpr
@@ -0,0 +1,11 @@
+// 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
new file mode 100644
index 000000000..6d5df8aef
--- /dev/null
+++ b/src/test/resources/counterexamples/predicate.vpr
@@ -0,0 +1,27 @@
+// 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
new file mode 100644
index 000000000..858a38372
--- /dev/null
+++ b/src/test/resources/counterexamples/ref-sequence.vpr
@@ -0,0 +1,12 @@
+// 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
new file mode 100644
index 000000000..2f9770447
--- /dev/null
+++ b/src/test/resources/counterexamples/sequence.vpr
@@ -0,0 +1,14 @@
+// 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
new file mode 100644
index 000000000..81082fab8
--- /dev/null
+++ b/src/test/resources/counterexamples/simple-refs-rec.vpr
@@ -0,0 +1,27 @@
+// 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
new file mode 100644
index 000000000..e098b63f4
--- /dev/null
+++ b/src/test/resources/counterexamples/simple-refs.vpr
@@ -0,0 +1,21 @@
+// 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
+}

From f6c716355b8fea8dfd1053a8641b23e68404da6b Mon Sep 17 00:00:00 2001
From: marcoeilers <eilers.marco@googlemail.com>
Date: Fri, 29 Aug 2025 18:07:57 +0200
Subject: [PATCH 6/9] Defining common interface for Silicon/Carbon CEs

---
 .../silver/verifier/Counterexample.scala      | 25 +++++++++++++++++--
 1 file changed, 23 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/viper/silver/verifier/Counterexample.scala b/src/main/scala/viper/silver/verifier/Counterexample.scala
index 5567ab39e..5b4985dba 100644
--- a/src/main/scala/viper/silver/verifier/Counterexample.scala
+++ b/src/main/scala/viper/silver/verifier/Counterexample.scala
@@ -6,6 +6,27 @@ import viper.silver.ast.{AbstractLocalVar, Exp, Type, Resource}
   * Classes used for to build "intermediate" and "extended" counterexamples.
   */
 
+trait IntermediateCounterexample {
+  val basicVariables: Seq[CEVariable]
+  val allSequences: Seq[CEValue]
+  val allSets: Seq[CEValue]
+  val allMultisets: Seq[CEValue]
+  val allCollections: Seq[CEValue] = allSequences ++ allSets ++ allMultisets
+  def basicHeaps: Seq[(String, BasicHeap)]
+
+  val domainEntries: Seq[BasicDomainEntry]
+  val nonDomainFunctions: Seq[BasicFunctionEntry]
+}
+
+trait ExtendedCounterexample {
+  val imCE: IntermediateCounterexample
+  val ceStore: StoreCounterexample
+  val ceHeaps: Seq[(String, HeapCounterexample)]
+  lazy val heapMap = ceHeaps.toMap
+  val domainEntries: Seq[BasicDomainEntry]
+  val functionEntries: Seq[BasicFunctionEntry]
+}
+
 case class StoreCounterexample(storeEntries: Seq[StoreEntry]) {
   override lazy val toString = storeEntries.map(x => x.toString).mkString("", "\n", "\n")
   lazy val asMap: Map[String, CEValue] = storeEntries.map(se => (se.id.name, se.entry)).toMap
@@ -123,7 +144,7 @@ case class BasicHeapEntry(reference: Seq[String], field: Seq[String], valueID: S
   }
 }
 
-case class BasicDomainEntry(name: String, types: Seq[ast.Type], functions: Seq[BasicFunction]) {
+case class BasicDomainEntry(name: String, types: Seq[ast.Type], functions: Seq[BasicFunctionEntry]) {
   override def toString: String = s"domain $valueName{\n ${functions.map(_.toString()).mkString("\n")}\n}"
   val valueName: String = s"$name${printTypes()}"
   private def printTypes(): String =
@@ -136,7 +157,7 @@ case class BasicDomainEntry(name: String, types: Seq[ast.Type], functions: Seq[B
 }
 
 
-case class BasicFunction(fname: String, argtypes: Seq[ast.Type], returnType: ast.Type, options: Map[Seq[String], String], default: String) {
+case class BasicFunctionEntry(fname: String, argtypes: Seq[ast.Type], returnType: ast.Type, options: Map[Seq[String], String], default: String) {
   override def toString: String = {
     if (options.nonEmpty)
       s"$fname${argtypes.mkString("(", ",", ")")}:${returnType}{\n" + options.map(o => "    " + o._1.mkString(" ") + " -> " + o._2).mkString("\n") + "\n    else -> " + default + "\n}"

From 062f25c4285e0dd700d6e61e43573026f339fd96 Mon Sep 17 00:00:00 2001
From: marcoeilers <eilers.marco@googlemail.com>
Date: Mon, 1 Sep 2025 14:38:20 +0200
Subject: [PATCH 7/9] Moving CE test infrastructure to silver

---
 .../silver/testing/BackendTypeTest.scala      |   6 +
 .../silver/verifier/Counterexample.scala      |   5 +-
 .../resources/counterexamples/functions.vpr   |   3 +-
 .../scala/CounterexampleVariablesTests.scala  |  21 --
 .../ExpectedCounterexampleAnnotation.scala    | 196 ++++++++++++++++++
 5 files changed, 207 insertions(+), 24 deletions(-)
 create mode 100644 src/test/scala/ExpectedCounterexampleAnnotation.scala

diff --git a/src/main/scala/viper/silver/testing/BackendTypeTest.scala b/src/main/scala/viper/silver/testing/BackendTypeTest.scala
index 3b070fe09..829a9ed97 100644
--- a/src/main/scala/viper/silver/testing/BackendTypeTest.scala
+++ b/src/main/scala/viper/silver/testing/BackendTypeTest.scala
@@ -1,3 +1,9 @@
+// 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-2015 ETH Zurich.
+
 package viper.silver.testing
 
 import org.scalatest.funsuite.AnyFunSuite
diff --git a/src/main/scala/viper/silver/verifier/Counterexample.scala b/src/main/scala/viper/silver/verifier/Counterexample.scala
index 5b4985dba..6a5f3c0b6 100644
--- a/src/main/scala/viper/silver/verifier/Counterexample.scala
+++ b/src/main/scala/viper/silver/verifier/Counterexample.scala
@@ -11,8 +11,8 @@ trait IntermediateCounterexample {
   val allSequences: Seq[CEValue]
   val allSets: Seq[CEValue]
   val allMultisets: Seq[CEValue]
-  val allCollections: Seq[CEValue] = allSequences ++ allSets ++ allMultisets
-  def basicHeaps: Seq[(String, BasicHeap)]
+  lazy val allCollections: Seq[CEValue] = allSequences ++ allSets ++ allMultisets
+  def allBasicHeaps: Seq[(String, BasicHeap)]
 
   val domainEntries: Seq[BasicDomainEntry]
   val nonDomainFunctions: Seq[BasicFunctionEntry]
@@ -25,6 +25,7 @@ trait ExtendedCounterexample {
   lazy val heapMap = ceHeaps.toMap
   val domainEntries: Seq[BasicDomainEntry]
   val functionEntries: Seq[BasicFunctionEntry]
+  lazy val domainsAndFunctions = domainEntries ++ functionEntries
 }
 
 case class StoreCounterexample(storeEntries: Seq[StoreEntry]) {
diff --git a/src/test/resources/counterexamples/functions.vpr b/src/test/resources/counterexamples/functions.vpr
index 7cff7b254..cb65beb59 100644
--- a/src/test/resources/counterexamples/functions.vpr
+++ b/src/test/resources/counterexamples/functions.vpr
@@ -9,7 +9,8 @@ function foo(z: Int): Int
 method bar()
   requires foo(3) == 42
 {
-  var x: Int := 5
+  var x: Int
+  assume x == 5
   var y: Int := foo(x)
   //:: ExpectedCounterexample(assert.failed:assertion.false, (x == 5, y == 42))
   assert(false)
diff --git a/src/test/scala/CounterexampleVariablesTests.scala b/src/test/scala/CounterexampleVariablesTests.scala
index 3d8548d06..4cc59bfd7 100644
--- a/src/test/scala/CounterexampleVariablesTests.scala
+++ b/src/test/scala/CounterexampleVariablesTests.scala
@@ -124,25 +124,4 @@ object CounterexampleComparison {
   def areEqualEntries(entry1: ModelEntry, entry2: ModelEntry): Boolean = (entry1, entry2) match {
     case (ConstantEntry(value1), ConstantEntry(value2)) => value1 == value2
   }
-}
-
-/**
-  * Simple input language to describe an expected counterexample with corresponding parser.
-  * Currently, a counterexample is expressed by a comma separated list of access predicates and equalities (using the
-  * same syntax as in Viper)
-  */
-class CounterexampleParser(fp: FastParser) {
-  import fp.{accessPred, eqExp}
-
-  def expectedCounterexample[_: P]: P[ExpectedCounterexample] =
-    (Start ~ "(" ~ (accessPred | eqExp).rep(0, ",") ~ ")" ~ End)
-      .map(ExpectedCounterexample)
-}
-
-case class ExpectedCounterexample(exprs: Seq[PExp]) {
-  assert(exprs.forall {
-    case _: PAccPred => true
-    case PBinExp(_, r, _) if r.rs == PSymOp.EqEq => true
-    case _ => false
-  })
 }
\ No newline at end of file
diff --git a/src/test/scala/ExpectedCounterexampleAnnotation.scala b/src/test/scala/ExpectedCounterexampleAnnotation.scala
new file mode 100644
index 000000000..d0e474d1e
--- /dev/null
+++ b/src/test/scala/ExpectedCounterexampleAnnotation.scala
@@ -0,0 +1,196 @@
+// 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.silver.testing
+
+import fastparse._
+import viper.silver.parser.FastParserCompanion.whitespace
+import viper.silver.ast
+import viper.silver.parser._
+import viper.silver.testing.{AbstractOutput, CustomAnnotation, DefaultAnnotatedTestInput, DefaultTestInput, OutputAnnotationId, SilOutput, TestAnnotation, TestAnnotationParser, TestCustomError, TestError, TestInput}
+import viper.silver.verifier._
+
+import java.nio.file.Path
+
+
+/** 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 {
+  override def matches(actual: AbstractOutput): Boolean =
+    id.matches(actual.fullId) && actual.isSameLine(file, forLineNr) && containsModel(actual)
+
+  /** returns true if the expected model (i.e. class parameter) is a subset of a model given in a failure context */
+  def containsModel(is: AbstractOutput): Boolean = is match {
+    case SilOutput(err) => err match {
+      case vErr: VerificationError => vErr.failureContexts.toVector.exists(containsExpectedCounterexample)
+      case _ => false
+    }
+    case _ => false
+  }
+
+  def containsExpectedCounterexample(failureContext: FailureContext): Boolean =
+    failureContext.counterExample match {
+      case Some(ce: ExtendedCounterexample) => meetsExpectations(expectedCounterexample, ce)
+      case _ => false
+    }
+
+  /** returns true if model2 contains at least the content expressed by model1 */
+  def meetsExpectations(model1: ExpectedCounterexample, model2: ExtendedCounterexample): Boolean = {
+    model1.exprs.forall {
+      case accPred: PAccPred => containsAccessPredicate(accPred, model2)
+      case PBinExp(lhs, r, rhs) if r.rs == PSymOp.EqEq => containsEquality(lhs, rhs, model2)
+    }
+  }
+
+  def containsAccessPredicate(accPred: PAccPred, model: ExtendedCounterexample): Boolean = {
+    resolve(Vector(accPred.loc, accPred.perm), model).exists {
+      case Vector((_, actualPermOpt), (expectedPermAmount, _)) =>
+        actualPermOpt.exists(actualPermAmount =>
+          areEqualEntries(expectedPermAmount,
+            CEValueOnly(ApplicationEntry("/", Seq(ConstantEntry(actualPermAmount.numerator.toString()), ConstantEntry(actualPermAmount.denominator.toString()))), Some(ast.Perm)))
+        )
+    }
+  }
+
+  def containsEquality(lhs: PExp, rhs: PExp, model: ExtendedCounterexample): Boolean =
+    resolveWoPerm(Vector(lhs, rhs), model).exists { case Vector(resolvedLhs, resolvedRhs) =>
+      areEqualEntries(resolvedLhs, resolvedRhs) }
+
+  /** resolves `expr` to a model entry in the given model. In case it's a field access, the corresponding permissions are returned as well */
+  def resolve(expr: PExp, model: ExtendedCounterexample): Option[(CEValue, Option[Rational])] = expr match {
+    case PIntLit(value) => Some(CEValueOnly(ConstantEntry(value.toString()), Some(viper.silver.ast.Int)), None)
+    case PUnExp(r, PIntLit(value)) if r.rs == PSymOp.Neg => Some(CEValueOnly(ApplicationEntry("-", Seq(ConstantEntry(value.toString()))), Some(ast.Int)), None)
+    case PBinExp(PIntLit(n), r, PIntLit(d)) if r.rs == PSymOp.Div =>
+      Some(CEValueOnly(ApplicationEntry("/", Seq(ConstantEntry(n.toString()), ConstantEntry(d.toString()))), Some(ast.Perm)), None)
+    case idnuse: PIdnUseExp =>
+      model.ceStore.asMap.get(idnuse.name).map((_, None))
+    case PFieldAccess(rcv, _, idnuse) =>
+      val rcvValue = resolveWoPerm(rcv, model)
+      rcvValue.flatMap {
+        case CEVariable(name, entry, _) => model.heapMap.get("current").flatMap(_.heapEntries.find({
+          case (f: ast.Field, ffi: FieldFinalEntry) if f.name == idnuse.name && (ffi.ref == name || ffi.ref == entry.toString) => true
+          case _ => false
+        }).map(he =>
+          (he._2.asInstanceOf[FieldFinalEntry].entry, he._2.asInstanceOf[FieldFinalEntry].perm)
+        ))
+      }
+    case PLookup(base, _, idx, _) => resolveWoPerm(Vector(base, idx), model).flatMap {
+      case Vector(s: CESequence, CEValueOnly(ConstantEntry(i), _)) =>
+        try {
+          val evaluatedIdx = BigInt(i)
+          val elemTyp = s.valueType match {
+            case Some(ast.SeqType(memberType)) => Some(memberType)
+            case _ => None
+          }
+          if (evaluatedIdx >= 0 && evaluatedIdx < s.length)
+            Some((CEValueOnly(ConstantEntry(s.entries(evaluatedIdx)), elemTyp), None))
+          else
+            None
+        } catch {
+          case _: NumberFormatException => None
+        }
+
+    }
+  }
+
+  def resolve(exprs: Vector[PExp], model: ExtendedCounterexample): Option[Vector[(CEValue, Option[Rational])]] = {
+    val entries = exprs.map(expr => resolve(expr, model)).collect{ case Some(entry) => entry }
+    if (exprs.size == entries.size) Some(entries) else None
+  }
+
+  def resolveWoPerm(expr: PExp, model: ExtendedCounterexample): Option[CEValue] =
+    resolve(expr, model).map(_._1)
+
+  def resolveWoPerm(exprs: Vector[PExp], model: ExtendedCounterexample): Option[Vector[CEValue]] = {
+    val entries = exprs.map(expr => resolveWoPerm(expr, model)).collect{ case Some(entry) => entry }
+    if (exprs.size == entries.size) Some(entries) else None
+  }
+
+  def areEqualEntries(entry1: CEValue, entry2: CEValue): Boolean = (entry1, entry2) match {
+    case (CEValueOnly(value1, _), CEValueOnly(value2, _)) => value1 == value2
+  }
+
+  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)
+}
+
+/** we use special annotations to express expected counterexamples */
+object CounterexampleTestInput extends TestAnnotationParser {
+  /**
+    * Creates an annotated test input by parsing all annotations in the files
+    * that belong to the given test input.
+    */
+  def apply(i: TestInput): DefaultAnnotatedTestInput =
+    DefaultAnnotatedTestInput(i.name, i.prefix, i.files, i.tags,
+      parseAnnotations(i.files))
+
+  def apply(file: Path, prefix: String): DefaultAnnotatedTestInput =
+    apply(DefaultTestInput(file, prefix))
+
+  override def getAnnotationFinders: Seq[(String, Path, Int) => Option[TestAnnotation]] = {
+    super.getAnnotationFinders :+ isExpectedCounterexample
+  }
+
+  // the use of comma is excluded from value ID (i.e. after the colon) to avoid ambiguities with the model
+  // note that the second capturing group could be turned into a non-capturing group but this would break compatibility
+  // with the parent trait
+  override val outputIdPattern: String = "([^:]*)(:([^,]*))?"
+
+  private def isExpectedCounterexample(annotation: String, file: Path, lineNr: Int): Option[TestAnnotation] = {
+    def parseExpectedCounterexample(id: OutputAnnotationId, expectedCounterexampleString: String): Option[ExpectedCounterexampleAnnotation] = {
+      // 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
+      val lines = expectedCounterexampleString.linesWithSeparators
+      fp._line_offset = (lines.map(_.length) ++ Seq(0)).toArray
+      var offset = 0
+      for (i <- fp._line_offset.indices) {
+        val line_length = fp._line_offset(i)
+        fp._line_offset(i) = offset
+        offset += line_length
+      }
+      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.Failure(_, _, extra) =>
+          println(s"Parsing expected counterexample failed in file $file: ${extra.trace().longAggregateMsg}")
+          None
+      }
+    }
+
+    val regex = ("""^ExpectedCounterexample\(""" + outputIdPattern + """, (.*)\)$""").r
+    annotation match {
+      case regex(keyId, _, null, counterexample) =>
+        parseExpectedCounterexample(OutputAnnotationId(keyId, None), counterexample)
+      case regex(keyId, _, valueId, counterexample) =>
+        parseExpectedCounterexample(OutputAnnotationId(keyId, Some(valueId)), counterexample)
+      case _ => None
+    }
+  }
+}
+
+/**
+  * Simple input language to describe an expected counterexample with corresponding parser.
+  * Currently, a counterexample is expressed by a comma separated list of access predicates and equalities (using the
+  * same syntax as in Viper)
+  */
+class CounterexampleParser(fp: FastParser) {
+  import fp.{accessPred, eqExp}
+
+  def expectedCounterexample[_: P]: P[ExpectedCounterexample] =
+    (Start ~ "(" ~ (accessPred | eqExp).rep(0, ",") ~ ")" ~ End)
+      .map(ExpectedCounterexample)
+}
+
+case class ExpectedCounterexample(exprs: Seq[PExp]) {
+  assert(exprs.forall {
+    case _: PAccPred => true
+    case PBinExp(_, r, _) if r.rs == PSymOp.EqEq => true
+    case _ => false
+  })
+}
+

From d7d7e95988e32881666d0dfbd10bfdc1472f5e65 Mon Sep 17 00:00:00 2001
From: marcoeilers <eilers.marco@googlemail.com>
Date: Mon, 1 Sep 2025 15:20:53 +0200
Subject: [PATCH 8/9] Adding quantified field example

---
 src/test/resources/counterexamples/qfield.vpr | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 src/test/resources/counterexamples/qfield.vpr

diff --git a/src/test/resources/counterexamples/qfield.vpr b/src/test/resources/counterexamples/qfield.vpr
new file mode 100644
index 000000000..4b771b005
--- /dev/null
+++ b/src/test/resources/counterexamples/qfield.vpr
@@ -0,0 +1,18 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+method foo(s: Seq[Ref], i: Int, m: Int)
+  requires forall j: Int, k: Int :: 0 <= j < k < |s| ==> s[j] != s[k]
+  requires forall j: Int :: 0 <= j < |s| ==> acc(s[j].f)
+  requires forall j: Int :: 0 <= j < |s| ==> s[j].f > 0
+  requires 0 <= i < |s|
+  requires 0 <= m < |s|
+  requires i < m
+{
+   if (s[i].f < 2) {
+     //:: ExpectedCounterexample(assert.failed:assertion.false, (s[m].f == 1, s[i].f == 1))
+     assert s[m].f > 1
+   }
+}
\ No newline at end of file

From 5e1fda95105708c4a64afc011f9cc7d3f21ac134 Mon Sep 17 00:00:00 2001
From: marcoeilers <eilers.marco@googlemail.com>
Date: Mon, 1 Sep 2025 15:59:00 +0200
Subject: [PATCH 9/9] Predicates in test annotations, fixed an output message

---
 .../silver/verifier/Counterexample.scala      |  2 +-
 .../qfield.vpr                                |  0
 .../counterexample_general/qpred.vpr          | 22 +++++++++++++++++++
 .../cyclic-ref.vpr                            |  0
 .../functions.vpr                             |  0
 .../lseg.vpr                                  |  1 +
 .../method-call.vpr                           |  0
 .../negative.vpr                              |  0
 .../permissions.vpr                           |  0
 .../predicate.vpr                             |  0
 .../ref-sequence.vpr                          |  0
 .../sequence.vpr                              |  0
 .../simple-refs-rec.vpr                       |  0
 .../simple-refs.vpr                           |  0
 .../ExpectedCounterexampleAnnotation.scala    | 16 +++++++++++++-
 15 files changed, 39 insertions(+), 2 deletions(-)
 rename src/test/resources/{counterexamples => counterexample_general}/qfield.vpr (100%)
 create mode 100644 src/test/resources/counterexample_general/qpred.vpr
 rename src/test/resources/{counterexamples => counterexample_mapped}/cyclic-ref.vpr (100%)
 rename src/test/resources/{counterexamples => counterexample_mapped}/functions.vpr (100%)
 rename src/test/resources/{counterexamples => counterexample_mapped}/lseg.vpr (90%)
 rename src/test/resources/{counterexamples => counterexample_mapped}/method-call.vpr (100%)
 rename src/test/resources/{counterexamples => counterexample_mapped}/negative.vpr (100%)
 rename src/test/resources/{counterexamples => counterexample_mapped}/permissions.vpr (100%)
 rename src/test/resources/{counterexamples => counterexample_mapped}/predicate.vpr (100%)
 rename src/test/resources/{counterexamples => counterexample_mapped}/ref-sequence.vpr (100%)
 rename src/test/resources/{counterexamples => counterexample_mapped}/sequence.vpr (100%)
 rename src/test/resources/{counterexamples => counterexample_mapped}/simple-refs-rec.vpr (100%)
 rename src/test/resources/{counterexamples => counterexample_mapped}/simple-refs.vpr (100%)

diff --git a/src/main/scala/viper/silver/verifier/Counterexample.scala b/src/main/scala/viper/silver/verifier/Counterexample.scala
index 6a5f3c0b6..359f27baf 100644
--- a/src/main/scala/viper/silver/verifier/Counterexample.scala
+++ b/src/main/scala/viper/silver/verifier/Counterexample.scala
@@ -49,7 +49,7 @@ case class HeapCounterexample(heapEntries: Seq[(Resource, FinalHeapEntry)]) {
   var containsQP = false
   heapEntries.foreach { case (re,he) => if (he.entryType == QPFieldType || he.entryType == QPPredicateType || he.entryType == QPMagicWandType) containsQP = true}
   if (containsQP)
-    finalString ++= "The heap contains Quantified Permissions. Thus, we might own some perm which are not presented in the Counterexample.\n"
+    finalString ++= "The heap contains quantified permissions. Thus, we might own some permissions which are not shown in the counterexample.\n"
   heapEntries.foreach { se => finalString ++= se._2.toString ++ "\n" }
   override lazy val toString = finalString
 }
diff --git a/src/test/resources/counterexamples/qfield.vpr b/src/test/resources/counterexample_general/qfield.vpr
similarity index 100%
rename from src/test/resources/counterexamples/qfield.vpr
rename to src/test/resources/counterexample_general/qfield.vpr
diff --git a/src/test/resources/counterexample_general/qpred.vpr b/src/test/resources/counterexample_general/qpred.vpr
new file mode 100644
index 000000000..a134ebf5e
--- /dev/null
+++ b/src/test/resources/counterexample_general/qpred.vpr
@@ -0,0 +1,22 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field x: Int
+field y: Int
+
+predicate P(this: Ref, n: Int) {
+  acc(this.x) && acc(this.y) && this.x == n
+}
+
+method foo(refs: Set[Ref], r2: Ref, r3: Ref)
+  requires forall r: Ref :: r in refs ==> P(r, 3)
+  requires forall i: Int, r: Ref :: r == r2 && i == 4 ==> P(r, i)
+{
+  if (r3 in refs) {
+    assert P(r3, 3);
+    exhale acc(P(r2, 4), 1/2)
+
+    //:: ExpectedCounterexample(assert.failed:assertion.false, (acc(P(r3, 3), 1/1), acc(P(r2, 4), 1/2)))
+    assert false
+  }
+}
\ No newline at end of file
diff --git a/src/test/resources/counterexamples/cyclic-ref.vpr b/src/test/resources/counterexample_mapped/cyclic-ref.vpr
similarity index 100%
rename from src/test/resources/counterexamples/cyclic-ref.vpr
rename to src/test/resources/counterexample_mapped/cyclic-ref.vpr
diff --git a/src/test/resources/counterexamples/functions.vpr b/src/test/resources/counterexample_mapped/functions.vpr
similarity index 100%
rename from src/test/resources/counterexamples/functions.vpr
rename to src/test/resources/counterexample_mapped/functions.vpr
diff --git a/src/test/resources/counterexamples/lseg.vpr b/src/test/resources/counterexample_mapped/lseg.vpr
similarity index 90%
rename from src/test/resources/counterexamples/lseg.vpr
rename to src/test/resources/counterexample_mapped/lseg.vpr
index 3efc72126..563518613 100644
--- a/src/test/resources/counterexamples/lseg.vpr
+++ b/src/test/resources/counterexample_mapped/lseg.vpr
@@ -19,6 +19,7 @@ method removeFirst(first: Ref, last: Ref, values: Seq[Int]) returns  (value: Int
   ensures  lseg(second, last, values[1..])
   // we have insufficient field permissions when second is equal to last:
   //:: ExpectedCounterexample(not.wellformed:insufficient.permission, (second == last))
+  //:: ExpectedCounterexample(postcondition.violated:assertion.false, (second == last))
   ensures  value != unfolding lseg(second, last, values[1..]) in second.elem
 {
   unfold lseg(first, last, values)
diff --git a/src/test/resources/counterexamples/method-call.vpr b/src/test/resources/counterexample_mapped/method-call.vpr
similarity index 100%
rename from src/test/resources/counterexamples/method-call.vpr
rename to src/test/resources/counterexample_mapped/method-call.vpr
diff --git a/src/test/resources/counterexamples/negative.vpr b/src/test/resources/counterexample_mapped/negative.vpr
similarity index 100%
rename from src/test/resources/counterexamples/negative.vpr
rename to src/test/resources/counterexample_mapped/negative.vpr
diff --git a/src/test/resources/counterexamples/permissions.vpr b/src/test/resources/counterexample_mapped/permissions.vpr
similarity index 100%
rename from src/test/resources/counterexamples/permissions.vpr
rename to src/test/resources/counterexample_mapped/permissions.vpr
diff --git a/src/test/resources/counterexamples/predicate.vpr b/src/test/resources/counterexample_mapped/predicate.vpr
similarity index 100%
rename from src/test/resources/counterexamples/predicate.vpr
rename to src/test/resources/counterexample_mapped/predicate.vpr
diff --git a/src/test/resources/counterexamples/ref-sequence.vpr b/src/test/resources/counterexample_mapped/ref-sequence.vpr
similarity index 100%
rename from src/test/resources/counterexamples/ref-sequence.vpr
rename to src/test/resources/counterexample_mapped/ref-sequence.vpr
diff --git a/src/test/resources/counterexamples/sequence.vpr b/src/test/resources/counterexample_mapped/sequence.vpr
similarity index 100%
rename from src/test/resources/counterexamples/sequence.vpr
rename to src/test/resources/counterexample_mapped/sequence.vpr
diff --git a/src/test/resources/counterexamples/simple-refs-rec.vpr b/src/test/resources/counterexample_mapped/simple-refs-rec.vpr
similarity index 100%
rename from src/test/resources/counterexamples/simple-refs-rec.vpr
rename to src/test/resources/counterexample_mapped/simple-refs-rec.vpr
diff --git a/src/test/resources/counterexamples/simple-refs.vpr b/src/test/resources/counterexample_mapped/simple-refs.vpr
similarity index 100%
rename from src/test/resources/counterexamples/simple-refs.vpr
rename to src/test/resources/counterexample_mapped/simple-refs.vpr
diff --git a/src/test/scala/ExpectedCounterexampleAnnotation.scala b/src/test/scala/ExpectedCounterexampleAnnotation.scala
index d0e474d1e..3578e251c 100644
--- a/src/test/scala/ExpectedCounterexampleAnnotation.scala
+++ b/src/test/scala/ExpectedCounterexampleAnnotation.scala
@@ -91,8 +91,22 @@ case class ExpectedCounterexampleAnnotation(id: OutputAnnotationId, file: Path,
         } catch {
           case _: NumberFormatException => None
         }
-
     }
+    case PCall(idnuse, args, _) =>
+      val argValues = args.inner.toSeq.map(a => resolveWoPerm(a, model) match {
+        case Some(CEVariable(_, entry, _)) => Some(entry.toString)
+        case _ => None
+      })
+      if (argValues.forall(_.isDefined)) {
+        model.heapMap.get("current").flatMap(_.heapEntries.find({
+          case (p: ast.Predicate, pe: PredFinalEntry) if p.name == idnuse.name && pe.args == argValues.map(_.get) => true
+          case _ => false
+        }).map(he =>
+          (CEValueOnly(ConstantEntry(""), None), he._2.asInstanceOf[PredFinalEntry].perm)
+        ))
+      } else {
+        None
+      }
   }
 
   def resolve(exprs: Vector[PExp], model: ExtendedCounterexample): Option[Vector[(CEValue, Option[Rational])]] = {