fix not semantics

a16z · Sep 20, 2023 · 773000a · 773000a
1 parent b92172d
commit 773000a
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py
@@ -2489,7 +2489,7 @@ def run(self, ex0: Exec) -> Tuple[List[Exec], Steps]:
                 elif opcode in [EVM.AND, EVM.OR, EVM.XOR]:
                     ex.st.push(lop(opcode, ex.st.pop(), ex.st.pop()))
                 elif opcode == EVM.NOT:
-                    ex.st.push(~ex.st.pop())  # bvnot
+                    ex.st.push(~b2i(ex.st.pop()))  # bvnot
                 elif opcode == EVM.SHL:
                     w = ex.st.pop()
                     ex.st.push(b2i(ex.st.pop()) << b2i(w))  # bvshl