An efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Third-Party Applications

Try CVC4 online!

15 July 2014

CVC4 1.4 Released

by Morgan Deters

This news post contains outdated information (e.g. links, instructions). Please refer to newer documentation for up-to-date information.

We are delighted to announce version 1.4 of CVC4, the open-source flagship SMT solver developed at New York University and the University of Iowa, available at

Version 1.4 features a new decision procedure for a theory of finite sets, numerous improvements to arithmetic, strings, bitvectors, and other theories, improved handling of quantified assertions, generally improved usability and stability, and many bugfixes. This 1.4 release is very near to the version submitted for this year’s CASC and SMT-COMP competitions.

We welcome feedback, feature requests, contributions, and collaborations. It is our hope that CVC4 will become a research platform for a broad and diverse set of users and developers. If you are interested in getting involved with the project, please contact a member of the development team:

The development of CVC4 is supported in part by the following organizations:

Downloads, documentation, tutorials, and more information are available at the CVC4 web site:

-The CVC4 team