smt-solving-with-z3-cvc5

SMT solving with Z3 and cvc5

Contract

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 encoding problem, so simplify the source property or add a lemma at the source. Done when: the calling tool's failure is traced to a backend choice or a source-level encoding change, and that change is applied.