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 http://cvc4.cs.stanford.edu.

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: http://cvc4.cs.stanford.edu

-The CVC4 team