diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index 6fe8e17c..e141bc1a 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -13,12 +13,9 @@ jobs:
     strategy:
       matrix:
         os: ["macos-latest", "ubuntu-latest", "windows-latest"]
-        python-version: ["3.8", "3.9", "3.10", "3.11", "3.8.13", "3.9.13", "3.10.6"]
+        python-version: ["3.8", "3.9", "3.10", "3.11"]
         parallel: ["", "--test-parallel", "--solver-parallel", "--test-parallel --solver-parallel"]
-        exclude:
-          # python 3.8.13 is not available in windows-2022
-          - os: "windows-latest"
-            python-version: "3.8.13"
+        custom-storage: ["", "--custom-storage-layout"]
 
     steps:
       - uses: actions/checkout@v3
@@ -42,4 +39,4 @@ jobs:
         run: pip install -e .
 
       - name: Run pytest
-        run: pytest -v -k "not long and not ffi" --halmos-options="-v -st --error-unknown ${{ matrix.parallel }} --solver-timeout-assertion 0"
+        run: pytest -v -k "not long and not ffi" --ignore=tests/lib --halmos-options="-v -st --error-unknown ${{ matrix.parallel }} ${{ matrix.custom-storage }} --solver-timeout-assertion 0"
diff --git a/.gitmodules b/.gitmodules
index ed2a80a8..2ecec2e0 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -10,3 +10,6 @@
 [submodule "tests/lib/solmate"]
 	path = tests/lib/solmate
 	url = https://github.com/transmissions11/solmate
+[submodule "tests/lib/solady"]
+	path = tests/lib/solady
+	url = https://github.com/Vectorized/solady
diff --git a/examples/tokens/ERC20/src/SoladyERC20.sol b/examples/tokens/ERC20/src/SoladyERC20.sol
new file mode 100644
index 00000000..03ddd418
--- /dev/null
+++ b/examples/tokens/ERC20/src/SoladyERC20.sol
@@ -0,0 +1,36 @@
+// SPDX-License-Identifier: AGPL-3.0
+pragma solidity >=0.8.0 <0.9.0;
+
+import {ERC20} from "solady/tokens/ERC20.sol";
+
+contract SoladyERC20 is ERC20 {
+    string internal _name;
+    string internal _symbol;
+    uint8 internal _decimals;
+
+    constructor(
+        string memory name_,
+        string memory symbol_,
+        uint8 decimals_,
+        uint256 initialSupply,
+        address deployer
+    ) {
+        _name = name_;
+        _symbol = symbol_;
+        _decimals = decimals_;
+
+        _mint(deployer, initialSupply);
+    }
+
+    function name() public view virtual override returns (string memory) {
+        return _name;
+    }
+
+    function symbol() public view virtual override returns (string memory) {
+        return _symbol;
+    }
+
+    function decimals() public view virtual override returns (uint8) {
+        return _decimals;
+    }
+}
diff --git a/examples/tokens/ERC20/test/CurveTokenV3.t.sol b/examples/tokens/ERC20/test/CurveTokenV3.t.sol
new file mode 100644
index 00000000..f0cead5a
--- /dev/null
+++ b/examples/tokens/ERC20/test/CurveTokenV3.t.sol
@@ -0,0 +1,69 @@
+// SPDX-License-Identifier: AGPL-3.0
+pragma solidity >=0.8.0 <0.9.0;
+
+import {SymTest} from "halmos-cheatcodes/SymTest.sol";
+import {ERC20Test} from "./ERC20Test.sol";
+
+// Auto-generated by https://bia.is/tools/abi2solidity/
+interface CurveTokenV3 {
+  function decimals (  ) external view returns ( uint256 );
+  function transfer ( address _to, uint256 _value ) external returns ( bool );
+  function transferFrom ( address _from, address _to, uint256 _value ) external returns ( bool );
+  function approve ( address _spender, uint256 _value ) external returns ( bool );
+  function increaseAllowance ( address _spender, uint256 _added_value ) external returns ( bool );
+  function decreaseAllowance ( address _spender, uint256 _subtracted_value ) external returns ( bool );
+  function mint ( address _to, uint256 _value ) external returns ( bool );
+  function burnFrom ( address _to, uint256 _value ) external returns ( bool );
+  function set_minter ( address _minter ) external;
+  function set_name ( string memory _name, string memory _symbol ) external;
+  function name (  ) external view returns ( string memory );
+  function symbol (  ) external view returns ( string memory );
+  function balanceOf ( address arg0 ) external view returns ( uint256 );
+  function allowance ( address arg0, address arg1 ) external view returns ( uint256 );
+  function totalSupply (  ) external view returns ( uint256 );
+  function minter (  ) external view returns ( address );
+}
+
+contract EmptyContract { }
+
+/// @custom:halmos --custom-storage-layout --solver-timeout-assertion 0
+contract CurveTokenV3Test is ERC20Test {
+    CurveTokenV3 token_;
+    address minter;
+
+    function setUp() public override {
+        token = address(new EmptyContract());
+        // Source of Deployed Bytecode: https://etherscan.io/address/0x06325440D014e39736583c165C2963BA99fAf14E#code
+        vm.etch(token, hex"341561000a57600080fd5b60043610156100185761092e565b600035601c5263313ce567600051141561003957601260005260206000f350005b63a9059cbb60005114156100ee5760043560a01c1561005757600080fd5b60023360e05260c052604060c02080546024358082101561007757600080fd5b80820390509050815550600260043560e05260c052604060c02080546024358181830110156100a557600080fd5b8082019050905081555060243561014052600435337fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef6020610140a3600160005260206000f350005b6323b872dd600051141561023c5760043560a01c1561010c57600080fd5b60243560a01c1561011c57600080fd5b600260043560e05260c052604060c02080546044358082101561013e57600080fd5b80820390509050815550600260243560e05260c052604060c020805460443581818301101561016c57600080fd5b80820190509050815550600360043560e05260c052604060c0203360e05260c052604060c02054610140527fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff6101405118156101fb5761014051604435808210156101d657600080fd5b80820390509050600360043560e05260c052604060c0203360e05260c052604060c020555b604435610160526024356004357fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef6020610160a3600160005260206000f350005b63095ea7b360005114156102b95760043560a01c1561025a57600080fd5b60243560033360e05260c052604060c02060043560e05260c052604060c0205560243561014052600435337f8c5be1e5ebec7d5bd14f71427d1e84f3dd0314c0f7b2291e5b200ac8c7c3b9256020610140a3600160005260206000f350005b633950935160005114156103725760043560a01c156102d757600080fd5b60033360e05260c052604060c02060043560e05260c052604060c0205460243581818301101561030657600080fd5b80820190509050610140526101405160033360e05260c052604060c02060043560e05260c052604060c020556101405161016052600435337f8c5be1e5ebec7d5bd14f71427d1e84f3dd0314c0f7b2291e5b200ac8c7c3b9256020610160a3600160005260206000f350005b63a457c2d760005114156104295760043560a01c1561039057600080fd5b60033360e05260c052604060c02060043560e05260c052604060c02054602435808210156103bd57600080fd5b80820390509050610140526101405160033360e05260c052604060c02060043560e05260c052604060c020556101405161016052600435337f8c5be1e5ebec7d5bd14f71427d1e84f3dd0314c0f7b2291e5b200ac8c7c3b9256020610160a3600160005260206000f350005b6340c10f1960005114156104e35760043560a01c1561044757600080fd5b600554331461045557600080fd5b6004805460243581818301101561046b57600080fd5b80820190509050815550600260043560e05260c052604060c020805460243581818301101561049957600080fd5b808201905090508155506024356101405260043560007fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef6020610140a3600160005260206000f350005b6379cc679060005114156105995760043560a01c1561050157600080fd5b600554331461050f57600080fd5b600480546024358082101561052357600080fd5b80820390509050815550600260043560e05260c052604060c02080546024358082101561054f57600080fd5b808203905090508155506024356101405260006004357fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef6020610140a3600160005260206000f350005b631652e9fc60005114156105cd5760043560a01c156105b757600080fd5b60055433146105c557600080fd5b600435600555005b63e1430e0660005114156107115760606004356004016101403760406004356004013511156105fb57600080fd5b60406024356004016101c037602060243560040135111561061b57600080fd5b3360206102806004638da5cb5b6102205261023c6005545afa61063d57600080fd5b601f3d1161064a57600080fd5b600050610280511461065b57600080fd5b61014080600060c052602060c020602082510161012060006003818352015b8261012051602002111561068d576106af565b61012051602002850151610120518501555b815160010180835281141561067a575b5050505050506101c080600160c052602060c020602082510161012060006002818352015b826101205160200211156106e757610709565b61012051602002850151610120518501555b81516001018083528114156106d4575b505050505050005b6306fdde0360005114156107ba5760008060c052602060c020610180602082540161012060006003818352015b8261012051602002111561075157610773565b61012051850154610120516020028501525b815160010180835281141561073e575b50505050505061018051806101a001818260206001820306601f82010390500336823750506020610160526040610180510160206001820306601f8201039050610160f350005b6395d89b4160005114156108635760018060c052602060c020610180602082540161012060006002818352015b826101205160200211156107fa5761081c565b61012051850154610120516020028501525b81516001018083528114156107e7575b50505050505061018051806101a001818260206001820306601f82010390500336823750506020610160526040610180510160206001820306601f8201039050610160f350005b6370a08231600051141561089d5760043560a01c1561088157600080fd5b600260043560e05260c052604060c0205460005260206000f350005b63dd62ed3e60005114156108f55760043560a01c156108bb57600080fd5b60243560a01c156108cb57600080fd5b600360043560e05260c052604060c02060243560e05260c052604060c0205460005260206000f350005b6318160ddd60005114156109115760045460005260206000f350005b6307546172600051141561092d5760055460005260206000f350005b5b60006000fd");
+        token_ = CurveTokenV3(token);
+
+        minter = token_.minter();
+        vm.prank(minter);
+        token_.mint(address(this), 1_000_000_000e18);
+        assert(token_.balanceOf(address(this)) == 1_000_000_000e18);
+
+        holders = new address[](3);
+        holders[0] = address(0x1001);
+        holders[1] = address(0x1002);
+        holders[2] = address(0x1003);
+
+        for (uint i = 0; i < holders.length; i++) {
+            address account = holders[i];
+            uint256 balance = svm.createUint256('balance');
+            token_.transfer(account, balance);
+            for (uint j = 0; j < i; j++) {
+                address other = holders[j];
+                uint256 amount = svm.createUint256('amount');
+                vm.prank(account);
+                token_.approve(other, amount);
+            }
+        }
+    }
+
+    function check_NoBackdoor(bytes4 selector, address caller, address other) public {
+        vm.assume(caller != minter);
+        vm.assume(selector != CurveTokenV3.set_name.selector);
+        bytes memory args = svm.createBytes(1024, 'data');
+        _checkNoBackdoor(selector, args, caller, other);
+    }
+}
diff --git a/examples/tokens/ERC20/test/SoladyERC20.t.sol b/examples/tokens/ERC20/test/SoladyERC20.t.sol
new file mode 100644
index 00000000..e617461c
--- /dev/null
+++ b/examples/tokens/ERC20/test/SoladyERC20.t.sol
@@ -0,0 +1,39 @@
+// SPDX-License-Identifier: AGPL-3.0
+pragma solidity >=0.8.0 <0.9.0;
+
+import {ERC20Test} from "./ERC20Test.sol";
+
+import {SoladyERC20} from "../src/SoladyERC20.sol";
+
+/// @custom:halmos --custom-storage-layout --solver-timeout-assertion 0
+contract SoladyERC20Test is ERC20Test {
+    function setUp() public override {
+        address deployer = address(0x1000);
+
+        SoladyERC20 token_ = new SoladyERC20("SoladyERC20", "SoladyERC20", 18, 1_000_000_000e18, deployer);
+        token = address(token_);
+
+        holders = new address[](3);
+        holders[0] = address(0x1001);
+        holders[1] = address(0x1002);
+        holders[2] = address(0x1003);
+
+        for (uint i = 0; i < holders.length; i++) {
+            address account = holders[i];
+            uint256 balance = svm.createUint256('balance');
+            vm.prank(deployer);
+            token_.transfer(account, balance);
+            for (uint j = 0; j < i; j++) {
+                address other = holders[j];
+                uint256 amount = svm.createUint256('amount');
+                vm.prank(account);
+                token_.approve(other, amount);
+            }
+        }
+    }
+
+    function check_NoBackdoor(bytes4 selector, address caller, address other) public {
+        bytes memory args = svm.createBytes(1024, 'data');
+        _checkNoBackdoor(selector, args, caller, other);
+    }
+}
diff --git a/examples/tokens/ERC721/src/SoladyERC721.sol b/examples/tokens/ERC721/src/SoladyERC721.sol
new file mode 100644
index 00000000..2ec6869a
--- /dev/null
+++ b/examples/tokens/ERC721/src/SoladyERC721.sol
@@ -0,0 +1,33 @@
+// SPDX-License-Identifier: AGPL-3.0
+pragma solidity >=0.8.0 <0.9.0;
+
+import {ERC721} from "solady/tokens/ERC721.sol";
+
+contract SoladyERC721 is ERC721 {
+    string internal _name;
+    string internal _symbol;
+
+    constructor(
+        string memory name_,
+        string memory symbol_,
+        uint256 initialSupply,
+        address deployer
+    ) {
+        _name = name_;
+        _symbol = symbol_;
+
+        for (uint256 i = 1; i <= initialSupply; i++) {
+            _mint(deployer, i);
+        }
+    }
+
+    function name() public view virtual override returns (string memory) {
+        return _name;
+    }
+
+    function symbol() public view virtual override returns (string memory) {
+        return _symbol;
+    }
+
+    function tokenURI(uint256) public view virtual override returns (string memory) {}
+}
diff --git a/examples/tokens/ERC721/test/SoladyERC721.t.sol b/examples/tokens/ERC721/test/SoladyERC721.t.sol
new file mode 100644
index 00000000..aa14eb8a
--- /dev/null
+++ b/examples/tokens/ERC721/test/SoladyERC721.t.sol
@@ -0,0 +1,44 @@
+// SPDX-License-Identifier: AGPL-3.0
+pragma solidity >=0.8.0 <0.9.0;
+
+import {ERC721Test} from "./ERC721Test.sol";
+
+import {SoladyERC721} from "../src/SoladyERC721.sol";
+
+/// @custom:halmos --custom-storage-layout --solver-timeout-assertion 0
+contract SoladyERC721Test is ERC721Test {
+    function setUp() public override {
+        deployer = address(0x1000);
+
+        SoladyERC721 token_ = new SoladyERC721("SoladyERC721", "SoladyERC721", 5, deployer);
+        token = address(token_);
+
+        accounts = new address[](3);
+        accounts[0] = address(0x1001);
+        accounts[1] = address(0x1002);
+        accounts[2] = address(0x1003);
+
+        tokenIds = new uint256[](5);
+        tokenIds[0] = 1;
+        tokenIds[1] = 2;
+        tokenIds[2] = 3;
+        tokenIds[3] = 4;
+        tokenIds[4] = 5;
+
+        // account0: {token0, token1}, account1: {token2}, account2: {token3}
+        vm.prank(deployer);
+        token_.transferFrom(deployer, accounts[0], tokenIds[0]);
+        vm.prank(deployer);
+        token_.transferFrom(deployer, accounts[0], tokenIds[1]);
+        vm.prank(deployer);
+        token_.transferFrom(deployer, accounts[1], tokenIds[2]);
+        vm.prank(deployer);
+        token_.transferFrom(deployer, accounts[2], tokenIds[3]);
+
+        vm.prank(accounts[0]);
+        token_.approve(accounts[2], tokenIds[0]);
+
+        vm.prank(accounts[1]);
+        token_.setApprovalForAll(accounts[2], true);
+    }
+}
diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py
index 4813b9c8..4dc0dc45 100644
--- a/src/halmos/__main__.py
+++ b/src/halmos/__main__.py
@@ -891,6 +891,7 @@ def mk_options(args: Namespace) -> Dict:
         "print_steps": args.print_steps,
         "unknown_calls_return_size": args.return_size_of_unknown_calls,
         "ffi": args.ffi,
+        "custom_storage_layout": args.custom_storage_layout,
     }
 
     if args.width is not None:
diff --git a/src/halmos/parser.py b/src/halmos/parser.py
index 7d7a5b39..535671c9 100644
--- a/src/halmos/parser.py
+++ b/src/halmos/parser.py
@@ -61,6 +61,12 @@ def mk_arg_parser() -> argparse.ArgumentParser:
         help="set the byte size of return data from uninterpreted unknown external calls (default: %(default)s)",
     )
 
+    parser.add_argument(
+        "--custom-storage-layout",
+        action="store_true",
+        help="allow for a custom (non-Solidity) storage layout",
+    )
+
     parser.add_argument(
         "--symbolic-storage",
         action="store_true",
diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py
index a65e0c91..fe3b611a 100644
--- a/src/halmos/sevm.py
+++ b/src/halmos/sevm.py
@@ -874,138 +874,6 @@ def balance_update(self, addr: Word, value: Word) -> None:
         self.balance = new_balance_var
         self.balances[new_balance_var] = new_balance
 
-    def empty_storage_of(self, addr: BitVecRef, slot: int, len_keys: int) -> ArrayRef:
-        return Array(
-            f"storage_{id_str(addr)}_{slot}_{len_keys}_00",
-            BitVecSorts[len_keys * 256],
-            BitVecSort256,
-        )
-
-    def sinit(self, addr: Any, slot: int, keys) -> None:
-        assert_address(addr)
-        if slot not in self.storage[addr]:
-            self.storage[addr][slot] = {}
-        if len(keys) not in self.storage[addr][slot]:
-            if len(keys) == 0:
-                if self.symbolic:
-                    label = f"storage_{id_str(addr)}_{slot}_{len(keys)}_00"
-                    self.storage[addr][slot][len(keys)] = BitVec(label, BitVecSort256)
-                else:
-                    self.storage[addr][slot][len(keys)] = con(0)
-            else:
-                # do not use z3 const array `K(BitVecSort(len(keys)*256), con(0))` when not self.symbolic
-                # instead use normal smt array, and generate emptyness axiom; see sload()
-                self.storage[addr][slot][len(keys)] = self.empty_storage_of(
-                    addr, slot, len(keys)
-                )
-
-    def sload(self, addr: Any, loc: Word) -> Word:
-        offsets = self.decode_storage_loc(loc)
-        if not len(offsets) > 0:
-            raise ValueError(offsets)
-        slot, keys = int_of(offsets[0], "symbolic storage base slot"), offsets[1:]
-        self.sinit(addr, slot, keys)
-        if len(keys) == 0:
-            return self.storage[addr][slot][0]
-        else:
-            if not self.symbolic:
-                # generate emptyness axiom for each array index, instead of using quantified formula; see sinit()
-                self.solver.add(
-                    Select(self.empty_storage_of(addr, slot, len(keys)), concat(keys))
-                    == con(0)
-                )
-            return self.select(
-                self.storage[addr][slot][len(keys)], concat(keys), self.storages
-            )
-
-    def sstore(self, addr: Any, loc: Any, val: Any) -> None:
-        offsets = self.decode_storage_loc(loc)
-        if not len(offsets) > 0:
-            raise ValueError(offsets)
-        slot, keys = int_of(offsets[0], "symbolic storage base slot"), offsets[1:]
-        self.sinit(addr, slot, keys)
-        if len(keys) == 0:
-            self.storage[addr][slot][0] = val
-        else:
-            new_storage_var = Array(
-                f"storage_{id_str(addr)}_{slot}_{len(keys)}_{1+len(self.storages):>02}",
-                BitVecSorts[len(keys) * 256],
-                BitVecSort256,
-            )
-            new_storage = Store(self.storage[addr][slot][len(keys)], concat(keys), val)
-            self.solver.add(new_storage_var == new_storage)
-            self.storage[addr][slot][len(keys)] = new_storage_var
-            self.storages[new_storage_var] = new_storage
-
-    def decode_storage_loc(self, loc: Any) -> Any:
-        def normalize(expr: Any) -> Any:
-            # Concat(Extract(255, 8, bvadd(x, y)), bvadd(Extract(7, 0, x), Extract(7, 0, y))) => x + y
-            if expr.decl().name() == "concat" and expr.num_args() == 2:
-                arg0 = expr.arg(0)  # Extract(255, 8, bvadd(x, y))
-                arg1 = expr.arg(1)  # bvadd(Extract(7, 0, x), Extract(7, 0, y))
-                if (
-                    arg0.decl().name() == "extract"
-                    and arg0.num_args() == 1
-                    and arg0.params() == [255, 8]
-                ):
-                    arg00 = arg0.arg(0)  # bvadd(x, y)
-                    if arg00.decl().name() == "bvadd":
-                        x = arg00.arg(0)
-                        y = arg00.arg(1)
-                        if arg1.decl().name() == "bvadd" and arg1.num_args() == 2:
-                            if eq(arg1.arg(0), simplify(Extract(7, 0, x))) and eq(
-                                arg1.arg(1), simplify(Extract(7, 0, y))
-                            ):
-                                return x + y
-            return expr
-
-        loc = normalize(loc)
-
-        if loc.decl().name() == "sha3_512":  # m[k] : hash(k.m)
-            args = loc.arg(0)
-            offset, base = simplify(Extract(511, 256, args)), simplify(
-                Extract(255, 0, args)
-            )
-            return self.decode_storage_loc(base) + (offset, con(0))
-        elif loc.decl().name() == "sha3_256":  # a[i] : hash(a)+i
-            base = loc.arg(0)
-            return self.decode_storage_loc(base) + (con(0),)
-        elif loc.decl().name() == "bvadd":
-            #   # when len(args) == 2
-            #   arg0 = self.decode_storage_loc(loc.arg(0))
-            #   arg1 = self.decode_storage_loc(loc.arg(1))
-            #   if len(arg0) == 1 and len(arg1) > 1: # i + hash(x)
-            #       return arg1[0:-1] + (arg1[-1] + arg0[0],)
-            #   elif len(arg0) > 1 and len(arg1) == 1: # hash(x) + i
-            #       return arg0[0:-1] + (arg0[-1] + arg1[0],)
-            #   elif len(arg0) == 1 and len(arg1) == 1: # i + j
-            #       return (arg0[0] + arg1[0],)
-            #   else: # hash(x) + hash(y) # ambiguous
-            #       raise ValueError(loc)
-            # when len(args) >= 2
-            args = loc.children()
-            if len(args) < 2:
-                raise ValueError(loc)
-            args = sorted(
-                map(self.decode_storage_loc, args), key=lambda x: len(x), reverse=True
-            )
-            if len(args[1]) > 1:
-                # only args[0]'s length >= 1, the others must be 1
-                raise ValueError(loc)
-            return args[0][0:-1] + (
-                reduce(lambda r, x: r + x[0], args[1:], args[0][-1]),
-            )
-        elif is_bv_value(loc):
-            (preimage, delta) = restore_precomputed_hashes(loc.as_long())
-            if preimage:  # loc == hash(preimage) + delta
-                return (con(preimage), con(delta))
-            else:
-                return (loc,)
-        elif is_bv(loc):
-            return (loc,)
-        else:
-            raise ValueError(loc)
-
     def sha3(self) -> None:
         loc: int = self.st.mloc()
         size: int = int_of(self.st.pop(), "symbolic SHA3 data size")
@@ -1104,6 +972,223 @@ def resolve_libs(self, creation_hexcode, deployed_hexcode, lib_references) -> st
         return (creation_hexcode, deployed_hexcode)
 
 
+class Storage:
+    @classmethod
+    def normalize(cls, expr: Any) -> Any:
+        # Concat(Extract(255, 8, bvadd(x, y)), bvadd(Extract(7, 0, x), Extract(7, 0, y))) => x + y
+        if expr.decl().name() == "concat" and expr.num_args() == 2:
+            arg0 = expr.arg(0)  # Extract(255, 8, bvadd(x, y))
+            arg1 = expr.arg(1)  # bvadd(Extract(7, 0, x), Extract(7, 0, y))
+            if (
+                arg0.decl().name() == "extract"
+                and arg0.num_args() == 1
+                and arg0.params() == [255, 8]
+            ):
+                arg00 = arg0.arg(0)  # bvadd(x, y)
+                if arg00.decl().name() == "bvadd":
+                    x = arg00.arg(0)
+                    y = arg00.arg(1)
+                    if arg1.decl().name() == "bvadd" and arg1.num_args() == 2:
+                        if eq(arg1.arg(0), simplify(Extract(7, 0, x))) and eq(
+                            arg1.arg(1), simplify(Extract(7, 0, y))
+                        ):
+                            return x + y
+        return expr
+
+
+class SolidityStorage(Storage):
+    @classmethod
+    def empty(cls, addr: BitVecRef, slot: int, len_keys: int) -> ArrayRef:
+        return Array(
+            f"storage_{id_str(addr)}_{slot}_{len_keys}_00",
+            BitVecSorts[len_keys * 256],
+            BitVecSort256,
+        )
+
+    @classmethod
+    def init(cls, ex: Exec, addr: Any, slot: int, keys) -> None:
+        assert_address(addr)
+        if slot not in ex.storage[addr]:
+            ex.storage[addr][slot] = {}
+        if len(keys) not in ex.storage[addr][slot]:
+            if len(keys) == 0:
+                if ex.symbolic:
+                    label = f"storage_{id_str(addr)}_{slot}_{len(keys)}_00"
+                    ex.storage[addr][slot][len(keys)] = BitVec(label, BitVecSort256)
+                else:
+                    ex.storage[addr][slot][len(keys)] = con(0)
+            else:
+                # do not use z3 const array `K(BitVecSort(len(keys)*256), con(0))` when not ex.symbolic
+                # instead use normal smt array, and generate emptyness axiom; see load()
+                ex.storage[addr][slot][len(keys)] = cls.empty(addr, slot, len(keys))
+
+    @classmethod
+    def load(cls, ex: Exec, addr: Any, loc: Word) -> Word:
+        offsets = cls.decode(loc)
+        if not len(offsets) > 0:
+            raise ValueError(offsets)
+        slot, keys = int_of(offsets[0], "symbolic storage base slot"), offsets[1:]
+        cls.init(ex, addr, slot, keys)
+        if len(keys) == 0:
+            return ex.storage[addr][slot][0]
+        else:
+            if not ex.symbolic:
+                # generate emptyness axiom for each array index, instead of using quantified formula; see init()
+                ex.solver.add(
+                    Select(cls.empty(addr, slot, len(keys)), concat(keys)) == con(0)
+                )
+            return ex.select(
+                ex.storage[addr][slot][len(keys)], concat(keys), ex.storages
+            )
+
+    @classmethod
+    def store(cls, ex: Exec, addr: Any, loc: Any, val: Any) -> None:
+        offsets = cls.decode(loc)
+        if not len(offsets) > 0:
+            raise ValueError(offsets)
+        slot, keys = int_of(offsets[0], "symbolic storage base slot"), offsets[1:]
+        cls.init(ex, addr, slot, keys)
+        if len(keys) == 0:
+            ex.storage[addr][slot][0] = val
+        else:
+            new_storage_var = Array(
+                f"storage_{id_str(addr)}_{slot}_{len(keys)}_{1+len(ex.storages):>02}",
+                BitVecSorts[len(keys) * 256],
+                BitVecSort256,
+            )
+            new_storage = Store(ex.storage[addr][slot][len(keys)], concat(keys), val)
+            ex.solver.add(new_storage_var == new_storage)
+            ex.storage[addr][slot][len(keys)] = new_storage_var
+            ex.storages[new_storage_var] = new_storage
+
+    @classmethod
+    def decode(cls, loc: Any) -> Any:
+        loc = cls.normalize(loc)
+        if loc.decl().name() == "sha3_512":  # m[k] : hash(k.m)
+            args = loc.arg(0)
+            offset = simplify(Extract(511, 256, args))
+            base = simplify(Extract(255, 0, args))
+            return cls.decode(base) + (offset, con(0))
+        elif loc.decl().name() == "sha3_256":  # a[i] : hash(a)+i
+            base = loc.arg(0)
+            return cls.decode(base) + (con(0),)
+        elif loc.decl().name() == "bvadd":
+            #   # when len(args) == 2
+            #   arg0 = cls.decode(loc.arg(0))
+            #   arg1 = cls.decode(loc.arg(1))
+            #   if len(arg0) == 1 and len(arg1) > 1: # i + hash(x)
+            #       return arg1[0:-1] + (arg1[-1] + arg0[0],)
+            #   elif len(arg0) > 1 and len(arg1) == 1: # hash(x) + i
+            #       return arg0[0:-1] + (arg0[-1] + arg1[0],)
+            #   elif len(arg0) == 1 and len(arg1) == 1: # i + j
+            #       return (arg0[0] + arg1[0],)
+            #   else: # hash(x) + hash(y) # ambiguous
+            #       raise ValueError(loc)
+            # when len(args) >= 2
+            args = loc.children()
+            if len(args) < 2:
+                raise ValueError(loc)
+            args = sorted(map(cls.decode, args), key=lambda x: len(x), reverse=True)
+            if len(args[1]) > 1:
+                # only args[0]'s length >= 1, the others must be 1
+                raise ValueError(loc)
+            return args[0][0:-1] + (
+                reduce(lambda r, x: r + x[0], args[1:], args[0][-1]),
+            )
+        elif is_bv_value(loc):
+            (preimage, delta) = restore_precomputed_hashes(loc.as_long())
+            if preimage:  # loc == hash(preimage) + delta
+                return (con(preimage), con(delta))
+            else:
+                return (loc,)
+        elif is_bv(loc):
+            return (loc,)
+        else:
+            raise ValueError(loc)
+
+
+class CustomStorage(Storage):
+    @classmethod
+    def empty(cls, addr: BitVecRef, loc: BitVecRef) -> ArrayRef:
+        return Array(
+            f"storage_{id_str(addr)}_{loc.size()}_00",
+            BitVecSorts[loc.size()],
+            BitVecSort256,
+        )
+
+    @classmethod
+    def init(cls, ex: Exec, addr: Any, loc: BitVecRef) -> None:
+        assert_address(addr)
+        if loc.size() not in ex.storage[addr]:
+            ex.storage[addr][loc.size()] = cls.empty(addr, loc)
+
+    @classmethod
+    def load(cls, ex: Exec, addr: Any, loc: Word) -> Word:
+        loc = cls.decode(loc)
+        cls.init(ex, addr, loc)
+        if not ex.symbolic:
+            # generate emptyness axiom for each array index, instead of using quantified formula; see init()
+            ex.solver.add(Select(cls.empty(addr, loc), loc) == con(0))
+        return ex.select(ex.storage[addr][loc.size()], loc, ex.storages)
+
+    @classmethod
+    def store(cls, ex: Exec, addr: Any, loc: Any, val: Any) -> None:
+        loc = cls.decode(loc)
+        cls.init(ex, addr, loc)
+        new_storage_var = Array(
+            f"storage_{id_str(addr)}_{loc.size()}_{1+len(ex.storages):>02}",
+            BitVecSorts[loc.size()],
+            BitVecSort256,
+        )
+        new_storage = Store(ex.storage[addr][loc.size()], loc, val)
+        ex.solver.add(new_storage_var == new_storage)
+        ex.storage[addr][loc.size()] = new_storage_var
+        ex.storages[new_storage_var] = new_storage
+
+    @classmethod
+    def decode(cls, loc: Any) -> Any:
+        loc = cls.normalize(loc)
+        if loc.decl().name() == "sha3_512":  # hash(hi,lo), recursively
+            args = loc.arg(0)
+            hi = cls.decode(simplify(Extract(511, 256, args)))
+            lo = cls.decode(simplify(Extract(255, 0, args)))
+            return cls.simple_hash(Concat(hi, lo))
+        elif loc.decl().name().startswith("sha3_"):
+            return cls.simple_hash(cls.decode(loc.arg(0)))
+        elif loc.decl().name() == "bvadd":
+            args = loc.children()
+            if len(args) < 2:
+                raise ValueError(loc)
+            return cls.add_all([cls.decode(arg) for arg in args])
+        elif is_bv_value(loc):
+            (preimage, delta) = restore_precomputed_hashes(loc.as_long())
+            if preimage:  # loc == hash(preimage) + delta
+                return cls.add_all([cls.simple_hash(con(preimage)), con(delta)])
+            else:
+                return loc
+        elif is_bv(loc):
+            return loc
+        else:
+            raise ValueError(loc)
+
+    @classmethod
+    def simple_hash(cls, x: BitVecRef) -> BitVecRef:
+        # simple injective function for collision-free (though not secure) hash semantics, comprising:
+        # - left-shift by 256 bits to ensure sufficient logical domain space
+        # - an additional 1-bit for disambiguation (e.g., between map[key] vs array[i][j])
+        return simplify(Concat(x, con(0, 257)))
+
+    @classmethod
+    def add_all(cls, args: List) -> BitVecRef:
+        bitsize = max([x.size() for x in args])
+        res = con(0, bitsize)
+        for x in args:
+            if x.size() < bitsize:
+                x = simplify(ZeroExt(bitsize - x.size(), x))
+            res += x
+        return simplify(res)
+
+
 #             x  == b   if sort(x) = bool
 # int_to_bool(x) == b   if sort(x) = int
 def test(x: Word, b: bool) -> Word:
@@ -1407,6 +1492,20 @@ def arith2(self, ex: Exec, op: int, w1: Word, w2: Word, w3: Word) -> Word:
         else:
             raise ValueError(op)
 
+    def sload(self, ex: Exec, addr: Any, loc: Word) -> Word:
+        if self.options["custom_storage_layout"]:
+            return CustomStorage.load(ex, addr, loc)
+        else:
+            return SolidityStorage.load(ex, addr, loc)
+
+    def sstore(self, ex: Exec, addr: Any, loc: Any, val: Any) -> None:
+        if is_bool(val):
+            val = If(val, con(1), con(0))
+        if self.options["custom_storage_layout"]:
+            CustomStorage.store(ex, addr, loc, val)
+        else:
+            SolidityStorage.store(ex, addr, loc, val)
+
     def resolve_address_alias(self, ex: Exec, target: Address) -> Address:
         if target in ex.code:
             return target
@@ -1648,8 +1747,15 @@ def call_unknown() -> None:
                 ret = None
 
             # TODO: cover other precompiled
-            if eq(to, con_addr(1)):  # ecrecover exit code is always 1
+
+            # ecrecover
+            if eq(to, con_addr(1)):
+                ex.solver.add(exit_code_var != con(0))
+
+            # identity
+            if eq(to, con_addr(4)):
                 ex.solver.add(exit_code_var != con(0))
+                ret = arg
 
             # TODO: factor out cheatcode semantics
             # halmos cheat code
@@ -1802,7 +1908,7 @@ def call_unknown() -> None:
                     store_value = simplify(Extract(255, 0, arg))
                     store_account_addr = self.resolve_address_alias(ex, store_account)
                     if store_account_addr is not None:
-                        ex.sstore(store_account_addr, store_slot, store_value)
+                        self.sstore(ex, store_account_addr, store_slot, store_value)
                     else:
                         ex.error = f"uninitialized account: {store_account}"
                         out.append(ex)
@@ -1816,7 +1922,7 @@ def call_unknown() -> None:
                     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 = ex.sload(load_account_addr, load_slot)
+                        ret = self.sload(ex, load_account_addr, load_slot)
                     else:
                         ex.error = f"uninitialized account: {load_account}"
                         out.append(ex)
@@ -1950,6 +2056,7 @@ def call_unknown() -> None:
         if (
             # precompile
             eq(to, con_addr(1))
+            or eq(to, con_addr(4))
             # cheatcode calls
             or eq(to, halmos_cheat_code.address)
             or eq(to, hevm_cheat_code.address)
@@ -2512,9 +2619,9 @@ def run(self, ex0: Exec) -> Tuple[List[Exec], Steps]:
                     ex.st.push(con(size))
 
                 elif opcode == EVM.SLOAD:
-                    ex.st.push(ex.sload(ex.this, ex.st.pop()))
+                    ex.st.push(self.sload(ex, ex.this, ex.st.pop()))
                 elif opcode == EVM.SSTORE:
-                    ex.sstore(ex.this, ex.st.pop(), ex.st.pop())
+                    self.sstore(ex, ex.this, ex.st.pop(), ex.st.pop())
 
                 elif opcode == EVM.RETURNDATASIZE:
                     ex.st.push(con(ex.returndatasize()))
diff --git a/tests/expected/all.json b/tests/expected/all.json
index 294c5abb..43419621 100644
--- a/tests/expected/all.json
+++ b/tests/expected/all.json
@@ -182,6 +182,7 @@
                 "name": "check_alias_1(address,uint256)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -190,6 +191,7 @@
                 "name": "check_alias_1a(bool,address,uint256)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -198,6 +200,7 @@
                 "name": "check_alias_2(address,uint256)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -206,6 +209,7 @@
                 "name": "check_alias_2a(bool,address,uint256)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -214,6 +218,7 @@
                 "name": "check_alias_3(address,uint256)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -222,6 +227,7 @@
                 "name": "check_alias_3a(bool,address,uint256)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -590,7 +596,7 @@
         "test/Getter.t.sol:GetterTest": [
             {
                 "name": "check_Getter(uint256)",
-                "exitcode": 1,
+                "exitcode": 0,
                 "num_models": 0,
                 "models": null,
                 "num_paths": null,
@@ -1116,6 +1122,7 @@
                 "name": "check_send(address,uint256,address,uint256)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -1191,6 +1198,7 @@
                 "name": "check_ecrecover(bytes32,uint8,bytes32,bytes32)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -1199,6 +1207,7 @@
                 "name": "check_isValidERC1271SignatureNow(bytes32,bytes)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -1207,6 +1216,7 @@
                 "name": "check_isValidSignatureNow(bytes32,bytes)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -1215,6 +1225,7 @@
                 "name": "check_tryRecover(address,bytes32,bytes)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -1242,6 +1253,17 @@
                 "num_bounded_loops": null
             }
         ],
+        "test/SmolWETH.t.sol:SmolWETHTest": [
+            {
+                "name": "check_deposit_once(address,uint256)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            }
+        ],
         "test/Solver.t.sol:SolverTest": [
             {
                 "name": "check_foo(uint256,uint256)",
@@ -1309,6 +1331,17 @@
                 "num_bounded_loops": null
             }
         ],
+        "test/Storage2.t.sol:Storage2Test": [
+            {
+                "name": "check_set((uint256,uint256,uint256,uint256,uint256,uint256,uint256,uint256,uint256,uint256,uint256,uint256,uint256,uint256,uint256,uint256,uint256,uint256,uint256,uint256,uint32,uint256,uint32,uint256,uint32,uint256,uint32,uint256,uint32,uint32,uint256,uint32,uint32,uint256,uint32,uint32,uint256,uint32,uint32,uint256,uint256,uint32,uint256,uint256,uint32,uint256,uint256,uint32,uint256,uint256,uint32,uint256,uint32,uint256,uint256,uint32,uint256,uint256,uint32,uint256,uint256,uint32,uint256,uint256,uint32,uint256,uint32,uint256,uint32,uint256,uint32,uint256,uint32,uint256,uint32,uint256,uint32,uint256,uint32,uint256))",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            }
+        ],
         "test/Store.t.sol:StoreTest": [
             {
                 "name": "check_store_Array(uint256,uint256)",
@@ -1405,6 +1438,7 @@
                 "name": "check_unknown_call(address,uint256,uint256)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -1413,6 +1447,7 @@
                 "name": "check_unknown_common_callbacks(address)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -1421,6 +1456,7 @@
                 "name": "check_unknown_not_allowed(address)",
                 "exitcode": 1,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -1429,6 +1465,7 @@
                 "name": "check_unknown_retsize_0(address)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -1437,6 +1474,7 @@
                 "name": "check_unknown_retsize_64(address)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -1445,6 +1483,7 @@
                 "name": "check_unknown_retsize_default(address)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -1453,6 +1492,7 @@
                 "name": "check_unknown_send(address,uint256,uint256)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -1461,6 +1501,7 @@
                 "name": "check_unknown_send_fail(address)",
                 "exitcode": 1,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -1469,6 +1510,7 @@
                 "name": "check_unknown_transfer(address,uint256,uint256)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -1573,4 +1615,4 @@
             }
         ]
     }
-}
+}
\ No newline at end of file
diff --git a/tests/expected/erc20.json b/tests/expected/erc20.json
index 04904aac..2bd2a5de 100644
--- a/tests/expected/erc20.json
+++ b/tests/expected/erc20.json
@@ -1,11 +1,41 @@
 {
     "exitcode": 1,
     "test_results": {
+        "test/CurveTokenV3.t.sol:CurveTokenV3Test": [
+            {
+                "name": "check_NoBackdoor(bytes4,address,address)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_transfer(address,address,address,uint256)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_transferFrom(address,address,address,address,uint256)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            }
+        ],
         "test/DEIStablecoin.t.sol:DEIStablecoinTest": [
             {
                 "name": "check_NoBackdoor(bytes4,address,address)",
                 "exitcode": 1,
                 "num_models": 1,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -14,6 +44,7 @@
                 "name": "check_transfer(address,address,address,uint256)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -22,6 +53,7 @@
                 "name": "check_transferFrom(address,address,address,address,uint256)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -32,6 +64,36 @@
                 "name": "check_NoBackdoor(bytes4,address,address)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_transfer(address,address,address,uint256)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_transferFrom(address,address,address,address,uint256)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            }
+        ],
+        "test/SoladyERC20.t.sol:SoladyERC20Test": [
+            {
+                "name": "check_NoBackdoor(bytes4,address,address)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -40,6 +102,7 @@
                 "name": "check_transfer(address,address,address,uint256)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -48,6 +111,7 @@
                 "name": "check_transferFrom(address,address,address,address,uint256)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -58,6 +122,7 @@
                 "name": "check_NoBackdoor(bytes4,address,address)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -66,6 +131,7 @@
                 "name": "check_transfer(address,address,address,uint256)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -74,6 +140,7 @@
                 "name": "check_transferFrom(address,address,address,address,uint256)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
diff --git a/tests/expected/erc721.json b/tests/expected/erc721.json
index 5239c747..e960329b 100644
--- a/tests/expected/erc721.json
+++ b/tests/expected/erc721.json
@@ -6,6 +6,7 @@
                 "name": "check_NoBackdoor(bytes4)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -14,6 +15,27 @@
                 "name": "check_transferFrom(address,address,address,address,uint256,uint256)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            }
+        ],
+        "test/SoladyERC721.t.sol:SoladyERC721Test": [
+            {
+                "name": "check_NoBackdoor(bytes4)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_transferFrom(address,address,address,address,uint256,uint256)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -24,6 +46,7 @@
                 "name": "check_NoBackdoor(bytes4)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
@@ -32,6 +55,7 @@
                 "name": "check_transferFrom(address,address,address,address,uint256,uint256)",
                 "exitcode": 0,
                 "num_models": 0,
+                "models": null,
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
diff --git a/tests/lib/solady b/tests/lib/solady
new file mode 160000
index 00000000..4d4a7572
--- /dev/null
+++ b/tests/lib/solady
@@ -0,0 +1 @@
+Subproject commit 4d4a7572ad01e84e96370e42bd10d1cc16c1fb65
diff --git a/tests/test/Getter.t.sol b/tests/test/Getter.t.sol
index e0e2b339..fb7c7214 100644
--- a/tests/test/Getter.t.sol
+++ b/tests/test/Getter.t.sol
@@ -3,11 +3,12 @@ pragma solidity >=0.8.0 <0.9.0;
 
 // from https://github.com/a16z/halmos/issues/82
 
+/// @custom:halmos --custom-storage-layout
 contract GetterTest {
     uint256[3] v;
     uint w;
 
     function check_Getter(uint256 i) public view {
-        assert(v[i] >= 0); // unsupported static storage arrays
+        assert(v[i] >= 0);
     }
 }
diff --git a/tests/test/SmolWETH.t.sol b/tests/test/SmolWETH.t.sol
new file mode 100644
index 00000000..253811ac
--- /dev/null
+++ b/tests/test/SmolWETH.t.sol
@@ -0,0 +1,61 @@
+// SPDX-License-Identifier: AGPL-3.0
+pragma solidity >=0.8.0 <0.9.0;
+
+import "forge-std/Test.sol";
+import {SymTest} from "halmos-cheatcodes/SymTest.sol";
+
+contract Dummy {}
+
+/// @notice don't use, this is very buggy on purpose
+contract SmolWETH {
+    function deposit() external payable {
+        // bug: we stomp any existing balance
+        assembly {
+            sstore(caller(), callvalue())
+        }
+    }
+
+    function withdraw(uint256) external {
+        assembly {
+            // revert if msg.value > 0
+            if gt(callvalue(), 0) {
+                revert(0, 0)
+            }
+
+            let amount := sload(caller())
+            let success := call(gas(), caller(), amount, 0, 0, 0, 0)
+
+            // bug: we always erase the balance, regardless of transfer success
+            // bug: we should erase the balance before making the call
+            sstore(caller(), 0)
+        }
+    }
+
+    function balanceOf(address account) external view returns (uint256) {
+        assembly {
+            mstore(0, sload(account))
+            return(0, 0x20)
+        }
+    }
+}
+
+/// @custom:halmos --custom-storage-layout
+contract SmolWETHTest is Test, SymTest {
+    SmolWETH weth;
+
+    function setUp() public {
+        weth = new SmolWETH();
+    }
+
+    function check_deposit_once(address alice, uint256 amount) external {
+        // fund alice
+        vm.deal(alice, amount);
+
+        // alice deposits
+        vm.prank(alice);
+        weth.deposit{value: amount}();
+
+        // alice's balance is updated
+        assertEq(weth.balanceOf(alice), amount);
+    }
+}
diff --git a/tests/test/Storage2.t.sol b/tests/test/Storage2.t.sol
new file mode 100644
index 00000000..f1b66a09
--- /dev/null
+++ b/tests/test/Storage2.t.sol
@@ -0,0 +1,246 @@
+// SPDX-License-Identifier: AGPL-3.0
+pragma solidity >=0.8.0 <0.9.0;
+
+import "forge-std/Test.sol";
+
+contract Storage {
+    struct Tuple1 {
+        uint x;
+    }
+
+    struct Tuple2 {
+        uint y;
+        uint z;
+    }
+
+    // m[k].f: #(k.m)+f                         km.f
+    mapping (uint => uint) public map1_uint;
+    mapping (uint => Tuple1) public map1_tuple1;
+    mapping (uint => Tuple2) public map1_tuple2;
+
+    // m[k][l].f: #(l.#(k.m))+f                 lkm.0.f
+    mapping (uint => mapping (uint => uint)) public map2_uint;
+    mapping (uint => mapping (uint => Tuple1)) public map2_tuple1;
+    mapping (uint => mapping (uint => Tuple2)) public map2_tuple2;
+
+    // a[i].f: #(a)+i*n+f                       a._
+    uint[] public arr1_uint;
+    Tuple1[] public arr1_tuple1;
+    Tuple2[] public arr1_tuple2;
+
+    // a[i][j].f: #(#(a)+i)+j*n+f               a.i._
+    uint[][] public arr2_uint;
+    Tuple1[][] public arr2_tuple1;
+    Tuple2[][] public arr2_tuple2;
+
+    // m[k][i].f: #(#(k.m))+i*n+f               km.0._
+    mapping (uint => uint[]) public map1_arr1_uint;
+    mapping (uint => Tuple1[]) public map1_arr1_tuple1;
+    mapping (uint => Tuple2[]) public map1_arr1_tuple2;
+
+    // a[i][k].f: #(k.(#(a)+i))+f               ka.i.f
+    mapping (uint => uint)[] public arr1_map1_uint;
+    mapping (uint => Tuple1)[] public arr1_map1_tuple1;
+    mapping (uint => Tuple2)[] public arr1_map1_tuple2;
+
+    // a[i][k][j].f: #(#(k.(#(a)+i)))+j*n+f     ka.i.0._
+    mapping (uint => uint[])[] public arr1_map1_arr1_uint;
+    mapping (uint => Tuple1[])[] public arr1_map1_arr1_tuple1;
+    mapping (uint => Tuple2[])[] public arr1_map1_arr1_tuple2;
+
+    constructor () { }
+
+    function maxsize_arr1() public {
+        assembly {
+            sstore(arr1_uint.slot, not(0))
+            sstore(arr1_tuple1.slot, not(0))
+            sstore(arr1_tuple2.slot, not(0))
+        }
+    }
+
+    function maxsize_arr2() public {
+        assembly {
+            sstore(arr2_uint.slot, not(0))
+            sstore(arr2_tuple1.slot, not(0))
+            sstore(arr2_tuple2.slot, not(0))
+        }
+    }
+
+    function maxsize_arr2(uint i) public {
+        uint[]   storage arr2_uint_i   = arr2_uint[i];
+        Tuple1[] storage arr2_tuple1_i = arr2_tuple1[i];
+        Tuple2[] storage arr2_tuple2_i = arr2_tuple2[i];
+        assembly {
+            sstore(arr2_uint_i.slot, not(0))
+            sstore(arr2_tuple1_i.slot, not(0))
+            sstore(arr2_tuple2_i.slot, not(0))
+        }
+    }
+
+    function maxsize_map1_arr1(uint k) public {
+        uint[]   storage map1_arr1_uint_k   = map1_arr1_uint[k];
+        Tuple1[] storage map1_arr1_tuple1_k = map1_arr1_tuple1[k];
+        Tuple2[] storage map1_arr1_tuple2_k = map1_arr1_tuple2[k];
+        assembly {
+            sstore(map1_arr1_uint_k.slot, not(0))
+            sstore(map1_arr1_tuple1_k.slot, not(0))
+            sstore(map1_arr1_tuple2_k.slot, not(0))
+        }
+    }
+
+    function maxsize_arr1_map1() public {
+        assembly {
+            sstore(arr1_map1_uint.slot, not(0))
+            sstore(arr1_map1_tuple1.slot, not(0))
+            sstore(arr1_map1_tuple2.slot, not(0))
+        }
+    }
+
+    function maxsize_arr1_map1_arr1() public {
+        assembly {
+            sstore(arr1_map1_arr1_uint.slot, not(0))
+            sstore(arr1_map1_arr1_tuple1.slot, not(0))
+            sstore(arr1_map1_arr1_tuple2.slot, not(0))
+        }
+    }
+
+    function maxsize_arr1_map1_arr1(uint i, uint k) public {
+        uint[]   storage arr1_map1_arr1_uint_i_k   = arr1_map1_arr1_uint[i][k];
+        Tuple1[] storage arr1_map1_arr1_tuple1_i_k = arr1_map1_arr1_tuple1[i][k];
+        Tuple2[] storage arr1_map1_arr1_tuple2_i_k = arr1_map1_arr1_tuple2[i][k];
+        assembly {
+            sstore(arr1_map1_arr1_uint_i_k.slot, not(0))
+            sstore(arr1_map1_arr1_tuple1_i_k.slot, not(0))
+            sstore(arr1_map1_arr1_tuple2_i_k.slot, not(0))
+        }
+    }
+}
+
+contract Storage2Test is Storage, Test {
+    struct Param {
+        uint k11; uint v11;
+        uint k12; uint v12;
+        uint k13; uint v13;
+        uint k14; uint v14;
+
+        uint k21; uint l21; uint v21;
+        uint k22; uint l22; uint v22;
+        uint k23; uint l23; uint v23;
+        uint k24; uint l24; uint v24;
+
+        uint32 i31; uint v31;
+        uint32 i32; uint v32;
+        uint32 i33; uint v33;
+        uint32 i34; uint v34;
+
+        uint32 i41; uint32 j41; uint v41;
+        uint32 i42; uint32 j42; uint v42;
+        uint32 i43; uint32 j43; uint v43;
+        uint32 i44; uint32 j44; uint v44;
+
+        uint k51; uint32 i51; uint v51;
+        uint k52; uint32 i52; uint v52;
+        uint k53; uint32 i53; uint v53;
+        uint k54; uint32 i54; uint v54;
+
+        uint32 i61; uint k61; uint v61;
+        uint32 i62; uint k62; uint v62;
+        uint32 i63; uint k63; uint v63;
+        uint32 i64; uint k64; uint v64;
+
+        uint32 i71; uint k71; uint32 j71; uint v71;
+        uint32 i72; uint k72; uint32 j72; uint v72;
+        uint32 i73; uint k73; uint32 j73; uint v73;
+        uint32 i74; uint k74; uint32 j74; uint v74;
+    }
+
+    function check_set(Param memory p) public {
+        map1_uint  [p.k11]   = p.v11;
+        map1_tuple1[p.k12].x = p.v12;
+        map1_tuple2[p.k13].y = p.v13;
+        map1_tuple2[p.k14].z = p.v14;
+
+        map2_uint  [p.k21][p.l21]   = p.v21;
+        map2_tuple1[p.k22][p.l22].x = p.v22;
+        map2_tuple2[p.k23][p.l23].y = p.v23;
+        map2_tuple2[p.k24][p.l24].z = p.v24;
+
+        maxsize_arr1();
+        arr1_uint  [p.i31]   = p.v31;
+        arr1_tuple1[p.i32].x = p.v32;
+        arr1_tuple2[p.i33].y = p.v33;
+        arr1_tuple2[p.i34].z = p.v34;
+
+        maxsize_arr2();
+        maxsize_arr2(p.i41);
+        maxsize_arr2(p.i42);
+        maxsize_arr2(p.i43);
+        maxsize_arr2(p.i44);
+        arr2_uint  [p.i41][p.j41]   = p.v41;
+        arr2_tuple1[p.i42][p.j42].x = p.v42;
+        arr2_tuple2[p.i43][p.j43].y = p.v43;
+        arr2_tuple2[p.i44][p.j44].z = p.v44;
+
+        maxsize_map1_arr1(p.k51);
+        maxsize_map1_arr1(p.k52);
+        maxsize_map1_arr1(p.k53);
+        maxsize_map1_arr1(p.k54);
+        map1_arr1_uint  [p.k51][p.i51]   = p.v51;
+        map1_arr1_tuple1[p.k52][p.i52].x = p.v52;
+        map1_arr1_tuple2[p.k53][p.i53].y = p.v53;
+        map1_arr1_tuple2[p.k54][p.i54].z = p.v54;
+
+        maxsize_arr1_map1();
+        arr1_map1_uint  [p.i61][p.k61]   = p.v61;
+        arr1_map1_tuple1[p.i62][p.k62].x = p.v62;
+        arr1_map1_tuple2[p.i63][p.k63].y = p.v63;
+        arr1_map1_tuple2[p.i64][p.k64].z = p.v64;
+
+        maxsize_arr1_map1_arr1();
+        maxsize_arr1_map1_arr1(p.i71, p.k71);
+        maxsize_arr1_map1_arr1(p.i72, p.k72);
+        maxsize_arr1_map1_arr1(p.i73, p.k73);
+        maxsize_arr1_map1_arr1(p.i74, p.k74);
+        arr1_map1_arr1_uint  [p.i71][p.k71][p.j71]   = p.v71;
+        arr1_map1_arr1_tuple1[p.i72][p.k72][p.j72].x = p.v72;
+        arr1_map1_arr1_tuple2[p.i73][p.k73][p.j73].y = p.v73;
+        arr1_map1_arr1_tuple2[p.i74][p.k74][p.j74].z = p.v74;
+
+        //
+
+        assert(map1_uint  [p.k11]   == p.v11);
+        assert(map1_tuple1[p.k12].x == p.v12);
+        assert(map1_tuple2[p.k13].y == p.v13);
+        assert(map1_tuple2[p.k14].z == p.v14);
+
+        assert(map2_uint  [p.k21][p.l21]   == p.v21);
+        assert(map2_tuple1[p.k22][p.l22].x == p.v22);
+        assert(map2_tuple2[p.k23][p.l23].y == p.v23);
+        assert(map2_tuple2[p.k24][p.l24].z == p.v24);
+
+        assert(arr1_uint  [p.i31]   == p.v31);
+        assert(arr1_tuple1[p.i32].x == p.v32);
+        assert(arr1_tuple2[p.i33].y == p.v33);
+        assert(arr1_tuple2[p.i34].z == p.v34);
+
+        assert(arr2_uint  [p.i41][p.j41]   == p.v41);
+        assert(arr2_tuple1[p.i42][p.j42].x == p.v42);
+        assert(arr2_tuple2[p.i43][p.j43].y == p.v43);
+        assert(arr2_tuple2[p.i44][p.j44].z == p.v44);
+
+        assert(map1_arr1_uint  [p.k51][p.i51]   == p.v51);
+        assert(map1_arr1_tuple1[p.k52][p.i52].x == p.v52);
+        assert(map1_arr1_tuple2[p.k53][p.i53].y == p.v53);
+        assert(map1_arr1_tuple2[p.k54][p.i54].z == p.v54);
+
+        assert(arr1_map1_uint  [p.i61][p.k61]   == p.v61);
+        assert(arr1_map1_tuple1[p.i62][p.k62].x == p.v62);
+        assert(arr1_map1_tuple2[p.i63][p.k63].y == p.v63);
+        assert(arr1_map1_tuple2[p.i64][p.k64].z == p.v64);
+
+        assert(arr1_map1_arr1_uint  [p.i71][p.k71][p.j71]   == p.v71);
+        assert(arr1_map1_arr1_tuple1[p.i72][p.k72][p.j72].x == p.v72);
+        assert(arr1_map1_arr1_tuple2[p.i73][p.k73][p.j73].y == p.v73);
+        assert(arr1_map1_arr1_tuple2[p.i74][p.k74][p.j74].z == p.v74);
+    }
+}