cvc5 Announcement

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:

• A simple, streamlined API, in C++, Python, and Java
• A fully redesigned proof system, capable of producing proof artifacts for all major reasoning components in cvc5, and capable of exporting those proofs in several backend formats
• Updated documentation, tutorials, websites
• A faster parser, with no dependencies on ANTLR or Java
• A new improved bit-vector solver
• A new improved solver for non-linear real arithmetic
• A new solver for sequences
• Better API support for creating and using multiple solver objects
• Support for the old “CVC” language will be discontinued; users will be encouraged to use the SMT-LIB standard input language instead

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

The cvc4 cvc5 team