From 41a5b930b60d083eef50aea953e8c27a8c5d82d2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 Nov 2021 11:21:51 -0800 Subject: [PATCH] update release notes Signed-off-by: Nikolaj Bjorner --- RELEASE_NOTES | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index dae1e81b8d2..790691c3d17 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -3,14 +3,18 @@ RELEASE NOTES Version 4.8.next ================ - Planned features - - 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. + - sat.euf + - a new CDCL core for SMT queries. It extends the SAT engine with theory solver plugins. + the current state is unstable. It lacks efficient ematching. + - polysat + - native word level bit-vector solving. - 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.13 +============== +The release integrates various bug fixes and tuning. + Version 4.8.12 ============== Release provided to fix git tag discrepancy issues with 4.8.11