Versioning preparation.
authorMorgan Deters <mdeters@cs.nyu.edu>
Mon, 16 Jun 2014 02:08:56 +0000 (22:08 -0400)
committerlianah <lianahady@gmail.com>
Thu, 19 Jun 2014 22:24:39 +0000 (18:24 -0400)
INSTALL
NEWS
README
RELEASE-NOTES
library_versions

diff --git a/INSTALL b/INSTALL
index bd16c0bf85f13507295f2b4a2f5240a09b47bd43..943d2f7e1e1b87e0e65d8eb901c3f2277768ef2a 100644 (file)
--- a/INSTALL
+++ b/INSTALL
@@ -1,4 +1,4 @@
-CVC4 release version 1.3.
+CVC4 release version 1.4.
 
 *** Quick-start instructions
 
diff --git a/NEWS b/NEWS
index 9f3e12562c020ed9baf38c87fd900f3f0cb0a145..4f0a96c14abbe94accfadebeb68e1a7ea3b3a6f7 100644 (file)
--- a/NEWS
+++ b/NEWS
@@ -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
diff --git a/README b/README
index c5b751d0a5200009c14c0b193788b67b813afebd..bd4f29b57d10a44a8f822744ea43cfe827513384 100644 (file)
--- a/README
+++ b/README
@@ -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
index b976d6033a7cf39c5fa7a30c609f355665dc10db..90840d99a29c36ce9bd92eb8bf8695c251b7c2d7 100644 (file)
@@ -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
index 966b1d8a85b5c0a6afc1e825f1143ea94481c91f..b4ba55bc197656fd4e87b271222cdab8f5321ecc 100644 (file)
@@ -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