CVC4 1.2 released

We are delighted to announce version 1.2 of CVC4, the open-source flagship SMT solver developed at New York University and the University of Iowa, available at http://cvc4.cs.nyu.edu.

In version 1.2, real arithmetic now has three simplex solvers for exact precision linear arithmetic: the classical dual solver and two new solvers based on techniques for minimizing the sum of infeasibilities.  GLPK can now be used as a heuristic backup to the exact precision solvers.  See cvc4 --help for more information on enabling these solvers.

Additionally, this release:

  • adds support for “bit0″ and “bit1″ bitvector constants in SMT-LIB v1.2
  • has support for theory “alternates”: new ability to prototype new decision procedures that are selectable at runtime
  • includes important bug fixes and performance improvements over the previous stable release (version 1.1)

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:

  •   Clark Barrett (NYU, project leader)
  •   Cesare Tinelli (U Iowa, project leader)
  •   Kshitij Bansal (NYU)
  •   François Bobot (Paris-Diderot University)
  •   Chris Conway (Google)
  •   Morgan Deters (NYU)
  •   Liana Hadarean (NYU)
  •   Dejan Jovanović (NYU)
  •   Tim King (NYU)
  •   Tianyi Liang (U Iowa)
  •   Andrew Reynolds (U Iowa)

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

  • The Air Force Office of Scientific Research (award FA9550-09-1-0596)
  • Intel Corporation
  • The National Science Foundation (grants 0644299,  0914956, 1049495, 1228765, 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.nyu.edu

-The CVC4 team