Silicon implementation of new backend-independent counterexample format - #940

Merged

marcoeilers merged 27 commits into

meilers_raoul_counterexamples

Aug 14, 2026

Commits on Jul 1, 2024

General counterexample extraction by Raoul
marcoeilers
committed
ba24447
Partial models option
marcoeilers
committed
0906ba2

Commits on Feb 10, 2025

Merge
marcoeilers
committed
12d3a98

Commits on Feb 12, 2025

Merge
marcoeilers
committed
59acea6

Commits on Aug 28, 2025

Merge
marcoeilers
committed
69edd32

Commits on Aug 29, 2025

Getting tests to run
marcoeilers
committed
77cc77b
Adding new test class
marcoeilers
committed
b87c241
Implementing new common interface
marcoeilers
committed
ea48308

Commits on Sep 1, 2025

Adapting to silver changes
marcoeilers
committed
d0e4cec
Adapting to silver changes
marcoeilers
committed
0d044e9
Adapting to silver changes
marcoeilers
committed
e5a2de5

Commits on Jul 13, 2026

Commits on Jul 15, 2026

Map extraction, some missing evaluator cases
marcoeilers
committed
d78ce19

Commits on Jul 16, 2026

Merge
marcoeilers
committed
12bea46

Commits on Jul 23, 2026

Cleanup, quantified wand support
marcoeilers
committed
794de46
Avoid showing uninterpretable internal values
marcoeilers
committed
35dbe0f

Commits on Jul 25, 2026

Cleaned up wand entries
marcoeilers
committed
819c877
Merge
marcoeilers
committed
82f42a7

Commits on Aug 13, 2026

Changes after code review
marcoeilers
committed
4f326a0
Merge
marcoeilers
committed
d813e28
Fixing mapped counterexample test
marcoeilers
committed
c2cffac

Commits on Aug 14, 2026

Splitting up large functions
marcoeilers
committed
fee2cad
Fixed evaluating fields inside predicates
marcoeilers
committed
aca9dba