diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index 7b8147bc..b80ad513 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -246,10 +246,6 @@ def wstore_partial( raise ValueError(data) -def is_byte(x: Any) -> bool: - return x in range(0, 256) or (is_bv(x) and eq(x.sort(), BitVecSort8)) - - def wstore_bytes( mem: List[UnionType[int, BitVecRef]], loc: int, size: int, arr: List[Byte] ) -> None: @@ -264,6 +260,15 @@ def wstore_bytes( mem[loc + i] = val +def is_byte(x: Any) -> bool: + if is_bv(x): + return eq(x.sort(), BitVecSort8) + elif isinstance(x, int): + return 0 <= x < 256 + else: + return False + + def normalize(expr: Any) -> Any: # Concat(Extract(255, 8, op(x, y)), op(Extract(7, 0, x), Extract(7, 0, y))) => op(x, y) def normalize_extract(arg0, arg1):