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:

• several built-in base theories: rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bit-vectors, strings, finite sets and relations, separation logic, floating point arithmetic, and equality over uninterpreted function symbols
• support for quantifiers
• an interactive text-based interface
• a rich C++ API for embedding in other systems
• model generation abilities

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.

Copyright

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.