[SwayamInSync]

A failure cvc5 found showed the error and nothing else. The certifier checked cvc5's model against the true definitions, and then the verifier dropped it:

• there was no counterexample note and no path;
• the JSON record had no counterexample, model, or trace, and SARIF had no code flow;
• under --lean-fallback, a race that cvc5 won wrote no Lean refutation (the solver's model gives the goal's variables no values).

The limitations page said so: cvc5's models "are not yet shown as source-level values". This is plan item D6, stacked on #105 (E6).

Before and after

clamp.cpp, the example this PR adds to chapter 17:

namespace cv = cppverify;

int clamp(int x)
  cv::pre(x > -100 && x < 100)
  cv::post(cv::result >= 0)
{
  if (x < 0)
    return x + 1;
  return x;
}

cpp-verify --backend=cvc5 clamp.cpp before:

clamp.cpp:5:23: error: verification failed: clamp [postcondition] [backend=cvc5] [reason=counterexample]
    5 |   cv::post(cv::result >= 0)
      |            ~~~~~~~~~~~^~~~
Summary: 1 failed in 0.0 s

and now, as Z3 reports it:

clamp.cpp:5:23: error: verification failed: clamp [postcondition] [backend=cvc5] [reason=counterexample]
    5 |   cv::post(cv::result >= 0)
      |            ~~~~~~~~~~~^~~~
clamp.cpp:5:23: note: counterexample: x = -2, result = -1
clamp.cpp:7:3: note: takes the true branch
    7 |   if (x < 0)
      |   ^
clamp.cpp:8:5: note: returns -1
    8 |     return x + 1;
      |     ^
Summary: 1 failed in 0.0 s

The same values and steps are in the JSON record (counterexample, model, trace), in SARIF (the message and the code flow), in the GitHub annotation, and in archive replay with --backend=cvc5.

How

describeCounterexample (Backend/Certify.cpp) describes a certified model. cvc5's models are read by the adapter, not by a solver API, so the certifier does it, in the model it has just checked, with its own evaluation (evaluateTerm): a value shown is a value the check used, and nothing completes the model. It fills:

• Model: the source variables of the obligation's query (candidateValues), listed by internal name, the order of Z3's models, so a cvc5 record lists its variables as a Z3 record does;
• OnPath: each version's guard, so a version of a branch the path does not take is left out of the text, as for Z3;
• Trace: the obligation's events up to its TraceEventCount; an event whose guard is false is dropped, and one the model does not decide is kept and marked undetermined. Each event's values are evaluated too;
• Assignment: the goal's variables, which a Lean refutation states.

The cvc5 adapter calls it at both places where it reports a certified failure: a model after sat, and a model cvc5 prints with unknown. cvc5 solves each obligation alone, so the query is always one obligation's.

Replay printed the counterexample note without a location (note: counterexample: ...) while every step had one. It is now at the failing check, as in a source run (Main.cpp).

Checks

On failure_notes.cpp there are 14 failures: branches, a call, stores, new/delete, local objects and references, loops, a long path, an undecided branch, a macro, and two overflows. cvc5's notes are Z3's line for line, except for values each solver picks itself (in heap, v = 0 for cvc5 and v = -1 for Z3). A script compared the 14 JSON records of the two solvers: each has the same obligation, the same model entries (names, versions, on_path), and the same trace events (kind, message, active, line). Before the order change, the only difference was the order of the model.

The Lean refutation of a race that cvc5 won was checked in a build where the race prefers cvc5's answer (a local change, not committed). On lean_refutation.cpp, --backend=race --lean-fallback wrote refutations for the four failures cvc5 settled. --lean-certify then reported each (confirmed in Lean). As with Z3, pick_one is not confirmed: Lean cannot decide the goal at the counterexample.

Tests

• suite/failure_notes_cvc5.test (new, needs cvc5) runs failure_notes.cpp on cvc5 and checks:
  • the text: the counterexample with its versions; the steps, with no untaken branch between them; a call's argument tied to the counterexample's value; a local object's address and stored value; a loop entered and left; the elision of a long path; an undecided branch; a check inside a loop whose path ends at the iteration;
  • JSON: the record's counterexample, the model's first entry (result, Z3's order), the version marked on_path: false, and a step's text;
  • replay with --backend=cvc5;
  • Inputs/failure_notes_quantified.cpp, a failure cvc5 answers unknown for, with a model that the certifier certifies.
• CertifyTest.CounterexamplesAreDescribedAlongTheFailingPath (unit) builds a module of two obligations and checks:
  • the model's order and on_path marks;
  • the second obligation's steps: a dropped branch, an undecided one, and a return's value;
  • the assignment;
  • that the first obligation gets its own, shorter path.
    It needs neither cvc5 nor a race.
• failure_notes.cpp: the replayed counterexample note is at its check.
• solver_race.cpp: the failure has its counterexample whichever solver wins the race.

On the base, failure_notes_cvc5.test fails at its first counterexample note, and the unit test does not compile (describeCounterexample does not exist).

Each mutant below, applied alone and rebuilt, is caught by failure_notes_cvc5.test, failure_notes.cpp, or the unit test (11 of 11):

Mutant	Change
D1	a model cvc5 finds after sat is not described
D2	a model cvc5 prints with unknown is not described
D3	the model keeps the query's order
D4	no version is marked off the path
D5	every step is marked taken
D6	steps the path does not take are kept
D7	step values are not evaluated
D8	every event of the module is a step
D9	no assignment
D10	the failing obligation is the module's first
R1	replay notes have no location

On a release build of this branch merged with main (#97 to #99, #104, and #105 merged forward, all pushed), the Verify suite ran 498 tests: 497 passed. The one failure was obligation_size_limit.cpp, a test from #48 that expected cppverify.diagnostic/1 records; it is updated on #105 (74cac50) and passes. The 57 tests that use cvc5, a race, the portfolio, archive replay, or a Lean fallback pass on the branch itself, and so does the new unit test. The full VerifyTests run was not finished here.

Stacked on #105.