diff options
| -rw-r--r-- | INSTALL | 2 | ||||
| -rw-r--r-- | NEWS | 2 | ||||
| -rw-r--r-- | README | 2 | ||||
| -rw-r--r-- | RELEASE-NOTES | 8 | ||||
| -rw-r--r-- | library_versions | 2 |
5 files changed, 8 insertions, 8 deletions
@@ -1,4 +1,4 @@ -CVC4 release version 1.3. +CVC4 release version 1.4. *** Quick-start instructions @@ -95,4 +95,4 @@ Changes since 1.0 "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> Thu, 05 Dec 2013 14:22:26 -0500 +-- Morgan Deters <mdeters@cs.nyu.edu> Mon, 16 Jun 2014 22:23:12 -0400 @@ -1,4 +1,4 @@ -This is CVC4 release version 1.3. For build and installation notes, +This is CVC4 release version 1.4. For build and installation notes, please see the INSTALL file included with this distribution. This first official release of CVC4 is the result of more than three diff --git a/RELEASE-NOTES b/RELEASE-NOTES index b976d6033..90840d99a 100644 --- a/RELEASE-NOTES +++ b/RELEASE-NOTES @@ -1,4 +1,4 @@ -Release Notes for CVC4 1.3, December 2013 +Release Notes for CVC4 1.4, June 2014 ** 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.3. This is an issue when mixing integers and +such, are not supported by CVC4 1.4. 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 @@ -118,7 +118,7 @@ heap. ** Proof support -CVC4 1.3 has limited support for proofs, and they are disabled by default. +CVC4 1.4 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.3 has a state-of-the-art linear arithmetic solver. However, there +CVC4 1.4 has a state-of-the-art linear arithmetic solver. However, there is extremely limited support for nonlinear arithmetic in this release. ** Portfolio solving diff --git a/library_versions b/library_versions index 966b1d8a8..b4ba55bc1 100644 --- a/library_versions +++ b/library_versions @@ -56,4 +56,4 @@ 1\.3 libcvc4:2:0:0 libcvc4parser:2:0:0 libcvc4compat:2:0:0 libcvc4bindings:2:0:0 1\.3\.1-prerelease libcvc4:2:0:0 libcvc4parser:2:0:0 libcvc4compat:2:0:0 libcvc4bindings:2:0:0 1\.4-prerelease libcvc4:2:0:0 libcvc4parser:2:0:0 libcvc4compat:2:0:0 libcvc4bindings:2:0:0 -# some things have changed in the API, 1.4 release should bump these numbers +1\.4 libcvc4:3:0:0 libcvc4parser:3:0:0 libcvc4compat:3:0:0 libcvc4bindings:3:0:0 |