19 June 2020
CVC4 1.8 Released
by Andres Noetzli
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
- New C++ and Python API: CVC4 has a new, more streamlined API. We plan to
make CVC4 1.8 the last version that ships with the legacy API.
- Strings: Full support of the new SMT-LIB standard for the theory of strings,
- Support for
- Support for new operator names (e.g.
str.in_re instead of
new escape sequences. The new syntax is enabled by default for smt2 files.
- Support for syntax-guided synthesis (SyGuS) problems in the new API. C++
examples of the SyGuS API can be found in
- Support for higher-order constraints. This includes treating function sorts
->) as first-class sorts and handling partially applied
function symbols. Support for higher-order constraints can be enabled by
- Support for set comprehension binders
- Eager bit-blasting: Support for SAT solver Kissat.
- API: Function definitions can now be requested to be global. If the
parameter is set to true, they persist after popping the user context.
- Java/Python bindings: The bindings now allow users to catch exceptions
- Arithmetic: Performance improvements
- Linear solver: New lemmas inspired by unit-cube tests
- Non-linear solver: Expanded set of axioms
- Ackermannization: The Ackermannization preprocessing pass now supports
uninterpreted sorts and as a result all QF_UFBV problems are supported in
combination with eager bit blasting.
- CVC language: Models printed in the CVC language now include an explicit end
marker to facilitate the communication over pipes with CVC4.
- API change:
SmtEngine::query() has been renamed to
Result::Validity has been renamed to
Result::Entailment along with corresponding changes to the enum values.
- Java API change: The name of CVC4’s package is now
- The default output language is changed from CVC to SMT-LIB 2.6. The
default output language is used when the problem language cannot be
easily inferred (for example when CVC4 is used from the API).
- Printing of BV constants: previously CVC4 would print BV constant
values as indexed symbols by default and in binary notation with the
option –bv-print-consts-in-binary. To be SMT-LIB compliant the
default behavior is now to print BV constant values in binary
notation and as indexed symbols with the new option
–bv-print-consts-as-indexed-symbols. The option
–bv-print-consts-in-binary has been removed.
- Updated to SyGuS language version 2.0 by default. This is the last release
that will support the SyGuS language version 1.0 (
script is provided to convert version 1.0 files to version 2.0, see
- Support for user-provided rewrite rule quantifiers has been removed.
- Support for certain option aliases has been removed.
- Support for parallel portfolio builds has been removed.
We welcome feedback, feature requests, contributions, and collaborations. It
is our hope that CVC4 will become a research platform for a broad and diverse
set of users and developers. If you are interested in getting involved with
the project, please contact a member of the development
The development of CVC4 is supported in part by the organizations listed in the
Downloads, documentation, tutorials, and more information are available at the
CVC4 web site: http://cvc4.cs.stanford.edu/
-The CVC4 team