smtkit

smtkit is a small Rust toolkit for reproducible SMT workflows:

• Build constraints (typed IR in smtkit-core).
• Emit SMT-LIB2 (smtkit-smtlib).
• Run an external solver over stdio (optional).
• Capture artifacts (capability matrix, SMT2 scripts, models/cores/proofs) so solver-driven behavior is debuggable and comparable across solvers.

Why it exists

SMT integrations tend to go wrong in the same ways:

• Tooling silently depends on solver quirks (Z3 vs cvc5 behavior).
• Results are hard to reproduce (no stable script, no determinism hooks recorded).
• Debugging “why UNSAT?” is opaque (no unsat core, no minimal fragment, no provenance).

smtkit is built around the opposite posture: emit the script, run the solver, and keep the evidence.

Crates

• smtkit: facade crate you depend on (re-exports the rest).
• smtkit-core: typed, backend-agnostic constraint IR.
• smtkit-smtlib: SMT-LIB2 s-expressions, script building, and an incremental stdio session.
• smtkit-z3: optional in-process Z3 backend (feature-gated).
• smtkit-ci: small CLI for CI + debugging (probe, smoke).

Quickstart: probe solver capabilities

If you have a solver on PATH (e.g. z3), run:

smtkit-ci probe

This prints JSON like:

• which command line was used (e.g. z3 -in -smt2)
• a capability matrix (best-effort):
  • check_sat_assuming
  • get_model
  • get_unsat_core
  • get_proof (solver-dependent; primarily a debugging hook)
  • whether :named assertions appear in cores

You can also generate repro scripts:

smtkit-ci probe --emit-demo-smt2 --demo-kind sat
smtkit-ci probe --emit-demo-smt2 --demo-kind unsat-core
smtkit-ci probe --emit-demo-smt2 --demo-kind unsat-proof

Or write artifacts to disk:

smtkit-ci probe --output-json /tmp/smtkit_probe.json \
  --emit-demo-smt2 --demo-kind unsat-core --demo-smt2-out /tmp/demo.smt2

If you want smtkit-ci to run the demo and capture a bounded result (including a proof preview), use:

smtkit-ci probe --capture-demo --demo-kind unsat-proof --demo-proof-max-chars 12000

Notes on solver “proofs”

Some solvers support (get-proof) behind :produce-proofs. smtkit exposes this via the session API and the capability probe (get_proof) so you can capture proof objects for debugging/provenance.

This is not a proof checker: verification of solver proofs (e.g. Alethe proof checking) is a separate layer.