CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.
SMT C++ Shell GAP Makefile Java Other
Latest commit 33ca2a3 Aug 17, 2017 @4tXJ7f 4tXJ7f committed on GitHub Remove unused SubrangeBound(s) classes (#221)
As discussed in pull request #220, commit
360d6ee mostly got rid of SubrangeBound(s).
There were still a few mentions of it left in the code, most of them commented
out. The occurrences in expr.i and expr_manager.i, however, created issues with
the Python wrapper. This commit removes the SubrangeBound(s) implementation and
other leftovers.
Failed to load latest commit information.
.settings BoolExpr removed and replaced with Expr Oct 5, 2012
config Use antlr-3.4 directory if already present in CVC4 root directory (#213) Aug 14, 2017
contrib Remove trailing slashes from directories if specified via command line. Jul 11, 2017
doc Modifying emptyset.h and sexpr. Adding SetLanguage. Dec 19, 2015
examples Moving from the gnu extensions for hash maps to the c++11 hash maps Jul 21, 2017
proofs Change remaining hash_set -> unordered_set (#208) Jul 30, 2017
src Remove unused SubrangeBound(s) classes (#221) Aug 17, 2017
test Remove unused SubrangeBound(s) classes (#221) Aug 17, 2017
.clang-format Adding a clang format file for the project. Sep 18, 2016
.cproject Whitespace difference Apr 23, 2015
.gitignore API documentation improvements. Jun 22, 2014
.mailmap update from the master Apr 20, 2016
.project IDL example theory (to be used with --use-theory=idl). Jun 6, 2013
.travis.yml Optionally split regression tests into test groups (#207) Aug 8, 2017
AUTHORS Updates to AUTHORS and THANKS for 1.5 (mostly done by Tim). Jun 30, 2017
COPYING Update to COPYING May 5, 2016
INSTALL updated INSTALL for version 1.5 Jul 5, 2017
Makefile Update competition build rules. Nov 7, 2014 More work on sygus. Add regress4 to Makefile. Mar 28, 2017 Fix build rule. Aug 25, 2014
Makefile.subdir Some fixes inspired by Fedora 15: Jun 18, 2011
NEWS Update unit test, news. Jul 5, 2017
README Update README for 1.5 release (#182) Jul 4, 2017
THANKS Updates to AUTHORS and THANKS for 1.5 (mostly done by Tim). Jun 30, 2017 Merge from my post-smtcomp branch. Includes: Sep 2, 2011 Fix help message for disable-unit-testing in (don't -> d… Aug 9, 2017
library_versions Prerelease versioning for master. Jul 10, 2017


This is CVC4 release version 1.5.  For build and installation notes,
please see the INSTALL file included with this distribution.

The project leaders are Clark Barrett (Stanford University) and Cesare
Tinelli (The University of Iowa).  For a full list of authors, please
refer to the AUTHORS file in the source distribution.

CVC4 is a tool for determining the satisfiability of a first order
formula modulo a first order theory (or a combination of such
theories).  It 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.

CVC4 is intended to be an open and extensible SMT engine.  It can be
used as a stand-alone tool or as a library.  It has been designed to
increase the performance and reduce the memory overhead of its
predecessors.  It is written entirely in C++ and is released under an
open-source software license (see the file COPYING in the source

*** Getting started with CVC4

For help installing CVC4, see the INSTALL file that comes with this

We recommend that you visit our CVC4 tutorials online at:

for help getting started using CVC4.

*** Contributing to the CVC4 project

We are always happy to hear feedback from our users:

* if you need help with using CVC4, please refer to

* if you need to report a bug with CVC4, or make a feature request,
  please visit our bugtracker at or
  write to the mailing list.  We are very
  grateful for bug reports, as they help us improve CVC4, and patches
  are generally reviewed and accepted quickly.

* if you are using CVC4 in your work, or incorporating it into
  software of your own, we'd like to invite you to leave a description
  and link to your project/software on our "Third Party Applications"
  page at

* if you are interested in contributing code (for example, a new
  decision procedure implementation) to the CVC4 project, please
  contact one of the project leaders.  We'd be happy to point you to
  some internals documentation to help you out.

Thank you for using CVC4!

*** The History of CVC4

The Cooperating Validity Checker series has a long history.  The
Stanford Validity Checker (SVC) came first in 1996, incorporating
theories and its own SAT solver.  Its successor, the Cooperating
Validity Checker (CVC), had a more optimized internal design, produced
proofs, used the Chaff SAT solver, and featured a number of usability
enhancements.  Its name comes from the cooperative nature of decision
procedures in Nelson-Oppen theory combination, which share amongst
each other equalities between shared terms.  CVC Lite, first made
available in 2003, was a rewrite of CVC that attempted to make CVC
more flexible (hence the "lite") while extending the feature set: CVC
Lite supported quantifiers where its predecessors did not.  CVC3 was a
major overhaul of portions of CVC Lite: it added better decision
procedure implementations, added support for using MiniSat in the
core, and had generally better performance.

CVC4 is the new version, the fifth generation of this validity checker
line that is now celebrating twenty-one years of heritage.  It
represents a complete re-evaluation of the core architecture to be
both performant and to serve as a cutting-edge research vehicle for
the next several years.  Rather than taking CVC3 and redesigning
problem parts, we've taken a clean-room approach, starting from
scratch.  Before using any designs from CVC3, we have thoroughly
scrutinized, vetted, and updated them.  Many parts of CVC4 bear only a
superficial resemblance, if any, to their correspondent in CVC3.

However, CVC4 is fundamentally similar to CVC3 and many other modern
SMT solvers: it is a DPLL(T) solver, with a SAT solver at its core and
a delegation path to different decision procedure implementations,
each in charge of solving formulas in some background theory.

The re-evaluation and ground-up rewrite was necessitated, we felt, by
the performance characteristics of CVC3.  CVC3 has many useful
features, but some core aspects of the design led to high memory use,
and the use of heavyweight computation (where more nimble engineering
approaches could suffice) makes CVC3 a much slower prover than other
tools.  As these designs are central to CVC3, a new version was
preferable to a selective re-engineering, which would have ballooned
in short order.

*** For more information

More information about CVC4 is available at: