diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py
index cc9ce3a5..4809f004 100644
--- a/src/halmos/__main__.py
+++ b/src/halmos/__main__.py
@@ -18,6 +18,7 @@
 from .utils import (
     create_solver,
     hexify,
+    stringify,
     indent_text,
     NamedTimer,
     yellow,
@@ -1066,14 +1067,14 @@ def select(var):
         return name.startswith("p_") or name.startswith("halmos_")
 
     select_model = filter(select, model) if not print_full_model else model
-    return {str(decl): hexify(model[decl]) for decl in select_model}
+    return {str(decl): stringify(str(decl), model[decl]) for decl in select_model}
 
 
 def render_model(model: UnionType[str, StrModel]) -> str:
     if isinstance(model, str):
         return model
 
-    formatted = [f"\n    {decl} = {hexify(val)}" for decl, val in model.items()]
+    formatted = [f"\n    {decl} = {val}" for decl, val in model.items()]
     return "".join(sorted(formatted)) if formatted else "∅"
 
 
diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py
index a81e20f4..15bafa1e 100644
--- a/src/halmos/cheatcodes.py
+++ b/src/halmos/cheatcodes.py
@@ -1,10 +1,69 @@
 # SPDX-License-Identifier: AGPL-3.0
 
+import json
+import re
+
+from subprocess import Popen, PIPE
 from typing import List, Dict, Set, Tuple, Any
 
 from z3 import *
 
-from .utils import assert_address, con_addr
+from .exceptions import FailCheatcode, HalmosException
+from .utils import *
+from .warnings import (
+    INTERNAL_ERROR,
+    warn,
+)
+
+
+def name_of(x: str) -> str:
+    return re.sub(r"\s+", "_", x)
+
+
+def extract_string_array_argument(calldata: BitVecRef, arg_idx: int):
+    """Extracts idx-th argument of string array from calldata"""
+
+    array_slot = int_of(extract_bytes(calldata, 4 + 32 * arg_idx, 32))
+    num_strings = int_of(extract_bytes(calldata, 4 + array_slot, 32))
+
+    string_array = []
+
+    for i in range(num_strings):
+        string_offset = int_of(
+            extract_bytes(calldata, 4 + array_slot + 32 * (i + 1), 32)
+        )
+        string_length = int_of(
+            extract_bytes(calldata, 4 + array_slot + 32 + string_offset, 32)
+        )
+        string_value = int_of(
+            extract_bytes(
+                calldata, 4 + array_slot + 32 + string_offset + 32, string_length
+            )
+        )
+        string_bytes = string_value.to_bytes(string_length, "big")
+        string_array.append(string_bytes.decode("utf-8"))
+
+    return string_array
+
+
+def stringified_bytes_to_bytes(string_bytes: str):
+    """Converts a string of bytes to a bytes memory type"""
+
+    string_bytes_len = (len(string_bytes) + 1) // 2
+    string_bytes_len_enc = hex(string_bytes_len).replace("0x", "").rjust(64, "0")
+
+    string_bytes_len_ceil = (string_bytes_len + 31) // 32 * 32
+
+    ret_bytes = (
+        "00" * 31
+        + "20"
+        + string_bytes_len_enc
+        + string_bytes.ljust(string_bytes_len_ceil * 2, "0")
+    )
+    ret_len = len(ret_bytes) // 2
+    ret_bytes = bytes.fromhex(ret_bytes)
+
+    return BitVecVal(int.from_bytes(ret_bytes, "big"), ret_len * 8)
 
 
 class Prank:
@@ -20,9 +79,9 @@ def __init__(self, addr: Any = None, keep: bool = False) -> None:
     def __str__(self) -> str:
         if self.addr:
             if self.keep:
-                return f"startPrank({str(addr)})"
+                return f"startPrank({str(self.addr)})"
             else:
-                return f"prank({str(addr)})"
+                return f"prank({str(self.addr)})"
         else:
             return "None"
 
@@ -63,28 +122,107 @@ def stopPrank(self) -> bool:
         return True
 
 
-class halmos_cheat_code:
-    # address constant SVM_ADDRESS =
-    #     address(bytes20(uint160(uint256(keccak256('svm cheat code')))));
-    address: BitVecRef = con_addr(0xF3993A62377BCD56AE39D773740A5390411E8BC9)
+def create_generic(ex, bits: int, var_name: str, type_name: str) -> BitVecRef:
+    label = f"halmos_{var_name}_{type_name}_{ex.new_symbol_id():>02}"
+    return BitVec(label, BitVecSorts[bits])
+
 
-    # bytes4(keccak256("createUint(uint256,string)"))
-    create_uint: int = 0x66830DFA
+def create_uint(ex, arg):
+    bits = int_of(
+        extract_bytes(arg, 4, 32), "symbolic bit size for halmos.createUint()"
+    )
+    if bits > 256:
+        raise HalmosException(f"bitsize larger than 256: {bits}")
 
-    # bytes4(keccak256("createBytes(uint256,string)"))
-    create_bytes: int = 0xEEF5311D
+    name = name_of(extract_string_argument(arg, 1))
+    return uint256(create_generic(ex, bits, name, f"uint{bits}"))
 
-    # bytes4(keccak256("createUint256(string)"))
-    create_uint256: int = 0xBC7BEEFC
 
-    # bytes4(keccak256("createBytes32(string)"))
-    create_bytes32: int = 0xBF72FA66
+def create_uint256(ex, arg):
+    name = name_of(extract_string_argument(arg, 0))
+    return create_generic(ex, 256, name, "uint256")
 
-    # bytes4(keccak256("createAddress(string)"))
-    create_address: int = 0x3B0FA01B
 
-    # bytes4(keccak256("createBool(string)"))
-    create_bool: int = 0x6E0BB659
+def create_int(ex, arg):
+    bits = int_of(
+        extract_bytes(arg, 4, 32), "symbolic bit size for halmos.createUint()"
+    )
+    if bits > 256:
+        raise HalmosException(f"bitsize larger than 256: {bits}")
+
+    name = name_of(extract_string_argument(arg, 1))
+    return int256(create_generic(ex, bits, name, f"int{bits}"))
+
+
+def create_int256(ex, arg):
+    name = name_of(extract_string_argument(arg, 0))
+    return create_generic(ex, 256, name, "int256")
+
+
+def create_bytes(ex, arg):
+    byte_size = int_of(
+        extract_bytes(arg, 4, 32), "symbolic byte size for halmos.createBytes()"
+    )
+    name = name_of(extract_string_argument(arg, 1))
+    symbolic_bytes = create_generic(ex, byte_size * 8, name, "bytes")
+    return Concat(con(32), con(byte_size), symbolic_bytes)
+
+
+def create_string(ex, arg):
+    byte_size = int_of(
+        extract_bytes(arg, 4, 32), "symbolic byte size for halmos.createString()"
+    )
+    name = name_of(extract_string_argument(arg, 1))
+    symbolic_string = create_generic(ex, byte_size * 8, name, "string")
+    return Concat(con(32), con(byte_size), symbolic_string)
+
+
+def create_bytes4(ex, arg):
+    name = name_of(extract_string_argument(arg, 0))
+    return uint256(create_generic(ex, 32, name, "bytes4"))
+
+
+def create_bytes32(ex, arg):
+    name = name_of(extract_string_argument(arg, 0))
+    return create_generic(ex, 256, name, "bytes32")
+
+
+def create_address(ex, arg):
+    name = name_of(extract_string_argument(arg, 0))
+    return uint256(create_generic(ex, 160, name, "address"))
+
+
+def create_bool(ex, arg):
+    name = name_of(extract_string_argument(arg, 0))
+    return uint256(create_generic(ex, 1, name, "bool"))
+
+
+class halmos_cheat_code:
+    # address constant SVM_ADDRESS =
+    #     address(bytes20(uint160(uint256(keccak256('svm cheat code')))));
+    address: BitVecRef = con_addr(0xF3993A62377BCD56AE39D773740A5390411E8BC9)
+
+    handlers = {
+        0x66830DFA: create_uint,  # createUint(uint256,string)
+        0xBC7BEEFC: create_uint256,  # createUint256(string)
+        0x49B9C7D4: create_int,  # createInt(uint256,string)
+        0xC2CE6AED: create_int256,  # createInt256(string)
+        0xEEF5311D: create_bytes,  # createBytes(uint256,string)
+        0xCE68656C: create_string,  # createString(uint256,string)
+        0xDE143925: create_bytes4,  # createBytes4(string)
+        0xBF72FA66: create_bytes32,  # createBytes32(string)
+        0x3B0FA01B: create_address,  # createAddress(string)
+        0x6E0BB659: create_bool,  # createBool(string)
+    }
+
+    @staticmethod
+    def handle(ex, arg: BitVecRef) -> BitVecRef:
+        funsig = int_of(extract_funsig(arg), "symbolic halmos cheatcode")
+        if handler := halmos_cheat_code.handlers.get(funsig):
+            return handler(ex, arg)
+
+        error_msg = f"Unknown halmos cheat code: function selector = 0x{funsig:0>8x}, calldata = {hexify(arg)}"
+        raise HalmosException(error_msg)
 
 
 class hevm_cheat_code:
@@ -154,11 +292,160 @@ class hevm_cheat_code:
     # bytes4(keccak256("ffi(string[])"))
     ffi_sig: int = 0x89160467
 
+    @staticmethod
+    def handle(sevm, ex, arg: BitVec) -> BitVec:
+        funsig: int = int_of(extract_funsig(arg), "symbolic hevm cheatcode")
+
+        # vm.fail()
+        # BitVecVal(hevm_cheat_code.fail_payload, 800)
+        if arg == hevm_cheat_code.fail_payload:
+            raise FailCheatcode()
+
+        # vm.assume(bool)
+        elif (
+            eq(arg.sort(), BitVecSorts[(4 + 32) * 8])
+            and funsig == hevm_cheat_code.assume_sig
+        ):
+            assume_cond = simplify(is_non_zero(Extract(255, 0, arg)))
+            ex.solver.add(assume_cond)
+            ex.path.append(str(assume_cond))
+
+        # vm.getCode(string)
+        elif funsig == hevm_cheat_code.get_code_sig:
+            calldata = bytes.fromhex(hex(arg.as_long())[2:])
+            path_len = int.from_bytes(calldata[36:68], "big")
+            path = calldata[68 : 68 + path_len].decode("utf-8")
+
+            if ":" in path:
+                [filename, contract_name] = path.split(":")
+                path = "out/" + filename + "/" + contract_name + ".json"
 
-class console:
-    # address constant CONSOLE_ADDRESS = address(0x000000000000000000636F6e736F6c652e6c6f67);
-    address: BitVecRef = con_addr(0x000000000000000000636F6E736F6C652E6C6F67)
+            target = sevm.options["target"].rstrip("/")
+            path = target + "/" + path
 
-    log_uint256: int = 0xF82C50F1  # bytes4(keccak256("log(uint256)"))
+            with open(path) as f:
+                artifact = json.loads(f.read())
 
-    log_string: int = 0x41304FAC  # bytes4(keccak256("log(string)"))
+            if artifact["bytecode"]["object"]:
+                bytecode = artifact["bytecode"]["object"].replace("0x", "")
+            else:
+                bytecode = artifact["bytecode"].replace("0x", "")
+
+            return stringified_bytes_to_bytes(bytecode)
+
+        # vm.prank(address)
+        elif funsig == hevm_cheat_code.prank_sig:
+            result = ex.prank.prank(uint160(Extract(255, 0, arg)))
+            if not result:
+                raise HalmosException("You have an active prank already.")
+
+        # vm.startPrank(address)
+        elif funsig == hevm_cheat_code.start_prank_sig:
+            result = ex.prank.startPrank(uint160(Extract(255, 0, arg)))
+            if not result:
+                raise HalmosException("You have an active prank already.")
+
+        # vm.stopPrank()
+        elif funsig == hevm_cheat_code.stop_prank_sig:
+            ex.prank.stopPrank()
+
+        # vm.deal(address,uint256)
+        elif funsig == hevm_cheat_code.deal_sig:
+            who = uint160(Extract(511, 256, arg))
+            amount = simplify(Extract(255, 0, arg))
+            ex.balance_update(who, amount)
+
+        # vm.store(address,bytes32,bytes32)
+        elif funsig == hevm_cheat_code.store_sig:
+            store_account = uint160(Extract(767, 512, arg))
+            store_slot = simplify(Extract(511, 256, arg))
+            store_value = simplify(Extract(255, 0, arg))
+            store_account_addr = sevm.resolve_address_alias(ex, store_account)
+            if store_account_addr is not None:
+                sevm.sstore(ex, store_account_addr, store_slot, store_value)
+            else:
+                raise HalmosException(f"uninitialized account: {store_account}")
+
+        # vm.load(address,bytes32)
+        elif funsig == hevm_cheat_code.load_sig:
+            load_account = uint160(Extract(511, 256, arg))
+            load_slot = simplify(Extract(255, 0, arg))
+            load_account_addr = sevm.resolve_address_alias(ex, load_account)
+            if load_account_addr is not None:
+                return sevm.sload(ex, load_account_addr, load_slot)
+            else:
+                raise HalmosException(f"uninitialized account: {store_account}")
+
+        # vm.fee(uint256)
+        elif funsig == hevm_cheat_code.fee_sig:
+            ex.block.basefee = simplify(Extract(255, 0, arg))
+
+        # vm.chainId(uint256)
+        elif funsig == hevm_cheat_code.chainid_sig:
+            ex.block.chainid = simplify(Extract(255, 0, arg))
+
+        # vm.coinbase(address)
+        elif funsig == hevm_cheat_code.coinbase_sig:
+            ex.block.coinbase = uint160(Extract(255, 0, arg))
+
+        # vm.difficulty(uint256)
+        elif funsig == hevm_cheat_code.difficulty_sig:
+            ex.block.difficulty = simplify(Extract(255, 0, arg))
+
+        # vm.roll(uint256)
+        elif funsig == hevm_cheat_code.roll_sig:
+            ex.block.number = simplify(Extract(255, 0, arg))
+
+        # vm.warp(uint256)
+        elif funsig == hevm_cheat_code.warp_sig:
+            ex.block.timestamp = simplify(Extract(255, 0, arg))
+
+        # vm.etch(address,bytes)
+        elif funsig == hevm_cheat_code.etch_sig:
+            who = extract_bytes(arg, 4 + 12, 20)
+
+            # who must be concrete
+            if not is_bv_value(who):
+                error_msg = f"vm.etch(address who, bytes code) must have concrete argument `who` but received {who}"
+                raise HalmosException(error_msg)
+
+            # code must be concrete
+            try:
+                code_offset = int_of(extract_bytes(arg, 4 + 32, 32))
+                code_length = int_of(extract_bytes(arg, 4 + code_offset, 32))
+                code_int = int_of(extract_bytes(arg, 4 + code_offset + 32, code_length))
+                code_bytes = code_int.to_bytes(code_length, "big")
+                ex.set_code(who, code_bytes)
+            except Exception as e:
+                error_msg = f"vm.etch(address who, bytes code) must have concrete argument `code` but received calldata {arg}"
+                raise HalmosException(error_msg) from e
+
+        # ffi(string[]) returns (bytes)
+        elif funsig == hevm_cheat_code.ffi_sig:
+            if not sevm.options.get("ffi"):
+                error_msg = "ffi cheatcode is disabled. Run again with `--ffi` if you want to enable it"
+                raise HalmosException(error_msg)
+            cmd = extract_string_array_argument(arg, 0)
+            process = Popen(cmd, stdout=PIPE, stderr=PIPE)
+
+            (stdout, stderr) = process.communicate()
+
+            if stderr:
+                warn(
+                    INTERNAL_ERROR,
+                    f"An exception has occurred during the usage of the ffi cheatcode:\n{stderr.decode('utf-8')}",
+                )
+
+            out_bytes = stdout.decode("utf-8")
+
+            if not out_bytes.startswith("0x"):
+                out_bytes = out_bytes.strip().encode("utf-8").hex()
+            else:
+                out_bytes = out_bytes.strip().replace("0x", "")
+
+            return stringified_bytes_to_bytes(out_bytes)
+
+        else:
+            # TODO: support other cheat codes
+            msg = f"Unsupported cheat code: calldata = {hexify(arg)}"
+            raise HalmosException(msg)
diff --git a/src/halmos/console.py b/src/halmos/console.py
new file mode 100644
index 00000000..1fa0ed27
--- /dev/null
+++ b/src/halmos/console.py
@@ -0,0 +1,111 @@
+from z3 import BitVecRef
+
+from .utils import *
+
+
+def log_uint256(arg: BitVec) -> None:
+    b = extract_bytes(arg, 4, 32)
+    console.log(render_uint(b))
+
+
+def log_string(arg: BitVec) -> None:
+    str_val = extract_string_argument(arg, 0)
+    console.log(str_val)
+
+
+def log_bytes(arg: BitVec) -> None:
+    b = extract_bytes_argument(arg, 0)
+    console.log(render_bytes(b))
+
+
+def log_string_address(arg: BitVec) -> None:
+    str_val = extract_string_argument(arg, 0)
+    addr = extract_bytes(arg, 36, 32)
+    console.log(f"{str_val} {render_address(addr)}")
+
+
+def log_address(arg: BitVec) -> None:
+    addr = extract_bytes(arg, 4, 32)
+    console.log(render_address(addr))
+
+
+def log_string_bool(arg: BitVec) -> None:
+    str_val = extract_string_argument(arg, 0)
+    bool_val = extract_bytes(arg, 36, 32)
+    console.log(f"{str_val} {render_bool(bool_val)}")
+
+
+def log_bool(arg: BitVec) -> None:
+    bool_val = extract_bytes(arg, 4, 32)
+    console.log(render_bool(bool_val))
+
+
+def log_string_string(arg: BitVec) -> None:
+    str1_val = extract_string_argument(arg, 0)
+    str2_val = extract_string_argument(arg, 1)
+    console.log(f"{str1_val} {str2_val}")
+
+
+def log_bytes32(arg: BitVec) -> None:
+    b = extract_bytes(arg, 4, 32)
+    console.log(hexify(b))
+
+
+def log_string_int256(arg: BitVec) -> None:
+    str_val = extract_string_argument(arg, 0)
+    int_val = extract_bytes(arg, 36, 32)
+    console.log(f"{str_val} {render_int(int_val)}")
+
+
+def log_int256(arg: BitVec) -> None:
+    int_val = extract_bytes(arg, 4, 32)
+    console.log(render_int(int_val))
+
+
+def log_string_uint256(arg: BitVec) -> None:
+    str_val = extract_string_argument(arg, 0)
+    uint_val = extract_bytes(arg, 36, 32)
+    console.log(f"{str_val} {render_uint(uint_val)}")
+
+
+class console:
+    # see forge-std/console2.sol
+    address: BitVecRef = con_addr(0x000000000000000000636F6E736F6C652E6C6F67)
+
+    handlers = {
+        0xF82C50F1: log_uint256,
+        0xF5B1BBA9: log_uint256,  # alias for 'log(uint)'
+        0x41304FAC: log_string,
+        0x0BE77F56: log_bytes,
+        0x319AF333: log_string_address,
+        0x2C2ECBC2: log_address,
+        0xC3B55635: log_string_bool,
+        0x32458EED: log_bool,
+        0x4B5C4277: log_string_string,
+        0x27B7CF85: log_bytes32,
+        0x3CA6268E: log_string_int256,
+        0x2D5B6CB9: log_int256,
+        0xB60E72CC: log_string_uint256,
+    }
+
+    @staticmethod
+    def log(what: str) -> None:
+        print(f"[console.log] {magenta(what)}")
+
+    @staticmethod
+    def handle(ex, arg: BitVec) -> None:
+        try:
+            funsig: int = int_of(
+                extract_funsig(arg), "symbolic console function selector"
+            )
+
+            if handler := console.handlers.get(funsig):
+                return handler(arg)
+
+            info(
+                f"Unsupported console function: selector = 0x{funsig:0>8x}, "
+                f"calldata = {hexify(arg)}"
+            )
+        except Exception as e:
+            # we don't want to fail execution because of an issue during console.log
+            warn(f"console.handle: {repr(e)} with arg={hexify(arg)}")
diff --git a/src/halmos/exceptions.py b/src/halmos/exceptions.py
index 4110ebe1..a8982f6e 100644
--- a/src/halmos/exceptions.py
+++ b/src/halmos/exceptions.py
@@ -8,6 +8,14 @@
 """
 
 
+class HalmosException(Exception):
+    pass
+
+
+class NotConcreteError(HalmosException):
+    pass
+
+
 class EvmException(Exception):
     """
     Base class for all EVM exceptions.
diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py
index d50c3fe6..a00b76a8 100644
--- a/src/halmos/sevm.py
+++ b/src/halmos/sevm.py
@@ -8,7 +8,6 @@
 from collections import defaultdict
 from dataclasses import dataclass, field
 from functools import reduce
-from subprocess import Popen, PIPE
 from typing import (
     Any,
     Dict,
@@ -23,33 +22,16 @@
 )
 from z3 import *
 
-from .cheatcodes import halmos_cheat_code, hevm_cheat_code, console, Prank
+from .cheatcodes import halmos_cheat_code, hevm_cheat_code, Prank
+from .console import console
 from .exceptions import *
-from .utils import (
-    create_solver,
-    EVM,
-    sha3_inv,
-    restore_precomputed_hashes,
-    str_opcode,
-    assert_address,
-    assert_uint256,
-    con_addr,
-    bv_value_to_bytes,
-    hexify,
-    color_info,
-)
+from .utils import *
 from .warnings import (
     warn,
-    UNSUPPORTED_OPCODE,
     LIBRARY_PLACEHOLDER,
-    UNINTERPRETED_UNKNOWN_CALLS,
     INTERNAL_ERROR,
 )
 
-Word = Any  # z3 expression (including constants)
-Byte = Any  # z3 expression (including constants)
-Bytes = Any  # z3 expression (including constants)
-Address = BitVecRef  # 160-bitvector
 
 Steps = Dict[int, Dict[str, Any]]  # execution tree
 
@@ -57,44 +39,6 @@
 MAX_CALL_DEPTH = 1024
 
 
-# dynamic BitVecSort sizes
-class BitVecSortCache:
-    def __init__(self):
-        self.cache = {}
-        for size in (
-            1,
-            8,
-            16,
-            32,
-            64,
-            128,
-            160,
-            256,
-            264,
-            288,
-            512,
-            544,
-            800,
-            1024,
-            1056,
-        ):
-            self.cache[size] = BitVecSort(size)
-
-    def __getitem__(self, size: int) -> BitVecSort:
-        hit = self.cache.get(size)
-        return hit if hit is not None else BitVecSort(size)
-
-
-BitVecSorts = BitVecSortCache()
-
-# known, fixed BitVecSort sizes
-BitVecSort1 = BitVecSorts[1]
-BitVecSort8 = BitVecSorts[8]
-BitVecSort160 = BitVecSorts[160]
-BitVecSort256 = BitVecSorts[256]
-BitVecSort264 = BitVecSorts[264]
-BitVecSort512 = BitVecSorts[512]
-
 # symbolic states
 # calldataload(index)
 f_calldataload = Function("calldataload", BitVecSort256, BitVecSort256)
@@ -165,22 +109,10 @@ def __len__(self) -> int:
         return instruction_length(self.opcode)
 
 
-class HalmosException(Exception):
-    pass
-
-
-class NotConcreteError(HalmosException):
-    pass
-
-
 def id_str(x: Any) -> str:
     return hexify(x).replace(" ", "")
 
 
-def name_of(x: str) -> str:
-    return re.sub(r"\s+", "_", x)
-
-
 def padded_slice(lst: List, start: int, size: int, default=0) -> List:
     """
     Return a slice of lst, starting at start and with size elements. If the slice
@@ -192,26 +124,6 @@ def padded_slice(lst: List, start: int, size: int, default=0) -> List:
     return [lst[i] if i < n else default for i in range(start, end)]
 
 
-def unbox_int(x: Any) -> Any:
-    """Convert int-like objects to int"""
-    if isinstance(x, bytes):
-        return int.from_bytes(x, "big")
-
-    if is_bv_value(x):
-        return x.as_long()
-
-    return x
-
-
-def int_of(x: Any, err: str = "expected concrete value but got") -> int:
-    res = unbox_int(x)
-
-    if isinstance(res, int):
-        return res
-
-    raise NotConcreteError(f"{err}: {x}")
-
-
 def iter_bytes(x: Any, _byte_length: int = -1):
     """Return an iterable over the bytes of x (concrete or symbolic)"""
 
@@ -251,50 +163,6 @@ def mnemonic(opcode) -> str:
         return str(opcode)
 
 
-def concat(args):
-    if len(args) > 1:
-        return Concat(args)
-    else:
-        return args[0]
-
-
-def uint256(x: BitVecRef) -> BitVecRef:
-    bitsize = x.size()
-    if bitsize > 256:
-        raise ValueError(x)
-    if bitsize == 256:
-        return x
-    return simplify(ZeroExt(256 - bitsize, x))
-
-
-def uint160(x: BitVecRef) -> BitVecRef:
-    bitsize = x.size()
-    if bitsize > 256:
-        raise ValueError(x)
-    if bitsize == 160:
-        return x
-    if bitsize > 160:
-        return simplify(Extract(159, 0, x))
-    else:
-        return simplify(ZeroExt(160 - bitsize, x))
-
-
-def con(n: int, size_bits=256) -> Word:
-    return BitVecVal(n, BitVecSorts[size_bits])
-
-
-def byte_length(x: Any) -> int:
-    if is_bv(x):
-        if x.size() % 8 != 0:
-            raise ValueError(x)
-        return x.size() >> 3
-
-    if isinstance(x, bytes):
-        return len(x)
-
-    raise ValueError(x)
-
-
 def instruction_length(opcode: Any) -> int:
     opcode = int_of(opcode)
     return (opcode - EVM.PUSH0 + 1) if EVM.PUSH1 <= opcode <= EVM.PUSH32 else 1
@@ -389,99 +257,6 @@ def wstore_bytes(
         mem[loc + i] = arr[i]
 
 
-def extract_bytes(data: BitVecRef, byte_offset: int, size_bytes: int) -> BitVecRef:
-    """Extract bytes from calldata. Zero-pad if out of bounds."""
-    n = data.size()
-    if n % 8 != 0:
-        raise ValueError(n)
-
-    # will extract hi - lo + 1 bits
-    hi = n - 1 - byte_offset * 8
-    lo = n - byte_offset * 8 - size_bytes * 8
-    lo = 0 if lo < 0 else lo
-
-    val = simplify(Extract(hi, lo, data))
-
-    zero_padding = size_bytes * 8 - val.size()
-    if zero_padding < 0:
-        raise ValueError(val)
-    if zero_padding > 0:
-        val = simplify(Concat(val, con(0, zero_padding)))
-
-    return val
-
-
-def extract_funsig(calldata: BitVecRef):
-    """Extracts the function signature (first 4 bytes) from calldata"""
-    return extract_bytes(calldata, 0, 4)
-
-
-def extract_string_argument(calldata: BitVecRef, arg_idx: int):
-    """Extracts idx-th argument of string from calldata"""
-    string_offset = int_of(
-        extract_bytes(calldata, 4 + arg_idx * 32, 32),
-        "symbolic offset for string argument",
-    )
-    string_length = int_of(
-        extract_bytes(calldata, 4 + string_offset, 32),
-        "symbolic size for string argument",
-    )
-    if string_length == 0:
-        return ""
-    string_value = int_of(
-        extract_bytes(calldata, 4 + string_offset + 32, string_length),
-        "symbolic string argument",
-    )
-    string_bytes = string_value.to_bytes(string_length, "big")
-    return string_bytes.decode("utf-8")
-
-
-def extract_string_array_argument(calldata: BitVecRef, arg_idx: int):
-    """Extracts idx-th argument of string array from calldata"""
-
-    array_slot = int_of(extract_bytes(calldata, 4 + 32 * arg_idx, 32))
-    num_strings = int_of(extract_bytes(calldata, 4 + array_slot, 32))
-
-    string_array = []
-
-    for i in range(num_strings):
-        string_offset = int_of(
-            extract_bytes(calldata, 4 + array_slot + 32 * (i + 1), 32)
-        )
-        string_length = int_of(
-            extract_bytes(calldata, 4 + array_slot + 32 + string_offset, 32)
-        )
-        string_value = int_of(
-            extract_bytes(
-                calldata, 4 + array_slot + 32 + string_offset + 32, string_length
-            )
-        )
-        string_bytes = string_value.to_bytes(string_length, "big")
-        string_array.append(string_bytes.decode("utf-8"))
-
-    return string_array
-
-
-def stringified_bytes_to_bytes(string_bytes: str):
-    """Converts a string of bytes to a bytes memory type"""
-
-    string_bytes_len = (len(string_bytes) + 1) // 2
-    string_bytes_len_enc = hex(string_bytes_len).replace("0x", "").rjust(64, "0")
-
-    string_bytes_len_ceil = (string_bytes_len + 31) // 32 * 32
-
-    ret_bytes = (
-        "00" * 31
-        + "20"
-        + string_bytes_len_enc
-        + string_bytes.ljust(string_bytes_len_ceil * 2, "0")
-    )
-    ret_len = len(ret_bytes) // 2
-    ret_bytes = bytes.fromhex(ret_bytes)
-
-    return BitVecVal(int.from_bytes(ret_bytes, "big"), ret_len * 8)
-
-
 @dataclass(frozen=True)
 class EventLog:
     """
@@ -914,6 +689,15 @@ def current_opcode(self) -> UnionType[int, BitVecRef]:
     def current_instruction(self) -> Instruction:
         return self.pgm.decode_instruction(self.pc)
 
+    def set_code(
+        self, who: Address, code: UnionType[bytes, BitVecRef, Contract]
+    ) -> None:
+        """
+        Sets the code at a given address.
+        """
+        assert_address(who)
+        self.code[who] = code if isinstance(code, Contract) else Contract(code)
+
     def str_cnts(self) -> str:
         return "".join(
             [
@@ -1356,31 +1140,6 @@ def add_all(cls, args: List) -> BitVecRef:
 SomeStorage = TypeVar("SomeStorage", bound=Storage)
 
 
-#             x  == b   if sort(x) = bool
-# int_to_bool(x) == b   if sort(x) = int
-def test(x: Word, b: bool) -> Word:
-    if is_bool(x):
-        if b:
-            return x
-        else:
-            return Not(x)
-    elif is_bv(x):
-        if b:
-            return x != con(0)
-        else:
-            return x == con(0)
-    else:
-        raise ValueError(x)
-
-
-def is_non_zero(x: Word) -> Word:
-    return test(x, True)
-
-
-def is_zero(x: Word) -> Word:
-    return test(x, False)
-
-
 def bitwise(op, x: Word, y: Word) -> Word:
     if is_bool(x) and is_bool(y):
         if op == EVM.AND:
@@ -1883,282 +1642,20 @@ def call_unknown() -> None:
                 ex.solver.add(exit_code_var != con(0))
                 ret = arg
 
-            # TODO: factor out cheatcode semantics
             # halmos cheat code
             if eq(to, halmos_cheat_code.address):
                 ex.solver.add(exit_code_var != con(0))
-
-                funsig: int = int_of(
-                    extract_funsig(arg), "symbolic halmos cheatcode function selector"
-                )
-
-                if self.options.get("debug"):
-                    print(f"Executing halmos cheat code: {hex(funsig)}")
-
-                # createUint(uint256,string) returns (uint256)
-                if funsig == halmos_cheat_code.create_uint:
-                    bit_size = int_of(
-                        extract_bytes(arg, 4, 32),
-                        "symbolic bit size for halmos.createUint()",
-                    )
-                    name = name_of(extract_string_argument(arg, 1))
-                    if bit_size <= 256:
-                        label = f"halmos_{name}_uint{bit_size}_{ex.new_symbol_id():>02}"
-                        ret = uint256(BitVec(label, BitVecSorts[bit_size]))
-                    else:
-                        raise HalmosException(f"bitsize larger than 256: {bit_size}")
-
-                # createBytes(uint256,string) returns (bytes)
-                elif funsig == halmos_cheat_code.create_bytes:
-                    byte_size = int_of(
-                        extract_bytes(arg, 4, 32),
-                        "symbolic byte size for halmos.createBytes()",
-                    )
-                    name = name_of(extract_string_argument(arg, 1))
-                    label = f"halmos_{name}_bytes_{ex.new_symbol_id():>02}"
-                    symbolic_bytes = BitVec(label, BitVecSorts[byte_size * 8])
-                    ret = Concat(con(32), con(byte_size), symbolic_bytes)
-
-                # createUint256(string) returns (uint256)
-                elif funsig == halmos_cheat_code.create_uint256:
-                    name = name_of(extract_string_argument(arg, 0))
-                    label = f"halmos_{name}_uint256_{ex.new_symbol_id():>02}"
-                    ret = BitVec(label, BitVecSort256)
-
-                # createBytes32(string) returns (bytes32)
-                elif funsig == halmos_cheat_code.create_bytes32:
-                    name = name_of(extract_string_argument(arg, 0))
-                    label = f"halmos_{name}_bytes32_{ex.new_symbol_id():>02}"
-                    ret = BitVec(label, BitVecSort256)
-
-                # createAddress(string) returns (address)
-                elif funsig == halmos_cheat_code.create_address:
-                    name = name_of(extract_string_argument(arg, 0))
-                    label = f"halmos_{name}_address_{ex.new_symbol_id():>02}"
-                    ret = uint256(BitVec(label, BitVecSort160))
-
-                # createBool(string) returns (bool)
-                elif funsig == halmos_cheat_code.create_bool:
-                    name = name_of(extract_string_argument(arg, 0))
-                    label = f"halmos_{name}_bool_{ex.new_symbol_id():>02}"
-                    ret = uint256(BitVec(label, BitVecSort1))
-
-                else:
-                    error_msg = f"Unknown halmos cheat code: function selector = 0x{funsig:0>8x}, calldata = {hexify(arg)}"
-                    raise HalmosException(error_msg)
+                ret = halmos_cheat_code.handle(ex, arg)
 
             # vm cheat code
             if eq(to, hevm_cheat_code.address):
                 ex.solver.add(exit_code_var != con(0))
-                # vm.fail()
-                # BitVecVal(hevm_cheat_code.fail_payload, 800)
-                if arg == hevm_cheat_code.fail_payload:
-                    raise FailCheatcode()
-
-                # vm.assume(bool)
-                elif (
-                    eq(arg.sort(), BitVecSorts[(4 + 32) * 8])
-                    and simplify(Extract(287, 256, arg)) == hevm_cheat_code.assume_sig
-                ):
-                    assume_cond = simplify(is_non_zero(Extract(255, 0, arg)))
-                    ex.solver.add(assume_cond)
-                    ex.path.append(str(assume_cond))
-
-                # vm.getCode(string)
-                elif (
-                    simplify(Extract(arg_size * 8 - 1, arg_size * 8 - 32, arg))
-                    == hevm_cheat_code.get_code_sig
-                ):
-                    calldata = bytes.fromhex(hex(arg.as_long())[2:])
-                    path_len = int.from_bytes(calldata[36:68], "big")
-                    path = calldata[68 : 68 + path_len].decode("utf-8")
-
-                    if ":" in path:
-                        [filename, contract_name] = path.split(":")
-                        path = "out/" + filename + "/" + contract_name + ".json"
-
-                    target = self.options["target"].rstrip("/")
-                    path = target + "/" + path
-
-                    with open(path) as f:
-                        artifact = json.loads(f.read())
-
-                    if artifact["bytecode"]["object"]:
-                        bytecode = artifact["bytecode"]["object"].replace("0x", "")
-                    else:
-                        bytecode = artifact["bytecode"].replace("0x", "")
-
-                    ret = stringified_bytes_to_bytes(bytecode)
-                # vm.prank(address)
-                elif (
-                    eq(arg.sort(), BitVecSorts[(4 + 32) * 8])
-                    and simplify(Extract(287, 256, arg)) == hevm_cheat_code.prank_sig
-                ):
-                    result = ex.prank.prank(uint160(Extract(255, 0, arg)))
-                    if not result:
-                        raise HalmosException("You have an active prank already.")
-
-                # vm.startPrank(address)
-                elif (
-                    eq(arg.sort(), BitVecSorts[(4 + 32) * 8])
-                    and simplify(Extract(287, 256, arg))
-                    == hevm_cheat_code.start_prank_sig
-                ):
-                    result = ex.prank.startPrank(uint160(Extract(255, 0, arg)))
-                    if not result:
-                        raise HalmosException("You have an active prank already.")
-
-                # vm.stopPrank()
-                elif (
-                    eq(arg.sort(), BitVecSorts[4 * 8])
-                    and simplify(Extract(31, 0, arg)) == hevm_cheat_code.stop_prank_sig
-                ):
-                    ex.prank.stopPrank()
-                # vm.deal(address,uint256)
-                elif (
-                    eq(arg.sort(), BitVecSorts[(4 + 32 * 2) * 8])
-                    and simplify(Extract(543, 512, arg)) == hevm_cheat_code.deal_sig
-                ):
-                    who = uint160(Extract(511, 256, arg))
-                    amount = simplify(Extract(255, 0, arg))
-                    ex.balance_update(who, amount)
-                # vm.store(address,bytes32,bytes32)
-                elif (
-                    eq(arg.sort(), BitVecSorts[(4 + 32 * 3) * 8])
-                    and simplify(Extract(799, 768, arg)) == hevm_cheat_code.store_sig
-                ):
-                    store_account = uint160(Extract(767, 512, arg))
-                    store_slot = simplify(Extract(511, 256, arg))
-                    store_value = simplify(Extract(255, 0, arg))
-                    store_account_addr = self.resolve_address_alias(ex, store_account)
-                    if store_account_addr is not None:
-                        self.sstore(ex, store_account_addr, store_slot, store_value)
-                    else:
-                        raise HalmosException(f"uninitialized account: {store_account}")
-
-                # vm.load(address,bytes32)
-                elif (
-                    eq(arg.sort(), BitVecSorts[(4 + 32 * 2) * 8])
-                    and simplify(Extract(543, 512, arg)) == hevm_cheat_code.load_sig
-                ):
-                    load_account = uint160(Extract(511, 256, arg))
-                    load_slot = simplify(Extract(255, 0, arg))
-                    load_account_addr = self.resolve_address_alias(ex, load_account)
-                    if load_account_addr is not None:
-                        ret = self.sload(ex, load_account_addr, load_slot)
-                    else:
-                        raise HalmosException(f"uninitialized account: {store_account}")
-
-                # vm.fee(uint256)
-                elif (
-                    eq(arg.sort(), BitVecSorts[(4 + 32) * 8])
-                    and simplify(Extract(287, 256, arg)) == hevm_cheat_code.fee_sig
-                ):
-                    ex.block.basefee = simplify(Extract(255, 0, arg))
-                # vm.chainId(uint256)
-                elif (
-                    eq(arg.sort(), BitVecSorts[(4 + 32) * 8])
-                    and simplify(Extract(287, 256, arg)) == hevm_cheat_code.chainid_sig
-                ):
-                    ex.block.chainid = simplify(Extract(255, 0, arg))
-                # vm.coinbase(address)
-                elif (
-                    eq(arg.sort(), BitVecSorts[(4 + 32) * 8])
-                    and simplify(Extract(287, 256, arg)) == hevm_cheat_code.coinbase_sig
-                ):
-                    ex.block.coinbase = uint160(Extract(255, 0, arg))
-                # vm.difficulty(uint256)
-                elif (
-                    eq(arg.sort(), BitVecSorts[(4 + 32) * 8])
-                    and simplify(Extract(287, 256, arg))
-                    == hevm_cheat_code.difficulty_sig
-                ):
-                    ex.block.difficulty = simplify(Extract(255, 0, arg))
-                # vm.roll(uint256)
-                elif (
-                    eq(arg.sort(), BitVecSorts[(4 + 32) * 8])
-                    and simplify(Extract(287, 256, arg)) == hevm_cheat_code.roll_sig
-                ):
-                    ex.block.number = simplify(Extract(255, 0, arg))
-                # vm.warp(uint256)
-                elif (
-                    eq(arg.sort(), BitVecSorts[(4 + 32) * 8])
-                    and simplify(Extract(287, 256, arg)) == hevm_cheat_code.warp_sig
-                ):
-                    ex.block.timestamp = simplify(Extract(255, 0, arg))
-                # vm.etch(address,bytes)
-                elif extract_funsig(arg) == hevm_cheat_code.etch_sig:
-                    who = extract_bytes(arg, 4 + 12, 20)
-
-                    # who must be concrete
-                    if not is_bv_value(who):
-                        error_msg = f"vm.etch(address who, bytes code) must have concrete argument `who` but received {who}"
-                        raise HalmosException(error_msg)
-
-                    # code must be concrete
-                    try:
-                        code_offset = int_of(extract_bytes(arg, 4 + 32, 32))
-                        code_length = int_of(extract_bytes(arg, 4 + code_offset, 32))
-                        code_int = int_of(
-                            extract_bytes(arg, 4 + code_offset + 32, code_length)
-                        )
-                        code_bytes = code_int.to_bytes(code_length, "big")
-
-                        ex.code[who] = Contract(code_bytes)
-                    except Exception as e:
-                        error_msg = f"vm.etch(address who, bytes code) must have concrete argument `code` but received calldata {arg}"
-                        raise HalmosException(error_msg) from e
-                # ffi(string[]) returns (bytes)
-                elif extract_funsig(arg) == hevm_cheat_code.ffi_sig:
-                    if not self.options.get("ffi"):
-                        error_msg = "ffi cheatcode is disabled. Run again with `--ffi` if you want to enable it"
-                        raise HalmosException(error_msg)
-                    cmd = extract_string_array_argument(arg, 0)
-                    process = Popen(cmd, stdout=PIPE, stderr=PIPE)
-
-                    (stdout, stderr) = process.communicate()
-
-                    if stderr:
-                        warn(
-                            INTERNAL_ERROR,
-                            f"An exception has occurred during the usage of the ffi cheatcode:\n{stderr.decode('utf-8')}",
-                        )
-
-                    out_bytes = stdout.decode("utf-8")
-
-                    if not out_bytes.startswith("0x"):
-                        out_bytes = out_bytes.strip().encode("utf-8").hex()
-                    else:
-                        out_bytes = out_bytes.strip().replace("0x", "")
-
-                    ret = stringified_bytes_to_bytes(out_bytes)
-
-                else:
-                    # TODO: support other cheat codes
-                    msg = f"Unsupported cheat code: calldata = {hexify(arg)}"
-                    raise HalmosException(msg)
+                ret = hevm_cheat_code.handle(self, ex, arg)
 
             # console
             if eq(to, console.address):
                 ex.solver.add(exit_code_var != con(0))
-
-                funsig: int = int_of(
-                    extract_funsig(arg), "symbolic console function selector"
-                )
-
-                if funsig == console.log_uint256:
-                    print(extract_bytes(arg, 4, 32))
-
-                # elif funsig == console.log_string:
-
-                else:
-                    # TODO: support other console functions
-                    print(
-                        color_info(
-                            f"Unsupported console function: selector = 0x{funsig:0>8x}, "
-                            f"calldata = {hexify(arg)}"
-                        )
-                    )
+                console.handle(ex, arg)
 
             # store return value
             if ret_size > 0:
diff --git a/src/halmos/utils.py b/src/halmos/utils.py
index 92102af5..f6e79cf5 100644
--- a/src/halmos/utils.py
+++ b/src/halmos/utils.py
@@ -3,10 +3,123 @@
 import re
 
 from timeit import default_timer as timer
-from typing import Dict, Tuple
+from typing import Dict, Tuple, Any, Union as UnionType
 
 from z3 import *
 
+from .exceptions import NotConcreteError
+
+
+Word = Any  # z3 expression (including constants)
+Byte = Any  # z3 expression (including constants)
+Bytes = Any  # z3 expression (including constants)
+Address = BitVecRef  # 160-bitvector
+
+
+# dynamic BitVecSort sizes
+class BitVecSortCache:
+    def __init__(self):
+        self.cache = {}
+        for size in (
+            1,
+            8,
+            16,
+            32,
+            64,
+            128,
+            160,
+            256,
+            264,
+            288,
+            512,
+            544,
+            800,
+            1024,
+            1056,
+        ):
+            self.cache[size] = BitVecSort(size)
+
+    def __getitem__(self, size: int) -> BitVecSort:
+        hit = self.cache.get(size)
+        return hit if hit is not None else BitVecSort(size)
+
+
+BitVecSorts = BitVecSortCache()
+
+# known, fixed BitVecSort sizes
+BitVecSort1 = BitVecSorts[1]
+BitVecSort8 = BitVecSorts[8]
+BitVecSort160 = BitVecSorts[160]
+BitVecSort256 = BitVecSorts[256]
+BitVecSort264 = BitVecSorts[264]
+BitVecSort512 = BitVecSorts[512]
+
+
+def concat(args):
+    if len(args) > 1:
+        return Concat(args)
+    else:
+        return args[0]
+
+
+def uint256(x: BitVecRef) -> BitVecRef:
+    bitsize = x.size()
+    if bitsize > 256:
+        raise ValueError(x)
+    if bitsize == 256:
+        return x
+    return simplify(ZeroExt(256 - bitsize, x))
+
+
+def int256(x: BitVecRef) -> BitVecRef:
+    bitsize = x.size()
+    if bitsize > 256:
+        raise ValueError(x)
+    if bitsize == 256:
+        return x
+    return simplify(SignExt(256 - bitsize, x))
+
+
+def uint160(x: BitVecRef) -> BitVecRef:
+    bitsize = x.size()
+    if bitsize > 256:
+        raise ValueError(x)
+    if bitsize == 160:
+        return x
+    if bitsize > 160:
+        return simplify(Extract(159, 0, x))
+    else:
+        return simplify(ZeroExt(160 - bitsize, x))
+
+
+def con(n: int, size_bits=256) -> Word:
+    return BitVecVal(n, BitVecSorts[size_bits])
+
+
+#             x  == b   if sort(x) = bool
+# int_to_bool(x) == b   if sort(x) = int
+def test(x: Word, b: bool) -> Word:
+    if is_bool(x):
+        if b:
+            return x
+        else:
+            return Not(x)
+    elif is_bv(x):
+        if b:
+            return x != con(0)
+        else:
+            return x == con(0)
+    else:
+        raise ValueError(x)
+
+
+def is_non_zero(x: Word) -> Word:
+    return test(x, True)
+
+
+def is_zero(x: Word) -> Word:
+    return test(x, False)
+
 
 def create_solver(logic="QF_AUFBV", ctx=None, timeout=0, max_memory=0):
     # QF_AUFBV: quantifier-free bitvector + array theory: https://smtlib.cs.uiowa.edu/logics.shtml
@@ -22,12 +135,98 @@ def create_solver(logic="QF_AUFBV", ctx=None, timeout=0, max_memory=0):
     return solver
 
 
+def extract_bytes_argument(calldata: BitVecRef, arg_idx: int) -> bytes:
+    """Extracts idx-th argument of string from calldata"""
+    offset = int_of(
+        extract_bytes(calldata, 4 + arg_idx * 32, 32),
+        "symbolic offset for bytes argument",
+    )
+    length = int_of(
+        extract_bytes(calldata, 4 + offset, 32),
+        "symbolic size for bytes argument",
+    )
+    if length == 0:
+        return b""
+
+    return bv_value_to_bytes(extract_bytes(calldata, 4 + offset + 32, length))
+
+
+def extract_string_argument(calldata: BitVecRef, arg_idx: int):
+    """Extracts idx-th argument of string from calldata"""
+    string_bytes = extract_bytes_argument(calldata, arg_idx)
+    return string_bytes.decode("utf-8") if string_bytes else ""
+
+
+def extract_bytes(data: BitVecRef, byte_offset: int, size_bytes: int) -> BitVecRef:
+    """Extract bytes from calldata. Zero-pad if out of bounds."""
+    n = data.size()
+    if n % 8 != 0:
+        raise ValueError(n)
+
+    # will extract hi - lo + 1 bits
+    hi = n - 1 - byte_offset * 8
+    lo = n - byte_offset * 8 - size_bytes * 8
+    lo = 0 if lo < 0 else lo
+
+    val = simplify(Extract(hi, lo, data))
+
+    zero_padding = size_bytes * 8 - val.size()
+    if zero_padding < 0:
+        raise ValueError(val)
+    if zero_padding > 0:
+        val = simplify(Concat(val, con(0, zero_padding)))
+
+    return val
+
+
+def extract_funsig(calldata: BitVecRef):
+    """Extracts the function signature (first 4 bytes) from calldata"""
+    return extract_bytes(calldata, 0, 4)
+
+
 def bv_value_to_bytes(x: BitVecNumRef) -> bytes:
     if x.size() % 8 != 0:
         raise ValueError(x, x.size())
     return x.as_long().to_bytes(x.size() // 8, "big")
 
 
+def unbox_int(x: Any) -> Any:
+    """
+    Attempts to convert int-like objects to int
+    """
+    if isinstance(x, bytes):
+        return int.from_bytes(x, "big")
+
+    if is_bv_value(x):
+        return x.as_long()
+
+    return x
+
+
+def int_of(x: Any, err: str = "expected concrete value but got") -> int:
+    """
+    Converts int-like objects to int or raises NotConcreteError
+    """
+    res = unbox_int(x)
+
+    if isinstance(res, int):
+        return res
+
+    raise NotConcreteError(f"{err}: {x}")
+
+
+def byte_length(x: Any) -> int:
+    if is_bv(x):
+        if x.size() % 8 != 0:
+            raise ValueError(x)
+        return x.size() >> 3
+
+    if isinstance(x, bytes):
+        return len(x)
+
+    raise ValueError(x)
+
+
 def hexify(x):
     if isinstance(x, str):
         return re.sub(r"\b(\d+)\b", lambda match: hex(int(match.group(1))), x)
@@ -36,13 +235,86 @@ def hexify(x):
     elif isinstance(x, bytes):
         return "0x" + x.hex()
     elif is_bv_value(x):
-        # preserving bitsize could be confusing due to some bv values given as strings; need refactoring to fix properly
-        # return hexify(x.as_long().to_bytes((x.size() + 7) // 8, 'big')) # bitsize may not be a multiple of 8
-        return hex(x.as_long())
+        # maintain the byte size of x
+        num_bytes = byte_length(x)
+        return f"0x{x.as_long():0{num_bytes * 2}x}"
     else:
         return hexify(str(x))
 
 
+def render_uint(x: BitVecRef) -> str:
+    val = int_of(x)
+    return f"0x{val:0{byte_length(x) * 2}x} ({val})"
+
+
+def render_int(x: BitVecRef) -> str:
+    val = x.as_signed_long()
+    return f"0x{x.as_long():0{byte_length(x) * 2}x} ({val})"
+
+
+def render_bool(b: BitVecRef) -> str:
+    return str(b.as_long() != 0).lower()
+
+
+def render_string(s: BitVecRef) -> str:
+    str_val = bytes.fromhex(hexify(s)[2:]).decode("utf-8")
+    return f'"{str_val}"'
+
+
+def render_bytes(b: UnionType[BitVecRef, bytes]) -> str:
+    if is_bv(b):
+        return f'hex"{hex(b.as_long())[2:]}"'
+    else:
+        return f'hex"{b.hex()[2:]}"'
+
+
+def render_address(a: BitVecRef) -> str:
+    return f"0x{a.as_long():040x}"
+
+
+def stringify(symbol_name: str, val: Any):
+    """
+    Formats a value based on the inferred type of the variable.
+
+    Expects symbol_name to be of the form 'p_<sourceVar>_<sourceType>', e.g. 'p_x_uint256'
+    """
+    if not is_bv_value(val):
+        warn(f"{val} is not a bitvector value")
+        return hexify(val)
+
+    tokens = symbol_name.split("_")
+    if len(tokens) < 3:
+        warn(f"Failed to infer type for symbol '{symbol_name}'")
+        return hexify(val)
+
+    if len(tokens) >= 4 and tokens[-1].isdigit():
+        # we may have something like p_val_bytes_01
+        # the last token being a symbol number, discard it
+        tokens.pop()
+
+    type_name = tokens[-1]
+
+    try:
+        if type_name.startswith("uint"):
+            return render_uint(val)
+        elif type_name.startswith("int"):
+            return render_int(val)
+        elif type_name == "bool":
+            return render_bool(val)
+        elif type_name == "string":
+            return render_string(val)
+        elif type_name == "bytes":
+            return render_bytes(val)
+        elif type_name == "address":
+            return render_address(val)
+        else:  # bytes32, bytes4, structs, etc.
+            return hexify(val)
+    except Exception as e:
+        # log error and move on
+        warn(f"Failed to stringify {val} of type {type_name}: {repr(e)}")
+        return hexify(val)
+
+
 def assert_address(x: BitVecRef) -> None:
     if x.size() != 160:
         raise ValueError(x)
@@ -77,6 +349,10 @@ def cyan(text: str) -> str:
     return f"\033[36m{text}\033[0m"
 
 
+def magenta(text: str) -> str:
+    return f"\033[35m{text}\033[0m"
+
+
 def color_good(text: str) -> str:
     return green(text)
 
diff --git a/tests/expected/all.json b/tests/expected/all.json
index 1f227576..4e09cdef 100644
--- a/tests/expected/all.json
+++ b/tests/expected/all.json
@@ -273,7 +273,79 @@
         ],
         "test/Console.t.sol:ConsoleTest": [
             {
-                "name": "check_log()",
+                "name": "check_log_address()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_log_bool()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_log_bytes()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_log_bytes32()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_log_int()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_log_string()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_log_uint()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_log_undecodable_string()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_log_unsupported()",
                 "exitcode": 0,
                 "num_models": 0,
                 "models": null,
@@ -807,6 +879,42 @@
                 "time": null,
                 "num_bounded_loops": null
             },
+            {
+                "name": "check_createBytes4()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_createInt()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_createInt256()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_createString()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
             {
                 "name": "check_createUint()",
                 "exitcode": 0,
diff --git a/tests/lib/halmos-cheatcodes b/tests/lib/halmos-cheatcodes
index c9e5f804..c0d86550 160000
--- a/tests/lib/halmos-cheatcodes
+++ b/tests/lib/halmos-cheatcodes
@@ -1 +1 @@
-Subproject commit c9e5f80441b9d8aeb2e724db07a1322e59aaeb82
+Subproject commit c0d865508c0fee0a11b97732c5e90f9cad6b65a5
diff --git a/tests/regression/remappings.txt b/tests/regression/remappings.txt
index 41f9d750..30f1086e 100644
--- a/tests/regression/remappings.txt
+++ b/tests/regression/remappings.txt
@@ -1,2 +1,3 @@
 openzeppelin/=../lib/openzeppelin-contracts/contracts/
 ds-test/=../lib/forge-std/lib/ds-test/src/
+forge-std/=../lib/forge-std/src/
diff --git a/tests/regression/test/Console.t.sol b/tests/regression/test/Console.t.sol
index 117a3c95..35002b78 100644
--- a/tests/regression/test/Console.t.sol
+++ b/tests/regression/test/Console.t.sol
@@ -2,10 +2,81 @@
 pragma solidity >=0.8.0 <0.9.0;
 
 import "forge-std/Test.sol";
+import {console2} from "forge-std/console2.sol";
 
 contract ConsoleTest is Test {
-    function check_log() public view {
-        console.log(0);
-        console.log(1);
+    function check_log_uint() public view {
+        console2.log("this is 0:", uint256(0));
+        console2.log("this is 1:", uint256(1));
+
+        console2.log(uint256(0));
+        console2.log(uint256(1));
+
+        console2.logUint(0);
+        console2.logUint(1);
+    }
+
+    function check_log_int() public view {
+        console2.log("this is -1:", -1);
+        console2.log("this is 1:", int256(1));
+
+        console2.log(-1);
+        console2.log(int256(1));
+
+        console2.logInt(-1);
+        console2.logInt(int256(1));
+    }
+
+    function check_log_bytes() public view {
+        bytes memory hello = "hello";
+        bytes memory empty = "";
+        console2.log("this is hello (bytes):");
+        console2.logBytes(hello);
+        console2.log("this is empty bytes:");
+        console2.logBytes(empty);
+    }
+
+    function check_log_bytes32() public view {
+        console2.log("this is keccak256(hello):");
+        console2.logBytes32(keccak256("hello"));
+
+        console2.log("this is keccak256():");
+        console2.logBytes32(keccak256(""));
+    }
+
+    function check_log_address() public view {
+        console2.log("this is address(0):", address(0));
+        console2.log("this is address(this):", address(this));
+
+        console2.log(address(0));
+        console2.log(address(this));
+    }
+
+    function check_log_bool() public view {
+        console2.log("this is true:", true);
+        console2.log("this is false:", false);
+
+        console2.log(true);
+        console2.log(false);
+    }
+
+    function check_log_string() public view {
+        string memory hello = "hello";
+        string memory empty = "";
+        console2.log("this is hello (string):", hello);
+        console2.log("this is empty string:", empty);
+
+        console2.log(hello);
+        console2.log(empty);
+    }
+
+    function check_log_undecodable_string() public view {
+        bytes memory badBytes = hex"ff";
+        string memory bad = string(badBytes);
+        console2.log("this is a string that won't decode to utf-8:", bad);
+    }
+
+    function check_log_unsupported() public {
+        console2._sendLogPayload(abi.encodeWithSignature("doesNotExist()"));
     }
 }
diff --git a/tests/regression/test/HalmosCheatCode.t.sol b/tests/regression/test/HalmosCheatCode.t.sol
index 1207ae48..ee928f81 100644
--- a/tests/regression/test/HalmosCheatCode.t.sol
+++ b/tests/regression/test/HalmosCheatCode.t.sol
@@ -13,6 +13,15 @@ contract HalmosCheatCodeTest is SymTest {
         assert(0 <= z && z <= type(uint8).max);
     }
 
+    function check_createInt() public {
+        int x = svm.createInt(256, 'x');
+        int y = svm.createInt(160, 'y');
+        int z = svm.createInt(8, 'z');
+        assert(type(int256).min <= x && x <= type(int256).max);
+        assert(type(int160).min <= y && y <= type(int160).max);
+        assert(type(int8).min <= z && z <= type(int8).max);
+    }
+
     function check_createBytes() public {
         bytes memory data = svm.createBytes(2, 'data');
         uint x = uint(uint8(data[0]));
@@ -21,11 +30,21 @@ contract HalmosCheatCodeTest is SymTest {
         assert(0 <= y && y <= type(uint8).max);
     }
 
+    function check_createString() public {
+        string memory data = svm.createString(5, 'str');
+        assert(bytes(data).length == 5);
+    }
+
     function check_createUint256() public {
         uint x = svm.createUint256('x');
         assert(0 <= x && x <= type(uint256).max);
     }
 
+    function check_createInt256() public {
+        int x = svm.createInt256('x');
+        assert(type(int256).min <= x && x <= type(int256).max);
+    }
+
     function check_createBytes32() public {
         bytes32 x = svm.createBytes32('x');
         assert(0 <= uint(x) && uint(x) <= type(uint256).max);
@@ -33,6 +52,14 @@ contract HalmosCheatCodeTest is SymTest {
         assert(0 <= y && y <= type(uint256).max);
     }
 
+    function check_createBytes4() public {
+        bytes4 x = svm.createBytes4('x');
+        uint256 x_uint = uint256(uint32(x));
+        assert(0 <= x_uint && x_uint <= type(uint32).max);
+        uint y; assembly { y := x }
+        assert(0 <= y && y <= type(uint256).max);
+    }
+
     function check_createAddress() public {
         address x = svm.createAddress('x');
         uint y; assembly { y := x }