Z3 cookbook

Nitpick's DbC verifier is useful when code is written in a solver-friendly style. This chapter collects practical patterns from the v0.34.x cycle.

Feed the solver named facts

Prefer explicit boundary constraints:

Rules:Percentage = { $ >= 0, $ <= 100 };

func:check = NIL(int32:x)
    requires x >= 0i32, x <= 100i32
{
    limit<Percentage> int32:pct = x;
    prove(pct <= 100i32);
    pass(NIL);
};

requires gives the function an assumption. limit<Rules> gives a local binding with a named range. prove locks the intended fact.

Keep clauses simple

Good clauses are usually comparisons over parameters, locals, and result:

requires x >= 0i32, x < 1000i32
ensures result > 0i32
invariant i >= 0i32, sum >= 0i32

Avoid nested calls or side-effect-like expressions inside contracts. v0.34.x purity checks reject calls in contract and invariant clauses because solver facts must not hide execution.

Understand proof outcomes

For user assertions, the verifier checks whether a counterexample exists:

• no counterexample: proof succeeds;
• counterexample: the claim is invalid;
• unknown: the current encoder/timeout could not discharge it.

prove treats invalid and unknown outcomes as hard errors. assert_static keeps a runtime fallback for unknown/dynamic cases, but CTFE-known false user assertions are ARIA-075 errors.

Use reports and dumps

Useful flags:

--verify
--verify-contracts
--prove-report
--debug-z3
--debug-contracts

• --prove-report prints proof outcomes for supported obligations.
• --debug-z3 dumps SMT-LIB for prove and assert_static obligations.
• --debug-contracts enables runtime checks for contract/invariant paths where applicable.

Make counterexamples smaller

When a proof fails unexpectedly:

1. Reduce the expression to one prove statement.
2. Add limit<Rules> bindings for inputs with known ranges.
3. Move facts from comments into requires / ensures.
4. Split helper functions so each has a small contract.
5. Run with --debug-z3 and inspect the dumped assumptions.

Choose the right surface

Known limits

The v0.34.x verifier is intentionally first-order and finite. Deferred work includes quantified collection contracts, proof tactics, user hints, and richer refinement types beyond limit<Rules>.