updated release notes

Signed-off-by: Nikolaj Bjorner <[email protected]>

Author: NikolajBjorner

RELEASE_NOTES

@@ -3,12 +3,34 @@ RELEASE NOTES
 Version 4.8.next
 ================
 - Planned features
-  - rewritten NIA (non-linear integer arithmetic) core solver 
+  - rewritten arithmetic solver replacing legacy arithmetic solver and on by default
   - self-contained character theory, direct support for UTF8, Unicode character sets
-  - recursive function representation without hoisting ite expressions. Issue #2601
+  - improvements to regular expression processing
   - specialized solver support for QF_ABV and ABV based on lazy SMT and dual reduction
-  - model-based interpolation for quantifier-free UF, arithmetic, arrays
-  - circuit optimization techniques for BV pre-processing
+    - the smtfd solver and tactic implement this strategy, but is not prime for users.
+  - introduction of simple induction lemmas to handle a limited repertoire of induction proofs.
+  - circuit optimization techniques for BV in-processing are available as the sat.cut
+    option, but at this point does not translate into benefits. It is currently 
+    turned off by default.
+
+Version 4.8.8
+=============
+- New features
+  - rewritten NIA (non-linear integer arithmetic) core solver 
+    It is enabled in selected theories as default. 
+    The legacy arithmetic solver remains the overall default in this release
+    as the rewritten solver shows regressions (on mainly NRA problems).
+  - recursive function representation without hoisting ite expressions. Issue #2601
+  - model-based interpolation for quantifier-free UF, arithmetic 
+  - Julia bindings over the C++ API, thanks to ahumenberger 
+- Bug fixes
+  - numerous, many based on extensive fuzz testing. 
+    Thanks to 5hadowblad3, muchang, numairmansur, rainoftime, wintered
+- Notes
+  - recursive functions are unfolded with separate increments based on unsat core
+    analysis of blocking literals that are separate for different recursive functions.   
+  - the seq (string) solver has been revised in several ways and likely shows some 
+    regressions in this release.
 
 Version 4.8.7
 =============

src/smt/params/smt_params_helper.pyg

@@ -41,7 +41,7 @@ def_module_params(module_name='smt',
                           ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'),
                           ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'),
                           ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
-                          ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
+                          ('arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
                           ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'),
                           ('arith.nl.gb', BOOL, True, 'groebner Basis computation, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=2'),
                           ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters, relevant only if smt.arith.solver=2'),

src/smt/smt_context.cpp

@@ -1601,7 +1601,7 @@ namespace smt {
             if (inconsistent())
                 return false;
         }
-#if 1
+#if 0 
         if (at_search_level() && induction::should_try(*this)) {
             get_induction()();
         }