Silicon implementation of new backend-independent counterexample format

[marcoeilers]

Silicon implementation of the new backend-independent counterexample format (see viperproject/silver#883), written by @rvandoren in his practical work project.

A lot of the code is used to evaluate arbitrary Silicon terms in a state described by a Z3 model, which is used for example to evaluate permission amounts that quantified chunks provide for specific heap locations.

[AndreaKe]

Some nitpicky comments, otherwise LGTM

[Copilot]

Pull request overview

Implements Silicon support for the new backend-independent counterexample format by introducing “raw” and “resolved” counterexample generation from SMT models, extending term evaluation to cover more Silicon term constructs, and wiring the new counterexample modes into symbolic execution.

Changes:

• Add SiliconResolvedCounterexample/SiliconRawCounterexample to transform Z3 models into Viper counterexamples (including collections/heaps/domains/functions).
• Extend Converter.evaluateTerm with environment binding and support for additional boolean/int/perm/map operations used by counterexample resolution.
• Update counterexample plumbing (model kinds, permission-term inlining) and adjust/replace counterexample test suites and Z3 configuration.

Reviewed changes

Copilot reviewed 20 out of 20 changed files in this pull request and generated 4 comments.

Show a summary per file

File	Description
src/test/scala/MappedCounterexampleTests.scala	Renames/retargets mapped counterexample test suite and annotation wrapper.
src/test/scala/GeneralCounterexampleTests.scala	Adds a general/resolved counterexample test suite and verifier config.
src/test/resources/counterexamples/simple-refs.vpr	Removes legacy counterexample test input.
src/test/resources/counterexamples/simple-refs-rec.vpr	Removes legacy counterexample test input.
src/test/resources/counterexamples/sequence.vpr	Removes legacy counterexample test input.
src/test/resources/counterexamples/ref-sequence.vpr	Removes legacy counterexample test input.
src/test/resources/counterexamples/predicate.vpr	Removes legacy counterexample test input.
src/test/resources/counterexamples/permissions.vpr	Removes legacy counterexample test input.
src/test/resources/counterexamples/negative.vpr	Removes legacy counterexample test input.
src/test/resources/counterexamples/method-call.vpr	Removes legacy counterexample test input.
src/test/resources/counterexamples/lseg.vpr	Removes legacy counterexample test input.
src/test/resources/counterexamples/functions.vpr	Removes legacy counterexample test input.
src/test/resources/counterexamples/cyclic-ref.vpr	Removes legacy counterexample test input.
src/main/scala/rules/SymbolicExecutionRules.scala	Wires in Raw/Resolved counterexample modes.
src/main/scala/rules/QuantifiedChunkSupport.scala	Avoids macros for permission terms when counterexamples are requested.
src/main/scala/rules/MoreCompleteExhaleSupporter.scala	Inlines pTaken term when counterexamples are requested to keep permission arithmetic evaluable.
src/main/scala/reporting/SiliconResolvedCounterexample.scala	Introduces raw/resolved counterexample construction from SMT models (large new implementation).
src/main/scala/reporting/Converter.scala	Extends term evaluation (env binding + more operations) for counterexample resolution.
src/main/resources/z3config.smt2	Enables partial models in Z3 configuration.

Suppressed comments (1)

src/test/scala/MappedCounterexampleTests.scala:21

• testDirectories points to counterexample_mapped, but this directory does not exist under src/test/resources in this branch, so this suite will either discover no tests or fail to load resources. Add the missing resource directory/files, or change testDirectories to an existing resource path.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.