Fix div_xy_y(): resolving word as_z3

Author: sidarth16

.hypothesis/unicode_data/13.0.0/charmap.json.gz

@@ -2105,35 +2105,37 @@ def __init__(self, options: HalmosConfig, fun_info: FunctionInfo) -> None:
     def div_xy_y(self, w1: Word, w2: Word, signed: bool = False) -> Word:
         # return the number of bits required to represent the given value. default = 256
         def bitsize(w: Word) -> int:
+            z3w = w.as_z3() if hasattr(w, "as_z3") else w
             if (
-                w.decl().name() == "concat"
-                and is_bv_value(w.arg(0))
-                and int(str(w.arg(0))) == 0
+                z3w.decl().name() == "concat"
+                and is_bv_value(z3w.arg(0))
+                and int(str(z3w.arg(0))) == 0
             ):
-                return 256 - w.arg(0).size()
+                return 256 - z3w.arg(0).size()
             return 256
 
-        w1 = normalize(w1)
+        w1_z3 = w1.as_z3() if hasattr(w1, "as_z3") else w1
+        w2_z3 = w2.as_z3() if hasattr(w2, "as_z3") else w2
 
-        if w1.decl().name() == "bvmul" and w1.num_args() == 2:
-            x = w1.arg(0)
-            y = w1.arg(1)
-            if eq(w2, x) or eq(w2, y):  # xy/x or xy/y
+        if w1_z3.decl().name() == "bvmul" and w1_z3.num_args() == 2:
+            x = w1_z3.arg(0)
+            y = w1_z3.arg(1)
+            if eq(w2_z3, x) or eq(w2_z3, y):  # xy/x or xy/y
                 if signed:
                     # Signed division: safe to simplify if divisor exactly matches factor
-                    if eq(w2, x):
-                        return y
-                    elif eq(w2, y):
-                        return x
+                    if eq(w2_z3, x):
+                        return BV(y, w1.size)  # wrap back
+                    elif eq(w2_z3, y):
+                        return BV(x, w1.size)
                 else:
                     # Unsigned division: check for overflow
                     size_x = bitsize(x)
                     size_y = bitsize(y)
                     if size_x + size_y <= 256:
-                        if eq(w2, x):  # xy/x == y
-                            return y
+                        if eq(w2_z3, x):  # xy/x == y
+                            return BV(y, w1.size)  # wrap back
                         else:  # xy/y == x
-                            return x
+                            return BV(x, w1.size)
         return None
 
     def mk_div(self, ex: Exec, x: Any, y: Any) -> Any:
@@ -2178,7 +2180,7 @@ def arith(self, ex: Exec, op: int, w1: Word, w2: Word) -> Word:
             return term
 
         if op == OP_SDIV:
-            # Try signed simplification
+            # Try signed simplification first
             simplified_sdiv = self.div_xy_y(w1, w2, signed=True)
             if simplified_sdiv is not None:
                 return simplified_sdiv

src/halmos/sevm.py

@@ -0,0 +1,17 @@
+{
+  "../lib/forge-std": {
+    "rev": "1eea5bae12ae557d589f9f0f0edae2faa47cb262"
+  },
+  "../lib/halmos-cheatcodes": {
+    "rev": "6da4e692c357ba6d641a2e677a28298cac9f76ab"
+  },
+  "../lib/openzeppelin-contracts": {
+    "rev": "dbb6104ce834628e473d2173bbc9d47f81a9eec3"
+  },
+  "../lib/solady": {
+    "rev": "4d4a7572ad01e84e96370e42bd10d1cc16c1fb65"
+  },
+  "../lib/solmate": {
+    "rev": "bfc9c25865a274a7827fea5abf6e4fb64fc64e6c"
+  }
+}