Some versioning in advance of the 1.3 release.

diff --git a/INSTALL b/INSTALL
index cbf8c8a86cf9b4c03115336322d2dbc4886d95f5..f0e1f6cc6408cffcc9657c89a43d69d9ed70404a 100644 (file)
--- 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 7b63d4b980347802a0a98ac60f58dfe3846f2c28..a706a3fa94e80823cc791f8c000def70d72ad7fe 100644 (file)
--- 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 <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

diff --git a/README b/README
index ddb8c856ef356f66e93fdd2eabb55e716fdef893..c09fe979cb4bea9f284c0b05e858b9dd048f70fe 100644 (file)
--- 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 136051d0ba15d222bc1c47b64b5e1230d9885720..b976d6033a7cf39c5fa7a30c609f355665dc10db 100644 (file)
--- 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 ad37ce67a1d4680c2964bd4dd2aaa5e6f843e55d..771fdf4ecfb269b6a53aa72c67968ac4e357ad79 100644 (file)
--- 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