Update AUTHORS, NEWS, README, RELEASE-NOTES and THANKS file for 1.6.

5 files changed, 43 insertions, 7 deletions

diff --git a/AUTHORS b/AUTHORS
index 92a4b702f..1d4a67e5b 100644
--- a/AUTHORS
+++ b/AUTHORS
@@ -24,6 +24,7 @@ The core designers and authors of CVC4 are:
   Mathias Preiner, Stanford University
   Andrew Reynolds, The University of Iowa, EPFL
   Cesare Tinelli, The University of Iowa
+  Yoni Zohar, Stanford University
 
 Other contributors to the CVC4 codebase are listed in the THANKS file.
 
diff --git a/NEWS b/NEWS
index f23833bb6..a9ce4d68f 100644
--- a/NEWS
+++ b/NEWS
@@ -1,5 +1,34 @@
 This file contains a summary of important user-visible changes. 
 
+Changes since 1.5
+=================
+
+New Features:
+* A new theory of floating points.
+* Novel approach for solving quantified bit-vectors (BV).
+* Eager bit-blasting: Support for SAT solver CaDiCaL.
+* A new Gaussian Elimination preprocessing pass for the theory of bit-vectors.
+* Support for transcendental functions (sin, cos, exp).
+* Support for new operators in strings, including string inequality (str.<=)
+  and string code (str.code).
+* Support for automated rewrite rule generation from sygus (*.sy) inputs using
+  syntax-guided enumeration (option --sygus-rr).
+
+Improvements:
+* Incremental unsat core support.
+* Strings rewriter.
+* Further development of rewrite rules for the theory of strings and regular
+  expressions.
+* Many optimizations for syntax-guided synthesis, including improved symmetry
+  breaking for enumerative search and specialized algorithms for
+  programming-by-examples conjectures.
+
+Changes:
+* Eager bit-blasting: Removed support for SAT solver CryptoMinisat 4, added
+  support for CryptoMinisat 5.
+* The LFSC proof checker now resides in its own repository on GitHub at
+  https://github.com/CVC4/LFSC. It is not distributed with CVC4 anymore.
+
 Changes since 1.4
 =================
 
diff --git a/README b/README
index 593a18bf2..0a8a37879 100644
--- a/README
+++ b/README
@@ -1,4 +1,4 @@
-This is CVC4 release version 1.5.  For build and installation notes,
+This is CVC4 release version 1.6.  For build and installation notes,
 please see the INSTALL file included with this distribution.
 
 The project leaders are Clark Barrett (Stanford University) and Cesare
diff --git a/RELEASE-NOTES b/RELEASE-NOTES
index 02c201003..c9c1fabb5 100644
--- a/RELEASE-NOTES
+++ b/RELEASE-NOTES
@@ -1,4 +1,4 @@
-Release Notes for CVC4 1.5, July 2017
+Release Notes for CVC4 1.6, June 2018
 
 ** 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.5.  This is an issue when mixing integers and
+such, are not supported by CVC4 1.6.  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
@@ -117,14 +117,14 @@ heap.
 
 ** Proof support
 
-CVC4 1.5 has support for proofs when using uninterpreted functions, arrays,
+CVC4 1.6 has support for proofs when using uninterpreted functions, arrays,
 bitvectors, or their combinations, and proofs are enabled by default.
 (Run the configure script with --disable-proof to disable proofs).  Proofs
 are exported in LFSC format.
 
 ** Nonlinear arithmetic
 
-CVC4 1.5 has a state-of-the-art linear arithmetic solver as well as some
+CVC4 1.6 has a state-of-the-art linear arithmetic solver as well as some
 heuristic support for non-linear arithmetic.
 
 ** Portfolio solving
diff --git a/THANKS b/THANKS
index 09fd9d44a..8eb19e8db 100644
--- a/THANKS
+++ b/THANKS
@@ -16,6 +16,8 @@ Thanks to:
 - Finn Haedicke of University of Bremen, Germany for fixing namespace specifiers
   in CVC4's version of minisat in 2015.
 
+- Pat Hawks for writing tests for CVC4's Java API.
+
 - Thomas Hunger for some important patches to CVC4's SWIG interfaces in March
   2014.
 
@@ -28,7 +30,11 @@ Thanks to:
 - Jordy Ruiz of University of Toulouse for fixing throw specifiers on the theory
   output channels in 2015.
 
-- Fabian Wolff in 2016 for fixing several spelling mistakes.
-
 - Clement Pit-Claudel of MIT for improving the signal handling support for
   Windows builds in 2017.
+
+- Arjun Viswanathan for improvements in the CVC and the SMT2 parser.
+
+- Fabian Wolff in 2016 for fixing several spelling mistakes.
+
+- Justin Xu for contributing to refactoring CVC4's preprocessing infrastructure.