This file contains a summary of important user-visible changes.

Changes since 1.2
=================

* SMT-LIB support for abs, to_real, to_int, is_int
* Expr::substitute() now capable of substituting operators (e.g.,
  function symbols under an APPLY_UF)
* Support in linear logics for /, div, and mod by constants.
* Support for TPTP's TFF and TFA formats.
* We no longer permit model or proof generation if there's been an
  intervening push/pop.
* Increased compliance to SMT-LIBv2, numerous bugs and usability issues
  resolved.
* New :command-verbosity SMT option to silence success and error messages
  on a per-command basis.  API changes to Command infrastructure to support.
* A new theory of strings.  Currently, only word equations are supported.

Changes since 1.1
=================

* 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.  GLPK must be enabled
  at configure time. See --help for more information on enabling these solvers.
* added support for "bit0" and "bit1" bitvector constants in SMT-LIB v1.2
* support for theory "alternates": new ability to prototype new decision
  procedures that are selectable at runtime
* various bugfixes

Changes since 1.0
=================

* bit-vector solver now has a specialized decision procedure for unsigned bit-
  vector inequalities
* numerous important bug fixes, performance improvements, and usability
  improvements
* support for multiline input in interactive mode
* Win32-building support via mingw
* SMT-LIB get-model output now is easier to machine-parse: contains (model...)
* user patterns for quantifier instantiation are now supported in the
  SMT-LIBv1.2 parser
* --finite-model-find was incomplete when using --incremental, now fixed
* the E-matching procedure is slightly improved
* Boolean terms are now supported in datatypes
* tuple and record support have been added to the compatibility library
* driver verbosity change: for printing all commands as they're executed, you
  now need verbosity level >= 3 (e.g., -vvv) instead of level 1 (-v).  This
  allows tracing the solver's activities (with -v and -vv) without having too
  much output.
* to make CVC4 quieter in abnormal (e.g., "warning" conditions), you can
  use -q.  Previously, this would silence all output (including "sat" or
  "unsat") as well.  Now, single -q silences messages and warnings, and
  double -qq silences all output (except on exception or signal).

-- Morgan Deters <mdeters@cs.nyu.edu>  Wed, 03 Apr 2013 13:06:35 -0400