From 890f4c762d745df507a6c72b7675002ef7153e63 Mon Sep 17 00:00:00 2001
From: Daejun Park <daejunpark@gmail.com>
Date: Fri, 10 Jan 2025 11:57:22 -0800
Subject: [PATCH] fix: hexify for extract and const terms

---
 src/halmos/utils.py | 8 +++++++-
 tests/test_cli.py   | 6 +++---
 2 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/src/halmos/utils.py b/src/halmos/utils.py
index 59e1a487..5b9e3326 100644
--- a/src/halmos/utils.py
+++ b/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)
 
diff --git a/tests/test_cli.py b/tests/test_cli.py
index 2a5b7f8b..559d1238 100644
--- a/tests/test_cli.py
+++ b/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)'