From 1debbc29c4695d5046cad7828fdc5b17a681a9e4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Jun 2018 14:59:33 -0700 Subject: [PATCH] release notes Signed-off-by: Nikolaj Bjorner --- RELEASE_NOTES | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 7439342de..e55b329db 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -26,12 +26,16 @@ Version 4.8.0 (known as ACCE, ABCE, CCE). Asymmetric branching also uses features introduced in Lingeling by exploiting binary implication graphs. Use sat.acce=true to enable the full repertoire of inprocessing methods. By default, clauses that are "eliminated" by acce are tagged as lemmas (redundant) and are garbage collected if their glue level is high. + - Substantial overhaul of the spacer horn clause engine. - Removed features: - interpolation API - duality engine for constrained Horn clauses. + - pdr engine for constrained Horn clauses. The engine's functionality has been + folded into spacer as one of optional strategies. - long deprecated API functions have been removed from z3_api.h + Version 4.7.1 =============