mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-05 17:14:07 +00:00
Code Activity

update release notes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-04 19:38:52 -08:00
parent 4a9b38e531
commit 5e3f1d988b
2 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
RELEASE_NOTES.md
View file

@ -9,7 +9,6 @@ Version 4.next
- polysat - polysat
- native word level bit-vector solving. - native word level bit-vector solving.
- introduction of simple induction lemmas to handle a limited repertoire of induction proofs. - 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 Version 4.12.3
============== ==============
@ -23,6 +22,10 @@ Version 4.12.3
- Various (ongoing) performance fixes and improvements to smt.arith.solver=6 - 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 - 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. 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 Version 4.12.2
============== ==============

2
scripts/release.yml
View file

@ -583,7 +583,7 @@ stages:
# Enable on release: # Enable on release:
- job: PyPIPublish - job: PyPIPublish
condition: eq(1,0) condition: eq(1,1)
displayName: "Publish to PyPI" displayName: "Publish to PyPI"
pool: pool:
vmImage: "ubuntu-latest" vmImage: "ubuntu-latest"