News

cvc5 Announcement
April 02, 2021

The cvc4 team has been hard at work on many major improvements to the system. For that and other reasons, we have decided that this is the right time to bump the “major version number,” meaning that we will soon be moving to cvc5. For those of you using cvc4, here is the relevant timeline and information:

CVC4 1.8 Released
June 19, 2020

We are delighted to announce version 1.8 of CVC4, the open-source flagship SMT solver. It is a joint project led by Stanford University and the University of Iowa. It is available at http://cvc4.cs.stanford.edu.

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:¹ 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.² 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.