From f2e7abbdc13182c3ba0898f8618659baaa50148a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 20 Oct 2025 08:28:08 +0200 Subject: [PATCH 1/4] disable manylinux until segfault is resolved Signed-off-by: Nikolaj Bjorner --- azure-pipelines.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 6368afdb4..0bf2aef61 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -66,6 +66,7 @@ jobs: pool: vmImage: "ubuntu-latest" container: "quay.io/pypa/manylinux2014_x86_64:latest" + condition: eq(0,1) steps: - script: curl -L -o /tmp/arm-toolchain.tar.xz 'https://developer.arm.com/-/media/Files/downloads/gnu/11.2-2022.02/binrel/gcc-arm-11.2-2022.02-x86_64-aarch64-none-linux-gnu.tar.xz?rev=33c6e30e5ac64e6dba8f0431f2c35f1b&hash=9918A05BF47621B632C7A5C8D2BB438FB80A4480' - script: mkdir -p /tmp/arm-toolchain/ From 06ed96dbda5ef3adc323ce2b4d3e5cfe13c1963a Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 20 Oct 2025 11:53:34 -0700 Subject: [PATCH 2/4] add the "noexcept" keyword to value_score=(value_score&&) declaration --- src/ast/sls/sls_bv_tracker.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/sls/sls_bv_tracker.h b/src/ast/sls/sls_bv_tracker.h index 37ef91480..5b228a36b 100644 --- a/src/ast/sls/sls_bv_tracker.h +++ b/src/ast/sls/sls_bv_tracker.h @@ -55,7 +55,7 @@ class sls_tracker { touched = other.touched; } ~value_score() { if (m) m->del(value); } - value_score& operator=(value_score&&) = default; + value_score& operator=(value_score&&) noexcept = default; value_score &operator=(const value_score &other) { if (this != &other) { if (m) From 9a2867aeb7eaefadce0792a4f54f9387a5f66aa2 Mon Sep 17 00:00:00 2001 From: Nelson Elhage Date: Tue, 21 Oct 2025 12:16:54 -0700 Subject: [PATCH 3/4] Add a fast-path to _coerce_exprs. (#7995) When the inputs are already the same sort, we can skip most of the coercion logic and just return. Currently, `_coerce_exprs` is by far the most expensive part of building up many common Z3 ASTs, so this fast-path is a substantial speedup for many use-cases. --- src/api/python/z3/z3.py | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 128726dae..df6230420 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1245,6 +1245,18 @@ def _coerce_expr_merge(s, a): else: return s +def _check_same_sort(a, b, ctx=None): + if not isinstance(a, ExprRef): + return False + if not isinstance(b, ExprRef): + return False + if ctx is None: + ctx = a.ctx + + a_sort = Z3_get_sort(ctx.ctx, a.ast) + b_sort = Z3_get_sort(ctx.ctx, b.ast) + return Z3_is_eq_sort(ctx.ctx, a_sort, b_sort) + def _coerce_exprs(a, b, ctx=None): if not is_expr(a) and not is_expr(b): @@ -1259,6 +1271,9 @@ def _coerce_exprs(a, b, ctx=None): if isinstance(b, float) and isinstance(a, ArithRef): b = RealVal(b, a.ctx) + if _check_same_sort(a, b, ctx): + return (a, b) + s = None s = _coerce_expr_merge(s, a) s = _coerce_expr_merge(s, b) From 68a7d1e1b1cbca5796e0cbf647d6a940b08b4cde Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Tue, 21 Oct 2025 21:17:35 +0200 Subject: [PATCH 4/4] Bump actions/setup-node from 5 to 6 (#7994) Bumps [actions/setup-node](https://github.com/actions/setup-node) from 5 to 6. - [Release notes](https://github.com/actions/setup-node/releases) - [Commits](https://github.com/actions/setup-node/compare/v5...v6) --- updated-dependencies: - dependency-name: actions/setup-node dependency-version: '6' dependency-type: direct:production update-type: version-update:semver-major ... Signed-off-by: dependabot[bot] Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> --- .github/workflows/wasm-release.yml | 2 +- .github/workflows/wasm.yml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/wasm-release.yml b/.github/workflows/wasm-release.yml index 5bb45bbb8..b2bba5126 100644 --- a/.github/workflows/wasm-release.yml +++ b/.github/workflows/wasm-release.yml @@ -24,7 +24,7 @@ jobs: uses: actions/checkout@v5 - name: Setup node - uses: actions/setup-node@v5 + uses: actions/setup-node@v6 with: node-version: "lts/*" registry-url: "https://registry.npmjs.org" diff --git a/.github/workflows/wasm.yml b/.github/workflows/wasm.yml index d32862f08..b95e86289 100644 --- a/.github/workflows/wasm.yml +++ b/.github/workflows/wasm.yml @@ -24,7 +24,7 @@ jobs: uses: actions/checkout@v5 - name: Setup node - uses: actions/setup-node@v5 + uses: actions/setup-node@v6 with: node-version: "lts/*"