by Morgan Deters
This news post contains outdated information (e.g. links, instructions). Please refer to newer documentation for up-to-date information.
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:
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:
Downloads, documentation, tutorials, and more information are available at the CVC4 web site: http://cvc4.cs.nyu.edu
-The CVC4 team