mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

Update RELEASE_NOTES.md for v4.17.0 (PRs #9798–#10116) (#10121)

Browse source 
Appends ~35 release note entries to the `Version 4.17.0` section,
covering the substantial changes since PR #9700 as catalogued in
discussion #10117.

## New features
- `z3regex` Python module bridging Python `re` syntax to Z3 regex ASTs
- `OP_RE_XOR` + bisimulation-based ground regex equivalence (Margus
Veanes)
- `bv_divrem_bounds_tactic` for bounded BV div/rem constraints
- Linear divisibility closure lemma for lp/nla solver
- Pyodide (WASM) wheel support; Bazel versioned shared objects
- rlimit support in fixedpoint/Horn parameters
- HO matching improvements: curry-order, variable shift, lazy MAM
deferral, throttle configs
- Go bindings: concurrent `dec_ref` for GC finalizers

## Bug fixes
- Three optimization soundness fixes (strict optima with delta-rational
/ infinitesimal bounds, unvalidated LP bound)
- Horn clause solver segfault on unused quantified variables
- .NET API memory leak (NativeContext finalizer, delegate lifetime, GC
pressure)
- Parallel solver unsigned overflow in conflict budget escalation
- `psmt`/`smt_parallel` infinite loops on theory-incomplete cubes
- `seq_rewriter` `re.range` empty-language and soundness fixes
- Mod rewriter non-termination on symbolic modulus
- `elim_uncnstr` disabled by `has_type_vars()` flag (issue #6260)
- MBQI timeout regression in HO term enumeration
- `bv2int_translator` assertion violation with `smt.bv.solver=2`

## API fixes
- Java `Sort.create()` returns `EnumSort` (not `DatatypeSort`) for enum
sorts

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This commit is contained in:
Copilot 2026-07-13 18:43:58 -07:00 • committed by GitHub
parent 5c0443591d
commit 627e19197c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 76 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

76
RELEASE_NOTES.md
View file

@ -131,6 +131,82 @@ Version 4.17.0
- Add fold-unfold tactic as an alternative to solve-eqs for variable elimination using
fold-unfold transformations. Also exposed as a simplifier.
- Handle SIGXCPU (OS timeout) like a regular `-T` timeout. Users should make sure to set the soft limit below the hard one, as in `ulimit -S -t 30 -H -t 31` for a 30s soft limit, so SIGXCPU is delivered before SIGKILL.
- Add `z3regex` Python module to translate Python `re` module regex syntax into Z3 regular expression ASTs, bridging Python regex and Z3 string/regex solving.
https://github.com/Z3Prover/z3/pull/10095
- Add `OP_RE_XOR` operator and union-find bisimulation algorithm for deciding ground regex equivalence. Thanks to Margus Veanes.
https://github.com/Z3Prover/z3/pull/9804
- Improve regex NFA representation: treat each transition-regex leaf as a single bisimulation state for more precise equivalence checking. Thanks to Margus Veanes.
https://github.com/Z3Prover/z3/pull/9871
- Port seq_split rule to master branch, improving sequence solver completeness. Thanks to Clemens Eisenhofer.
https://github.com/Z3Prover/z3/pull/9840
- Add linear divisibility closure lemma for lp/nla solver: derive divisibility constraints from LP solutions to improve nonlinear arithmetic solving.
https://github.com/Z3Prover/z3/pull/10107
- Add `bv_divrem_bounds_tactic`: new tactic for handling bounded bitvector division and remainder constraints (Issue 438).
https://github.com/Z3Prover/z3/pull/10085
- Improve higher-order matching (ho_matching): fix imitation curry-order, instance-assembly ordering, variable shift bugs, and callback scope nesting. Defer ho-matching to lazy MAM and add throttle configurations.
- Improve pattern inference to handle binders correctly, support patterns with variables outside of scope, and fix variable shift.
- Improve generation accounting for quantifier instantiation.
https://github.com/Z3Prover/z3/pull/10009
- Mark quantifier instances that lead to conflicts as relevant to improve solver pruning. Thanks to Can Cebeci.
https://github.com/Z3Prover/z3/pull/10064
- Add constant-bound contradiction shortcut for string `<` (str.lt) constraints in `theory_seq` to quickly detect unsatisfiable string ordering constraints.
https://github.com/Z3Prover/z3/pull/10112
- Add rlimit (resource limit) support in fixedpoint (Horn clause) parameters. Thanks to Eric Astor.
https://github.com/Z3Prover/z3/pull/9798
- Support building a PyPI-publishable Pyodide (PEP 783) wheel for running Z3 in browser environments (WebAssembly). Thanks to Alcides Fonseca.
https://github.com/Z3Prover/z3/pull/9891
- Add versioned shared object names in Bazel build rules for better ABI compatibility management. Thanks to Shantanu Gontia.
https://github.com/Z3Prover/z3/pull/9838
- Go bindings: enable concurrent dec_ref for GC-driven finalizers, improving memory management in multi-goroutine use.
https://github.com/Z3Prover/z3/pull/10002
- LP performance: batch fixed-column bound-witness linearization per row in `lar_solver` for improved arithmetic solving throughput.
https://github.com/Z3Prover/z3/pull/10029
- LP performance: hoist loop-invariant pivot reads in HNF `pivot_column_non_fractional`.
https://github.com/Z3Prover/z3/pull/10073
- Fix optimization soundness: validate strict optimization optima faithfully with delta-rational bounds.
https://github.com/Z3Prover/z3/pull/10059
- Fix optimization soundness: preserve strict supremum/infimum optima with infinitesimal component.
https://github.com/Z3Prover/z3/pull/10052
- Fix inconsistent optimization result with unvalidated LP bound.
https://github.com/Z3Prover/z3/pull/10040
- Fix `elim_uncnstr` simplification disabled by manager-wide `has_type_vars()` flag (issue #6260).
https://github.com/Z3Prover/z3/pull/10063
- Fix segfault in Horn clause solver on formulas with unused quantified variables.
https://github.com/Z3Prover/z3/pull/10091
- Fix .NET API memory leak: NativeContext finalizer, delegate lifetime, and GC memory pressure registration.
https://github.com/Z3Prover/z3/pull/10090
- Fix unsigned overflow in parallel solver conflict budget escalation.
https://github.com/Z3Prover/z3/pull/10076
- Fix Spacer quantifier elimination: avoid assertion failure on extended arithmetic model values.
https://github.com/Z3Prover/z3/pull/10096
- Fix non-termination in mod rewriter for symbolic modulus expressions.
https://github.com/Z3Prover/z3/pull/10105
- Fix assertion violation in `bv2int_translator` when using `smt.bv.solver=2`.
https://github.com/Z3Prover/z3/pull/10109
- Fix `seq_rewriter`: `re.range` with a provably-empty bound must produce the empty language.
https://github.com/Z3Prover/z3/pull/10047
- Fix soundness regression in symbolic `re.range`: keep non-empty; fix range membership checking.
https://github.com/Z3Prover/z3/pull/10017
- Fix `bv_rewriter`: keep `(= var concat)` intact so DER can eliminate the bound variable (issue #4525).
https://github.com/Z3Prover/z3/pull/10034
- Fix `psmt` and `smt_parallel` infinite loops on theory-incomplete cubes; report unknown instead of hanging.
https://github.com/Z3Prover/z3/pull/9983, https://github.com/Z3Prover/z3/pull/9999
- Fix `qsat`: decide quantifier-free goals so `qe2` returns `sat` instead of `unknown`.
https://github.com/Z3Prover/z3/pull/9970
- Fix MBQI timeout regression: bound ho_var term enumeration and honor cancellation/timeout in bottom-up term enumeration.
https://github.com/Z3Prover/z3/pull/9939, https://github.com/Z3Prover/z3/pull/9956
- Java API: `Sort.create()` now returns `EnumSort` instead of `DatatypeSort` for enumeration sorts, fixing the return type.
https://github.com/Z3Prover/z3/pull/10104
- Thanks to several pull requests improving code quality and build compatibility. Thanks to David Detlefs, Nuno Lopes, Can Cebeci, and others.
- https://github.com/Z3Prover/z3/pull/9800
- https://github.com/Z3Prover/z3/pull/9879
- https://github.com/Z3Prover/z3/pull/9883
- https://github.com/Z3Prover/z3/pull/9892
- https://github.com/Z3Prover/z3/pull/9903
- https://github.com/Z3Prover/z3/pull/9906
- https://github.com/Z3Prover/z3/pull/9923
- https://github.com/Z3Prover/z3/pull/9933
- https://github.com/Z3Prover/z3/pull/10020
Version 4.16.0
==============