diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-03 13:08:00 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-04-03 13:08:00 -0400 |
commit | 89ce2eb5c066d4fb6d6e9a23cd9c80ca39eb2493 (patch) | |
tree | 5ad57159d571756118d16867e62615a2b21c384d /RELEASE-NOTES | |
parent | c9c41118eb3af8c882019a6e978e838ac793002d (diff) |
Some final minor changes before cutting 1.1.
* update documentation
* update the cut-release script
* spelling/wording updates
* add a (previously-failing) fuzzer regression
Diffstat (limited to 'RELEASE-NOTES')
-rw-r--r-- | RELEASE-NOTES | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/RELEASE-NOTES b/RELEASE-NOTES index 38d1459ad..43d87487a 100644 --- a/RELEASE-NOTES +++ b/RELEASE-NOTES @@ -1,4 +1,4 @@ -Release Notes for CVC4 1.0, December 2012 +Release Notes for CVC4 1.1, April 2013 ** Getting started @@ -17,7 +17,7 @@ this, you can use the --lang option. The CVC family of systems relies on Type Correctness Conditions (TCCs) when mixing two types that have a compatible base type. TCCs, and the checking of -such, are not supported by CVC4 1.0. This is an issue when mixing integers and +such, are not supported by CVC4 1.1. This is an issue when mixing integers and reals. A function defined only on integers can be applied to REAL (as INT is a subtype of REAL), and CVC4 will not complain. It is up to the user to ensure that the REAL expression must be an integer. If the REAL expression is not @@ -84,12 +84,12 @@ processed. For the latest news on SMT-LIB compliance, please check: - http://church.cims.nyu.edu/wiki/SMT-LIB_Compliance + http://cvc4.cs.nyu.edu/wiki/SMT-LIB_Compliance ** Getting statistics Statistics can be dumped on exit (both normal and abnormal exits) with -the --statistics command line option. +the --stats command line option. ** Time and resource limits @@ -118,7 +118,7 @@ heap. ** Proof support -CVC4 1.0 has limited support for proofs, and they are disabled by default. +CVC4 1.1 has limited support for proofs, and they are disabled by default. (Run the configure script with --enable-proof to enable proofs). Proofs are exported in LFSC format and are limited to the propositional backbone of the discovered proof (theory lemmas are stated without proof in this @@ -126,7 +126,7 @@ release). ** Nonlinear arithmetic -CVC4 1.0 has a state-of-the-art linear arithmetic solver. However, there +CVC4 1.1 has a state-of-the-art linear arithmetic solver. However, there is extremely limited support for nonlinear arithmetic in this release. ** Portfolio solving |