Rust bindings for the Z3 solver.
-
Updated
Jun 3, 2024 - Rust
Rust bindings for the Z3 solver.
A simple (unfinished) SMT solver for QF_ABV.
Sparse Merkle tree for a key-value map.
A bounded model checker for an IMP-style imperative language.
The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).
WIP - Library for efficient Presburger Arithmetic
A 'Sparse Merkle Tree' with versioned features, based on vsdb.
Carcará is a proof checker and elaborator for SMT proofs in the Alethe format.
Add a description, image, and links to the smt topic page so that developers can more easily learn about it.
To associate your repository with the smt topic, visit your repo's landing page and select "manage topics."