Merge branch 'Z3Prover:master' into param-tuning

.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"

.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/*"
 

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/

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)

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)