fix: hexify for extract and const terms

src/halmos/utils.py

@@ -31,6 +31,7 @@
     is_bool,
     is_bv,
     is_bv_value,
+    is_const,
     is_not,
     simplify,
     substitute,
@@ -454,7 +455,12 @@ def hexify(x, contract_name: str = None):
             f"0x{x.as_long():0{num_bytes * 2}x}", contract_name
         )
     elif is_app(x):
-        return f"{str(x.decl())}({', '.join(map(partial(hexify, contract_name=contract_name), x.children()))})"
+        params_and_children = (
+            f"({', '.join(map(partial(hexify, contract_name=contract_name), x.params() + x.children()))})"
+            if not is_const(x)
+            else ""
+        )
+        return f"{str(x.decl())}{params_and_children}"
     else:
         return hexify(str(x), contract_name)
 

tests/test_cli.py

@@ -101,7 +101,7 @@ def test_decode_mixed_bytecode():
     )
 
     disassembly = " ".join([str(insn) for insn in insns])
-    assert disassembly == "PUSH20 x() PUSH0 MSTORE PUSH1 0x14 PUSH1 0x0c RETURN"
+    assert disassembly == "PUSH20 x PUSH0 MSTORE PUSH1 0x14 PUSH1 0x0c RETURN"
 
     # jump destination scanning
     assert contract.valid_jump_destinations() == set()
@@ -141,7 +141,7 @@ def test_decode_hex():
 def test_decode():
     code = Contract(Concat(BitVecVal(EVM.PUSH32, 8), BitVec("x", 256)))
     assert len(code) == 33
-    assert str(code.decode_instruction(0)) == "PUSH32 x()"
+    assert str(code.decode_instruction(0)) == "PUSH32 x"
     assert str(code.decode_instruction(33)) == "STOP"
 
     code = Contract(BitVec("x", 256))
@@ -150,7 +150,7 @@ def test_decode():
 
     code = Contract(Concat(BitVecVal(EVM.PUSH3, 8), BitVec("x", 16)))
     assert (
-        str(code.decode_instruction(0)) == "PUSH3 Concat(x(), 0x00)"
+        str(code.decode_instruction(0)) == "PUSH3 Concat(x, 0x00)"
     )  # 'PUSH3 ERROR x (1 bytes missed)'