Cutting release 1.2.1.2

6 files changed, 17 insertions, 8 deletions

diff --git a/INSTALL b/INSTALL
index 57620bd72..cbf8c8a86 100644
--- 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 8c93b1478..17a934729 100644
--- 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 bda916610..ddb8c856e 100644
--- 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 43d87487a..b45602d87 100644
--- 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/configure.ac b/configure.ac
index e860461b9..760c8dcce 100644
--- a/configure.ac
+++ b/configure.ac
@@ -4,7 +4,7 @@
 m4_define(_CVC4_MAJOR,          1)       dnl version (major)
 m4_define(_CVC4_MINOR,          2)       dnl version (minor)
 m4_define(_CVC4_RELEASE,        0)       dnl version (alpha)
-m4_define(_CVC4_EXTRAVERSION,   [-prerelease])      dnl version (extra)
+m4_define(_CVC4_EXTRAVERSION,   [])      dnl version (extra)
 m4_define(_CVC4_RELEASE_STRING, _CVC4_MAJOR[.]_CVC4_MINOR[]m4_if(_CVC4_RELEASE,[0],,[.]_CVC4_RELEASE)_CVC4_EXTRAVERSION) dnl version string
 
 dnl Preprocess CL args. Defined in config/cvc4.m4
diff --git a/library_versions b/library_versions
index 1cf417e36..f88f8e40b 100644
--- 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