Update release notes and lib version (#2933)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 9af357790700015655ddf419bb02ae365e1b880a..31f249a278e2665234c86f6db3beacd1ea15bd07 100644 (file)
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -13,7 +13,7 @@ set(CVC4_RELEASE 0) # Release component of the version of CVC4.
 set(CVC4_EXTRAVERSION "-prerelease")
 
 # Shared library versioning. Increment SOVERSION for every new CVC4 release.
-set(CVC4_SOVERSION 5)
+set(CVC4_SOVERSION 6)
 
 # Full release string for CVC4.
 if(CVC4_RELEASE)

diff --git a/RELEASE-NOTES b/RELEASE-NOTES
index c9c1fabb5d8652d771b7d1aa278923aab9ea7f19..6e8d997003c46642714c92f67f7f22e9605a43db 100644 (file)
--- a/RELEASE-NOTES
+++ b/RELEASE-NOTES
@@ -1,4 +1,4 @@
-Release Notes for CVC4 1.6, June 2018
+Release Notes for CVC4 1.7, April 2019
 
 ** Getting started
 
@@ -17,14 +17,14 @@ 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.6.  This is an issue when mixing integers and
+such, are not supported by CVC4 1.7.  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 
+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
 an integer and is used where an INT is expected, CVC4 may produce strange
 results.
 
-For example: 
+For example:
 
   f : INT -> INT;
   ASSERT f(1/3) = 0;
@@ -82,10 +82,6 @@ standard.  To make CVC4 adhere more strictly to the standard, use the
 somewhat lenient; some non-conforming input may still be parsed and
 processed.
 
-For the latest news on SMT-LIB compliance, please check:
-
-  http://cvc4.cs.stanford.edu/wiki/SMT-LIB_Compliance
-
 ** Getting statistics
 
 Statistics can be dumped on exit (both normal and abnormal exits) with
@@ -117,14 +113,14 @@ heap.
 
 ** Proof support
 
-CVC4 1.6 has support for proofs when using uninterpreted functions, arrays,
+CVC4 1.7 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.6 has a state-of-the-art linear arithmetic solver as well as some
+CVC4 1.7 has a state-of-the-art linear arithmetic solver as well as some
 heuristic support for non-linear arithmetic.
 
 ** Portfolio solving