CVC4

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

About
News
Downloads
Publications
People
History
Third-Party Applications
Acknowledgements

Try CVC4 online!


News

CVC4 1.7 Released
April 09, 2019

We are delighted to announce version 1.7 of CVC4, the open-source flagship SMT solver developed at Stanford University, New York University and the University of Iowa, available at http://cvc4.cs.stanford.edu.


CVC4 1.6 Released
June 25, 2018

We are delighted to announce version 1.6 of CVC4, the open-source flagship SMT solver developed at Stanford University, New York University and the University of Iowa, available at http://cvc4.cs.stanford.edu.


CVC4 1.5 Released
July 10, 2017

We are delighted to announce version 1.5 of CVC4, the open-source flagship SMT solver developed at Stanford University, New York University and the University of Iowa, available at http://cvc4.cs.stanford.edu.


2015 Competition Results
November 24, 2015

CVC4 won several honors at competitions this year. As with last year, CVC4 won the most divisions of the main track of the SMT-COMP competition:1 of 28 competitive divisions, CVC4 won 12, Yices won 11, Boolector won 3, and CVC3 and AProVE each won one. CVC4 was also the overall winner.2 Note that once again, Z3 was not an official competitor this year, but it was run on the competition benchmarks for comparison purposes. If Z3 had been in the competition, the number of competitive divisions would have increased to 38 with the following breakdown: CVC4 wins 14, Z3 wins 12, Yices wins 8, Boolector wins 3, CVC3 wins 1.


CVC4 at Vienna Summer of Logic
July 28, 2014

CVC4 won several honors at the “Olympic Games” at the Vienna Summer of Logic. CVC4 won the most divisions of the SMT-COMP competition (14). Yices won the second most divisions (10). Unfortunately, both CVC4 and Yices got wrong answers due to bugs uncovered by the benchmark scrambling, disqualifying them from receiving an olympic medal. Medals instead went to veriT and SMTInterpol.


CVC4 1.4 Released
July 15, 2014

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 http://cvc4.cs.nyu.edu.


CVC4 1.3 Released
December 09, 2013

We are delighted to announce version 1.3 of CVC4, the open-source flagship SMT solver developed at New York University and the University of Iowa, available at http://cvc4.cs.nyu.edu.


CVC4 1.2 Released
May 10, 2013

We are delighted to announce version 1.2 of CVC4, the open-source flagship SMT solver developed at New York University and the University of Iowa, available at http://cvc4.cs.nyu.edu.


CVC4 1.1 Released
April 03, 2013

We are delighted to announce version 1.1 of CVC4, the open-source flagship SMT solver developed at New York University and the University of Iowa, available at http://cvc4.cs.nyu.edu.


Mac and Win32 Nightly Builds Available
March 26, 2013

As mentioned on the users’ mailing list the other day, Win32 binaries are now available for our nightly development builds (and will be available for the next stable release, coming soon).


CVC4 Tutorial to Run at CADE-24
December 12, 2012

Our tutorial entitled “Becoming a power user of SMT: The CVC4 solver, how it works, and how best to use it” was just accepted to run at CADE-24 in June 2013 in Lake Placid, NY. We are excited to have the opportunity to demonstrate the capabilities of CVC4 and to use it as a teaching device.


Announcing the Release of CVC4, Version 1.0
December 03, 2012

We are pleased to announce the first public release of CVC4, version 1.0, the open-source flagship SMT solver developed at New York University and the University of Iowa, available at http://cvc4.cs.nyu.edu.