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 | 5 |
5 files changed, 9 insertions, 10 deletions
@@ -1,4 +1,4 @@ -CVC4 release version 1.2. +CVC4 release version 1.3. *** Quick-start instructions @@ -57,4 +57,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> Wed, 03 Apr 2013 13:06:35 -0400 +-- Morgan Deters <mdeters@cs.nyu.edu> Wed, 27 Nov 2013 11:20:58 -0500 @@ -1,4 +1,4 @@ -This is CVC4 release version 1.2. For build and installation notes, +This is CVC4 release version 1.3. 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 136051d0b..b976d6033 100644 --- a/RELEASE-NOTES +++ b/RELEASE-NOTES @@ -1,4 +1,4 @@ -Release Notes for CVC4 1.2, May 2013 +Release Notes for CVC4 1.3, December 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.2. This is an issue when mixing integers and +such, are not supported by CVC4 1.3. 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.2 has limited support for proofs, and they are disabled by default. +CVC4 1.3 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.2 has a state-of-the-art linear arithmetic solver. However, there +CVC4 1.3 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 ad37ce67a..771fdf4ec 100644 --- a/library_versions +++ b/library_versions @@ -52,6 +52,5 @@ 1\.2-prerelease libcvc4:1:0:0 libcvc4parser:1:0:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0 1\.2 libcvc4:1:1:1 libcvc4parser:1:1:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0 1\.2\.1-prerelease libcvc4:1:1:1 libcvc4parser:1:1:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0 -1\.3-prerelease libcvc4:1:1:1 libcvc4parser:1:1:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0 -# note: SmtEngine::setLogicString() exceptions have changed, bump library version on next release? -# note: removed Parser::getDeclarationLevel(), added other interfaces +1\.3-prerelease libcvc4:2:0:0 libcvc4parser:2:0:0 libcvc4compat:2:0:0 libcvc4bindings:2:0:0 +1\.3 libcvc4:2:0:0 libcvc4parser:2:0:0 libcvc4compat:2:0:0 libcvc4bindings:2:0:0 |