diff options
| -rw-r--r-- | CMakeLists.txt | 2 | ||||
| -rw-r--r-- | RELEASE-NOTES | 16 |
2 files changed, 7 insertions, 11 deletions
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 |