Nl2lin by ValentinPromies · Pull Request #8752 · Z3Prover/z3

ValentinPromies · 2026-02-24T16:00:48Z

Merge master into nl2lin and move linear cell construction into levelwise

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

This fixes the install_name_tool issue on macOS where the tool fails with "larger updated load commands do not fit". The linker flag -Wl,-headerpad_max_install_names ensures sufficient header padding in the Mach-O binary for install_name_tool to modify install names. Changes made: - CMake: Added flag to libz3, z3java, z3jl shared libraries on Darwin - Python build: Changed flag from ML-only to all macOS builds - OCaml CMake: Added flag to OCaml stublib build on APPLE Fixes Z3Prover#7623 (regression in 4.15.5) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

…alse Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

Added release notes for version 4.15.6, including optimizations and fixes.

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

…ation test paths Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

This reverts commit 2f4abe2.

…ns in m_todo Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

…atterns (Z3Prover#8543)

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

…eep 4 passing tests Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

Disable failure on a nullified polynomial in levelwise

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

…oop bound Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

…s-ff-by-one Fix off-by-one vulnerabilities in ackermannization module

…age-gaps Add unit tests covering ackermannization module and Z3_algebraic_eval

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

…dd A3 Python badge Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

…banners-remove-workflows Update README.md build status banners

Finite sets

levnach · 2026-02-25T01:32:33Z

There were some issues.
Z3 has a test environment at https://github.com/Z3Prover/z3test. It is a good idea to clone it ,for example, to directory “tz3” and run “python tz3/scripts/test_benchmarks.py ./z3 tz3/regressions/smt2”. This test currently gives me several incorrect results and a few timeouts: and it should work even on the debug version of z3.
I noticed that the new code produces empty explanations, which cause the unsound “unsat” results.
There was also exponential growth of the coefficients on , for example, problem tz3/regressions/smt2/8099.smt2.
Some more useful debug tricks:
Run z3 with nlsat.check_lemmas=true: I believe this option works now, even in the release build.
Run z3 with nlsat.log_lemmas=true, capture the output, including stderr, and then run z3 again on the output. There should not be lemmas which are “sat”.
I have not tried the last two options on the PR.

NikolajBjorner · 2026-02-26T03:06:08Z

you can just run the CI/CD checks. They will run z3test regression tests.

NikolajBjorner · 2026-02-26T03:30:34Z

Z3 build/z3) produced unexpected output for z3test/regressions/smt2/3689.smt2:
EXPECTED
sat
PRODUCED
unsat

NikolajBjorner and others added 30 commits February 18, 2026 20:58

update version

ccaa346

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

remove obsoleted ADO workflows

8672d26

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

version updated on workflows

29ad07c

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

remove redundant assert

1fa4304

mpz: use pointer tagging to save space (Z3Prover#8447)

70626ac

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

constructor

e73c897

Store rational by value in parameter variant (Z3Prover#8518)

3a8b688

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

Initial plan

62bfb13

fix nlsat_explain.cpp that the regression tests would pass with lws=f…

f0c3a5b

…alse Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

Remove unused swap() methods (Z3Prover#8538)

0761e91

Update RELEASE_NOTES.md for version 4.15.6

3e54f23

Added release notes for version 4.15.6, including optimizations and fixes.

update version

d245610

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

Initial plan

5528eac

Add macOS dylib headerpad validation to nightly and release workflows

bde5553

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

Add documentation for macOS headerpad validation

2b3afe1

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

Fix install_name_tool command and runner consistency in validation jobs

c291c7c

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

Apply headerpad fix to build systems (Python and CMake) and fix valid…

3ae8d70

…ation test paths Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

Fix CMake variable name and clarify test path documentation

3c401f1

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

Fix OCaml linker flag and align validation runners with build runners

51fd4b2

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

Delete .github/workflows/README-macos-headerpad.md

1387b2a

Initial plan

b670727

Remove OCaml Build badge from README status table

df02476

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

Revert "mpz: use pointer tagging to save space (Z3Prover#8447)"

0be8dee

This reverts commit 2f4abe2.

fix the logic of adding all coefficients and blocking double insertio…

4c43bf5

…ns in m_todo Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

update to next version

a7dbe16

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

update release

2aab748

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

update release

b8cfce9

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

update readme with workflows

c50d41a

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

Replace user-defined swap with C++11 move semantics for covert move p…

58431ec

…atterns (Z3Prover#8543)

levnach and others added 25 commits February 19, 2026 09:31

cleanup regarding levelwise

23560ba

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

Fix test_ackermannize_bv_model: skip crashing model converter test, k…

5e5d9eb

…eep 4 passing tests Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

Initial plan

f414c79

fixup API functions

c94eb5d

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

Merge pull request Z3Prover#8691 from Z3Prover/no_fail

426f839

Disable failure on a nullified polynomial in levelwise

update examples to use arrays

ee03533

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

add parameter validation

5bd7d93

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

Add ackermannize tests for mutation coverage

093e227

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

Fix off-by-one vulnerabilities: use range-based for on goals; cache l…

dbd7cd7

…oop bound Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

Merge pull request Z3Prover#8699 from Z3Prover/copilot/fix-missed-bug…

3698903

…s-ff-by-one Fix off-by-one vulnerabilities in ackermannization module

Merge pull request Z3Prover#8693 from Z3Prover/copilot/fix-test-cover…

bf73fdd

…age-gaps Add unit tests covering ackermannization module and Z3_algebraic_eval

remove lattice component

38ce088

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

try optimize handle_nullified_poly

385f913

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

set the default of lws_spt_threshold to 4

9c4e172

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

Initial plan

1521c43

Update README.md banners: remove disabled workflows, fix WASM link, a…

e37624a

…dd A3 Python badge Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

update params

3d8dd0d

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

update macos runner id

99e1ba3

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

Merge pull request Z3Prover#8700 from Z3Prover/copilot/update-readme-…

c56e033

…banners-remove-workflows Update README.md build status banners

Fix badge links in README.md

30e4c9a

Merge pull request Z3Prover#8686 from Z3Prover/finite-sets

8314aec

Finite sets

Merge branch 'master' into nl2lin

8f9c527

fix

6d3f3f2

move linear cell construction to levelwise

95afda3

fix

3a995bb

NikolajBjorner requested a review from levnach February 24, 2026 16:35

fix

77d81de

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Nl2lin#8752

Nl2lin#8752
ValentinPromies wants to merge 1489 commits intoZ3Prover:nl2linfrom
ValentinPromies:nl2lin

ValentinPromies commented Feb 24, 2026

Uh oh!

levnach commented Feb 25, 2026

Uh oh!

NikolajBjorner commented Feb 26, 2026

Uh oh!

NikolajBjorner commented Feb 26, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Conversation

ValentinPromies commented Feb 24, 2026

Uh oh!

levnach commented Feb 25, 2026

Uh oh!

NikolajBjorner commented Feb 26, 2026

Uh oh!

NikolajBjorner commented Feb 26, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants