/smt-solving-with-z3-cvc5

name: smt-solving-with-z3-cvc5
description: 'Use when a query needs direct SMT solving, an unsat core needs debugging, or another tool reports a solver timeout or unknown. Not for deciding what to prove: use proof-driven.'
disable-model-invocation: true

SMT solving with Z3 and cvc5

Contract

| Field | Bound contract | |---|---| | Trigger | A constraint problem needs an SMT-LIB query written and solved, an `unsat` result needs its core explained, or a verifier built on Z3 or cvc5 (Apalache, Kani, Verus, Frama-C WP, Dafny, Why3) reports `unknown` or a timeout that must be diagnosed. | | Authority | Reversible local: writes `.smt2` files and solver logs; rollback is deleting them. No remote mutation. | | Side effect | Query files and captured solver output on disk. Solver runs are bounded by an explicit timeout. | | Done | Every query has a recorded verdict of `sat` with a model, `unsat` with a core, or `unknown` with the solver's reason and the change that resolves it. |

Inputs

The constraint problem, or the failing query dumped by the calling tool. Solver pins from the grounded set: Z3 z3-5.1.0 (`pip install z3-solver`, or `apt`, `brew`, prebuilt binaries, or source) and cvc5 cvc5-1.3.4 (`pip install cvc5`, prebuilt binaries, or source). The input language is SMT-LIB 2.7 (reference document revision 2026-03-27, https://smt-lib.org/). Optional: a target logic, a per-query timeout budget, and the calling tool's own solver options.

Procedure

1. Choose the logic and declare the sorts. Open the file with `(set-logic L)` where `L` is the narrowest fragment that fits: `QF_LIA` for linear integers, `QF_BV` for fixed-width bit-vectors, `QF_UFLIA` when uninterpreted functions join linear arithmetic, `QF_ABV` for bit-vectors with arrays. Quantifier-free fragments decide; quantified ones may return `unknown`. Z3 and cvc5 both accept `ALL` as a solver keyword that enables every theory, but `ALL` is not a logic named by the standard, so use it only for exploration. Declare each variable with `(declare-const x Int)` and each function with `(declare-fun f (Int) Bool)`. Done when: the header names one logic and every symbol is declared before use. 2. Write the assertions with names. Turn on the options first, because the standard requires `(set-option :produce-models true)` and `(set-option :produce-unsat-cores true)` before any declaration or assertion. Wrap every assertion whose origin matters as `(assert (! <term> :named a1))`. Names are what an unsat core reports, so one assertion per requirement and one name per source line. End with `(check-sat)` and, on the expected branch, `(get-model)` or `(get-unsat-core)`. Done when: every assertion carries a name that maps back to a requirement. 3. Run with a timeout. Z3: `z3 -smt2 -T:30 query.smt2` sets a hard 30-second limit for the whole process; `-t:30000` sets a soft limit in milliseconds that ends only the current query; `-st` prints statistics. cvc5: `cvc5 --lang smt2 --tlimit=30000 query.smt2` limits the whole run in milliseconds and `--tlimit-per=30000` limits each `check-sat`; `--stats` prints statistics. Run both solvers on any query that matters: agreement on `unsat` is the cross-check, disagreement is a bug in the query or a solver. Done when: both solvers have printed a verdict or a timeout under the recorded budget. 4. Read `sat`. Issue `(get-model)`; the reply is a list of `define-fun` forms, one per declared symbol. A model is a witness that the assertions are jointly satisfiable, so when the query encodes "the property can be violated", the model is the counterexample: substitute its values into the original requirement and confirm by hand that it breaks. Done when: the model has been replayed against the property and the violation is understood or the encoding is fixed. 5. Read `unsat`. Issue `(get-unsat-core)`; the reply is a subset of the named assertions that is already unsatisfiable. When the query encodes "the property can be violated", `unsat` is the proof and the core names which assumptions the proof needs. When the query encodes a system that should have solutions, `unsat` means the requirements conflict and the core is the smallest set to argue about. Remove one core member at a time and rerun to confirm that each is necessary. For assumption sets that change between checks, use `(check-sat-assuming (a1 a2))` with `(set-option :produce-unsat-assumptions true)` and read `(get-unsat-assumptions)`, which keeps the base assertions fixed and avoids a `push`/`pop` cycle. Done when: every core member is confirmed necessary and mapped to its requirement. 6. Read `unknown` and timeouts. After `unknown`, issue `(get-info :reason-unknown)`; the standard defines `memout` and `incomplete`, and each solver adds its own strings (Z3 prints `timeout` and `canceled`; cvc5 names `TIMEOUT`, `RESOURCEOUT`, `MEMOUT`, `INCOMPLETE`, and `REQUIRES_FULL_CHECK`). Z3 exits 102 on a hard `-T:` timeout after printing `timeout`; cvc5 exits 0 after a completed run whatever the verdict and 1 on an option or API error, so read the printed verdict and not the exit code. Resolve in this order: narrow the logic (quantified to quantifier-free, `Int` to `BitVec` when the domain is finite), remove quantifiers by instantiating the finite domain, split one large query into per-property queries, then raise the timeout once with a written reason. Done when: the query returns `sat` or `unsat`, or the reason it cannot is recorded with the reductions tried. 7. Diagnose another tool's solver failure. Get the tool to dump its query (Frama-C WP writes its proof obligations to the directory named by `-wp-out`; Apalache selects its backend with `--smt-solver=z3` or `cvc5`; Kani accepts `#[kani::solver(z3)]` or `cvc5` on the harness). Run the dumped `.smt2` through steps 3 to 6 with both solvers. A query that one solver settles in seconds and the other cannot is a backend choice, so switch the calling tool's backend. A query neither solver settles is an encod