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/*" 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/ diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index b9aa9856e..5a6ce8ab9 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) 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)