CVC4 1.5 released

We are delighted to announce version 1.5 of CVC4, the open-source flagship SMT solver developed at Stanford University, New York University and the University of Iowa, available at

Version 1.5 now supports unsat cores, proofs (for uninterpreted functions, arrays and bit-vectors and their combinations), and features numerous improvements to non-linear arithmetic, strings, sets and other theories, improved handling of quantifiers, native support for syntax-guided synthesis (SyGuS), generally improved usability and stability, and many bugfixes. This version is very close to the version of CVC4 submitted to the SMT-competition 2017.

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
  • Google
  • Intel Corporation
  • The National Science Foundation (grants 0644299, 0914956, 1049495, 1228768, 1320583)
  • The Semiconductor Research Corporation (tasks 1850.001, 1850.002)

Downloads, documentation, tutorials, and more information are available at the CVC4 web site:

-The CVC4 team