25 June 2018
CVC4 1.6 Released
by Aina Niemetz
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
This version is very close to the version of CVC4 submitted to the
- A new theory of floating points.
- Novel approach for solving quantified bit-vectors (
- Eager bit-blasting: Support for SAT solver CaDiCaL.
- A new Gaussian Elimination preprocessing pass for the theory of bit-vectors.
- Support for transcendental functions (
sin, cos, exp). In SMT2 input, this
can be enabled by adding T to the logic (e.g.,
- Support for new operators in strings, including string inequality (
and string code (
- Support for automated rewrite rule generation from sygus (
using syntax-guided enumeration (option
- Incremental unsat core support.
- Further development of rewrite rules for the theory of strings and regular
- Many optimizations for syntax-guided synthesis, including improved symmetry
breaking for enumerative search and specialized algorithms for
- Eager bit-blasting: Removed support for SAT solver CryptoMinisat 4, added
support for CryptoMinisat 5.
- The LFSC proof checker now resides in its own repository on GitHub. It is not
distributed with CVC4 anymore.
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)
- The Defense Advanced Research Projects Agency (award FA8750-13-2-0241)
- The European Research Council (grant 306595 “STATOR”)
- GE Global Research
- Intel Corporation
- The National Science Foundation (grants 0644299, 0914956, 1049495, 1228768,
- The Semiconductor Research Corporation (tasks 1850.001, 1850.002)
Downloads, documentation, tutorials, and more information are available at the
CVC4 web site: http://cvc4.cs.stanford.edu
-The CVC4 team