CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination.
CVC4 is the fourth in the Cooperating Validity Checker family of tools (CVC, CVC Lite, CVC3) but does not directly incorporate code from any previous version. A joint project of Stanford University and U Iowa, CVC4 aims to support the features of CVC3 and SMT-LIBv2 while optimizing the design of the core system architecture and decision procedures to take advantage of recent engineering and algorithmic advances.
CVC4 is intended to be an open and extensible SMT engine. It can be used as a stand-alone tool or as a library, with essentially no limit on its use for research or commercial purposes (see license). To contribute to CVC4, please refer to our contribution guidelines.
CVC4 works with a version of first-order logic with polymorphic types and has a wide variety of features including:
Please visit the documentation page.
This page describes the possible input languages to CVC4.
Please refer to the Publications page.
Both pre-compiled binaries and the source code for CVC4 are available for download from Downloads.
The source code for CVC4 is also available on GitHub.
Find copyright and (lack of) warranty information for CVC4 here.
For bug reports, please use the CVC4 issue tracker. If you have a question, a feature request, or would like to contribute in some way, please contact one of the project leaders. The CVC-USERS list is for users of CVC3 and CVC4. We will make periodic announcements to this list and users are also encouraged to use it for discussion.