From 86de0cbd7164dceabd214c2fb1a12fd1b21c8fd9 Mon Sep 17 00:00:00 2001 From: davedets Date: Tue, 16 Jun 2026 06:55:18 -0700 Subject: [PATCH 01/13] 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 02/13] 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 03/13] 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 04/13] 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 05/13] 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 06/13] 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 07/13] 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 08/13] 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 09/13] =?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); } From 8c2a425e4bfc41a4f654e8f5afa184f5176a49e4 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Tue, 16 Jun 2026 13:58:56 -0600 Subject: [PATCH 10/13] Smart constructors for regex ranges: canonical form at construction time (#9814) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Regex range expressions (`re.range`) and Boolean operations over them were left in unsimplified form, defeating downstream optimisations (bisimulation classical fast-path, derivative engine) and producing semantically-empty terms not syntactically equal to `re.none`. ## Changes ### `seq_decl_plugin.h` / `seq_decl_plugin.cpp` - **`seq_util::rex::mk_range(sort*, unsigned lo, unsigned hi)`** — new smart constructor that normalises at call time: - `lo > hi` → `re.empty` - `lo == hi` → `str.to_re` (singleton string) - `lo < hi` → `re.range` - **`mk_info_rec` `OP_RE_RANGE`** — concrete non-empty ranges (both bounds are single-char literals with `lo ≤ hi`) now return `classical = true`, enabling the XOR-bisimulation `classical_distinguishing` fast-path on character-predicate leaves. Symbolic/unknown ranges retain `classical = false`. ### `seq_rewriter.cpp` - **`mk_re_range`** — singleton collapse: `(re.range "a" "a")` → `(str.to_re "a")` - **`mk_regex_inter_normalize`** — range × range intersection: `[a,b] ∩ [c,d]` → `[max(a,c), min(b,d)]`, or `re.none` (disjoint), or `str.to_re` (boundary singleton); now delegates to `re().mk_range(sort*, lo, hi)` - **`mk_regex_union_normalize`** — range × range union for overlapping/adjacent ranges: `[a,b] ∪ [c,d]` → `[min(a,c), max(b,d)]`; disjoint ranges fall through to existing `merge_regex_sets`; now delegates to `re().mk_range(sort*, lo, hi)` - **`mk_re_complement`** — range complement expands to one or two concrete ranges instead of an opaque `re.comp` node; now delegates to `re().mk_range(sort*, lo, hi)`: - `comp([0, b])` → `[b+1, max]` - `comp([a, max])` → `[0, a-1]` - `comp([a, b])` → `[0, a-1] ∪ [b+1, max]` ``` (simplify (re.range "z" "a")) ; → re.none (simplify (re.range "a" "a")) ; → (str.to_re "a") (simplify (re.inter (re.range "a" "z") (re.range "f" "k"))); → (re.range "f" "k") (simplify (re.union (re.range "a" "f") (re.range "g" "k"))); → (re.range "a" "k") (simplify (re.comp (re.range "b" "y"))) ; → (re.union [0,a] [z,max]) ``` ### Tests New `src/test/seq_rewriter.cpp` with 14 cases covering all the above reductions plus downstream propagation (star/concat/union/inter absorbing empty ranges). --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 58 ++++++++- src/ast/seq_decl_plugin.cpp | 21 +++- src/ast/seq_decl_plugin.h | 2 + src/test/CMakeLists.txt | 1 + src/test/main.cpp | 1 + src/test/seq_rewriter.cpp | 193 ++++++++++++++++++++++++++++++ 6 files changed, 272 insertions(+), 4 deletions(-) create mode 100644 src/test/seq_rewriter.cpp diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index ac0261f61..7dabfe364 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -3336,6 +3336,18 @@ expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) { result = r1; else if (re().is_dot_plus(r2) && re().get_info(r1).min_length > 0) result = r2; + else { + // Range ∪ Range: [a,b] ∪ [c,d] = [min(a,c), max(b,d)] when overlapping or adjacent + unsigned lo1_v = 0, hi1_v = 0, lo2_v = 0, hi2_v = 0; + if (re().is_range(r1, lo1_v, hi1_v) && re().is_range(r2, lo2_v, hi2_v) && + lo2_v <= hi1_v + 1 && lo1_v <= hi2_v + 1) { + unsigned new_lo = std::min(lo1_v, lo2_v); + unsigned new_hi = std::max(hi1_v, hi2_v); + result = re().mk_range(r1->get_sort(), new_lo, new_hi); + } + else + result = merge_regex_sets(r1, r2, re().mk_full_seq(r1->get_sort()), test, compose); + } // (R1 \ R2) U (R2 \ R1) = R1 xor R2 else if (false && re().is_intersection(r1, a1, a2) && re().is_intersection(r2, b1, b2) && is_complement(a1, b2) && is_complement(a2, b1)) { @@ -3375,8 +3387,17 @@ expr_ref seq_rewriter::mk_regex_inter_normalize(expr* r1, expr* r2) { result = r2; else if (re().is_dot_plus(r2) && re().get_info(r1).min_length > 0) result = r1; - else - result = merge_regex_sets(r1, r2, re().mk_empty(r1->get_sort()), test, compose); + else { + // Range ∩ Range: [a,b] ∩ [c,d] = [max(a,c), min(b,d)] or empty + unsigned lo1_v = 0, hi1_v = 0, lo2_v = 0, hi2_v = 0; + if (re().is_range(r1, lo1_v, hi1_v) && re().is_range(r2, lo2_v, hi2_v)) { + unsigned new_lo = std::max(lo1_v, lo2_v); + unsigned new_hi = std::min(hi1_v, hi2_v); + result = re().mk_range(r1->get_sort(), new_lo, new_hi); + } + else + result = merge_regex_sets(r1, r2, re().mk_empty(r1->get_sort()), test, compose); + } return result; } @@ -4805,6 +4826,34 @@ br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) { result = re().mk_plus(re().mk_full_char(a->get_sort())); return BR_DONE; } + // Range complement: comp([a,b]) → [0,a-1] ∪ [b+1,max] (or one half when a=0 or b=max) + unsigned lo_v = 0, hi_v = 0; + if (re().is_range(a, lo_v, hi_v)) { + unsigned max_c = u().max_char(); + sort* srt = a->get_sort(); + bool has_left = (lo_v > 0); + bool has_right = (hi_v < max_c); + if (!has_left && !has_right) { + // [0, max_c]: complement is empty + result = re().mk_empty(srt); + return BR_DONE; + } + if (!has_left) { + // [0, b]: complement is [b+1, max] + result = re().mk_range(srt, hi_v + 1, max_c); + return BR_REWRITE1; + } + if (!has_right) { + // [a, max]: complement is [0, a-1] + result = re().mk_range(srt, 0u, lo_v - 1); + return BR_REWRITE1; + } + // General: [a, b] → [0, a-1] ∪ [b+1, max] + auto left = re().mk_range(srt, 0u, lo_v - 1); + auto right = re().mk_range(srt, hi_v + 1, max_c); + result = re().mk_union(left, right); + return BR_REWRITE1; + } return BR_FAILED; } @@ -5102,6 +5151,11 @@ br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) { result = re().mk_empty(srt); return BR_DONE; } + // Singleton: re.range "a" "a" → str.to_re "a" + if (slo.length() == 1 && shi.length() == 1 && slo[0] == shi[0]) { + result = re().mk_to_re(lo); + return BR_DONE; + } return BR_FAILED; } diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 59f5d046c..29949a151 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -1208,6 +1208,15 @@ app* seq_util::rex::mk_of_pred(expr* p) { return m.mk_app(m_fid, OP_RE_OF_PRED, 0, nullptr, 1, &p); } +app* seq_util::rex::mk_range(sort* re_sort, unsigned lo, unsigned hi) { + if (lo > hi) + return mk_empty(re_sort); + app* lo_str = u.str.mk_string(zstring(lo)); + if (lo == hi) + return mk_to_re(lo_str); + return mk_range(lo_str, u.str.mk_string(zstring(hi))); +} + bool seq_util::rex::is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi) const { if (is_loop(n)) { app const* a = to_app(n); @@ -1671,11 +1680,19 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const { case OP_RE_OPTION: i1 = get_info_rec(e->get_arg(0)); return i1.opt(); - case OP_RE_RANGE: + case OP_RE_RANGE: { + // A concrete range [lo, hi] with lo <= hi is non-empty and classical. + zstring slo, shi; + if (u.str.is_string(e->get_arg(0), slo) && slo.length() == 1 && + u.str.is_string(e->get_arg(1), shi) && shi.length() == 1 && + slo[0] <= shi[0]) + return info(true, l_false, 1, true); + // Symbolic or unknown: not classical + return info(true, l_false, 1, false); + } case OP_RE_FULL_CHAR_SET: case OP_RE_OF_PRED: //TBD: check if the character predicate contains uninterpreted symbols or is nonground or is unsat - //TBD: check if the range is unsat return info(true, l_false, 1, false); case OP_RE_CONCAT: i1 = get_info_rec(e->get_arg(0)); diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 75995ef7b..c643d8356 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -521,6 +521,8 @@ public: app* mk_to_re(expr* s) { return m.mk_app(m_fid, OP_SEQ_TO_RE, 1, &s); } app* mk_in_re(expr* s, expr* r) { return m.mk_app(m_fid, OP_SEQ_IN_RE, s, r); } app* mk_range(expr* s1, expr* s2) { return m.mk_app(m_fid, OP_RE_RANGE, s1, s2); } + // Smart constructor: returns re.empty / str.to_re / re.range based on lo vs hi. + app* mk_range(sort* re_sort, unsigned lo, unsigned hi); app* mk_concat(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_CONCAT, r1, r2); } app* mk_union(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_UNION, r1, r2); } app* mk_inter(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_INTERSECT, r1, r2); } diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index ef5902c0c..d84892cd5 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -24,6 +24,7 @@ add_executable(test-z3 api_datalog.cpp parametric_datatype.cpp arith_rewriter.cpp + seq_rewriter.cpp arith_simplifier_plugin.cpp ast.cpp bdd.cpp diff --git a/src/test/main.cpp b/src/test/main.cpp index 4a5239f19..4eb66798f 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -113,6 +113,7 @@ X(api_bug) \ X(api_special_relations) \ X(arith_rewriter) \ + X(seq_rewriter) \ X(check_assumptions) \ X(smt_context) \ X(theory_dl) \ diff --git a/src/test/seq_rewriter.cpp b/src/test/seq_rewriter.cpp new file mode 100644 index 000000000..b95008cde --- /dev/null +++ b/src/test/seq_rewriter.cpp @@ -0,0 +1,193 @@ +/*++ +Copyright (c) 2024 Microsoft Corporation + +Regression tests for seq_rewriter smart constructors for regex ranges. + +Tests: + 1. Empty range (lo > hi) → re.none + 2. Singleton range (lo == hi) → str.to_re lo + 3. Range ∩ Range → reduced range or re.none + 4. Range ∪ Range → merged range for overlapping/adjacent + 5. Complement of range → one or two ranges + 6. Downstream operators absorb empty ranges correctly +--*/ + +#include "ast/ast_pp.h" +#include "ast/reg_decl_plugins.h" +#include "ast/rewriter/th_rewriter.h" +#include "ast/seq_decl_plugin.h" +#include + +// Build a single-char string literal expression. +static expr_ref mk_str(ast_manager& m, seq_util& su, unsigned c) { + return expr_ref(su.str.mk_string(zstring(c)), m); +} + +void tst_seq_rewriter() { + ast_manager m; + reg_decl_plugins(m); + th_rewriter rw(m); + seq_util su(m); + + sort* str_sort = su.str.mk_string_sort(); + sort* re_sort = su.re.mk_re(str_sort); + + auto range = [&](unsigned lo, unsigned hi) -> expr_ref { + return expr_ref(su.re.mk_range(mk_str(m, su, lo), mk_str(m, su, hi)), m); + }; + + // Arbitrary regex variable for downstream tests. + app_ref R(m.mk_fresh_const("R", re_sort), m); + + // ----------------------------------------------------------------------- + // 1. Empty range (lo > hi) → re.none + // ----------------------------------------------------------------------- + { + expr_ref e = range('z', 'a'); + rw(e); + std::cout << "empty range lo>hi: " << mk_pp(e, m) << "\n"; + ENSURE(su.re.is_empty(e)); + } + + // ----------------------------------------------------------------------- + // 2. Singleton range (lo == hi) → str.to_re lo + // ----------------------------------------------------------------------- + { + expr_ref e = range('a', 'a'); + rw(e); + std::cout << "singleton range: " << mk_pp(e, m) << "\n"; + expr* inner = nullptr; + ENSURE(su.re.is_to_re(e, inner)); + } + + // ----------------------------------------------------------------------- + // 3. Range intersection: overlapping → smaller range + // ----------------------------------------------------------------------- + { + expr_ref e(su.re.mk_inter(range('a', 'z'), range('f', 'k')), m); + rw(e); + std::cout << "range inter overlapping: " << mk_pp(e, m) << "\n"; + unsigned lo = 0, hi = 0; + ENSURE(su.re.is_range(e, lo, hi) && lo == 'f' && hi == 'k'); + } + + // ----------------------------------------------------------------------- + // 4. Range intersection: disjoint → re.none + // ----------------------------------------------------------------------- + { + expr_ref e(su.re.mk_inter(range('a', 'f'), range('k', 'z')), m); + rw(e); + std::cout << "range inter disjoint: " << mk_pp(e, m) << "\n"; + ENSURE(su.re.is_empty(e)); + } + + // ----------------------------------------------------------------------- + // 5. Range intersection: touching at boundary → singleton (str.to_re "f") + // ----------------------------------------------------------------------- + { + expr_ref e(su.re.mk_inter(range('a', 'f'), range('f', 'z')), m); + rw(e); + std::cout << "range inter touching: " << mk_pp(e, m) << "\n"; + expr* inner = nullptr; + ENSURE(su.re.is_to_re(e, inner)); + } + + // ----------------------------------------------------------------------- + // 6. Range union: overlapping → merged range + // ----------------------------------------------------------------------- + { + expr_ref e(su.re.mk_union(range('a', 'f'), range('e', 'k')), m); + rw(e); + std::cout << "range union overlapping: " << mk_pp(e, m) << "\n"; + unsigned lo = 0, hi = 0; + ENSURE(su.re.is_range(e, lo, hi) && lo == 'a' && hi == 'k'); + } + + // ----------------------------------------------------------------------- + // 7. Range union: adjacent → merged range + // ----------------------------------------------------------------------- + { + expr_ref e(su.re.mk_union(range('a', 'f'), range('g', 'k')), m); + rw(e); + std::cout << "range union adjacent: " << mk_pp(e, m) << "\n"; + unsigned lo = 0, hi = 0; + ENSURE(su.re.is_range(e, lo, hi) && lo == 'a' && hi == 'k'); + } + + // ----------------------------------------------------------------------- + // 8. Range union: disjoint → stays as union + // ----------------------------------------------------------------------- + { + expr_ref e(su.re.mk_union(range('a', 'c'), range('m', 'z')), m); + rw(e); + std::cout << "range union disjoint (stays as union): " << mk_pp(e, m) << "\n"; + ENSURE(!su.re.is_range(e)); + } + + // ----------------------------------------------------------------------- + // 9. Range complement (general): no longer a complement node + // ----------------------------------------------------------------------- + { + expr_ref e(su.re.mk_complement(range('b', 'y')), m); + rw(e); + std::cout << "range comp general: " << mk_pp(e, m) << "\n"; + ENSURE(!su.re.is_complement(e)); + } + + // ----------------------------------------------------------------------- + // 10. Range complement (lo = 0): single range [hi+1, max] + // ----------------------------------------------------------------------- + { + expr_ref lo_str(su.str.mk_string(zstring(0u)), m); + expr_ref hi_str(su.str.mk_string(zstring((unsigned)'f')), m); + expr_ref e(su.re.mk_complement(su.re.mk_range(lo_str, hi_str)), m); + rw(e); + std::cout << "range comp lo=min: " << mk_pp(e, m) << "\n"; + ENSURE(!su.re.is_complement(e)); + ENSURE(su.re.is_range(e)); + } + + // ----------------------------------------------------------------------- + // 11. Downstream: (re.* (re.range "z" "a")) → str.to_re "" + // ----------------------------------------------------------------------- + { + expr_ref e(su.re.mk_star(range('z', 'a')), m); + rw(e); + std::cout << "star of empty range: " << mk_pp(e, m) << "\n"; + expr* inner = nullptr; + // star of empty → epsilon (str.to_re "") + ENSURE(su.re.is_to_re(e, inner) && su.str.is_empty(inner)); + } + + // ----------------------------------------------------------------------- + // 12. Downstream: concat absorbs empty range → re.none + // ----------------------------------------------------------------------- + { + expr_ref e(su.re.mk_concat(R, su.re.mk_concat(range('z', 'a'), R)), m); + rw(e); + std::cout << "concat absorbs empty range: " << mk_pp(e, m) << "\n"; + ENSURE(su.re.is_empty(e)); + } + + // ----------------------------------------------------------------------- + // 13. Downstream: union absorbs empty range → R + // ----------------------------------------------------------------------- + { + expr_ref e(su.re.mk_union(R, range('z', 'a')), m); + rw(e); + std::cout << "union absorbs empty range: " << mk_pp(e, m) << "\n"; + ENSURE(e.get() == R.get()); + } + + // ----------------------------------------------------------------------- + // 14. Downstream: inter absorbs empty range → re.none + // ----------------------------------------------------------------------- + { + expr_ref e(su.re.mk_inter(R, range('z', 'a')), m); + rw(e); + std::cout << "inter absorbs empty range: " << mk_pp(e, m) << "\n"; + ENSURE(su.re.is_empty(e)); + } + + std::cout << "tst_seq_rewriter: all tests passed\n"; +} From 1d9c770d74d3072581907c556fc4a8b33e00e3f7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 16 Jun 2026 14:02:24 -0600 Subject: [PATCH 11/13] Fix reference to recfun::util in lia2card_tactic.cpp --- src/tactic/arith/lia2card_tactic.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index c9c675ac0..b45457349 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -20,6 +20,7 @@ Notes: #include "ast/ast_ll_pp.h" #include "ast/pb_decl_plugin.h" #include "ast/arith_decl_plugin.h" +#include "ast/recfun_decl_plugin.h" #include "ast/rewriter/rewriter_def.h" #include "ast/rewriter/expr_safe_replace.h" #include "ast/ast_util.h" @@ -185,7 +186,7 @@ public: expr_safe_replace rep(m); tactic_report report("lia2card", *g); - if (recfun::util(m()).has_rec_defs()) { + if (recfun::util(m).has_rec_defs()) { result.push_back(g.get()); return; } From bcc3523b237fbecb014cfdae8abf8b29b58eb88a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 16 Jun 2026 14:14:49 -0600 Subject: [PATCH 12/13] Update seq_rewriter.cpp --- src/ast/rewriter/seq_rewriter.cpp | 21 ++++++++++----------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 7dabfe364..2b9d738c0 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -3336,6 +3336,15 @@ expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) { result = r1; else if (re().is_dot_plus(r2) && re().get_info(r1).min_length > 0) result = r2; + // (R1 \ R2) U (R2 \ R1) = R1 xor R2 + else if (false && re().is_intersection(r1, a1, a2) && re().is_intersection(r2, b1, b2) && + is_complement(a1, b2) && is_complement(a2, b1)) { + result = re().mk_xor(a1, re().mk_complement(a2)); + } + else if (false && re().is_intersection(r1, a1, a2) && re().is_intersection(r2, b1, b2) && + is_complement(a1, b1) && is_complement(a2, b2)) { + result = re().mk_xor(a1, re().mk_complement(a2)); + } else { // Range ∪ Range: [a,b] ∪ [c,d] = [min(a,c), max(b,d)] when overlapping or adjacent unsigned lo1_v = 0, hi1_v = 0, lo2_v = 0, hi2_v = 0; @@ -3348,17 +3357,7 @@ expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) { else result = merge_regex_sets(r1, r2, re().mk_full_seq(r1->get_sort()), test, compose); } - // (R1 \ R2) U (R2 \ R1) = R1 xor R2 - else if (false && re().is_intersection(r1, a1, a2) && re().is_intersection(r2, b1, b2) && - is_complement(a1, b2) && is_complement(a2, b1)) { - result = re().mk_xor(a1, re().mk_complement(a2)); - } - else if (false && re().is_intersection(r1, a1, a2) && re().is_intersection(r2, b1, b2) && - is_complement(a1, b1) && is_complement(a2, b2)) { - result = re().mk_xor(a1, re().mk_complement(a2)); - } - else - result = merge_regex_sets(r1, r2, re().mk_full_seq(r1->get_sort()), test, compose); + return result; } From 9091df56cbb91c668c6ef3e26899d2839d38e8a5 Mon Sep 17 00:00:00 2001 From: davedets Date: Tue, 16 Jun 2026 15:09:18 -0700 Subject: [PATCH 13/13] Fix instance of "flexible array member". (#9883) This is another PR towards the goal of getting a clean build with clang, using the compiler options used in building clang-tidy. In https://github.com/Z3Prover/z3/pull/9800, we changed the build flags to eliminate a warning for zero-length arrays. In that PR, I missed this one: there was one instance of m_arr[] instead of m_arr[0]. In the clang-tidy build, that gives warnings like: ``` /Users/daviddetlefs/llvm-project/build_dbg/_deps/z3-src/src/model/func_interp.h:43:12: warning: flexible array members are a C99 feature [-Wc99-extensions] ``` The PR fixes this, making it a zero-length array, the idiom used in all the other similar cases. I also added the compiler flag that produced this warning, so we can notice such changes in the future. --- src/model/func_interp.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/model/func_interp.h b/src/model/func_interp.h index e531e01cf..e3935e05e 100644 --- a/src/model/func_interp.h +++ b/src/model/func_interp.h @@ -40,7 +40,7 @@ class func_entry { // m_result and m_args[i] must be ground terms. expr * m_result; - expr * m_args[]; + expr * m_args[0]; static unsigned get_obj_size(unsigned arity) { return sizeof(func_entry) + arity * sizeof(expr*); } func_entry(ast_manager & m, unsigned arity, expr * const * args, expr * result);