From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Thu, 4 Apr 2019 02:06:25 +0000 (-0500)
Subject: Update release notes and lib version (#2933)
X-Git-Tag: cvc5-1.0.0~4194
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ae712e32aae0947205f506f7caacc670311c6763;p=cvc5.git

Update release notes and lib version (#2933)
---

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 9af357790..31f249a27 100644
--- 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 c9c1fabb5..6e8d99700 100644
--- 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