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!


Scaling Up DPLL(T) String Solvers using Context-Dependent Simplification

Andrew Reynolds, Maverick Woo, Clark Barrett, David Brumley, Tianyi Liang, Cesare Tinelli

This site provides our paper Scaling Up DPLL(T) String Solvers using Context-Dependent Simplification and related material at CAV 2017.

Downloads

Solver Configurations

To enable individual configurations of CVC4:

Results

Our evaluation used the StarExec cluster for evaluation. We provide a spreadsheet results-cav17.xlsx containing detailed results of the experiments. The columns of this spreadsheet show all benchmark/solver pairs, as well as various additional tests to verify the correctness of models produced by z3 and cvc4, on benchmarks where solvers gave different answers, including timeouts. For instance the column “z3 : +cvc4-m” indicates the result of z3 on the original benchmark plus constraints corresponding to cvc4’s model. The scripts used to test the consistency of models can be found here.