Skip to content

Commit 745087e

Browse files
update release notes
Signed-off-by: Nikolaj Bjorner <[email protected]>
1 parent c88295a commit 745087e

File tree

1 file changed

+12
-0
lines changed

1 file changed

+12
-0
lines changed

RELEASE_NOTES.md

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,18 @@ Version 4.next
77
- CDCL core for SMT queries. It extends the SAT engine with theory solver plugins.
88
- add global incremental pre-processing for the legacy core.
99

10+
Version 4.15.4
11+
==============
12+
- Add methods to create polymorphic datatype constructors over the API. The prior method was that users had to manage
13+
parametricity using their own generation of instances. The updated API allows to work with polymorphic datatype declarations
14+
directly.
15+
- MSVC build by default respect security flags, https://github.com/Z3Prover/z3/pull/7988
16+
- Using a new algorithm for smt.threads=k, k > 1 using a shared search tree. Thanks to Ilana Shapiro.
17+
- Thanks for several pull requests improving usability, including
18+
- https://github.com/Z3Prover/z3/pull/7955
19+
- https://github.com/Z3Prover/z3/pull/7995
20+
- https://github.com/Z3Prover/z3/pull/7947
21+
1022
Version 4.15.3
1123
==============
1224
- Add UserPropagator callback option for quantifier instantiations. It allows the user propagator to

0 commit comments

Comments
 (0)