From 5e3f1d988b2435620a45906b974bdea1d605332d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 4 Dec 2023 19:38:52 -0800 Subject: [PATCH] update release notes Signed-off-by: Nikolaj Bjorner --- RELEASE_NOTES.md | 5 ++++- scripts/release.yml | 2 +- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index f46f32a1af..b00cb23980 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -9,7 +9,6 @@ Version 4.next - polysat - native word level bit-vector solving. - introduction of simple induction lemmas to handle a limited repertoire of induction proofs. - - Light quantifier elimination based on term graphs (egraphs), and corresponding Model Based Projection for arrays and ADTs. Used by Spacer and QSAT. Version 4.12.3 ============== @@ -23,6 +22,10 @@ Version 4.12.3 - Various (ongoing) performance fixes and improvements to smt.arith.solver=6 - A working version of solver.proof.trim=true option. Proofs logs created when using sat.smt=true may be trimmed by running z3 on the generated proof log using the option solver.proof.trim=true. +- Optimizations LIA and NIA (linear integer arithmetic and non-linear integer (and real) arithmetic reasoning). + smt.arith.solver=6 is the default for most use cases. It trails smt.arith.solver=2 in some scenarios and the gap has been either removed or reduced. + smt.arith.solver=6 is complete for integrations of non-linear real arithmetic and theories, smt.arith.solver=2 is not. +- qel: Light quantifier elimination based on term graphs (egraphs), and corresponding Model Based Projection for arrays and ADTs. Used by Spacer and QSAT. Version 4.12.2 ============== diff --git a/scripts/release.yml b/scripts/release.yml index b400860a7c..49679d12e5 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -583,7 +583,7 @@ stages: # Enable on release: - job: PyPIPublish - condition: eq(1,0) + condition: eq(1,1) displayName: "Publish to PyPI" pool: vmImage: "ubuntu-latest"