From c67bb140dcd361174151b128980030b95673aaf3 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Mon, 15 Jun 2026 10:59:41 -0700 Subject: [PATCH 01/10] Treat each transition-regex leaf as a single bisimulation state (#9871) ## Summary egex_bisim::collect_leaves used to descend through `re.union` and `re.antimirov_union` at the top of each leaf of the transition regex, splitting a single bisimulation state into multiple states before they were merged into the union-find. This contradicts the bisimulation invariant: **each leaf of a t-regex represents one state, regardless of its top-level shape**. The fix descends into `ite` only (which is the actual structural splitter of guarded transitions). ## Why it matters The split happens to be *sound* for the current algorithm when the goal is asserting `L(union(A, B)) = empty` (since `L(A) = empty AND L(B) = empty` is equivalent), but it: 1. Adds spurious merges to the union-find that distort state-class identities. 2. Slows convergence on hard equivalence queries (and causes early timeouts in practice). 3. Creates latent unsoundness risk for any extension that interprets leaves more semantically (XOR pair handling, classical-flag propagation, future antimirov re-enable, etc.). ## Empirical validation Run on the 1523-file regex-equivalence corpus, 5s/file timeout, 8 workers: | metric | pre-fix master | post-fix | |---|---|---| | sat | 1008 | 1014 | | unsat | 368 | 368 | | timeout | 145 | 139 | | unknown | 2 | 2 | | SAT↔UNSAT verdict flips | — | **0** | | timeout→sat flips | — | 6 | | commonly-solved wall ratio | 1.000x | **0.902x** | The 6 `timeout` → `sat` cases all return the *same* `sat` under pre-fix master if given 60s; they are previously-slow cases not previously-wrong ones. Z3 unit tests: 89/89 pass (`test-z3 /a`). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/ast/rewriter/seq_regex_bisim.cpp | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/src/ast/rewriter/seq_regex_bisim.cpp b/src/ast/rewriter/seq_regex_bisim.cpp index 5e849017c..e296d5b3e 100644 --- a/src/ast/rewriter/seq_regex_bisim.cpp +++ b/src/ast/rewriter/seq_regex_bisim.cpp @@ -86,9 +86,15 @@ namespace seq { } /* - Collect the leaves of a t-regex der (an ITE / antimirov union / - union-tree with regex leaves) into the output vector. Empty - (re.empty) leaves are dropped. + Collect the leaves of a t-regex der (an ITE-tree whose leaves are + regex expressions) into the output vector. Empty (re.empty) leaves + are dropped. + + Each leaf is treated as a single bisimulation state regardless of + its top-level shape (including re.union and re.antimirov_union): + descending into a union at the leaf would split one state into + several, which is semantically unsound for the bisimulation / + union-find merging that follows. Returns false if we encountered an unexpected node (e.g. a free variable creeping in) — in that case the caller should bail out. @@ -102,9 +108,7 @@ namespace seq { expr* e = work.back(); work.pop_back(); expr* c = nullptr, * t = nullptr, * f = nullptr; - if (m.is_ite(e, c, t, f) || - m_util.re.is_union(e, t, f) || - m_util.re.is_antimirov_union(e, t, f)) { + if (m.is_ite(e, c, t, f)) { if (seen.insert_if_not_there(t)) work.push_back(t); if (seen.insert_if_not_there(f)) From 86de0cbd7164dceabd214c2fb1a12fd1b21c8fd9 Mon Sep 17 00:00:00 2001 From: davedets Date: Tue, 16 Jun 2026 06:55:18 -0700 Subject: [PATCH 02/10] Eliminate unused private fields and local variables. (#9875) This is another PR towards the goal of getting a clean build with clang, using the compiler options used in building clang-tidy. By default, without any new -W flags, clang warns about unused local variables and private class fields. This PR deletes the handful of these that clang found. I'm assuming that the class "enode" in smt_context.cpp is the one in smt_enode.h, so that ``` parent->get_expr() ``` calls a const method with no side effects. --- src/ast/simplifiers/dependent_expr_state.h | 2 +- src/smt/smt_context.cpp | 1 - src/smt/theory_sls.h | 1 - src/solver/parallel_tactical2.cpp | 3 +-- 4 files changed, 2 insertions(+), 5 deletions(-) diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h index 504f67ad0..ed34d4a19 100644 --- a/src/ast/simplifiers/dependent_expr_state.h +++ b/src/ast/simplifiers/dependent_expr_state.h @@ -45,7 +45,7 @@ Author: class dependent_expr_state { unsigned m_qhead = 0; bool m_suffix_frozen = false; - unsigned m_num_recfun = 0, m_num_lambdas = 0; + unsigned m_num_recfun = 0; lbool m_has_quantifiers = l_undef; ast_mark m_frozen; func_decl_ref_vector m_frozen_trail; diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 098240fc9..c23da2bba 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4672,7 +4672,6 @@ namespace smt { theory_id th_id = l->get_id(); for (enode * parent : enode::parents(n)) { - auto p = parent->get_expr(); family_id fid = parent->get_family_id(); if (fid != th_id && fid != m.get_basic_family_id()) { if (is_beta_redex(parent, n)) diff --git a/src/smt/theory_sls.h b/src/smt/theory_sls.h index 2b65783b4..856f8f3d2 100644 --- a/src/smt/theory_sls.h +++ b/src/smt/theory_sls.h @@ -66,7 +66,6 @@ namespace smt { unsigned m_final_check_ls_steps = 30000; unsigned m_final_check_ls_steps_delta = 10000; unsigned m_final_check_ls_steps_min = 10000; - unsigned m_final_check_ls_steps_max = 30000; bool m_has_unassigned_clause_after_resolve = false; unsigned m_after_resolve_decide_gap = 4; unsigned m_after_resolve_decide_count = 0; diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index ebae4cb57..dffb5f15c 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -460,7 +460,6 @@ class parallel_solver { }; unsigned id; - parallel_solver& p; batch_manager& b; ast_manager m; /* worker-local manager */ ref s; /* translated solver copy */ @@ -579,7 +578,7 @@ class parallel_solver { worker(unsigned id, parallel_solver& p, solver& src, params_ref const& params, expr_ref_vector const& src_asms) - : id(id), p(p), b(p.m_batch_manager), + : id(id), b(p.m_batch_manager), asms(m), m_g2l(src.get_manager(), m), m_l2g(m, src.get_manager()) { /* create translated solver copy */ From ff2e0a3ab09e2f60f032c8df2830fec9e7a9aa5a Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 16 Jun 2026 14:55:59 +0100 Subject: [PATCH 03/10] Remove a few unneeded constructors (#9879) --- src/util/obj_hashtable.h | 16 ++++++---------- src/util/obj_pair_hashtable.h | 12 ++++-------- src/util/obj_triple_hashtable.h | 15 +++++---------- src/util/symbol_table.h | 17 +++-------------- 4 files changed, 18 insertions(+), 42 deletions(-) diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index 5020377e0..0b39163ea 100644 --- a/src/util/obj_hashtable.h +++ b/src/util/obj_hashtable.h @@ -62,10 +62,6 @@ public: struct key_data { Key * m_key = nullptr; Value m_value; - key_data() = default; - key_data(Key* k): m_key(k) {} - key_data(Key* k, Value const& v): m_key(k), m_value(v) {} - key_data(Key* k, Value&& v): m_key(k), m_value(std::move(v)) {} Value const & get_value() const { return m_value; } Key & get_key () const { return *m_key; } unsigned hash() const { return m_key->hash(); } @@ -136,15 +132,15 @@ public: } void insert(Key * const k, Value const & v) { - m_table.insert(key_data(k, v)); + m_table.insert(key_data{k, v}); } void insert(Key * const k, Value && v) { - m_table.insert(key_data(k, std::move(v))); + m_table.insert(key_data{k, std::move(v)}); } Value& insert_if_not_there(Key * k, Value const & v) { - return m_table.insert_if_not_there2(key_data(k, v))->get_data().m_value; + return m_table.insert_if_not_there2(key_data{k, v})->get_data().m_value; } Value& insert_if_not_there(Key * k, Value && v) { @@ -194,7 +190,7 @@ public: } iterator find_iterator(Key * k) const { - return m_table.find(key_data(k)); + return m_table.find(key_data{k}); } bool contains(Key * k) const { @@ -202,7 +198,7 @@ public: } void remove(Key * k) { - m_table.remove(key_data(k)); + m_table.remove(key_data{k}); } void erase(Key * k) { @@ -213,7 +209,7 @@ public: void get_collisions(Key * k, vector& collisions) { vector cs; - m_table.get_collisions(key_data(k), cs); + m_table.get_collisions(key_data{k}, cs); for (key_data const& kd : cs) { collisions.push_back(kd.m_key); } diff --git a/src/util/obj_pair_hashtable.h b/src/util/obj_pair_hashtable.h index e9d2e9bb5..78355b9bb 100644 --- a/src/util/obj_pair_hashtable.h +++ b/src/util/obj_pair_hashtable.h @@ -59,17 +59,13 @@ protected: class entry; public: class key_data { - Key1 * m_key1; - Key2 * m_key2; + Key1 * m_key1 = nullptr; + Key2 * m_key2 = nullptr; Value m_value; - unsigned m_hash; + unsigned m_hash = 0; friend class entry; public: - key_data(): - m_key1(nullptr), - m_key2(nullptr), - m_hash(0) { - } + key_data() = default; key_data(Key1 * k1, Key2 * k2): m_key1(k1), m_key2(k2) { diff --git a/src/util/obj_triple_hashtable.h b/src/util/obj_triple_hashtable.h index 7d75084fe..00a7a2845 100644 --- a/src/util/obj_triple_hashtable.h +++ b/src/util/obj_triple_hashtable.h @@ -60,19 +60,14 @@ protected: class entry; public: class key_data { - Key1 * m_key1; - Key2 * m_key2; - Key3 * m_key3; + Key1 * m_key1 = nullptr; + Key2 * m_key2 = nullptr; + Key3 * m_key3 = nullptr; Value m_value; - unsigned m_hash; + unsigned m_hash = 0; friend class entry; public: - key_data(): - m_key1(nullptr), - m_key2(nullptr), - m_key3(nullptr), - m_hash(0) { - } + key_data() = default; key_data(Key1 * k1, Key2 * k2, Key3 * k3): m_key1(k1), m_key2(k2), diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index 5d2cce726..c6dbb9f82 100644 --- a/src/util/symbol_table.h +++ b/src/util/symbol_table.h @@ -30,17 +30,6 @@ class symbol_table { struct key_data { symbol m_key; T m_data; - - key_data() = default; - - explicit key_data(symbol k): - m_key(k) { - } - - key_data(symbol k, const T & d): - m_key(k), - m_data(d) { - } }; struct key_data_hash_proc { @@ -129,7 +118,7 @@ public: } bool contains(symbol key) const { - return m_sym_table.contains(key_data(key)); + return m_sym_table.contains(key_data{key}); } unsigned get_scope_level() const { @@ -148,11 +137,11 @@ public: m_trail_stack.push_back(dummy); key_data & new_entry = m_trail_stack.back(); new_entry.m_key = symbol::mark(new_entry.m_key); - m_sym_table.insert(key_data(key, data)); + m_sym_table.insert(key_data{key, data}); } } else { - m_sym_table.insert(key_data(key, data)); + m_sym_table.insert(key_data{key, data}); } } From b6c7ef2f680cf7361956f613a4ae9cd97d8aa1c2 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Tue, 16 Jun 2026 09:52:04 -0600 Subject: [PATCH 04/10] dotnet: force PlatformTarget=AnyCPU to fix arm64 host load failure (#9868) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `Microsoft.Z3.dll` was being emitted with PE `Machine=0x8664` (AMD64) despite being pure IL, because the Windows x64 CI environment (`vcvarsall.bat x64`) injects `Platform=x64` into MSBuild, which sets the COFF machine type when `PlatformTarget` is not explicitly specified. This causes `FS0193` / architecture mismatch errors on any arm64 .NET host (macOS Apple Silicon, Linux aarch64, Windows on ARM). ## Changes - **`scripts/mk_util.py`** — Add `AnyCPU` to the in-memory `.csproj` template generated by the Python build system (`mk_win_dist.py`, `mk_unix_dist.py`) - **`src/api/dotnet/Microsoft.Z3.csproj.in`** — Add `AnyCPU` to the CMake build system template Both paths now produce `Machine=0x014C` (i386/AnyCPU) regardless of host or CI environment, matching the assembly's actual nature (`ILONLY=True`, `32BIT_REQUIRED=False`). The native side already ships six RIDs; no changes needed there. --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> --- scripts/mk_util.py | 1 + src/api/dotnet/Microsoft.Z3.csproj.in | 1 + 2 files changed, 2 insertions(+) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index ff04bfb68..89d82303a 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1804,6 +1804,7 @@ class DotNetDLLComponent(Component): Z3 is a satisfiability modulo theories solver from Microsoft Research. Copyright Microsoft Corporation. All rights reserved. smt constraint solver theorem prover + AnyCPU %s diff --git a/src/api/dotnet/Microsoft.Z3.csproj.in b/src/api/dotnet/Microsoft.Z3.csproj.in index cf5aacf46..55cb100be 100644 --- a/src/api/dotnet/Microsoft.Z3.csproj.in +++ b/src/api/dotnet/Microsoft.Z3.csproj.in @@ -60,6 +60,7 @@ 4 true $(OutputPath)\Microsoft.Z3.xml + AnyCPU From 66795ea3228e7e43fe73db501c3eb4b06384900f Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Tue, 16 Jun 2026 11:16:19 -0600 Subject: [PATCH 05/10] ci: validate Microsoft.Z3.dll PE Machine field is AnyCPU in nightly build validation (#9873) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `Microsoft.Z3.dll` ships with PE `Machine=0x8664` (AMD64), causing the CLR loader to reject it on arm64 .NET hosts (macOS/Linux/Windows ARM) even though the assembly is pure IL (`CorFlags.ILONLY=True`) and arm64 native libraries are already bundled in the package. ## Changes - **`.github/workflows/nightly-validation.yml`** — adds `validate-dotnet-anycpu` job to the Nightly Build Validation workflow: - Downloads the nightly NuGet package from the GitHub release - Extracts `lib/netstandard2.0/Microsoft.Z3.dll` (NuGet packages are ZIP archives) - Reads the COFF `Machine` field from the PE header using Python `struct` - Fails with an actionable error if `Machine` is `0x8664` (AMD64) or `0xAA64` (ARM64); passes for `0x014C` (i386/AnyCPU) or `0x0000` The check catches any regression where the managed wrapper is compiled architecture-specific, blocking non-x64 .NET hosts from loading it. --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> --- .github/workflows/nightly-validation.yml | 94 ++++++++++++++++++++++++ 1 file changed, 94 insertions(+) diff --git a/.github/workflows/nightly-validation.yml b/.github/workflows/nightly-validation.yml index f4daced79..bec816438 100644 --- a/.github/workflows/nightly-validation.yml +++ b/.github/workflows/nightly-validation.yml @@ -844,3 +844,97 @@ jobs: - name: Run build script unit tests run: python -m unittest discover -s scripts/tests -p "test_*.py" -v + + # ============================================================================ + # DOTNET MANAGED WRAPPER ARCHITECTURE VALIDATION + # ============================================================================ + + validate-dotnet-anycpu: + name: "Validate Microsoft.Z3.dll is AnyCPU (issue #9863)" + runs-on: ubuntu-latest + if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }} + timeout-minutes: 15 + steps: + - name: Checkout code + uses: actions/checkout@v6.0.3 + + - name: Download NuGet package from release + env: + GH_TOKEN: ${{ github.token }} + run: | + TAG="${{ github.event.inputs.release_tag }}" + if [ -z "$TAG" ]; then + TAG="Nightly" + fi + gh release download $TAG --pattern "*.nupkg" --dir nuget-packages + + - name: Extract managed DLL from NuGet package + run: | + # NuGet packages are ZIP archives; exclude the symbols package + NUPKG=$(ls nuget-packages/*.nupkg | grep -v '\.symbols\.' | grep -v '\.snupkg' | head -n 1) + echo "Checking package: $NUPKG" + unzip -q "$NUPKG" "lib/netstandard2.0/Microsoft.Z3.dll" -d nupkg-extracted + + - name: Check PE Machine field is AnyCPU (not architecture-specific) + run: | + python3 - <<'EOF' + import struct + import sys + + dll_path = "nupkg-extracted/lib/netstandard2.0/Microsoft.Z3.dll" + + with open(dll_path, 'rb') as f: + # Verify MZ magic + if f.read(2) != b'MZ': + print("ERROR: Not a valid PE file (missing MZ header)") + sys.exit(1) + + # Read PE header offset stored at 0x3C in the DOS stub + f.seek(0x3C) + pe_offset = struct.unpack(' Date: Tue, 16 Jun 2026 11:25:14 -0600 Subject: [PATCH 06/10] block lia2card on recursive functions Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/lia2card_tactic.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index 17d8de908..c9c675ac0 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -185,6 +185,10 @@ public: expr_safe_replace rep(m); tactic_report report("lia2card", *g); + if (recfun::util(m()).has_rec_defs()) { + result.push_back(g.get()); + return; + } bound_manager bounds(m); for (unsigned i = 0; i < g->size(); ++i) From d457f9f5d3c4bb82b682b93a2bacbb664d099707 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Tue, 16 Jun 2026 11:34:20 -0600 Subject: [PATCH 07/10] Bump markdown-it from 14.1.0 to 14.2.0 in /src/api/js (#9881) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Bumps [markdown-it](https://github.com/markdown-it/markdown-it) from 14.1.0 to 14.2.0.
Changelog

Sourced from markdown-it's changelog.

[14.2.0] - 2026-05-24

Added

  • isPunctCharCode to utilities.

Fixed

  • Don't end HTML comment blocks on a blank line, #1155.
  • Properly recognize astral chars (surrogates) in delimiter scans for emphasis-like markers, #1072. Big thanks to @​tats-u for his global efforts with improving CJK support.
  • Preserve unicode whitespaces when trimm headings/paragraphs, #1074.
  • More strict entities decode to avoid false positives ;, #1096.
  • Restore block parser state on fail in lheading rule, #1131.

Security

  • Fixed poor smartquotes perfomance on > 70k quotes in single block
  • Bumped linkify-it to 5.0.1 with fixed potential perfomance issues.

[14.1.1] - 2026-01-11

Security

  • Fixed regression from v13 in linkify inline rule. Specific patterns could cause high CPU use. Thanks to @​ltduc147 for report.
Commits

[![Dependabot compatibility score](https://dependabot-badges.githubapp.com/badges/compatibility_score?dependency-name=markdown-it&package-manager=npm_and_yarn&previous-version=14.1.0&new-version=14.2.0)](https://docs.github.com/en/github/managing-security-vulnerabilities/about-dependabot-security-updates#about-compatibility-scores) Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting `@dependabot rebase`. [//]: # (dependabot-automerge-start) [//]: # (dependabot-automerge-end) ---
Dependabot commands and options
You can trigger Dependabot actions by commenting on this PR: - `@dependabot rebase` will rebase this PR - `@dependabot recreate` will recreate this PR, overwriting any edits that have been made to it - `@dependabot show ignore conditions` will show all of the ignore conditions of the specified dependency - `@dependabot ignore this major version` will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this minor version` will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this dependency` will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself) You can disable automated security fix PRs for this repo from the [Security Alerts page](https://github.com/Z3Prover/z3/network/alerts).
Signed-off-by: dependabot[bot] Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> --- src/api/js/package-lock.json | 34 +++++++++++++++++++++++++++------- 1 file changed, 27 insertions(+), 7 deletions(-) diff --git a/src/api/js/package-lock.json b/src/api/js/package-lock.json index 5c11307f4..be3675354 100644 --- a/src/api/js/package-lock.json +++ b/src/api/js/package-lock.json @@ -5400,10 +5400,20 @@ "dev": true }, "node_modules/linkify-it": { - "version": "5.0.0", - "resolved": "https://registry.npmjs.org/linkify-it/-/linkify-it-5.0.0.tgz", - "integrity": "sha512-5aHCbzQRADcdP+ATqnDuhhJ/MRIqDkZX5pyjFHRRysS8vZ5AbqGEoFIb6pYHPZ+L/OC2Lc+xT8uHVVR5CAK/wQ==", + "version": "5.0.1", + "resolved": "https://registry.npmjs.org/linkify-it/-/linkify-it-5.0.1.tgz", + "integrity": "sha512-wVoTjP4Q6R0NW5hiZkVJaFZPWgtXfoGF+6LucL3/FtiNjmcHhYjEr5f1Kqjirc1nBW07J/ZuRFumqr2oqccEWg==", "dev": true, + "funding": [ + { + "type": "github", + "url": "https://github.com/sponsors/puzrin" + }, + { + "type": "github", + "url": "https://github.com/sponsors/markdown-it" + } + ], "license": "MIT", "dependencies": { "uc.micro": "^2.0.0" @@ -5501,15 +5511,25 @@ } }, "node_modules/markdown-it": { - "version": "14.1.0", - "resolved": "https://registry.npmjs.org/markdown-it/-/markdown-it-14.1.0.tgz", - "integrity": "sha512-a54IwgWPaeBCAAsv13YgmALOF1elABB08FxO9i+r4VFk5Vl4pKokRPeX8u5TCgSsPi6ec1otfLjdOpVcgbpshg==", + "version": "14.2.0", + "resolved": "https://registry.npmjs.org/markdown-it/-/markdown-it-14.2.0.tgz", + "integrity": "sha512-1TGiQiJVRQ3NPmZH6sx5Cfnmg6GQm9jvC1ch4TK511NjSJvjzKLzn5pPfZRNZkRPZP0HqCioSndqH8v2nRaWVQ==", "dev": true, + "funding": [ + { + "type": "github", + "url": "https://github.com/sponsors/puzrin" + }, + { + "type": "github", + "url": "https://github.com/sponsors/markdown-it" + } + ], "license": "MIT", "dependencies": { "argparse": "^2.0.1", "entities": "^4.4.0", - "linkify-it": "^5.0.0", + "linkify-it": "^5.0.1", "mdurl": "^2.0.0", "punycode.js": "^2.3.1", "uc.micro": "^2.1.0" From 3d691fe234a3fc0f12c5a24cd53efcc9829f5488 Mon Sep 17 00:00:00 2001 From: Shantanu Gontia Date: Tue, 16 Jun 2026 23:05:21 +0530 Subject: [PATCH 08/10] Add versioned shared object names in Bazel rules (#9838) Adds versioned shared library names (`libz3.so.4.17`, `libz3.4.17.dylib`, etc.) alongside the unversioned ones to enable Bazel rules to locate the correct library binaries. --- BUILD.bazel | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/BUILD.bazel b/BUILD.bazel index f4d69a747..ef78b6e83 100644 --- a/BUILD.bazel +++ b/BUILD.bazel @@ -19,14 +19,23 @@ filegroup( cmake( name = "z3_dynamic", generate_args = [ - "-G Ninja", + "-G Ninja", "-D Z3_EXPORTED_TARGETS=", # prevents installation, leaving symlinks between dylibs intact on copy ], lib_source = ":all_files", out_binaries = ["z3"], out_shared_libs = select({ - "@platforms//os:linux": ["libz3.so"], - # "@platforms//os:osx": ["libz3.dylib"], # FIXME: this is not working, libz3.dylib is not copied + # NOTE: These will need to be manually bumped along side the version in MODULE.bazel/VERSION.txt/CMake + "@platforms//os:linux": [ + "libz3.so", + "libz3.so.4.17", + "libz3.so.4.17.0.0", + ], + "@platforms//os:osx": [ + "libz3.dylib", + "libz3.4.17.dylib", + "libz3.4.17.0.0.dylib", + ], "@platforms//os:windows": ["libz3.dll"], "//conditions:default": ["@platforms//:incompatible"], }), @@ -36,7 +45,7 @@ cmake( cmake( name = "z3_static", generate_args = [ - "-G Ninja", + "-G Ninja", "-D BUILD_SHARED_LIBS=OFF", "-D Z3_BUILD_LIBZ3_SHARED=OFF", ], From ec7462024a3813d5d62df7891d8f07719a171f5b Mon Sep 17 00:00:00 2001 From: "Peter Chen J." <34339487+peter941221@users.noreply.github.com> Date: Wed, 17 Jun 2026 01:36:13 +0800 Subject: [PATCH 09/10] Strengthen historical nlsat regression tests (#9857) This tightens two historical `nlsat` regressions that were still print-only. Closes #9859. In `tst_16`, the test already exercises the old `lws2380` shape, but it only dumped the projected clause. On current `master`, both projection paths still keep the `x7`-linked root constraints, so this change turns that observation into an assertion and updates the stale comment to describe the current invariant. In `tst_22`, the test already computes whether the projected lemma is falsified at the stored counterexample. It previously printed the result and kept going. This change adds `ENSURE(!all_false)` so the test fails if that historical unsoundness shape comes back. Testing: `cmake --build . --target test-z3 -j1` `./test-z3 /seq nlsat` --- src/test/nlsat.cpp | 49 +++++++++++++++++++++++++++++++++++++++------- 1 file changed, 42 insertions(+), 7 deletions(-) diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index 9709a36bf..ab2749c3a 100644 --- a/src/test/nlsat.cpp +++ b/src/test/nlsat.cpp @@ -452,7 +452,7 @@ static void project(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsigned std::cout << "\n"; } -static void project_fa(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsigned num, nlsat::literal const* lits) { +static nlsat::scoped_literal_vector project_fa(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsigned num, nlsat::literal const* lits) { std::cout << "Project "; nlsat::scoped_literal_vector result(s); ex.compute_conflict_explanation(num, lits, result); @@ -464,6 +464,7 @@ static void project_fa(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsig s.display(std::cout << " ", ~lits[i]); } std::cout << ")\n"; + return result; } static nlsat::literal mk_gt(nlsat::solver& s, nlsat::poly* p) { @@ -490,6 +491,39 @@ static nlsat::literal mk_root_eq(nlsat::solver& s, nlsat::poly* p, nlsat::var x, return nlsat::literal(b, false); } +static bool contains_var(nlsat::var_vector const& vars, nlsat::var x) { + for (auto v : vars) { + if (v == x) + return true; + } + return false; +} + +static bool clause_contains_root_dependency( + nlsat::solver& s, + nlsat::scoped_literal_vector const& result, + nlsat::atom::kind kind, + nlsat::var target, + unsigned root_index, + nlsat::var dep1, + nlsat::var dep2, + nlsat::var dep3) { + nlsat::pmanager& pm = s.pm(); + nlsat::var_vector vars; + for (auto l : result) { + nlsat::atom* a = s.bool_var2atom(l.var()); + if (!a || !a->is_root_atom() || a->get_kind() != kind) + continue; + nlsat::root_atom* ra = nlsat::to_root_atom(a); + if (ra->x() != target || ra->i() != root_index || pm.max_var(ra->p()) != target) + continue; + s.vars(l, vars); + if (contains_var(vars, dep1) && contains_var(vars, dep2) && contains_var(vars, dep3)) + return true; + } + return false; +} + static void set_assignment_value(nlsat::assignment& as, anum_manager& am, nlsat::var v, rational const& val) { scoped_anum tmp(am); am.set(tmp, val.to_mpq()); @@ -1183,8 +1217,8 @@ static void tst_15() { auto cell = lws.single_cell(); } -// Test case for unsound lemma lws2380 - comparing standard projection vs levelwise -// The issue: x7 is unconstrained in levelwise output but affects the section polynomial +// Historical lws2380 regression test: both projection paths should preserve +// the x7-linked section/root constraints that witness the projected dependency. static void tst_16() { // enable_trace("nlsat_explain"); @@ -1283,8 +1317,9 @@ static void tst_16() { lits.push_back(mk_gt(s, p0.get())); // x13 > 0 lits.push_back(mk_gt(s, p1.get())); // p1 > 0 - project_fa(s, ex, x13, lits.size(), lits.data()); + auto result = project_fa(s, ex, x13, lits.size(), lits.data()); std::cout << "\n"; + ENSURE(clause_contains_root_dependency(s, result, nlsat::atom::ROOT_EQ, x11, 1, x7, x8, x10)); }; run_test(false); // Standard projection @@ -2144,11 +2179,11 @@ static void tst_22() { } } - if (all_false) { + if (all_false) std::cout << "*** ALL literals FALSE at counterexample - LEMMA IS UNSOUND! ***\n"; - } else { + else std::cout << "At least one literal is TRUE - lemma is sound at this point\n"; - } + ENSURE(!all_false); }; run_test(false); // lws=false (buggy) From 897c4475af6c075697e4aa9bde3e3d31ac647232 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Tue, 16 Jun 2026 12:09:20 -0600 Subject: [PATCH 10/10] =?UTF-8?q?goal2sat:=20drop=20unsafe=20ref=5Fcount?= =?UTF-8?q?=E2=89=A41=20cache-skip=20optimization;=20keep=20bit=5Fblaster?= =?UTF-8?q?=20mk=5Feq=20improvement=20(#9882)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PR #9872 caused timeouts in QF_UFBV, QF_BV, and QF_FP regressions (`t135`, `t136`, `nl53`, `3397`, `4841-1`, `fp-lt-gt`, `fp-rem-11`). ## Root cause The `goal2sat` change skipped caching AST nodes with `ref_count ≤ 1` under the assumption they're visited only once. This assumption is wrong: EUF, BV, and FP theory extensions all call `internalize()` from the theory solver side, outside the main DFS traversal. On the second `internalize(n)` call, the missing cache entry causes the entire subtree to be re-encoded with a fresh literal — inconsistent encoding and exponential blowup. ## Changes - **`goal2sat.cpp`**: revert the `ref_count ≤ 1` skip-caching optimization entirely; it is unsafe whenever any theory extension is active. - **`bit_blaster_tpl_def.h`**: retain the `mk_eq` micro-optimization from #9872 — pre-size with `resize(sz)` and use index assignment instead of `push_back`. This is correct: `resize` null-initializes slots and `element_ref::operator=` handles ref-counting via `inc_ref`/`dec_ref`. --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> --- src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index 342ff5ed8..87785d8f8 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -768,9 +768,10 @@ void bit_blaster_tpl::mk_smod(unsigned sz, expr * const * a_bits, expr * co template void bit_blaster_tpl::mk_eq(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref & out) { expr_ref_vector out_bits(m()); + out_bits.resize(sz); for (unsigned i = 0; i < sz; ++i) { mk_iff(a_bits[i], b_bits[i], out); - out_bits.push_back(out); + out_bits[i] = out; } mk_and(out_bits.size(), out_bits.data(), out); }