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!


About CVC4

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 The University of Iowa, CVC4 aims to support the features of CVC3 and Version 2 of the SMT-LIB standard 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).

CVC4 is succeeded by cvc5.


Features

CVC4 works with a version of first-order logic with polymorphic types and has a wide variety of features including:

Documentation

Please visit the documentation page.

Input Languages

This page describes the possible input languages to CVC4.

Citing CVC4

Please refer to the Publications page.

Getting CVC4

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.

Technical Support

CVC4 is succeeded by cvc5.

For bug reports, please first check if the problem persists after switching to cvc5. If yes, report issues via the cvc5 issue tracker.