update versioning

diff --git a/INSTALL b/INSTALL
index 57620bd72c4d36d4d8ee873b21b14881801972c0..cbf8c8a86cf9b4c03115336322d2dbc4886d95f5 100644 (file)
--- a/INSTALL
+++ b/INSTALL
@@ -1,4 +1,4 @@
-CVC4 release version 1.1.
+CVC4 release version 1.2.
 
 *** Quick-start instructions
 

diff --git a/NEWS b/NEWS
index 8c93b1478137b9cbc1de8ca70de3c509a7cb9e5b..17a934729c09da6991acd4979b0a622074a51c07 100644 (file)
--- a/NEWS
+++ b/NEWS
@@ -3,7 +3,15 @@ This file contains a summary of important user-visible changes.
 Changes since 1.1
 =================
 
-* nothing notable yet
+* Real arithmetic now has three simplex solvers for exact precision linear
+  arithmetic: the classical dual solver and two new solvers based on
+  techniques for minimizing the sum of infeasibilities. GLPK can now be used
+  as a heuristic backup to the exact precision solvers.  GLPK must be enabled
+  at configure time. See --help for more information on enabling these solvers.
+* added support for "bit0" and "bit1" bitvector constants in SMT-LIB v1.2
+* support for theory "alternates": new ability to prototype new decision
+  procedures that are selectable at runtime
+* various bugfixes
 
 Changes since 1.0
 =================

diff --git a/README b/README
index bda91661096c7f1e1527c8850fe233b3a9396a04..ddb8c856ef356f66e93fdd2eabb55e716fdef893 100644 (file)
--- a/README
+++ b/README
@@ -1,4 +1,4 @@
-This is CVC4 release version 1.1.  For build and installation notes,
+This is CVC4 release version 1.2.  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 43d87487ad423e5b40c876f6cd51ec202173ee8f..b45602d8755cd443013d6fe39019ee15ce0814f2 100644 (file)
--- a/RELEASE-NOTES
+++ b/RELEASE-NOTES
@@ -1,4 +1,4 @@
-Release Notes for CVC4 1.1, April 2013
+Release Notes for CVC4 1.2, May 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.1.  This is an issue when mixing integers and
+such, are not supported by CVC4 1.2.  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.1 has limited support for proofs, and they are disabled by default.
+CVC4 1.2 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.1 has a state-of-the-art linear arithmetic solver.  However, there
+CVC4 1.2 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 1cf417e36e3fe646a80438192838c564322f4f5a..f88f8e40b76bcdd55411be40cb090dbaff072248 100644 (file)
--- a/library_versions
+++ b/library_versions
@@ -50,3 +50,4 @@
 1\.1 libcvc4:1:0:0 libcvc4parser:1:0:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0
 1\.1\.1-prerelease libcvc4:1:0:0 libcvc4parser:1:0:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0
 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