From 5569aec29d73dcba445dcbebab7e49f93148a529 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 27 Nov 2013 11:23:01 -0500 Subject: [PATCH] Some versioning in advance of the 1.3 release. --- INSTALL | 2 +- NEWS | 2 +- README | 2 +- RELEASE-NOTES | 8 ++++---- library_versions | 5 ++--- 5 files changed, 9 insertions(+), 10 deletions(-) diff --git a/INSTALL b/INSTALL index cbf8c8a86..f0e1f6cc6 100644 --- a/INSTALL +++ b/INSTALL @@ -1,4 +1,4 @@ -CVC4 release version 1.2. +CVC4 release version 1.3. *** Quick-start instructions diff --git a/NEWS b/NEWS index 7b63d4b98..a706a3fa9 100644 --- a/NEWS +++ b/NEWS @@ -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 Wed, 03 Apr 2013 13:06:35 -0400 +-- Morgan Deters Wed, 27 Nov 2013 11:20:58 -0500 diff --git a/README b/README index ddb8c856e..c09fe979c 100644 --- a/README +++ b/README @@ -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 -- 2.30.2