An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.
About
News
Downloads
Documentation
Publications
Awards
People
History
Third-Party Applications
Acknowledgements
This site provides our paper Designing Theory Solvers with Extensions and related material at FROCOS 2017.
The benchmarks considered in this section can be downloaded here.
The spreadsheet summarizing the results for the strings benchmarks considered in this paper can be accessed here: results-strings.xlsx.
We considered the sage2 family of benchmarks from the QF_BV division of SMT LIB. For instructions downloading these benchmarks, see this page.
The spreadsheet summarizing the results for the strings benchmarks considered in this paper can be accessed here: results-bv.xlsx.
We considered all benchmarks from the QF_NRA and QF_NIA divisions of SMT LIB. For instructions downloading these benchmarks, see this page.
The spreadsheet summarizing the results for the strings benchmarks considered in this paper for QF_NRA can be accessed here: results-nra.xlsx, and QF_NIA can be accessed here: results-nia.xlsx.