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

Relational Constraint Solving in SMT

Baoluo Meng, Andrew Reynolds, Cesare Tinelli, Clark Barrett

This site provides our paper Relational Constraint Solving in SMT and related material at CADE 2017.

An extended version of our paper at CADE 2017 can be found below.

All materials to reproduce the experimental evaluation in our paper can be found below.

Downloads

Alloy Experiment

We run CVC4 with two configurations:

OWL Experiment

We run cvc4 with “–finite-model-find” enabled.