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

Third-Party Applications

Try CVC4 online!

2 April 2021

cvc5 Announcement

by cvc5 team

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:

May 1, 2021: GitHub migration

We will create a new cvc5 organization on GitHub, move the cvc4 repository there, and rename it cvc5. Note that by doing it this way, all previous GitHub links involving the old organization or repository will be redirected to the new organization and repository. The old cvc4 organization will contain an archived copy of the cvc4 repository up through the last cvc4 release (version 1.8, released in June 2020). For those of you using that release, please continue to use it. If you are using a recent nightly build, we recommend that you move to the new cvc5 nightly build as of May 1, as there will no longer be cvc4 nightly builds.

Fall 2021: First cvc5 release

We expect to have the first stable release of cvc5 in Fall 2021 (probably October or November - exact date to be determined). Here are some of the new features that cvc5 will offer:

Stay tuned for more information about the release. We hope to welcome you as a cvc5 user soon!

The cvc4 cvc5 team