Menu

Individual skill

smt-solving-with-z3-cvc5

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.

.devin/skills/smt-solving-with-z3-cvc5/SKILL.md

Read pinned source

Source commit b0e8ce89a19fac880251dc3ea1babfeb4503a4fe

What was checked

Matches the observed repository HEAD
Yes
Scanner rules are current
Yes
Repository scan complete
No
Skill scan complete
No
Observed behavior
Instructions only
Last checked
Nov 4, 2026

These are observations at the recorded commit, not a guarantee of safety. Review the source before running it.

Install this skill

Choose an agent in your Stack or copy a command below. Commands fetch the pinned commit and copy only this skill directory. Existing destinations are refused. Copying a command does not install anything.

An install command is unavailable: current rules, complete repository and skill scans, an eligible behavior level and a permitted license are required.

Repository context

Repository stars (not skill ratings)
55
Repository last updated
Sep 28, 2026
License
Apache-2.0

Observed agent integration: No specific integration evidence. Standard SKILL.md installation does not imply verified compatibility.

Files and excerpt

File metadata and permitted, redacted excerpts come from the recorded scan. Source links are pinned to that commit.

Browse files
Read excerpt

# 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.