diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py
index e4457e2e..de8c728d 100644
--- a/src/halmos/sevm.py
+++ b/src/halmos/sevm.py
@@ -22,7 +22,7 @@
     hexify,
 )
 from .cheatcodes import halmos_cheat_code, hevm_cheat_code, console, Prank
-from .warnings import warn, UNSUPPORTED_OPCODE
+from .warnings import warn, UNSUPPORTED_OPCODE, LIBRARY_PLACEHOLDER
 
 Word = Any  # z3 expression (including constants)
 Byte = Any  # z3 expression (including constants)
@@ -501,7 +501,13 @@ def from_hexcode(hexcode: str):
         if hexcode.startswith("0x"):
             hexcode = hexcode[2:]
 
-        return Contract(bytes.fromhex(hexcode))
+        if "__" in hexcode:
+            warn(LIBRARY_PLACEHOLDER, f"contract hexcode contains library placeholder")
+
+        try:
+            return Contract(bytes.fromhex(hexcode))
+        except ValueError as e:
+            raise ValueError(f"{e} (hexcode={hexcode})")
 
     def decode_instruction(self, pc: int) -> Instruction:
         opcode = int_of(self[pc])
diff --git a/src/halmos/warnings.py b/src/halmos/warnings.py
index c3b99a73..0a4ea7c7 100644
--- a/src/halmos/warnings.py
+++ b/src/halmos/warnings.py
@@ -22,6 +22,7 @@ def url(self) -> str:
 COUNTEREXAMPLE_UNKNOWN = ErrorCode("counterexample-unknown")
 INTERNAL_ERROR = ErrorCode("internal-error")
 UNSUPPORTED_OPCODE = ErrorCode("unsupported-opcode")
+LIBRARY_PLACEHOLDER = ErrorCode("library-placeholder")
 
 LOOP_BOUND = ErrorCode("loop-bound")