CVC4

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

Try CVC4 online!


CI

Designing Theory Solvers with Extensions

Andrew Reynolds, Cesare Tinelli, Dejan Jovanovic, Clark Barrett

This site provides our paper Designing Theory Solvers with Extensions and related material at FROCOS 2017.

Downloads

Extended Theory of Strings

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.

Lazy Bit-blasting for Expensive Bit-Vector Operators

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.

Lightweight Techniques for Non-linear Arithmetic

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.