# CVC4

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

9 April 2019

# CVC4 1.7 Released

by Haniel Barbosa

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.

New Features:

• Proofs:
• Support for bit-vector proofs with eager bitblasting (older versions only supported proofs with lazy bitblasting).
• Strings:
• Support for str.replaceall operator.
• New option --re-elim to reduce regular expressions to extended string operators, resulting in better performance on regular expression benchmarks (enabled by default).
• SyGuS:
• Support for abduction (--sygus-abduct). Given a formula, this option uses CVC4’s SyGuS solver to find a sufficient condition such that the conjunction of the condition and the formula is unsatisfiable.
• Support for two new term enumerator strategies: variable agnostic (--sygus-active-gen=var-agnostic) and fast (--sygus-active-gen=enum). By default, CVC4 tries to choose the best term enumerator strategy automatically based on the input (--sygus-active-gen=auto).
• Support for streaming solutions of increasingly smaller size when using the PBE solver (--sygus-stream --sygus-pbe). After the first solution is found and printed, the solver will continue to look for new solutions and print those, if any, that are smaller than previously printed solutions.
• Support for unification-based techniques in non-separable specifications (--sygus-unif). For solving invariant problems a dedicate mode (--sygus-unif-boolean-heuristic-dt) is available that builds candidate solutions using heuristic decision tree learning.

Improvements:

• Strings:
• Significantly better performance on string benchmarks over the core theory and those with extended string functions like substring, contains, and replace.

Changes:

• API change: Expr::iffExpr() is renamed to Expr::eqExpr() to reflect its actual behavior.
• Compiling the language bindings now requires SWIG 3 instead of SWIG 2.
• The CVC3 compatibility layer has been removed.
• The build system now uses CMake instead of Autotools. Please refer to INSTALL.md for up-to-date instructions on how to build CVC4.

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 team.

The development of CVC4 is supported in part by the following organizations:

• The Air Force Office of Scientific Research (award FA9550-09-1-0596)
• Amazon AWS Automated Reasoning Group
• The Defense Advanced Research Projects Agency (awards FA8750-13-2-0241, FA8750-15-C-0113, N66001-18-C-4012, FA8650-18-2-7854, FA8650-18-2-7861)
• The European Research Council (grant 306595 “STATOR”)
• GE Global Research