From ee00542e7666495e5268f985153fc006bd595a93 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 10 Sep 2020 04:05:08 -0700 Subject: [PATCH] update release notes Signed-off-by: Nikolaj Bjorner --- RELEASE_NOTES | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 7c5aefe64..899869f8b 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -5,7 +5,6 @@ Version 4.8.next - Planned features - rewritten arithmetic solver replacing legacy arithmetic solver and on by default - self-contained character theory, direct support for UTF8, Unicode character sets - - improvements to regular expression processing - specialized solver support for QF_ABV and ABV based on lazy SMT and dual reduction - 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. @@ -13,6 +12,20 @@ Version 4.8.next option, but at this point does not translate into benefits. It is currently turned off by default. +Version 4.8.9 +============= +- New features + - significant improvements to regular expression solving + - expose user theory plugin. It is a leaner user theory plugin that was once available. + It allows for registering callbacks that react to when bit-vector and Boolean variables + receive fixed values. +- Bug fixes + - many +- Notes + - the new arithmetic theory is turned on by default. It _does_ introduce regressions on + several scenarios, but has its own advantages. Users can turn on the old solver by setting smt.arith.solver=2. + Depending on feedback, we may turn toggle this default setting again back to smt.arith.solver=2. + Version 4.8.8 ============= - New features