A generic library to interact with SMT-LIB 2 compliant solvers running in a separate system process, such as Z3 and CVC4.
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
rsc
src
.appveyor.yml
.gitignore
.travis.yml
CHANGES.md
Cargo.lock
Cargo.toml
LICENSE-APACHE
LICENSE-MIT
README.md
_config.yml

README.md

rsmt2

linux windows
Build Status Build status Latest Version codecov

A generic library to interact with SMT-LIB 2 compliant solvers running in a separate system process, such as Z3 and CVC4. Currently only tested with z3.

Crate.io documentation.

If you use this library consider contacting us on the repository so that we can add your project to the readme.

See CHANGES.md for the list of changes.

Future features (if requested)

  • support for solvers other than z3
  • get-proof

Known projects using rsmt2

  • kinō, a model-checker for transition systems (abandoned)
  • hoice, a machine-learning-based predicate synthesizer for horn clauses

License

MIT/Apache-2.0