Debugging SMT failures

You added @verify(formal) to a function, the compiler says the solver can't prove the postcondition, and you don't know why. This page is the playbook.

The four states

Solver says	Meaning	Your move
unsat	obligation is true	nothing — compile proceeds
sat + counter-example	false — the obligation can be violated	fix the code or weaken the contract
unknown	can't decide in time / too hard	make the obligation easier
timeout	didn't finish in smt_timeout_ms	simplify or raise the budget

Read the counter-example

verum verify prints a per-function report, not a source-anchored diagnostic. Captured directly (not reconstructed) from fn abs_maybe(x: Int) -> Int ensures result > 0 { x }, a minimal postcondition violation:

Verification Report:
============================================================
  ✗ abs_maybe: Failed in 0.01s
      Counterexample: Counterexample:
  result = 0
  x = 0

Violates: postcondition violation

Summary: 1 proved, 1 failed, 0 timeout, 0 skipped

There's no source line or caret — the counter-example is a flat list of bindings under Counterexample:, and it's the weakest violating input the solver found by checking the function symbolically, not necessarily a value tied to any specific call site. For a push-style obligation you'd read the same shape with self's fields and the pushed value in place of result/x:

Often the counter-example reveals an edge case you hadn't
considered (overflow, empty collection, NaN).

### Diagnostic flags

Ask the prover to narrate what it did:

```bash
$ VERUM_TRACE_PROOFS=1 verum verify src/stack.vr

Each line names the tactic, the goal it faced and the outcome; an apply additionally reports how the lemma was instantiated and, on a failure, both sides of the unification. This distinguishes the two failures that look identical from the outside: a goal that is hard, and a goal that is unconstrained because its predicate never reflected.

There is currently no flag that writes the generated SMT-LIB to disk.

Time each obligation:

$ verum analyze --refinement
 obligation                          routed      ms   result
 stack.push/postcond#1              smt-backend           8   unsat
 stack.push/postcond#2              smt-backend         340   unsat   ← slow
 stack.merge/postcond#3             smt-backend        72   unsat
 stack.balance/postcond#1           portfolio  800   unknown  ← problem

Playbook — "solver can't prove a true obligation"

1. Is it actually true?

Obvious but essential. Trace by hand; write a property test:

@property
fn push_grows_len(s: Stack<Int>, x: Int) {
    let before = s.len();
    let after = s.push(x).len();
    assert_eq(after, before + 1);
}

If the property test finds a counter-example, the claim is false.

2. Missing invariant

For loops: the invariant clauses must imply the postcondition when combined with the exit condition. Common omissions:

• Loop-variable bounds (0 <= i && i <= n).
• Accumulator invariants (sum == i * (i+1) / 2).
• Structural invariants (xs.iter().take(i).all(|x| pred(x))).

Write the post-loop state as a conjunction; each conjunct needs explicit support from an invariant.

3. Missing decreases

Loop termination isn't proven automatically for complex loops. Supply an explicit decreases measure; clause.

4. Quantifier trouble

forall x: Int. P(x) — unbounded — forces the solver to synthesise instantiations. Bound it:

forall i in 0..n. P(i)               // has bounds
forall x: Int where 0 <= x && x <= max. P(x)

5. Nonlinear arithmetic

Different solver adapters vary in nonlinear strength. The capability router already routes nonlinear goals to the strongest available adapter, but if that's still not enough, escalate:

@verify(thorough) fn nonlinear_fn(...) -> ... { ... }

thorough races the available solver adapters and tactic-based proof search in parallel and takes the first success. Otherwise, supply lemmas that linearise the reasoning.

6. The helper never reflected

If the predicate calls a helper, that helper must qualify for reflection (pure, single expression, parameterised). Otherwise the solver sees an uninterpreted function it cannot unfold — and the goal is unconstrained rather than hard. The reflection warnings name the leaf that failed.

See Logic functions.

7. Too many obligations in one function

Split the function. Each obligation is solved independently; smaller goals are easier.

Playbook — "solver times out"

1. Raise the budget (temporarily, to see if it's a hard-limit issue):

   [verify]
   solver_timeout_ms = 30_000

2. Simplify the body. Extract intermediate computations into helper functions with their own contracts. Split conjunctive postconditions.

3. Escalate the strategy:

   @verify(thorough)    // races the SMT layer + proof search in parallel
   @verify(certified)   // thorough + orthogonal cross-validation

   The capability router already routes nonlinear / string / finite-model-finding goals to the strongest available adapter and LIA / bitvector / array goals to the cheapest one, so you do not need to pin a backend — escalating the strategy is the right lever.

4. Supply inductive hints:

   // Prove a lemma separately; use it inside the main proof.
   lemma helper_monotonic(a: Int, b: Int)
       requires a <= b
       ensures f(a) <= f(b)
   { by induction a { ... } }

5. Use assume sparingly to prune search:

   if !likely_to_help { return result; }
   assume(condition_that_holds);       // hint to solver
   // ... rest of function ...

Playbook — "counter-example is weird"

"Weird" usually means one of:

• Integer overflow: Int is 64-bit; the counter-example may involve values near Int.MAX. Add explicit bounds.
• NaN / infinity: Floats allow NaN which is ≠ to everything. Use is_finite() guard.
• Empty collection: sizes zero break many invariants. Add a self.len() > 0 refinement or handle the empty case.
• Ghost field: a field whose value is unconstrained. Add an invariant linking it to observable state.

Playbook — "portfolio disagreement"

With @verify(thorough) several adapters race the same obligation. If two return conflicting verdicts, that is a potential solver bug rather than a defect in your code. Action:

1. Re-run each strategy on its own to see which adapter produced which verdict.
2. Check for timeouts — sometimes unknown is reported as sat by one tool and unsat by another due to resource limits.
3. File a bug with the minimal reproducer — both to Verum and to the upstream solver maintainer.

General tips

• Start small: verify one short function completely before adding @verify(formal) project-wide.
• Incremental proving: prove sub-claims as named lemmas that the main theorem can apply.
• Cache awareness: if you edit only the body and the solver suddenly complains, try verum smt-stats --reset.
• Print debug info: verum verify --trace obligation_id=push_postcond#1 shows the SMT interaction step by step.

See also

• Verification → SMT routing — which solver handles what.
• Verification → proofs — when SMT isn't enough, write a proof.
• Architecture → verification pipeline — internal architecture of the SMT verification subsystem.