[SMT-LIB] Announcing CVC3

[Clark Barrett]

We are pleased to announce the first official release of CVC3, version 1.0.

CVC3 is an automatic theorem prover for Satisfiability Modulo Theories (SMT)
problems.  It can be used to prove the validity (or, dually, the satisfiability)
of first-order formulas in a large number of built-in logical theories and
their combination.

CVC3 is the latest in a series of popular SMT provers, which originated
at Stanford University with the SVC system.  In particular, it builds on and
replaces its most recent predecessor, CVC Lite.  CVC3 is being developed as a
joint project of New York University and the University of Iowa.  The project
leaders are Clark Barrett and Cesare Tinelli.

Some of the new features in CVC3 include:
- A theory of inductive data types
- Better support for quantifiers
- Performance improvements

For more information about CVC3, including downloads, an updated user's manual,
and more, please visit the CVC3 webpage at http://www.cs.nyu.edu/acsys/cvc3.

If you are interested in using or hearing about future releases of CVC3, we
encourage you to join the cvc-users mailing list.  Instructions for doing so
can be found on the web page (under Support).

Finally, a note to those interested in using CVC3 for non-research purposes.
You are free to do so.  However, you must first remove a few files that have a
more restrictive license.  Refer to the LICENSE document (under Documentation
on the web page) for instructions on how to do this.  Removing these files
does not affect the performance of CVC3.  It simply disables the option to use
an alternative SAT solver.

Clark Barrett