diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index 4d3a9d4d8..db06a2307 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -99,7 +99,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        backend: ['legacy', 'booster']
+        backend: ['booster']
     timeout-minutes: 180
     steps:
       - name: 'Check out code'
diff --git a/package/version b/package/version
index 98eb27154..5076ee806 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.124
+0.1.125
diff --git a/pyproject.toml b/pyproject.toml
index a09d47f1f..64fb90e99 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.124"
+version = "0.1.125"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py
index b76b1c3ee..d5354c218 100644
--- a/src/kontrol/__init__.py
+++ b/src/kontrol/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.124'
+VERSION: Final = '0.1.125'
diff --git a/src/tests/integration/test-data/contracts.k.expected b/src/tests/integration/test-data/contracts.k.expected
index 9d5a91bd1..1df322a9c 100644
--- a/src/tests/integration/test-data/contracts.k.expected
+++ b/src/tests/integration/test-data/contracts.k.expected
@@ -577,7 +577,7 @@ module S2KtestZModAllowChangesTest-CONTRACT
     
       
     
-    rule  ( #initBytecode ( S2KtestZModAllowChangesTest ) => #parseByteStack ( "0x608060405260078054600160ff199182168117909255600b8054909116909117905534801561002d57600080fd5b506113288061003d6000396000f3fe608060405234801561001057600080fd5b50600436106101005760003560e01c8063b5508aa911610097578063e20c9f7111610066578063e20c9f71146101de578063f6243db1146101e6578063f8a8fd6d146101ee578063fa7626d4146101f657600080fd5b8063b5508aa914610177578063ba414fa61461017f578063d6a2ec7614610197578063dc20bc5b146101d657600080fd5b80635b31d527116100d35780635b31d5271461013d57806366d9a9a01461014557806385226c811461015a578063916a17c61461016f57600080fd5b80631ed7831c146101055780633e5e3c23146101235780633f7286f41461012b5780634b453a5914610133575b600080fd5b61010d610203565b60405161011a9190610f9c565b60405180910390f35b61010d610265565b61010d6102c5565b61013b610325565b005b61013b6104c1565b61014d61062b565b60405161011a9190610fe9565b61016261071a565b60405161011a91906110cc565b61014d6107ea565b6101626108d0565b6101876109a0565b604051901515815260200161011a565b6101be7f885cb69240a935d632d79c317109709ecfa91a80626ff3989d68f67f5b1dd12d81565b6040516001600160a01b03909116815260200161011a565b61013b610acd565b61010d610c36565b61013b610c96565b61013b610e01565b6007546101879060ff1681565b6060601480548060200260200160405190810160405280929190818152602001828054801561025b57602002820191906000526020600020905b81546001600160a01b0316815260019091019060200180831161023d575b5050505050905090565b6060601680548060200260200160405190810160405280929190818152602001828054801561025b576020028201919060005260206000209081546001600160a01b0316815260019091019060200180831161023d575050505050905090565b6060601580548060200260200160405190810160405280929190818152602001828054801561025b576020028201919060005260206000209081546001600160a01b0316815260019091019060200180831161023d575050505050905090565b600060405161033390610f90565b604051809103906000f08015801561034f573d6000803e3d6000fd5b509050600060405161036090610f90565b604051809103906000f08015801561037c573d6000803e3d6000fd5b50604051631b94398d60e21b81526001600160a01b0384166004820152909150737109709ecfa91a80626ff3989d68f67f5b1dd12d90636e50e63490602401600060405180830381600087803b1580156103d557600080fd5b505af11580156103e9573d6000803e3d6000fd5b5050604051633eb205c360e21b81526001600160a01b038516600482015260006024820152737109709ecfa91a80626ff3989d68f67f5b1dd12d925063fac8170c9150604401600060405180830381600087803b15801561044957600080fd5b505af115801561045d573d6000803e3d6000fd5b505060405163616b8d0560e01b815261280560048201526001600160a01b038416925063616b8d0591506024015b600060405180830381600087803b1580156104a557600080fd5b505af11580156104b9573d6000803e3d6000fd5b505050505050565b60006040516104cf90610f90565b604051809103906000f0801580156104eb573d6000803e3d6000fd5b50905060006040516104fc90610f90565b604051809103906000f080158015610518573d6000803e3d6000fd5b50604051631b94398d60e21b81526001600160a01b0384166004820152909150737109709ecfa91a80626ff3989d68f67f5b1dd12d90636e50e63490602401600060405180830381600087803b15801561057157600080fd5b505af1158015610585573d6000803e3d6000fd5b5050604051633eb205c360e21b81526001600160a01b038516600482015260006024820152737109709ecfa91a80626ff3989d68f67f5b1dd12d925063fac8170c9150604401600060405180830381600087803b1580156105e557600080fd5b505af11580156105f9573d6000803e3d6000fd5b5050604051630af33d5360e11b8152615b9c60048201526001600160a01b03851692506315e67aa6915060240161048b565b60606019805480602002602001604051908101604052809291908181526020016000905b828210156107115760008481526020908190206040805180820182526002860290920180546001600160a01b031683526001810180548351818702810187019094528084529394919385830193928301828280156106f957602002820191906000526020600020906000905b82829054906101000a900460e01b6001600160e01b031916815260200190600401906020826003010492830192600103820291508084116106bb5790505b5050505050815250508152602001906001019061064f565b50505050905090565b60606018805480602002602001604051908101604052809291908181526020016000905b8282101561071157838290600052602060002001805461075d90611146565b80601f016020809104026020016040519081016040528092919081815260200182805461078990611146565b80156107d65780601f106107ab576101008083540402835291602001916107d6565b820191906000526020600020905b8154815290600101906020018083116107b957829003601f168201915b50505050508152602001906001019061073e565b6060601a805480602002602001604051908101604052809291908181526020016000905b828210156107115760008481526020908190206040805180820182526002860290920180546001600160a01b031683526001810180548351818702810187019094528084529394919385830193928301828280156108b857602002820191906000526020600020906000905b82829054906101000a900460e01b6001600160e01b0319168152602001906004019060208260030104928301926001038202915080841161087a5790505b5050505050815250508152602001906001019061080e565b60606017805480602002602001604051908101604052809291908181526020016000905b8282101561071157838290600052602060002001805461091390611146565b80601f016020809104026020016040519081016040528092919081815260200182805461093f90611146565b801561098c5780601f106109615761010080835404028352916020019161098c565b820191906000526020600020905b81548152906001019060200180831161096f57829003601f168201915b5050505050815260200190600101906108f4565b600754600090610100900460ff16156109c25750600754610100900460ff1690565b6000737109709ecfa91a80626ff3989d68f67f5b1dd12d3b15610ac85760408051737109709ecfa91a80626ff3989d68f67f5b1dd12d602082018190526519985a5b195960d21b82840152825180830384018152606083019093526000929091610a50917f667f9d70ca411d70ead50d8d5c22070dafc36ad75f3dcf5e7237b22ade9aecc491608001611180565b60408051601f1981840301815290829052610a6a916111b1565b6000604051808303816000865af19150503d8060008114610aa7576040519150601f19603f3d011682016040523d82523d6000602084013e610aac565b606091505b5091505080806020019051810190610ac491906111cd565b9150505b919050565b6000604051610adb90610f90565b604051809103906000f080158015610af7573d6000803e3d6000fd5b5090506000604051610b0890610f90565b604051809103906000f080158015610b24573d6000803e3d6000fd5b50604051631b94398d60e21b81526001600160a01b0384166004820152909150737109709ecfa91a80626ff3989d68f67f5b1dd12d90636e50e63490602401600060405180830381600087803b158015610b7d57600080fd5b505af1158015610b91573d6000803e3d6000fd5b5050604051633eb205c360e21b81526001600160a01b038516600482015260006024820152737109709ecfa91a80626ff3989d68f67f5b1dd12d925063fac8170c9150604401600060405180830381600087803b158015610bf157600080fd5b505af1158015610c05573d6000803e3d6000fd5b505060405163616b8d0560e01b8152605560048201526001600160a01b038516925063616b8d05915060240161048b565b6060601380548060200260200160405190810160405280929190818152602001828054801561025b576020028201919060005260206000209081546001600160a01b0316815260019091019060200180831161023d575050505050905090565b6000604051610ca490610f90565b604051809103906000f080158015610cc0573d6000803e3d6000fd5b5090506000604051610cd190610f90565b604051809103906000f080158015610ced573d6000803e3d6000fd5b50604051631b94398d60e21b81526001600160a01b0384166004820152909150737109709ecfa91a80626ff3989d68f67f5b1dd12d90636e50e63490602401600060405180830381600087803b158015610d4657600080fd5b505af1158015610d5a573d6000803e3d6000fd5b5050604051633eb205c360e21b81526001600160a01b038516600482015260006024820152737109709ecfa91a80626ff3989d68f67f5b1dd12d925063fac8170c9150604401600060405180830381600087803b158015610dba57600080fd5b505af1158015610dce573d6000803e3d6000fd5b5050604051630af33d5360e11b81526203941960048201526001600160a01b03851692506315e67aa6915060240161048b565b610e0b6001610e0d565b565b80610e81577f41304facd9323d75b11bcdd609cb38effffdb05710f7caf0e9b16c6d9d709f50604051610e719060208082526017908201527f4572726f723a20417373657274696f6e204661696c6564000000000000000000604082015260600190565b60405180910390a1610e81610e84565b50565b737109709ecfa91a80626ff3989d68f67f5b1dd12d3b15610f7f5760408051737109709ecfa91a80626ff3989d68f67f5b1dd12d602082018190526519985a5b195960d21b9282019290925260016060820152600091907f70ca10bbd0dbfd9020a9f4b13402c16cb120705e0d1c0aeab10fa353ae586fc49060800160408051601f1981840301815290829052610f1e9291602001611180565b60408051601f1981840301815290829052610f38916111b1565b6000604051808303816000865af19150503d8060008114610f75576040519150601f19603f3d011682016040523d82523d6000602084013e610f7a565b606091505b505050505b6007805461ff001916610100179055565b60fc806111f783390190565b6020808252825182820181905260009190848201906040850190845b81811015610fdd5783516001600160a01b031683529284019291840191600101610fb8565b50909695505050505050565b60006020808301818452808551808352604092508286019150828160051b8701018488016000805b8481101561108d57898403603f19018652825180516001600160a01b03168552880151888501889052805188860181905290890190839060608701905b808310156110785783516001600160e01b0319168252928b019260019290920191908b019061104e565b50978a01979550505091870191600101611011565b50919998505050505050505050565b60005b838110156110b757818101518382015260200161109f565b838111156110c6576000848401525b50505050565b6000602080830181845280855180835260408601915060408160051b870101925083870160005b8281101561113957878503603f190184528151805180875261111a818989018a850161109c565b601f01601f1916959095018601945092850192908501906001016110f3565b5092979650505050505050565b600181811c9082168061115a57607f821691505b60208210810361117a57634e487b7160e01b600052602260045260246000fd5b50919050565b6001600160e01b03198316815281516000906111a381600485016020870161109c565b919091016004019392505050565b600082516111c381846020870161109c565b9190910192915050565b6000602082840312156111df57600080fd5b815180151581146111ef57600080fd5b939250505056fe608060405234801561001057600080fd5b5060dd8061001f6000396000f3fe6080604052348015600f57600080fd5b506004361060465760003560e01c806315e67aa614604b5780633033413b14605d5780635d33a27f146077578063616b8d0514607f575b600080fd5b605b6056366004608f565b600155565b005b606560005481565b60405190815260200160405180910390f35b606560015481565b605b608a366004608f565b600055565b60006020828403121560a057600080fd5b503591905056fea26469706673582212206bdd86857ffc836e2336598d65d527c12a9255331ebc5651122cdc157f5648f564736f6c634300080d0033a264697066735822122041e2cd859acf91fa5a4f37c6719e05563f45fc3aa1b75b07909d7ffd1377ec9d64736f6c634300080d0033" ) )
+    rule  ( #initBytecode ( S2KtestZModAllowChangesTest ) => #parseByteStack ( "0x608060405260078054600160ff199182168117909255600b8054909116909117905534801561002d57600080fd5b506111aa8061003d6000396000f3fe608060405234801561001057600080fd5b50600436106100f55760003560e01c8063916a17c611610097578063dc20bc5b11610066578063dc20bc5b146101cb578063e20c9f71146101d3578063f8a8fd6d146101db578063fa7626d4146101e357600080fd5b8063916a17c614610164578063b5508aa91461016c578063ba414fa614610174578063d6a2ec761461018c57600080fd5b80634b453a59116100d35780634b453a59146101285780635b31d5271461013257806366d9a9a01461013a57806385226c811461014f57600080fd5b80631ed7831c146100fa5780633e5e3c23146101185780633f7286f414610120575b600080fd5b6101026101f0565b60405161010f9190610e1e565b60405180910390f35b610102610252565b6101026102b2565b610130610312565b005b6101306104ae565b610142610618565b60405161010f9190610e6b565b610157610707565b60405161010f9190610f4e565b6101426107d7565b6101576108bd565b61017c61098d565b604051901515815260200161010f565b6101b37f885cb69240a935d632d79c317109709ecfa91a80626ff3989d68f67f5b1dd12d81565b6040516001600160a01b03909116815260200161010f565b610130610aba565b610102610c23565b610130610c83565b60075461017c9060ff1681565b6060601480548060200260200160405190810160405280929190818152602001828054801561024857602002820191906000526020600020905b81546001600160a01b0316815260019091019060200180831161022a575b5050505050905090565b60606016805480602002602001604051908101604052809291908181526020018280548015610248576020028201919060005260206000209081546001600160a01b0316815260019091019060200180831161022a575050505050905090565b60606015805480602002602001604051908101604052809291908181526020018280548015610248576020028201919060005260206000209081546001600160a01b0316815260019091019060200180831161022a575050505050905090565b600060405161032090610e12565b604051809103906000f08015801561033c573d6000803e3d6000fd5b509050600060405161034d90610e12565b604051809103906000f080158015610369573d6000803e3d6000fd5b50604051631b94398d60e21b81526001600160a01b0384166004820152909150737109709ecfa91a80626ff3989d68f67f5b1dd12d90636e50e63490602401600060405180830381600087803b1580156103c257600080fd5b505af11580156103d6573d6000803e3d6000fd5b5050604051633eb205c360e21b81526001600160a01b038516600482015260006024820152737109709ecfa91a80626ff3989d68f67f5b1dd12d925063fac8170c9150604401600060405180830381600087803b15801561043657600080fd5b505af115801561044a573d6000803e3d6000fd5b505060405163616b8d0560e01b815261280560048201526001600160a01b038416925063616b8d0591506024015b600060405180830381600087803b15801561049257600080fd5b505af11580156104a6573d6000803e3d6000fd5b505050505050565b60006040516104bc90610e12565b604051809103906000f0801580156104d8573d6000803e3d6000fd5b50905060006040516104e990610e12565b604051809103906000f080158015610505573d6000803e3d6000fd5b50604051631b94398d60e21b81526001600160a01b0384166004820152909150737109709ecfa91a80626ff3989d68f67f5b1dd12d90636e50e63490602401600060405180830381600087803b15801561055e57600080fd5b505af1158015610572573d6000803e3d6000fd5b5050604051633eb205c360e21b81526001600160a01b038516600482015260006024820152737109709ecfa91a80626ff3989d68f67f5b1dd12d925063fac8170c9150604401600060405180830381600087803b1580156105d257600080fd5b505af11580156105e6573d6000803e3d6000fd5b5050604051630af33d5360e11b8152615b9c60048201526001600160a01b03851692506315e67aa69150602401610478565b60606019805480602002602001604051908101604052809291908181526020016000905b828210156106fe5760008481526020908190206040805180820182526002860290920180546001600160a01b031683526001810180548351818702810187019094528084529394919385830193928301828280156106e657602002820191906000526020600020906000905b82829054906101000a900460e01b6001600160e01b031916815260200190600401906020826003010492830192600103820291508084116106a85790505b5050505050815250508152602001906001019061063c565b50505050905090565b60606018805480602002602001604051908101604052809291908181526020016000905b828210156106fe57838290600052602060002001805461074a90610fc8565b80601f016020809104026020016040519081016040528092919081815260200182805461077690610fc8565b80156107c35780601f10610798576101008083540402835291602001916107c3565b820191906000526020600020905b8154815290600101906020018083116107a657829003601f168201915b50505050508152602001906001019061072b565b6060601a805480602002602001604051908101604052809291908181526020016000905b828210156106fe5760008481526020908190206040805180820182526002860290920180546001600160a01b031683526001810180548351818702810187019094528084529394919385830193928301828280156108a557602002820191906000526020600020906000905b82829054906101000a900460e01b6001600160e01b031916815260200190600401906020826003010492830192600103820291508084116108675790505b505050505081525050815260200190600101906107fb565b60606017805480602002602001604051908101604052809291908181526020016000905b828210156106fe57838290600052602060002001805461090090610fc8565b80601f016020809104026020016040519081016040528092919081815260200182805461092c90610fc8565b80156109795780601f1061094e57610100808354040283529160200191610979565b820191906000526020600020905b81548152906001019060200180831161095c57829003601f168201915b5050505050815260200190600101906108e1565b600754600090610100900460ff16156109af5750600754610100900460ff1690565b6000737109709ecfa91a80626ff3989d68f67f5b1dd12d3b15610ab55760408051737109709ecfa91a80626ff3989d68f67f5b1dd12d602082018190526519985a5b195960d21b82840152825180830384018152606083019093526000929091610a3d917f667f9d70ca411d70ead50d8d5c22070dafc36ad75f3dcf5e7237b22ade9aecc491608001611002565b60408051601f1981840301815290829052610a5791611033565b6000604051808303816000865af19150503d8060008114610a94576040519150601f19603f3d011682016040523d82523d6000602084013e610a99565b606091505b5091505080806020019051810190610ab1919061104f565b9150505b919050565b6000604051610ac890610e12565b604051809103906000f080158015610ae4573d6000803e3d6000fd5b5090506000604051610af590610e12565b604051809103906000f080158015610b11573d6000803e3d6000fd5b50604051631b94398d60e21b81526001600160a01b0384166004820152909150737109709ecfa91a80626ff3989d68f67f5b1dd12d90636e50e63490602401600060405180830381600087803b158015610b6a57600080fd5b505af1158015610b7e573d6000803e3d6000fd5b5050604051633eb205c360e21b81526001600160a01b038516600482015260006024820152737109709ecfa91a80626ff3989d68f67f5b1dd12d925063fac8170c9150604401600060405180830381600087803b158015610bde57600080fd5b505af1158015610bf2573d6000803e3d6000fd5b505060405163616b8d0560e01b8152605560048201526001600160a01b038516925063616b8d059150602401610478565b60606013805480602002602001604051908101604052809291908181526020018280548015610248576020028201919060005260206000209081546001600160a01b0316815260019091019060200180831161022a575050505050905090565b610c8d6001610c8f565b565b80610d03577f41304facd9323d75b11bcdd609cb38effffdb05710f7caf0e9b16c6d9d709f50604051610cf39060208082526017908201527f4572726f723a20417373657274696f6e204661696c6564000000000000000000604082015260600190565b60405180910390a1610d03610d06565b50565b737109709ecfa91a80626ff3989d68f67f5b1dd12d3b15610e015760408051737109709ecfa91a80626ff3989d68f67f5b1dd12d602082018190526519985a5b195960d21b9282019290925260016060820152600091907f70ca10bbd0dbfd9020a9f4b13402c16cb120705e0d1c0aeab10fa353ae586fc49060800160408051601f1981840301815290829052610da09291602001611002565b60408051601f1981840301815290829052610dba91611033565b6000604051808303816000865af19150503d8060008114610df7576040519150601f19603f3d011682016040523d82523d6000602084013e610dfc565b606091505b505050505b6007805461ff001916610100179055565b60fc8061107983390190565b6020808252825182820181905260009190848201906040850190845b81811015610e5f5783516001600160a01b031683529284019291840191600101610e3a565b50909695505050505050565b60006020808301818452808551808352604092508286019150828160051b8701018488016000805b84811015610f0f57898403603f19018652825180516001600160a01b03168552880151888501889052805188860181905290890190839060608701905b80831015610efa5783516001600160e01b0319168252928b019260019290920191908b0190610ed0565b50978a01979550505091870191600101610e93565b50919998505050505050505050565b60005b83811015610f39578181015183820152602001610f21565b83811115610f48576000848401525b50505050565b6000602080830181845280855180835260408601915060408160051b870101925083870160005b82811015610fbb57878503603f1901845281518051808752610f9c818989018a8501610f1e565b601f01601f191695909501860194509285019290850190600101610f75565b5092979650505050505050565b600181811c90821680610fdc57607f821691505b602082108103610ffc57634e487b7160e01b600052602260045260246000fd5b50919050565b6001600160e01b0319831681528151600090611025816004850160208701610f1e565b919091016004019392505050565b60008251611045818460208701610f1e565b9190910192915050565b60006020828403121561106157600080fd5b8151801515811461107157600080fd5b939250505056fe608060405234801561001057600080fd5b5060dd8061001f6000396000f3fe6080604052348015600f57600080fd5b506004361060465760003560e01c806315e67aa614604b5780633033413b14605d5780635d33a27f146077578063616b8d0514607f575b600080fd5b605b6056366004608f565b600155565b005b606560005481565b60405190815260200160405180910390f35b606560015481565b605b608a366004608f565b600055565b60006020828403121560a057600080fd5b503591905056fea2646970667358221220e01828abfb0d8f6781a159d416a0ba0978322a001261cfd36b80c3d5a0457db764736f6c634300080d0033a26469706673582212206fe5fc046525336c4c2a748bc4c6a693fd082f9c50c3da60a53c4164d546b64364736f6c634300080d0033" ) )
       
     
     syntax Field ::= S2KtestZModAllowChangesTestField
@@ -695,8 +695,6 @@ module S2KtestZModAllowChangesTest-CONTRACT
     
     syntax S2KtestZModAllowChangesTestMethod ::= "S2KtestAllow" "(" ")" [symbol(), klabel(method_AllowChangesTest_S2KtestAllow_)]
     
-    syntax S2KtestZModAllowChangesTestMethod ::= "S2KtestAllowZUndfail" "(" ")" [symbol(), klabel(method_AllowChangesTest_S2KtestAllowZUndfail_)]
-    
     syntax S2KtestZModAllowChangesTestMethod ::= "S2KtestFailAllowCallsToAddress" "(" ")" [symbol(), klabel(method_AllowChangesTest_S2KtestFailAllowCallsToAddress_)]
     
     syntax S2KtestZModAllowChangesTestMethod ::= "S2KtestFailAllowChangesToStorage" "(" ")" [symbol(), klabel(method_AllowChangesTest_S2KtestFailAllowChangesToStorage_)]
@@ -740,9 +738,6 @@ module S2KtestZModAllowChangesTest-CONTRACT
     rule  ( S2KtestZModAllowChangesTest . S2KtestAllow ( ) => #abiCallData ( "testAllow" , .TypedArgs ) )
       
     
-    rule  ( S2KtestZModAllowChangesTest . S2KtestAllowZUndfail ( ) => #abiCallData ( "testAllow_fail" , .TypedArgs ) )
-      
-    
     rule  ( S2KtestZModAllowChangesTest . S2KtestFailAllowCallsToAddress ( ) => #abiCallData ( "testFailAllowCallsToAddress" , .TypedArgs ) )
       
     
@@ -788,9 +783,6 @@ module S2KtestZModAllowChangesTest-CONTRACT
     rule  ( selector ( "testAllow()" ) => 3693132891 )
       
     
-    rule  ( selector ( "testAllow_fail()" ) => 4129570225 )
-      
-    
     rule  ( selector ( "testFailAllowCallsToAddress()" ) => 1262828121 )
       
     
@@ -808,7 +800,7 @@ module S2KtestZModValueStore-CONTRACT
     
       
     
-    rule  ( #initBytecode ( S2KtestZModValueStore ) => #parseByteStack ( "0x608060405234801561001057600080fd5b5060dd8061001f6000396000f3fe6080604052348015600f57600080fd5b506004361060465760003560e01c806315e67aa614604b5780633033413b14605d5780635d33a27f146077578063616b8d0514607f575b600080fd5b605b6056366004608f565b600155565b005b606560005481565b60405190815260200160405180910390f35b606560015481565b605b608a366004608f565b600055565b60006020828403121560a057600080fd5b503591905056fea26469706673582212206bdd86857ffc836e2336598d65d527c12a9255331ebc5651122cdc157f5648f564736f6c634300080d0033" ) )
+    rule  ( #initBytecode ( S2KtestZModValueStore ) => #parseByteStack ( "0x608060405234801561001057600080fd5b5060dd8061001f6000396000f3fe6080604052348015600f57600080fd5b506004361060465760003560e01c806315e67aa614604b5780633033413b14605d5780635d33a27f146077578063616b8d0514607f575b600080fd5b605b6056366004608f565b600155565b005b606560005481565b60405190815260200160405180910390f35b606560015481565b605b608a366004608f565b600055565b60006020828403121560a057600080fd5b503591905056fea2646970667358221220e01828abfb0d8f6781a159d416a0ba0978322a001261cfd36b80c3d5a0457db764736f6c634300080d0033" ) )
       
     
     syntax Field ::= S2KtestZModValueStoreField
diff --git a/src/tests/integration/test-data/foundry-prove-all b/src/tests/integration/test-data/foundry-prove-all
index a253c7204..3bf983b2e 100644
--- a/src/tests/integration/test-data/foundry-prove-all
+++ b/src/tests/integration/test-data/foundry-prove-all
@@ -295,14 +295,14 @@ UintTypeTest.test_uint88_fail(uint88)
 UintTypeTest.test_uint8_fail(uint8)
 UintTypeTest.test_uint96(uint96)
 UintTypeTest.test_uint96_fail(uint96)
-IntTypeTest.testFail_uint128(uint128)
-IntTypeTest.testFail_uint256(uint256)
-IntTypeTest.testFail_uint64(uint64)
-IntTypeTest.test_uint128(uint128)
-IntTypeTest.test_uint128_fail(uint128)
-IntTypeTest.test_uint256(uint256)
-IntTypeTest.test_uint256_fail(uint256)
-IntTypeTest.test_uint64(uint64)
-IntTypeTest.test_uint64_fail(uint64)
+IntTypeTest.testFail_int128(uint128)
+IntTypeTest.testFail_int256(uint256)
+IntTypeTest.testFail_int64(uint64)
+IntTypeTest.test_int128(uint128)
+IntTypeTest.test_int128_fail(uint128)
+IntTypeTest.test_int256(uint256)
+IntTypeTest.test_int256_fail(uint256)
+IntTypeTest.test_int64(uint64)
+IntTypeTest.test_int64_fail(uint64)
 StructTypeTest.test_vars((uint8,uint32,bytes32))
 WarpTest.test_warp_setup()
\ No newline at end of file
diff --git a/src/tests/integration/test-data/foundry-prove-skip b/src/tests/integration/test-data/foundry-prove-skip
index b7246b03d..16aded8cb 100644
--- a/src/tests/integration/test-data/foundry-prove-skip
+++ b/src/tests/integration/test-data/foundry-prove-skip
@@ -10,10 +10,10 @@ AllowChangesTest.testAllow_fail()
 ArithmeticTest.test_decreasing_div(uint256,uint256)
 ArithmeticTest.test_max1_broken(uint256,uint256)
 ArithmeticTest.test_wdiv_rounding(uint256,uint256)
-ArithmeticTest.test_wmul_increasing(uint256,uint256)
 ArithmeticTest.test_wmul_increasing_gt_one(uint256,uint256)
 ArithmeticTest.test_wmul_increasing_overflow(uint256,uint256)
 ArithmeticTest.test_wmul_increasing_positive(uint256,uint256)
+ArithmeticTest.test_wmul_increasing(uint256,uint256)
 ArithmeticTest.test_wmul_rounding(uint256,uint256)
 ArithmeticTest.test_wmul_wdiv_inverse(uint256,uint256)
 ArithmeticTest.test_wmul_wdiv_inverse_underflow(uint256,uint256)
@@ -71,20 +71,29 @@ ForkTest.testRPCUrl()
 ForkTest.testRPCUrlRevert()
 GasTest.testInfiniteGas()
 GetCodeTest.testGetCode()
+IntTypeTest.testFail_int128(uint128)
+IntTypeTest.testFail_int256(uint256)
+IntTypeTest.testFail_int64(uint64)
+IntTypeTest.test_int128_fail(uint128)
+IntTypeTest.test_int128(uint128)
+IntTypeTest.test_int256_fail(uint256)
+IntTypeTest.test_int256(uint256)
+IntTypeTest.test_int64_fail(uint64)
+IntTypeTest.test_int64(uint64)
 LoopsTest.testIsNotPrime(uint256)
-LoopsTest.testIsPrime(uint256,uint256)
 LoopsTest.testIsPrimeBroken(uint256,uint256)
 LoopsTest.testIsPrimeOpt(uint256)
-LoopsTest.testMax(uint256[])
+LoopsTest.testIsPrime(uint256,uint256)
 LoopsTest.testMaxBroken(uint256[])
+LoopsTest.testMax(uint256[])
 LoopsTest.testNthPrime(uint256,uint256)
-LoopsTest.testSort(uint256[])
 LoopsTest.testSortBroken(uint256[])
+LoopsTest.testSort(uint256[])
 LoopsTest.testSqrt(uint256)
 LoopsTest.test_sum_100()
 LoopsTest.test_sum_1000()
-LoopsTest.testSumToN(uint256)
 LoopsTest.testSumToNBroken(uint256)
+LoopsTest.testSumToN(uint256)
 MockCallTest.testMockCall()
 MockCallTest.testMockCalls()
 MockCallTest.testMockCallValue()
@@ -122,9 +131,9 @@ UintTypeTest.testFail_uint128(uint128)
 UintTypeTest.testFail_uint136(uint136)
 UintTypeTest.testFail_uint144(uint144)
 UintTypeTest.testFail_uint152(uint152)
-UintTypeTest.testFail_uint16(uint16)
 UintTypeTest.testFail_uint160(uint160)
 UintTypeTest.testFail_uint168(uint168)
+UintTypeTest.testFail_uint16(uint16)
 UintTypeTest.testFail_uint176(uint176)
 UintTypeTest.testFail_uint184(uint184)
 UintTypeTest.testFail_uint192(uint192)
@@ -133,9 +142,9 @@ UintTypeTest.testFail_uint208(uint208)
 UintTypeTest.testFail_uint216(uint216)
 UintTypeTest.testFail_uint224(uint224)
 UintTypeTest.testFail_uint232(uint232)
-UintTypeTest.testFail_uint24(uint24)
 UintTypeTest.testFail_uint240(uint240)
 UintTypeTest.testFail_uint248(uint248)
+UintTypeTest.testFail_uint24(uint24)
 UintTypeTest.testFail_uint256(uint256)
 UintTypeTest.testFail_uint32(uint32)
 UintTypeTest.testFail_uint40(uint40)
@@ -143,79 +152,70 @@ UintTypeTest.testFail_uint48(uint48)
 UintTypeTest.testFail_uint56(uint56)
 UintTypeTest.testFail_uint64(uint64)
 UintTypeTest.testFail_uint72(uint72)
-UintTypeTest.testFail_uint8(uint8)
 UintTypeTest.testFail_uint80(uint80)
 UintTypeTest.testFail_uint88(uint88)
+UintTypeTest.testFail_uint8(uint8)
 UintTypeTest.testFail_uint96(uint96)
-UintTypeTest.test_uint104(uint104)
 UintTypeTest.test_uint104_fail(uint104)
-UintTypeTest.test_uint112(uint112)
+UintTypeTest.test_uint104(uint104)
 UintTypeTest.test_uint112_fail(uint112)
-UintTypeTest.test_uint120(uint120)
+UintTypeTest.test_uint112(uint112)
 UintTypeTest.test_uint120_fail(uint120)
-UintTypeTest.test_uint128(uint128)
+UintTypeTest.test_uint120(uint120)
 UintTypeTest.test_uint128_fail(uint128)
-UintTypeTest.test_uint136(uint136)
+UintTypeTest.test_uint128(uint128)
 UintTypeTest.test_uint136_fail(uint136)
-UintTypeTest.test_uint144(uint144)
+UintTypeTest.test_uint136(uint136)
 UintTypeTest.test_uint144_fail(uint144)
-UintTypeTest.test_uint152(uint152)
+UintTypeTest.test_uint144(uint144)
 UintTypeTest.test_uint152_fail(uint152)
-UintTypeTest.test_uint16(uint16)
-UintTypeTest.test_uint160(uint160)
+UintTypeTest.test_uint152(uint152)
 UintTypeTest.test_uint160_fail(uint160)
-UintTypeTest.test_uint168(uint168)
+UintTypeTest.test_uint160(uint160)
 UintTypeTest.test_uint168_fail(uint168)
+UintTypeTest.test_uint168(uint168)
 UintTypeTest.test_uint16_fail(uint16)
-UintTypeTest.test_uint176(uint176)
+UintTypeTest.test_uint16(uint16)
 UintTypeTest.test_uint176_fail(uint176)
-UintTypeTest.test_uint184(uint184)
+UintTypeTest.test_uint176(uint176)
 UintTypeTest.test_uint184_fail(uint184)
-UintTypeTest.test_uint192(uint192)
+UintTypeTest.test_uint184(uint184)
 UintTypeTest.test_uint192_fail(uint192)
-UintTypeTest.test_uint200(uint200)
+UintTypeTest.test_uint192(uint192)
 UintTypeTest.test_uint200_fail(uint200)
-UintTypeTest.test_uint208(uint208)
+UintTypeTest.test_uint200(uint200)
 UintTypeTest.test_uint208_fail(uint208)
-UintTypeTest.test_uint216(uint216)
+UintTypeTest.test_uint208(uint208)
 UintTypeTest.test_uint216_fail(uint216)
-UintTypeTest.test_uint224(uint224)
+UintTypeTest.test_uint216(uint216)
 UintTypeTest.test_uint224_fail(uint224)
-UintTypeTest.test_uint232(uint232)
+UintTypeTest.test_uint224(uint224)
 UintTypeTest.test_uint232_fail(uint232)
-UintTypeTest.test_uint24(uint24)
-UintTypeTest.test_uint240(uint240)
+UintTypeTest.test_uint232(uint232)
 UintTypeTest.test_uint240_fail(uint240)
-UintTypeTest.test_uint248(uint248)
+UintTypeTest.test_uint240(uint240)
 UintTypeTest.test_uint248_fail(uint248)
+UintTypeTest.test_uint248(uint248)
 UintTypeTest.test_uint24_fail(uint24)
+UintTypeTest.test_uint24(uint24)
 UintTypeTest.test_uint256_fail(uint256)
-UintTypeTest.test_uint32(uint32)
 UintTypeTest.test_uint32_fail(uint32)
-UintTypeTest.test_uint40(uint40)
+UintTypeTest.test_uint32(uint32)
 UintTypeTest.test_uint40_fail(uint40)
-UintTypeTest.test_uint48(uint48)
+UintTypeTest.test_uint40(uint40)
 UintTypeTest.test_uint48_fail(uint48)
-UintTypeTest.test_uint56(uint56)
+UintTypeTest.test_uint48(uint48)
 UintTypeTest.test_uint56_fail(uint56)
-UintTypeTest.test_uint64(uint64)
+UintTypeTest.test_uint56(uint56)
 UintTypeTest.test_uint64_fail(uint64)
-UintTypeTest.test_uint72(uint72)
+UintTypeTest.test_uint64(uint64)
 UintTypeTest.test_uint72_fail(uint72)
-UintTypeTest.test_uint8(uint8)
-UintTypeTest.test_uint80(uint80)
+UintTypeTest.test_uint72(uint72)
 UintTypeTest.test_uint80_fail(uint80)
-UintTypeTest.test_uint88(uint88)
+UintTypeTest.test_uint80(uint80)
 UintTypeTest.test_uint88_fail(uint88)
+UintTypeTest.test_uint88(uint88)
 UintTypeTest.test_uint8_fail(uint8)
-UintTypeTest.test_uint96(uint96)
+UintTypeTest.test_uint8(uint8)
 UintTypeTest.test_uint96_fail(uint96)
-IntTypeTest.testFail_uint128(uint128)
-IntTypeTest.testFail_uint256(uint256)
-IntTypeTest.testFail_uint64(uint64)
-IntTypeTest.test_uint128(uint128)
-IntTypeTest.test_uint128_fail(uint128)
-IntTypeTest.test_uint256(uint256)
-IntTypeTest.test_uint256_fail(uint256)
-IntTypeTest.test_uint64(uint64)
-IntTypeTest.test_uint64_fail(uint64)
+UintTypeTest.test_uint96(uint96)
diff --git a/src/tests/integration/test-data/foundry-prove-skip-legacy b/src/tests/integration/test-data/foundry-prove-skip-legacy
index b32a798ea..c177395c2 100644
--- a/src/tests/integration/test-data/foundry-prove-skip-legacy
+++ b/src/tests/integration/test-data/foundry-prove-skip-legacy
@@ -100,15 +100,15 @@ ForkTest.testRPCUrlRevert()
 GasTest.testInfiniteGas()
 GetCodeTest.testGetCode()
 InitCodeTest.test_init()
-IntTypeTest.testFail_uint128(uint128)
-IntTypeTest.testFail_uint256(uint256)
-IntTypeTest.testFail_uint64(uint64)
-IntTypeTest.test_uint128_fail(uint128)
-IntTypeTest.test_uint128(uint128)
-IntTypeTest.test_uint256_fail(uint256)
-IntTypeTest.test_uint256(uint256)
-IntTypeTest.test_uint64_fail(uint64)
-IntTypeTest.test_uint64(uint64)
+IntTypeTest.testFail_int128(uint128)
+IntTypeTest.testFail_int256(uint256)
+IntTypeTest.testFail_int64(uint64)
+IntTypeTest.test_int128_fail(uint128)
+IntTypeTest.test_int128(uint128)
+IntTypeTest.test_int256_fail(uint256)
+IntTypeTest.test_int256(uint256)
+IntTypeTest.test_int64_fail(uint64)
+IntTypeTest.test_int64(uint64)
 LoopsTest.sum_N(uint256)
 LoopsTest.testIsNotPrime(uint256)
 LoopsTest.testIsPrimeBroken(uint256,uint256)
diff --git a/src/tests/integration/test-data/foundry/test/AllowChangesTest.t.sol b/src/tests/integration/test-data/foundry/test/AllowChangesTest.t.sol
index aa382a1cf..6dc35c27e 100644
--- a/src/tests/integration/test-data/foundry/test/AllowChangesTest.t.sol
+++ b/src/tests/integration/test-data/foundry/test/AllowChangesTest.t.sol
@@ -52,13 +52,4 @@ contract AllowChangesTest is Test, KEVMCheats {
 		canChange.changeValue2(23452);
 	}
 
-	function testAllow_fail() public {
-		ValueStore canChange = new ValueStore();
-		ValueStore cannotChange = new ValueStore();
-
-		kevm.allowCallsToAddress(address(canChange));
-		kevm.allowChangesToStorage(address(canChange), 0);
-
-		canChange.changeValue2(234521);
-	}
 }
diff --git a/src/tests/integration/test-data/gas-abstraction.expected b/src/tests/integration/test-data/gas-abstraction.expected
index e2a243b74..5a51bd0d4 100644
--- a/src/tests/integration/test-data/gas-abstraction.expected
+++ b/src/tests/integration/test-data/gas-abstraction.expected
@@ -390,8 +390,7 @@ Node 6:
 #And ( { true #Equals 0 <=Int NUMBER_CELL:Int }
 #And ( { true #Equals CALLER_ID:Int <Int pow160 }
 #And ( { true #Equals ORIGIN_ID:Int <Int pow160 }
-#And ( { true #Equals NUMBER_CELL:Int <=Int maxSInt256 }
-#And { true #Equals ( VGAS:Int +Int -298 ) <Int ( VGAS:Int +Int -207 ) } ) ) ) ) ) ) )
+#And { true #Equals NUMBER_CELL:Int <=Int maxSInt256 } ) ) ) ) ) )
 
 
 
@@ -603,7 +602,6 @@ Node 6:
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
                ))))))
-       ensures ( VGAS:Int +Int -298 ) <Int ( VGAS:Int +Int -207 )
       [label(BASIC-BLOCK-1-TO-3)]
     
     rule [BASIC-BLOCK-4-TO-5]: <foundry>
@@ -814,8 +812,7 @@ Node 6:
        andBool ( CALLER_ID:Int <Int pow160
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( ( VGAS:Int +Int -298 ) <Int ( VGAS:Int +Int -207 )
-               )))))))
+               ))))))
       [label(BASIC-BLOCK-4-TO-5)]
     
     rule [BASIC-BLOCK-5-TO-6]: <foundry>
@@ -1026,8 +1023,7 @@ Node 6:
        andBool ( CALLER_ID:Int <Int pow160
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( ( VGAS:Int +Int -298 ) <Int ( VGAS:Int +Int -207 )
-               )))))))
+               ))))))
       [label(BASIC-BLOCK-5-TO-6)]
 
 endmodule
@@ -1043,8 +1039,7 @@ Failing nodes:
     #And ( { true #Equals 0 <=Int NUMBER_CELL:Int }
     #And ( { true #Equals CALLER_ID:Int <Int pow160 }
     #And ( { true #Equals ORIGIN_ID:Int <Int pow160 }
-    #And ( { true #Equals NUMBER_CELL:Int <=Int maxSInt256 }
-    #And { true #Equals ( VGAS:Int +Int -298 ) <Int ( VGAS:Int +Int -207 ) } ) ) ) ) ) ) #Implies { true #Equals foundry_success ( ... statusCode: EVMC_REVERT , failed: #lookup ( .Map , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } )
+    #And { true #Equals NUMBER_CELL:Int <=Int maxSInt256 } ) ) ) ) ) #Implies { true #Equals foundry_success ( ... statusCode: EVMC_REVERT , failed: #lookup ( .Map , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) } )
   Path condition:
     #Top
 
diff --git a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected
index a657f8a77..acd5178ea 100644
--- a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected
+++ b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected
@@ -5,64 +5,57 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (856 steps)
+│  (547 steps)
 ├─ 3
-│   k: STATICCALL ( VGAS:Int +Int -3019 ) 645326474426547203313410069153905908525362434 ...
+│   k: STATICCALL 0 645326474426547203313410069153905908525362434349 128 36 128 0 ~> #p ...
 │   pc: 563
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
 │  (1 step)
 ├─ 4
-│   k: #checkCall 728815563385977040452943777879061427756277306518 0 ~> #call 728815563 ...
+│   k: #accessAccounts 645326474426547203313410069153905908525362434349 ~> #checkCall 7 ...
 │   pc: 563
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
 │  (1000 steps)
 ├─ 5
-│   k: #gas [ MSTORE , MSTORE 192 46308022326495007027972728677917914892729792999299745 ...
-│   pc: 3667
+│   k: #addr [ ISZERO ] ~> #exec [ ISZERO ] ~> #pc [ ISZERO ] ~> #execute ~> CONTINUATI ...
+│   pc: 4206
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (1000 steps)
+│  (827 steps)
 ├─ 6
-│   k: #next [ DUP ( 2 ) ] ~> #execute ~> CONTINUATION:K
-│   pc: 4451
-│   callDepth: 0
-│   statusCode: STATUSCODE:StatusCode
-│
-│  (797 steps)
-├─ 7
-│   k: CALL ( VGAS:Int +Int -10131 ) 645326474426547203313410069153905908525362434349 0 ...
+│   k: CALL 0 645326474426547203313410069153905908525362434349 0 388 100 388 0 ~> #pc [ ...
 │   pc: 3785
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
 │  (1 step)
-├─ 8
-│   k: #checkCall 728815563385977040452943777879061427756277306518 0 ~> #call 728815563 ...
+├─ 7
+│   k: #accessAccounts 645326474426547203313410069153905908525362434349 ~> #checkCall 7 ...
 │   pc: 3785
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (387 steps)
-├─ 9
+│  (244 steps)
+├─ 8
 │   k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
 │   pc: 281
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
 │  (1 step)
-├─ 10
+├─ 9
 │   k: #halt ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
 │   pc: 281
 │   callDepth: 0
 │   statusCode: EVMC_SUCCESS
 │
 │  (2 steps)
-├─ 11 (terminal)
+├─ 10 (terminal)
 │   k: #halt ~> CONTINUATION:K
 │   pc: 281
 │   callDepth: 0
@@ -84,7 +77,7 @@
     rule [BASIC-BLOCK-1-TO-3]: <foundry>
            <kevm>
              <k>
-               ( .K => STATICCALL ( VGAS:Int +Int -3019 ) 645326474426547203313410069153905908525362434349 128 36 128 0
+               ( .K => STATICCALL 0 645326474426547203313410069153905908525362434349 128 36 128 0
                ~> #pc [ STATICCALL ] )
                ~> #execute
                ~> _CONTINUATION
@@ -95,6 +88,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <callStack>
@@ -127,10 +123,10 @@
                    ...
                    ...
                    <memoryUsed>
-                     ( 0 => 6 )
+                     0
                    </memoryUsed>
                    <callGas>
-                     ( _CALLGAS_CELL => #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3019 ) , ( VGAS:Int +Int -3019 ) , 100 ) ) )
+                     0
                    </callGas>
                    <static>
                      false
@@ -143,6 +139,9 @@
                    <log>
                      .List
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      ( .Set => SetItem ( 645326474426547203313410069153905908525362434349 ) )
                    </accessedAccounts>
@@ -292,7 +291,8 @@
     rule [BASIC-BLOCK-3-TO-4]: <foundry>
            <kevm>
              <k>
-               ( STATICCALL ( VGAS:Int +Int -3019 ) 645326474426547203313410069153905908525362434349 128 36 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0
+               ( STATICCALL 0 645326474426547203313410069153905908525362434349 128 36 128 0 => #accessAccounts 645326474426547203313410069153905908525362434349
+               ~> #checkCall 728815563385977040452943777879061427756277306518 0
                ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( ( notBool VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) ) ) true
                ~> #return 128 0 )
                ~> #pc [ STATICCALL ]
@@ -305,6 +305,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <callStack>
@@ -337,10 +340,10 @@
                    ...
                    ...
                    <memoryUsed>
-                     6
+                     0
                    </memoryUsed>
                    <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3019 ) , ( VGAS:Int +Int -3019 ) , 100 ) )
+                     0
                    </callGas>
                    <static>
                      false
@@ -353,6 +356,9 @@
                    <log>
                      .List
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      SetItem ( 645326474426547203313410069153905908525362434349 )
                    </accessedAccounts>
@@ -502,12 +508,13 @@
     rule [BASIC-BLOCK-4-TO-5]: <foundry>
            <kevm>
              <k>
-               ( #checkCall 728815563385977040452943777879061427756277306518 0
+               ( #accessAccounts 645326474426547203313410069153905908525362434349
+               ~> #checkCall 728815563385977040452943777879061427756277306518 0
                ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( ( notBool VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) ) ) true
                ~> #return 128 0
-               ~> #pc [ STATICCALL ] => #gas [ MSTORE , MSTORE 192 46308022326495007027972728677917914892729792999299745830475596687180801507328 ]
-               ~> MSTORE 192 46308022326495007027972728677917914892729792999299745830475596687180801507328
-               ~> #pc [ MSTORE ] )
+               ~> #pc [ STATICCALL ] => #addr [ ISZERO ]
+               ~> #exec [ ISZERO ]
+               ~> #pc [ ISZERO ] )
                ~> #execute
                ~> _CONTINUATION
              </k>
@@ -517,6 +524,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -544,18 +554,18 @@
                      0
                    </callValue>
                    <wordStack>
-                     ( ( 164 => 128 ) : ( ( selector ( "assume(bool)" ) => 645326474426547203313410069153905908525362434349 ) : ( ( 645326474426547203313410069153905908525362434349 => 594 ) : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( ( 280 => 594 ) : ( ( selector ( "testFail_assume_true(uint256,uint256)" ) => VV1_b_114b9705:Int ) : ( .WordStack => ( VV0_a_114b9705:Int : ( 280 : ( selector ( "testFail_assume_true(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) ) ) )
+                     ( ( 164 => 1 ) : ( ( selector ( "assume(bool)" ) => 64 ) : ( ( 645326474426547203313410069153905908525362434349 => 160 ) : ( ( VV1_b_114b9705:Int => 292 ) : ( ( VV0_a_114b9705:Int => 96 ) : ( ( 280 => 4586 ) : ( ( selector ( "testFail_assume_true(uint256,uint256)" ) => 96 ) : ( .WordStack => ( 0 : ( 288 : ( 128 : ( 51016057639858100040180367130768047423658391221723556551037572491782395555780 : ( 3745 : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 280 : ( selector ( "testFail_assume_true(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                    </wordStack>
                    <localMem>
-                     ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( ( notBool VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) ) ) => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n     Right\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" )
+                     ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( ( notBool VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) ) ) => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00p\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" )
                    </localMem>
                    ...
                    ...
                    <memoryUsed>
-                     ( 6 => 8 )
+                     0
                    </memoryUsed>
                    <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3019 ) , ( VGAS:Int +Int -3019 ) , 100 ) )
+                     0
                    </callGas>
                    <static>
                      false
@@ -568,6 +578,9 @@
                    <log>
                      ( .List => ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 29485693714967335757563038618841744472215891622979272243827124658718922284880 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\"Error: a == b not satisfied [uint]\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV0_a_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n      Left\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV1_b_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n     Right\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) )
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      SetItem ( 645326474426547203313410069153905908525362434349 )
                    </accessedAccounts>
@@ -712,17 +725,16 @@
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
                ))))))))))
-       ensures ( VV0_a_114b9705:Int =/=K VV1_b_114b9705:Int
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
-               ))
+       ensures VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
       [label(BASIC-BLOCK-4-TO-5)]
     
     rule [BASIC-BLOCK-5-TO-6]: <foundry>
            <kevm>
              <k>
-               ( #gas [ MSTORE , MSTORE 192 46308022326495007027972728677917914892729792999299745830475596687180801507328 ]
-               ~> MSTORE 192 46308022326495007027972728677917914892729792999299745830475596687180801507328
-               ~> #pc [ MSTORE ] => #next [ DUP ( 2 ) ] )
+               ( #addr [ ISZERO ]
+               ~> #exec [ ISZERO ]
+               ~> #pc [ ISZERO ] => CALL 0 645326474426547203313410069153905908525362434349 0 388 100 388 0
+               ~> #pc [ CALL ] )
                ~> #execute
                ~> _CONTINUATION
              </k>
@@ -732,6 +744,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -759,18 +774,18 @@
                      0
                    </callValue>
                    <wordStack>
-                     ( ( 128 => 4461 ) : ( ( 645326474426547203313410069153905908525362434349 => 100 ) : ( ( 594 => 0 ) : ( ( VV1_b_114b9705:Int => 388 ) : ( ( VV0_a_114b9705:Int => 256 ) : ( ( 594 => 3771 ) : ( ( VV1_b_114b9705:Int => 645326474426547203313410069153905908525362434349 ) : ( ( VV0_a_114b9705:Int => 0 ) : ( ( 280 => 594 ) : ( ( selector ( "testFail_assume_true(uint256,uint256)" ) => VV1_b_114b9705:Int ) : ( .WordStack => ( VV0_a_114b9705:Int : ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 280 : ( selector ( "testFail_assume_true(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
+                     ( ( 1 => 488 ) : ( ( 64 => 645326474426547203313410069153905908525362434349 ) : ( ( 160 => 0 ) : ( ( 292 => 594 ) : ( ( 96 => VV1_b_114b9705:Int ) : ( ( 4586 => VV0_a_114b9705:Int ) : ( ( 96 => 594 ) : ( ( 0 => VV1_b_114b9705:Int ) : ( ( 288 => VV0_a_114b9705:Int ) : ( ( 128 => 280 ) : ( ( 51016057639858100040180367130768047423658391221723556551037572491782395555780 => selector ( "testFail_assume_true(uint256,uint256)" ) ) : ( ( 3745 : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 280 : ( selector ( "testFail_assume_true(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) ) ) ) => .WordStack ) ) ) ) ) ) ) ) ) ) ) )
                    </wordStack>
                    <localMem>
-                     ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n     Right\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x84\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00dp\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" )
+                     ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00p\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x84\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00dp\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01p\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" )
                    </localMem>
                    ...
                    ...
                    <memoryUsed>
-                     ( 8 => 13 )
+                     0
                    </memoryUsed>
                    <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3019 ) , ( VGAS:Int +Int -3019 ) , 100 ) )
+                     0
                    </callGas>
                    <static>
                      false
@@ -783,6 +798,9 @@
                    <log>
                      ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 29485693714967335757563038618841744472215891622979272243827124658718922284880 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\"Error: a == b not satisfied [uint]\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV0_a_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n      Left\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV1_b_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n     Right\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } )
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      SetItem ( 645326474426547203313410069153905908525362434349 )
                    </accessedAccounts>
@@ -918,236 +936,23 @@
          </foundry>
       requires ( 0 <=Int CALLER_ID:Int
        andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( VV0_a_114b9705:Int =/=K VV1_b_114b9705:Int
        andBool ( 0 <=Int NUMBER_CELL:Int
        andBool ( 0 <=Int VV0_a_114b9705:Int
        andBool ( 0 <=Int VV1_b_114b9705:Int
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
        andBool ( CALLER_ID:Int <Int pow160
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
-               ))))))))))))
+               )))))))))))
       [label(BASIC-BLOCK-5-TO-6)]
     
     rule [BASIC-BLOCK-6-TO-7]: <foundry>
            <kevm>
              <k>
-               ( #next [ DUP ( 2 ) ] => CALL ( VGAS:Int +Int -10131 ) 645326474426547203313410069153905908525362434349 0 388 100 388 0
-               ~> #pc [ CALL ] )
-               ~> #execute
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   b""
-                 </output>
-                 <callStack>
-                   .List
-                 </callStack>
-                 <interimStates>
-                   .List
-                 </interimStates>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     728815563385977040452943777879061427756277306518
-                   </id>
-                   <caller>
-                     CALLER_ID:Int
-                   </caller>
-                   <callData>
-                     b"\x0e\xb6V\xda" +Bytes #buf ( 32 , VV0_a_114b9705:Int ) +Bytes #buf ( 32 , VV1_b_114b9705:Int )
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     ( ( 4461 => 488 ) : ( ( 100 => 645326474426547203313410069153905908525362434349 ) : ( 0 : ( ( 388 => 594 ) : ( ( 256 => VV1_b_114b9705:Int ) : ( ( 3771 => VV0_a_114b9705:Int ) : ( ( 645326474426547203313410069153905908525362434349 => 594 ) : ( ( 0 => VV1_b_114b9705:Int ) : ( ( 594 => VV0_a_114b9705:Int ) : ( ( VV1_b_114b9705:Int => 280 ) : ( ( VV0_a_114b9705:Int => selector ( "testFail_assume_true(uint256,uint256)" ) ) : ( ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 280 : ( selector ( "testFail_assume_true(uint256,uint256)" ) : .WordStack ) ) ) ) ) => .WordStack ) ) ) ) ) ) ) ) ) ) ) )
-                   </wordStack>
-                   <localMem>
-                     ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x84\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00dp\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x84\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00dp\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01p\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" )
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     ( 13 => 17 )
-                   </memoryUsed>
-                   <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int ( -3019 => -10131 ) ) , ( VGAS:Int +Int ( -3019 => -10131 ) ) , 100 ) )
-                   </callGas>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     0
-                   </callDepth>
-                 </callState>
-                 <substate>
-                   <log>
-                     ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 29485693714967335757563038618841744472215891622979272243827124658718922284880 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\"Error: a == b not satisfied [uint]\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV0_a_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n      Left\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV1_b_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n     Right\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } )
-                   </log>
-                   <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
-                   </accessedAccounts>
-                   <accessedStorage>
-                     .Map
-                   </accessedStorage>
-                   ...
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( VV0_a_114b9705:Int =/=K VV1_b_114b9705:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( 0 <=Int VV0_a_114b9705:Int
-       andBool ( 0 <=Int VV1_b_114b9705:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VV0_a_114b9705:Int <Int pow256
-       andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
-               ))))))))))))
-      [label(BASIC-BLOCK-6-TO-7)]
-    
-    rule [BASIC-BLOCK-7-TO-8]: <foundry>
-           <kevm>
-             <k>
-               ( CALL ( VGAS:Int +Int -10131 ) 645326474426547203313410069153905908525362434349 0 388 100 388 0 => #checkCall 728815563385977040452943777879061427756277306518 0
+               ( CALL 0 645326474426547203313410069153905908525362434349 0 388 100 388 0 => #accessAccounts 645326474426547203313410069153905908525362434349
+               ~> #checkCall 728815563385977040452943777879061427756277306518 0
                ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"p\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" false
                ~> #return 388 0 )
                ~> #pc [ CALL ]
@@ -1160,6 +965,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1195,10 +1003,10 @@
                    ...
                    ...
                    <memoryUsed>
-                     17
+                     0
                    </memoryUsed>
                    <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -10131 ) , ( VGAS:Int +Int -10131 ) , 100 ) )
+                     0
                    </callGas>
                    <static>
                      false
@@ -1211,6 +1019,9 @@
                    <log>
                      ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 29485693714967335757563038618841744472215891622979272243827124658718922284880 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\"Error: a == b not satisfied [uint]\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV0_a_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n      Left\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV1_b_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n     Right\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } )
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      SetItem ( 645326474426547203313410069153905908525362434349 )
                    </accessedAccounts>
@@ -1346,23 +1157,23 @@
          </foundry>
       requires ( 0 <=Int CALLER_ID:Int
        andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( VV0_a_114b9705:Int =/=K VV1_b_114b9705:Int
        andBool ( 0 <=Int NUMBER_CELL:Int
        andBool ( 0 <=Int VV0_a_114b9705:Int
        andBool ( 0 <=Int VV1_b_114b9705:Int
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
        andBool ( CALLER_ID:Int <Int pow160
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
-               ))))))))))))
-      [label(BASIC-BLOCK-7-TO-8)]
+               )))))))))))
+      [label(BASIC-BLOCK-6-TO-7)]
     
-    rule [BASIC-BLOCK-8-TO-9]: <foundry>
+    rule [BASIC-BLOCK-7-TO-8]: <foundry>
            <kevm>
              <k>
-               ( #checkCall 728815563385977040452943777879061427756277306518 0
+               ( #accessAccounts 645326474426547203313410069153905908525362434349
+               ~> #checkCall 728815563385977040452943777879061427756277306518 0
                ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"p\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" false
                ~> #return 388 0
                ~> #pc [ CALL ] => #end EVMC_SUCCESS
@@ -1376,6 +1187,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1411,10 +1225,10 @@
                    ...
                    ...
                    <memoryUsed>
-                     17
+                     0
                    </memoryUsed>
                    <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -10131 ) , ( VGAS:Int +Int -10131 ) , 100 ) )
+                     0
                    </callGas>
                    <static>
                      false
@@ -1427,6 +1241,9 @@
                    <log>
                      ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 29485693714967335757563038618841744472215891622979272243827124658718922284880 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\"Error: a == b not satisfied [uint]\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV0_a_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n      Left\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV1_b_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n     Right\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } )
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      SetItem ( 645326474426547203313410069153905908525362434349 )
                    </accessedAccounts>
@@ -1562,20 +1379,19 @@
          </foundry>
       requires ( 0 <=Int CALLER_ID:Int
        andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( VV0_a_114b9705:Int =/=K VV1_b_114b9705:Int
        andBool ( 0 <=Int NUMBER_CELL:Int
        andBool ( 0 <=Int VV0_a_114b9705:Int
        andBool ( 0 <=Int VV1_b_114b9705:Int
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
        andBool ( CALLER_ID:Int <Int pow160
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
-               ))))))))))))
-      [label(BASIC-BLOCK-8-TO-9)]
+               )))))))))))
+      [label(BASIC-BLOCK-7-TO-8)]
     
-    rule [BASIC-BLOCK-9-TO-10]: <foundry>
+    rule [BASIC-BLOCK-8-TO-9]: <foundry>
            <kevm>
              <k>
                ( #end EVMC_SUCCESS => #halt )
@@ -1589,6 +1405,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1627,10 +1446,10 @@
                    ...
                    ...
                    <memoryUsed>
-                     17
+                     0
                    </memoryUsed>
                    <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -10131 ) , ( VGAS:Int +Int -10131 ) , 100 ) )
+                     0
                    </callGas>
                    <static>
                      false
@@ -1643,6 +1462,9 @@
                    <log>
                      ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 29485693714967335757563038618841744472215891622979272243827124658718922284880 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\"Error: a == b not satisfied [uint]\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV0_a_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n      Left\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV1_b_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n     Right\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } )
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      SetItem ( 645326474426547203313410069153905908525362434349 )
                    </accessedAccounts>
@@ -1778,20 +1600,19 @@
          </foundry>
       requires ( 0 <=Int CALLER_ID:Int
        andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( VV0_a_114b9705:Int =/=K VV1_b_114b9705:Int
        andBool ( 0 <=Int NUMBER_CELL:Int
        andBool ( 0 <=Int VV0_a_114b9705:Int
        andBool ( 0 <=Int VV1_b_114b9705:Int
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
        andBool ( CALLER_ID:Int <Int pow160
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
-               ))))))))))))
-      [label(BASIC-BLOCK-9-TO-10)]
+               )))))))))))
+      [label(BASIC-BLOCK-8-TO-9)]
     
-    rule [BASIC-BLOCK-10-TO-11]: <foundry>
+    rule [BASIC-BLOCK-9-TO-10]: <foundry>
            <kevm>
              <k>
                #halt
@@ -1805,6 +1626,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1843,10 +1667,10 @@
                    ...
                    ...
                    <memoryUsed>
-                     17
+                     0
                    </memoryUsed>
                    <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -10131 ) , ( VGAS:Int +Int -10131 ) , 100 ) )
+                     0
                    </callGas>
                    <static>
                      false
@@ -1859,6 +1683,9 @@
                    <log>
                      ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 29485693714967335757563038618841744472215891622979272243827124658718922284880 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\"Error: a == b not satisfied [uint]\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV0_a_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n      Left\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV1_b_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n     Right\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } )
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      SetItem ( 645326474426547203313410069153905908525362434349 )
                    </accessedAccounts>
@@ -1994,18 +1821,17 @@
          </foundry>
       requires ( 0 <=Int CALLER_ID:Int
        andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( VV0_a_114b9705:Int =/=K VV1_b_114b9705:Int
        andBool ( 0 <=Int NUMBER_CELL:Int
        andBool ( 0 <=Int VV0_a_114b9705:Int
        andBool ( 0 <=Int VV1_b_114b9705:Int
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
        andBool ( CALLER_ID:Int <Int pow160
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
-       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int ==Bool true
-               ))))))))))))
-      [label(BASIC-BLOCK-10-TO-11)]
+               )))))))))))
+      [label(BASIC-BLOCK-9-TO-10)]
 
 endmodule
 0 Failure nodes. (0 pending and 0 failing)
diff --git a/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected
index 3c03327a2..787f82bd2 100644
--- a/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected
+++ b/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected
@@ -278,10 +278,10 @@ Node 10:
 </generatedTop>
 #And ( { true #Equals 0 <=Int CALLER_ID:Int }
 #And ( { true #Equals 0 <=Int ORIGIN_ID:Int }
-#And ( #Not ( { VV0_a_114b9705:Int #Equals VV1_b_114b9705:Int } )
 #And ( { true #Equals 0 <=Int NUMBER_CELL:Int }
 #And ( { true #Equals 0 <=Int VV0_a_114b9705:Int }
 #And ( { true #Equals 0 <=Int VV1_b_114b9705:Int }
+#And ( { true #Equals VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int }
 #And ( { true #Equals CALLER_ID:Int <Int pow160 }
 #And ( { true #Equals ORIGIN_ID:Int <Int pow160 }
 #And ( { true #Equals NUMBER_CELL:Int <=Int maxSInt256 }
@@ -943,7 +943,7 @@ Node 10:
        andBool ( VV0_a_114b9705:Int <Int pow256
        andBool ( VV1_b_114b9705:Int <Int pow256
                ))))))))))
-       ensures VV0_a_114b9705:Int =/=K VV1_b_114b9705:Int
+       ensures VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
       [label(BASIC-BLOCK-4-TO-5)]
     
     rule [BASIC-BLOCK-5-TO-6]: <foundry>
@@ -1154,10 +1154,10 @@ Node 10:
          </foundry>
       requires ( 0 <=Int CALLER_ID:Int
        andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( VV0_a_114b9705:Int =/=K VV1_b_114b9705:Int
        andBool ( 0 <=Int NUMBER_CELL:Int
        andBool ( 0 <=Int VV0_a_114b9705:Int
        andBool ( 0 <=Int VV1_b_114b9705:Int
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
        andBool ( CALLER_ID:Int <Int pow160
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
@@ -1375,10 +1375,10 @@ Node 10:
          </foundry>
       requires ( 0 <=Int CALLER_ID:Int
        andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( VV0_a_114b9705:Int =/=K VV1_b_114b9705:Int
        andBool ( 0 <=Int NUMBER_CELL:Int
        andBool ( 0 <=Int VV0_a_114b9705:Int
        andBool ( 0 <=Int VV1_b_114b9705:Int
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
        andBool ( CALLER_ID:Int <Int pow160
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
@@ -1597,10 +1597,10 @@ Node 10:
          </foundry>
       requires ( 0 <=Int CALLER_ID:Int
        andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( VV0_a_114b9705:Int =/=K VV1_b_114b9705:Int
        andBool ( 0 <=Int NUMBER_CELL:Int
        andBool ( 0 <=Int VV0_a_114b9705:Int
        andBool ( 0 <=Int VV1_b_114b9705:Int
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
        andBool ( CALLER_ID:Int <Int pow160
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
@@ -1818,10 +1818,10 @@ Node 10:
          </foundry>
       requires ( 0 <=Int CALLER_ID:Int
        andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( VV0_a_114b9705:Int =/=K VV1_b_114b9705:Int
        andBool ( 0 <=Int NUMBER_CELL:Int
        andBool ( 0 <=Int VV0_a_114b9705:Int
        andBool ( 0 <=Int VV1_b_114b9705:Int
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
        andBool ( CALLER_ID:Int <Int pow160
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
@@ -2039,10 +2039,10 @@ Node 10:
          </foundry>
       requires ( 0 <=Int CALLER_ID:Int
        andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( VV0_a_114b9705:Int =/=K VV1_b_114b9705:Int
        andBool ( 0 <=Int NUMBER_CELL:Int
        andBool ( 0 <=Int VV0_a_114b9705:Int
        andBool ( 0 <=Int VV1_b_114b9705:Int
+       andBool ( VV0_a_114b9705:Int =/=Int VV1_b_114b9705:Int
        andBool ( CALLER_ID:Int <Int pow160
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
@@ -2076,8 +2076,8 @@ Failing nodes:
     CALLER_ID = 0
     NUMBER_CELL = 0
     ORIGIN_ID = 0
-    VV0_a_114b9705 = 1
-    VV1_b_114b9705 = 0
+    VV0_a_114b9705 = 0
+    VV1_b_114b9705 = 1
 
 Join the Runtime Verification Discord server for support: https://discord.com/invite/CurfmXNtbN
 
diff --git a/src/tests/integration/test-data/show/LoopsTest.sum_N(uint256).expected b/src/tests/integration/test-data/show/LoopsTest.sum_N(uint256).expected
index 1eb35d384..4b4fbe8f7 100644
--- a/src/tests/integration/test-data/show/LoopsTest.sum_N(uint256).expected
+++ b/src/tests/integration/test-data/show/LoopsTest.sum_N(uint256).expected
@@ -5,35 +5,35 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (808 steps)
+│  (526 steps)
 ├─ 3
-│   k: STATICCALL ( VGAS:Int +Int -3034 ) 645326474426547203313410069153905908525362434 ...
+│   k: STATICCALL 0 645326474426547203313410069153905908525362434349 128 36 128 0 ~> #p ...
 │   pc: 2255
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
 │  (1 step)
 ├─ 4
-│   k: #checkCall 728815563385977040452943777879061427756277306518 0 ~> #call 728815563 ...
+│   k: #accessAccounts 645326474426547203313410069153905908525362434349 ~> #checkCall 7 ...
 │   pc: 2255
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (355 steps)
+│  (222 steps)
 ├─ 5
-│   k: CALL ( VGAS:Int +Int -3376 ) 645326474426547203313410069153905908525362434349 0  ...
+│   k: CALL 0 645326474426547203313410069153905908525362434349 0 128 36 128 0 ~> #pc [  ...
 │   pc: 2363
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
 │  (1 step)
 ├─ 6
-│   k: #checkCall 728815563385977040452943777879061427756277306518 0 ~> #call 728815563 ...
+│   k: #accessAccounts 645326474426547203313410069153905908525362434349 ~> #checkCall 7 ...
 │   pc: 2363
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (152 steps)
+│  (98 steps)
 ├─ 7 (split)
 │   k: JUMPI 2423 bool2Word ( VV0_n_114b9705:Int ==Int 0 ) ~> #pc [ JUMPI ] ~> #execute ...
 │   pc: 2393
@@ -49,7 +49,7 @@
 ┃  │   callDepth: 0
 ┃  │   statusCode: STATUSCODE:StatusCode
 ┃  │
-┃  │  (162 steps)
+┃  │  (100 steps)
 ┃  ├─ 10
 ┃  │   k: #end EVMC_SUCCESS ~> #pc [ RETURN ] ~> #execute ~> CONTINUATION:K
 ┃  │   pc: 477
@@ -86,7 +86,7 @@
    │   callDepth: 0
    │   statusCode: STATUSCODE:StatusCode
    │
-   │  (162 steps)
+   │  (100 steps)
    ├─ 11
    │   k: #end EVMC_SUCCESS ~> #pc [ RETURN ] ~> #execute ~> CONTINUATION:K
    │   pc: 477
@@ -123,7 +123,7 @@
     rule [BASIC-BLOCK-1-TO-3]: <foundry>
            <kevm>
              <k>
-               ( .K => STATICCALL ( VGAS:Int +Int -3034 ) 645326474426547203313410069153905908525362434349 128 36 128 0
+               ( .K => STATICCALL 0 645326474426547203313410069153905908525362434349 128 36 128 0
                ~> #pc [ STATICCALL ] )
                ~> #execute
                ~> _CONTINUATION
@@ -134,6 +134,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <callStack>
@@ -166,10 +169,10 @@
                    ...
                    ...
                    <memoryUsed>
-                     ( 0 => 6 )
+                     0
                    </memoryUsed>
                    <callGas>
-                     ( _CALLGAS_CELL => #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3034 ) , ( VGAS:Int +Int -3034 ) , 100 ) ) )
+                     0
                    </callGas>
                    <static>
                      false
@@ -182,6 +185,9 @@
                    <log>
                      .List
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      ( .Set => SetItem ( 645326474426547203313410069153905908525362434349 ) )
                    </accessedAccounts>
@@ -329,7 +335,8 @@
     rule [BASIC-BLOCK-3-TO-4]: <foundry>
            <kevm>
              <k>
-               ( STATICCALL ( VGAS:Int +Int -3034 ) 645326474426547203313410069153905908525362434349 128 36 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0
+               ( STATICCALL 0 645326474426547203313410069153905908525362434349 128 36 128 0 => #accessAccounts 645326474426547203313410069153905908525362434349
+               ~> #checkCall 728815563385977040452943777879061427756277306518 0
                ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) true
                ~> #return 128 0 )
                ~> #pc [ STATICCALL ]
@@ -342,6 +349,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <callStack>
@@ -374,10 +384,10 @@
                    ...
                    ...
                    <memoryUsed>
-                     6
+                     0
                    </memoryUsed>
                    <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3034 ) , ( VGAS:Int +Int -3034 ) , 100 ) )
+                     0
                    </callGas>
                    <static>
                      false
@@ -390,6 +400,9 @@
                    <log>
                      .List
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      SetItem ( 645326474426547203313410069153905908525362434349 )
                    </accessedAccounts>
@@ -537,10 +550,11 @@
     rule [BASIC-BLOCK-4-TO-5]: <foundry>
            <kevm>
              <k>
-               ( #checkCall 728815563385977040452943777879061427756277306518 0
+               ( #accessAccounts 645326474426547203313410069153905908525362434349
+               ~> #checkCall 728815563385977040452943777879061427756277306518 0
                ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) true
                ~> #return 128 0
-               ~> #pc [ STATICCALL ] => CALL ( VGAS:Int +Int -3376 ) 645326474426547203313410069153905908525362434349 0 128 36 128 0
+               ~> #pc [ STATICCALL ] => CALL 0 645326474426547203313410069153905908525362434349 0 128 36 128 0
                ~> #pc [ CALL ] )
                ~> #execute
                ~> _CONTINUATION
@@ -551,6 +565,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -586,10 +603,10 @@
                    ...
                    ...
                    <memoryUsed>
-                     6
+                     0
                    </memoryUsed>
                    <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int ( -3034 => -3376 ) ) , ( VGAS:Int +Int ( -3034 => -3376 ) ) , 100 ) )
+                     0
                    </callGas>
                    <static>
                      false
@@ -602,6 +619,9 @@
                    <log>
                      .List
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      SetItem ( 645326474426547203313410069153905908525362434349 )
                    </accessedAccounts>
@@ -744,13 +764,14 @@
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_n_114b9705:Int <Int pow256
                ))))))))
-       ensures VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
+       ensures VV0_n_114b9705:Int <=Int 51816696836262767
       [label(BASIC-BLOCK-4-TO-5)]
     
     rule [BASIC-BLOCK-5-TO-6]: <foundry>
            <kevm>
              <k>
-               ( CALL ( VGAS:Int +Int -3376 ) 645326474426547203313410069153905908525362434349 0 128 36 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0
+               ( CALL 0 645326474426547203313410069153905908525362434349 0 128 36 128 0 => #accessAccounts 645326474426547203313410069153905908525362434349
+               ~> #checkCall 728815563385977040452943777879061427756277306518 0
                ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5" false
                ~> #return 128 0 )
                ~> #pc [ CALL ]
@@ -763,6 +784,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -798,10 +822,10 @@
                    ...
                    ...
                    <memoryUsed>
-                     6
+                     0
                    </memoryUsed>
                    <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3376 ) , ( VGAS:Int +Int -3376 ) , 100 ) )
+                     0
                    </callGas>
                    <static>
                      false
@@ -814,6 +838,9 @@
                    <log>
                      .List
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      SetItem ( 645326474426547203313410069153905908525362434349 )
                    </accessedAccounts>
@@ -951,18 +978,19 @@
        andBool ( 0 <=Int ORIGIN_ID:Int
        andBool ( 0 <=Int NUMBER_CELL:Int
        andBool ( 0 <=Int VV0_n_114b9705:Int
+       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767
        andBool ( CALLER_ID:Int <Int pow160
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
                )))))))))
       [label(BASIC-BLOCK-5-TO-6)]
     
     rule [BASIC-BLOCK-6-TO-7]: <foundry>
            <kevm>
              <k>
-               ( #checkCall 728815563385977040452943777879061427756277306518 0
+               ( #accessAccounts 645326474426547203313410069153905908525362434349
+               ~> #checkCall 728815563385977040452943777879061427756277306518 0
                ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5" false
                ~> #return 128 0
                ~> #pc [ CALL ] => JUMPI 2423 bool2Word ( VV0_n_114b9705:Int ==Int 0 )
@@ -976,6 +1004,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1011,10 +1042,10 @@
                    ...
                    ...
                    <memoryUsed>
-                     6
+                     0
                    </memoryUsed>
                    <callGas>
-                     ( #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3376 ) , ( VGAS:Int +Int -3376 ) , 100 ) ) => 0 )
+                     0
                    </callGas>
                    <static>
                      false
@@ -1027,6 +1058,9 @@
                    <log>
                      .List
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      SetItem ( 645326474426547203313410069153905908525362434349 )
                    </accessedAccounts>
@@ -1164,11 +1198,11 @@
        andBool ( 0 <=Int ORIGIN_ID:Int
        andBool ( 0 <=Int NUMBER_CELL:Int
        andBool ( 0 <=Int VV0_n_114b9705:Int
+       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767
        andBool ( CALLER_ID:Int <Int pow160
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
                )))))))))
       [label(BASIC-BLOCK-6-TO-7)]
     
@@ -1187,6 +1221,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1222,7 +1259,7 @@
                    ...
                    ...
                    <memoryUsed>
-                     6
+                     0
                    </memoryUsed>
                    <callGas>
                      0
@@ -1238,6 +1275,9 @@
                    <log>
                      .List
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      SetItem ( 645326474426547203313410069153905908525362434349 )
                    </accessedAccounts>
@@ -1376,11 +1416,11 @@
        andBool ( 0 <=Int NUMBER_CELL:Int
        andBool ( 0 <=Int VV0_n_114b9705:Int
        andBool ( VV0_n_114b9705:Int ==Int 0
+       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767
        andBool ( CALLER_ID:Int <Int pow160
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
                ))))))))))
        ensures VV0_n_114b9705:Int ==K 0
       [label(BASIC-BLOCK-8-TO-10)]
@@ -1400,6 +1440,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1435,7 +1478,7 @@
                    ...
                    ...
                    <memoryUsed>
-                     6
+                     0
                    </memoryUsed>
                    <callGas>
                      0
@@ -1451,6 +1494,9 @@
                    <log>
                      .List
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      SetItem ( 645326474426547203313410069153905908525362434349 )
                    </accessedAccounts>
@@ -1588,40 +1634,19 @@
        andBool ( 0 <=Int ORIGIN_ID:Int
        andBool ( 0 <=Int NUMBER_CELL:Int
        andBool ( 0 <=Int VV0_n_114b9705:Int
+       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767
        andBool ( CALLER_ID:Int <Int pow160
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( VV0_n_114b9705:Int =/=Int 0
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
                ))))))))))
-       ensures ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <Int VV0_n_114b9705:Int
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772579
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772582
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772585
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772588
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772591
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772594
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772597
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772598
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772601
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772604
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772607
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772610
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772613
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772616
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772619
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
+       ensures ( 0 <Int VV0_n_114b9705:Int
+       andBool ( VV0_n_114b9705:Int =/=Int 0
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772693
        andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
        andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               ))))))))))))))))))))))))))
+               )))))
       [label(BASIC-BLOCK-9-TO-11)]
     
     rule [BASIC-BLOCK-10-TO-12]: <foundry>
@@ -1638,6 +1663,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1676,7 +1704,7 @@
                    ...
                    ...
                    <memoryUsed>
-                     6
+                     0
                    </memoryUsed>
                    <callGas>
                      0
@@ -1692,6 +1720,9 @@
                    <log>
                      .List
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      SetItem ( 645326474426547203313410069153905908525362434349 )
                    </accessedAccounts>
@@ -1849,6 +1880,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1887,7 +1921,7 @@
                    ...
                    ...
                    <memoryUsed>
-                     6
+                     0
                    </memoryUsed>
                    <callGas>
                      0
@@ -1903,6 +1937,9 @@
                    <log>
                      .List
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      SetItem ( 645326474426547203313410069153905908525362434349 )
                    </accessedAccounts>
@@ -2036,42 +2073,21 @@
              </whitelist>
            </cheatcodes>
          </foundry>
-      requires ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <=Int CALLER_ID:Int
+      requires ( 0 <=Int CALLER_ID:Int
        andBool ( 0 <=Int ORIGIN_ID:Int
        andBool ( 0 <=Int NUMBER_CELL:Int
        andBool ( 0 <Int VV0_n_114b9705:Int
        andBool ( 0 <=Int VV0_n_114b9705:Int
+       andBool ( VV0_n_114b9705:Int =/=Int 0
+       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767
        andBool ( CALLER_ID:Int <Int pow160
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772579
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772582
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772585
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772588
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772591
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772594
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772597
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772598
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772601
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772604
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772607
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772610
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772613
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772616
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772619
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772693
        andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
        andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               )))))))))))))))))))))))))))))))))))
+               ))))))))))))))
       [label(BASIC-BLOCK-11-TO-13)]
     
     rule [BASIC-BLOCK-12-TO-14]: <foundry>
@@ -2088,6 +2104,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -2126,7 +2145,7 @@
                    ...
                    ...
                    <memoryUsed>
-                     6
+                     0
                    </memoryUsed>
                    <callGas>
                      0
@@ -2142,6 +2161,9 @@
                    <log>
                      .List
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      SetItem ( 645326474426547203313410069153905908525362434349 )
                    </accessedAccounts>
@@ -2299,6 +2321,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -2337,7 +2362,7 @@
                    ...
                    ...
                    <memoryUsed>
-                     6
+                     0
                    </memoryUsed>
                    <callGas>
                      0
@@ -2353,6 +2378,9 @@
                    <log>
                      .List
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      SetItem ( 645326474426547203313410069153905908525362434349 )
                    </accessedAccounts>
@@ -2486,42 +2514,21 @@
              </whitelist>
            </cheatcodes>
          </foundry>
-      requires ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <=Int CALLER_ID:Int
+      requires ( 0 <=Int CALLER_ID:Int
        andBool ( 0 <=Int ORIGIN_ID:Int
        andBool ( 0 <=Int NUMBER_CELL:Int
        andBool ( 0 <Int VV0_n_114b9705:Int
        andBool ( 0 <=Int VV0_n_114b9705:Int
+       andBool ( VV0_n_114b9705:Int =/=Int 0
+       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767
        andBool ( CALLER_ID:Int <Int pow160
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772579
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772582
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772585
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772588
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772591
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772594
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772597
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772598
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772601
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772604
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772607
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772610
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772613
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772616
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772619
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772693
        andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
        andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               )))))))))))))))))))))))))))))))))))
+               ))))))))))))))
       [label(BASIC-BLOCK-13-TO-15)]
 
 endmodule
diff --git a/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected b/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected
index ec41cfc1b..079551a10 100644
--- a/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected
+++ b/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected
@@ -5,78 +5,71 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (1000 steps)
+│  (713 steps)
 ├─ 3
-│   k: #accessStorage 491460923342184218035706888008750043977755113263 0 ~> 0 ~> #deduc ...
-│   pc: 79
-│   callDepth: 1
-│   statusCode: STATUSCODE:StatusCode
-│
-│  (70 steps)
-├─ 4
 │   k: #end EVMC_SUCCESS ~> #pc [ RETURN ] ~> #execute ~> #codeDeposit 4914609233421842 ...
 │   pc: 145
 │   callDepth: 1
 │   statusCode: STATUSCODE:StatusCode
 │
 │  (1 step)
-├─ 5
+├─ 4
 │   k: #halt ~> #pc [ RETURN ] ~> #execute ~> #codeDeposit 4914609233421842180357068880 ...
 │   pc: 145
 │   callDepth: 1
 │   statusCode: EVMC_SUCCESS
 │
 │  (2 steps)
-├─ 6
+├─ 5
 │   k: #halt ~> #codeDeposit 491460923342184218035706888008750043977755113263 ~> #pc [  ...
 │   pc: 145
 │   callDepth: 1
 │   statusCode: EVMC_SUCCESS
 │
-│  (236 steps)
-├─ 7
+│  (162 steps)
+├─ 6
 │   k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
 │   pc: 194
 │   callDepth: 0
 │   statusCode: EVMC_SUCCESS
 │
 │  (1 step)
-├─ 8
+├─ 7
 │   k: #halt ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
 │   pc: 194
 │   callDepth: 0
 │   statusCode: EVMC_SUCCESS
 │
 │  (2 steps)
-├─ 9 (terminal)
+├─ 8 (terminal)
 │   k: #halt ~> CONTINUATION:K
 │   pc: 194
 │   callDepth: 0
 │   statusCode: EVMC_SUCCESS
 │
 │  (1 step)
-├─ 10
+├─ 9
 │   k: #execute ~> CONTINUATION:K
 │   pc: 0
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (531 steps)
-├─ 12
+│  (349 steps)
+├─ 11
 │   k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
 │   pc: 194
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
 │  (1 step)
-├─ 13
+├─ 12
 │   k: #halt ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
 │   pc: 194
 │   callDepth: 0
 │   statusCode: EVMC_SUCCESS
 │
 │  (2 steps)
-├─ 14 (terminal)
+├─ 13 (terminal)
 │   k: #halt ~> CONTINUATION:K
 │   pc: 194
 │   callDepth: 0
@@ -84,7 +77,7 @@
 │
 ┊  constraint: true
 ┊  subst: OMITTED SUBST
-└─ 11 (leaf, target, terminal)
+└─ 10 (leaf, target, terminal)
     k: #halt ~> CONTINUATION:K
     pc: PC_CELL_5d410f2a:Int
     callDepth: CALLDEPTH_CELL_5d410f2a:Int
@@ -98,11 +91,8 @@
     rule [BASIC-BLOCK-1-TO-3]: <foundry>
            <kevm>
              <k>
-               ( .K => #accessStorage 491460923342184218035706888008750043977755113263 0
-               ~> 0
-               ~> #deductGas
-               ~> SSTORE 0 0
-               ~> #pc [ SSTORE ]
+               ( .K => #end EVMC_SUCCESS
+               ~> #pc [ RETURN ]
                ~> #execute
                ~> #codeDeposit 491460923342184218035706888008750043977755113263
                ~> #pc [ CREATE ] )
@@ -115,418 +105,122 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
-                   ( _OUTPUT_CELL => b"" )
+                   ( _OUTPUT_CELL => b"`\x80`@R`\x046\x10a\x00CW`\x005`\xe0\x1c\x80c\f\x11\xde\xdd\x14a\x00OW\x80c'\xe25\xe3\x14a\x00uW\x80cp\xa0\x821\x14a\x00\xa2W\x80c\xfc\fTj\x14a\x00\xd8W`\x00\x80\xfd[6a\x00JW\x00[`\x00\x80\xfd[a\x00ba\x00]6`\x04a\x01[V[a\x01\x10V[`@Q\x90\x81R` \x01[`@Q\x80\x91\x03\x90\xf3[4\x80\x15a\x00\x81W`\x00\x80\xfd[Pa\x00ba\x00\x906`\x04a\x01[V[`\x01` R`\x00\x90\x81R`@\x90 T\x81V[4\x80\x15a\x00\xaeW`\x00\x80\xfd[Pa\x00ba\x00\xbd6`\x04a\x01[V[`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[4\x80\x15a\x00\xe4W`\x00\x80\xfd[P`\x00Ta\x00\xf8\x90`\x01`\x01`\xa0\x1b\x03\x16\x81V[`@Q`\x01`\x01`\xa0\x1b\x03\x90\x91\x16\x81R` \x01a\x00lV[`\x01`\x01`\xa0\x1b\x03\x81\x16`\x00\x90\x81R`\x01` R`@\x81 \x80T4\x91\x90\x83\x90a\x01:\x90\x84\x90a\x01\x8bV[\x90\x91UPPP`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[`\x00` \x82\x84\x03\x12\x15a\x01mW`\x00\x80\xfd[\x815`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x01\x84W`\x00\x80\xfd[\x93\x92PPPV[`\x00\x82\x19\x82\x11\x15a\x01\xacWcNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[P\x01\x90V\xfe\xa2dipfsX\"\x12 \xa2\xe1\xe3\x00(\x01\xe6\n\xb4\xa6\xf0\\P2\x83h\x00\xc3\xacq\x8bm\n\xa0\xb4\xb7\xb6\xd2\x16\x88\x05\xb4dsolcC\x00\x08\r\x003" )
                  </output>
                  <callStack>
-                   ( .List => ListItem ( <callState>-fragment ... ... <id>
-                     728815563385977040452943777879061427756277306518
-                   </id> <caller>
-                     CALLER_ID:Int
-                   </caller> <callData>
-                     b"\n\x92T\xe4"
-                   </callData> <callValue>
-                     0
-                   </callValue> <wordStack>
-                     ( 193 : ( selector ( "setUp()" ) : .WordStack ) )
-                   </wordStack> <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`@Qa\x02z8\x03\x80a\x02z\x839\x81\x01`@\x81\x90Ra\x00/\x91a\x00TV[`\x00\x80T`\x01`\x01`\xa0\x1b\x03\x19\x16`\x01`\x01`\xa0\x1b\x03\x92\x90\x92\x16\x91\x90\x91\x17\x90Ua\x00\x84V[`\x00` \x82\x84\x03\x12\x15a\x00fW`\x00\x80\xfd[\x81Q`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x00}W`\x00\x80\xfd[\x93\x92PPPV[a\x01\xe7\x80a\x00\x93`\x009`\x00\xf3\xfe`\x80`@R`\x046\x10a\x00CW`\x005`\xe0\x1c\x80c\f\x11\xde\xdd\x14a\x00OW\x80c'\xe25\xe3\x14a\x00uW\x80cp\xa0\x821\x14a\x00\xa2W\x80c\xfc\fTj\x14a\x00\xd8W`\x00\x80\xfd[6a\x00JW\x00[`\x00\x80\xfd[a\x00ba\x00]6`\x04a\x01[V[a\x01\x10V[`@Q\x90\x81R` \x01[`@Q\x80\x91\x03\x90\xf3[4\x80\x15a\x00\x81W`\x00\x80\xfd[Pa\x00ba\x00\x906`\x04a\x01[V[`\x01` R`\x00\x90\x81R`@\x90 T\x81V[4\x80\x15a\x00\xaeW`\x00\x80\xfd[Pa\x00ba\x00\xbd6`\x04a\x01[V[`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[4\x80\x15a\x00\xe4W`\x00\x80\xfd[P`\x00Ta\x00\xf8\x90`\x01`\x01`\xa0\x1b\x03\x16\x81V[`@Q`\x01`\x01`\xa0\x1b\x03\x90\x91\x16\x81R` \x01a\x00lV[`\x01`\x01`\xa0\x1b\x03\x81\x16`\x00\x90\x81R`\x01` R`@\x81 \x80T4\x91\x90\x83\x90a\x01:\x90\x84\x90a\x01\x8bV[\x90\x91UPPP`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[`\x00` \x82\x84\x03\x12\x15a\x01mW`\x00\x80\xfd[\x815`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x01\x84W`\x00\x80\xfd[\x93\x92PPPV[`\x00\x82\x19\x82\x11\x15a\x01\xacWcNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[P\x01\x90V\xfe\xa2dipfsX\"\x12 \xa2\xe1\xe3\x00(\x01\xe6\n\xb4\xa6\xf0\\P2\x83h\x00\xc3\xacq\x8bm\n\xa0\xb4\xb7\xb6\xd2\x16\x88\x05\xb4dsolcC\x00\x08\r\x003\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"
-                   </localMem> ... ... <memoryUsed>
-                     25
-                   </memoryUsed> <callGas>
-                     #gas ( #allBut64th ( ( VGAS:Int +Int -32419 ) ) )
-                   </callGas> <static>
-                     false
-                   </static> <callDepth>
-                     0
-                   </callDepth> </callState>-fragment ) )
-                 </callStack>
-                 <interimStates>
-                   ( .List => ListItem ( { <accounts>-fragment ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
+                   ( .List => ListItem ( <callState>
                      ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       2
-                     </nonce>
-                   </account> ) </accounts>-fragment | <substate>-fragment <selfDestruct>
-                     SELFDESTRUCT_CELL:Set
-                   </selfDestruct> <log>
-                     .List
-                   </log> <refund>
-                     REFUND_CELL:Int
-                   </refund> <accessedAccounts>
-                     SetItem ( 491460923342184218035706888008750043977755113263 )
-                   </accessedAccounts> <accessedStorage>
-                     .Map
-                   </accessedStorage> </substate>-fragment } ) )
-                 </interimStates>
-                 <touchedAccounts>
-                   ( TOUCHEDACCOUNTS_CELL:Set => TOUCHEDACCOUNTS_CELL:Set |Set SetItem ( 728815563385977040452943777879061427756277306518 ) |Set SetItem ( 491460923342184218035706888008750043977755113263 ) )
-                 </touchedAccounts>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 )
-                   </id>
-                   <caller>
-                     ( CALLER_ID:Int => 728815563385977040452943777879061427756277306518 )
-                   </caller>
-                   <callData>
-                     ( b"\n\x92T\xe4" => b"" )
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     .WordStack
-                   </wordStack>
-                   <localMem>
-                     ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xa0\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" )
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     ( 0 => 5 )
-                   </memoryUsed>
-                   <callGas>
-                     ( _CALLGAS_CELL => 0 )
-                   </callGas>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     ( 0 => 1 )
-                   </callDepth>
-                 </callState>
-                 <substate>
-                   <selfDestruct>
-                     SELFDESTRUCT_CELL:Set
-                   </selfDestruct>
-                   <log>
-                     .List
-                   </log>
-                   <refund>
-                     REFUND_CELL:Int
-                   </refund>
-                   <accessedAccounts>
-                     ( .Set => ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) )
-                   </accessedAccounts>
-                   <accessedStorage>
-                     ( .Map => ( 491460923342184218035706888008750043977755113263 |-> SetItem ( 0 ) ) )
-                   </accessedStorage>
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       ( 645326474426547203313410069153905908525362434349 => 491460923342184218035706888008750043977755113263 )
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
                      ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       ( 0 => 1 )
-                     </nonce>
-                   </account>
-                   ( <account>
-                     <acctID>
+                     <id>
                        728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
+                     </id>
+                     <caller>
+                       CALLER_ID:Int
+                     </caller>
+                     <callData>
+                       b"\n\x92T\xe4"
+                     </callData>
+                     <callValue>
                        0
-                     </balance>
+                     </callValue>
+                     <wordStack>
+                       ( 193 : ( selector ( "setUp()" ) : .WordStack ) )
+                     </wordStack>
+                     <localMem>
+                       b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`@Qa\x02z8\x03\x80a\x02z\x839\x81\x01`@\x81\x90Ra\x00/\x91a\x00TV[`\x00\x80T`\x01`\x01`\xa0\x1b\x03\x19\x16`\x01`\x01`\xa0\x1b\x03\x92\x90\x92\x16\x91\x90\x91\x17\x90Ua\x00\x84V[`\x00` \x82\x84\x03\x12\x15a\x00fW`\x00\x80\xfd[\x81Q`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x00}W`\x00\x80\xfd[\x93\x92PPPV[a\x01\xe7\x80a\x00\x93`\x009`\x00\xf3\xfe`\x80`@R`\x046\x10a\x00CW`\x005`\xe0\x1c\x80c\f\x11\xde\xdd\x14a\x00OW\x80c'\xe25\xe3\x14a\x00uW\x80cp\xa0\x821\x14a\x00\xa2W\x80c\xfc\fTj\x14a\x00\xd8W`\x00\x80\xfd[6a\x00JW\x00[`\x00\x80\xfd[a\x00ba\x00]6`\x04a\x01[V[a\x01\x10V[`@Q\x90\x81R` \x01[`@Q\x80\x91\x03\x90\xf3[4\x80\x15a\x00\x81W`\x00\x80\xfd[Pa\x00ba\x00\x906`\x04a\x01[V[`\x01` R`\x00\x90\x81R`@\x90 T\x81V[4\x80\x15a\x00\xaeW`\x00\x80\xfd[Pa\x00ba\x00\xbd6`\x04a\x01[V[`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[4\x80\x15a\x00\xe4W`\x00\x80\xfd[P`\x00Ta\x00\xf8\x90`\x01`\x01`\xa0\x1b\x03\x16\x81V[`@Q`\x01`\x01`\xa0\x1b\x03\x90\x91\x16\x81R` \x01a\x00lV[`\x01`\x01`\xa0\x1b\x03\x81\x16`\x00\x90\x81R`\x01` R`@\x81 \x80T4\x91\x90\x83\x90a\x01:\x90\x84\x90a\x01\x8bV[\x90\x91UPPP`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[`\x00` \x82\x84\x03\x12\x15a\x01mW`\x00\x80\xfd[\x815`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x01\x84W`\x00\x80\xfd[\x93\x92PPPV[`\x00\x82\x19\x82\x11\x15a\x01\xacWcNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[P\x01\x90V\xfe\xa2dipfsX\"\x12 \xa2\xe1\xe3\x00(\x01\xe6\n\xb4\xa6\xf0\\P2\x83h\x00\xc3\xacq\x8bm\n\xa0\xb4\xb7\xb6\xd2\x16\x88\x05\xb4dsolcC\x00\x08\r\x003\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"
+                     </localMem>
                      ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> => ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
                      ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
+                     <memoryUsed>
                        0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
+                     </memoryUsed>
+                     <callGas>
                        0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       2
-                     </nonce>
-                   </account> ) ) )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-               ))))))
-      [label(BASIC-BLOCK-1-TO-3)]
-    
-    rule [BASIC-BLOCK-3-TO-4]: <foundry>
-           <kevm>
-             <k>
-               ( #accessStorage 491460923342184218035706888008750043977755113263 0
-               ~> 0
-               ~> #deductGas
-               ~> SSTORE 0 0
-               ~> #pc [ SSTORE ] => #end EVMC_SUCCESS
-               ~> #pc [ RETURN ] )
-               ~> #execute
-               ~> #codeDeposit 491460923342184218035706888008750043977755113263
-               ~> #pc [ CREATE ]
-               ~> #execute
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   ( b"" => b"`\x80`@R`\x046\x10a\x00CW`\x005`\xe0\x1c\x80c\f\x11\xde\xdd\x14a\x00OW\x80c'\xe25\xe3\x14a\x00uW\x80cp\xa0\x821\x14a\x00\xa2W\x80c\xfc\fTj\x14a\x00\xd8W`\x00\x80\xfd[6a\x00JW\x00[`\x00\x80\xfd[a\x00ba\x00]6`\x04a\x01[V[a\x01\x10V[`@Q\x90\x81R` \x01[`@Q\x80\x91\x03\x90\xf3[4\x80\x15a\x00\x81W`\x00\x80\xfd[Pa\x00ba\x00\x906`\x04a\x01[V[`\x01` R`\x00\x90\x81R`@\x90 T\x81V[4\x80\x15a\x00\xaeW`\x00\x80\xfd[Pa\x00ba\x00\xbd6`\x04a\x01[V[`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[4\x80\x15a\x00\xe4W`\x00\x80\xfd[P`\x00Ta\x00\xf8\x90`\x01`\x01`\xa0\x1b\x03\x16\x81V[`@Q`\x01`\x01`\xa0\x1b\x03\x90\x91\x16\x81R` \x01a\x00lV[`\x01`\x01`\xa0\x1b\x03\x81\x16`\x00\x90\x81R`\x01` R`@\x81 \x80T4\x91\x90\x83\x90a\x01:\x90\x84\x90a\x01\x8bV[\x90\x91UPPP`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[`\x00` \x82\x84\x03\x12\x15a\x01mW`\x00\x80\xfd[\x815`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x01\x84W`\x00\x80\xfd[\x93\x92PPPV[`\x00\x82\x19\x82\x11\x15a\x01\xacWcNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[P\x01\x90V\xfe\xa2dipfsX\"\x12 \xa2\xe1\xe3\x00(\x01\xe6\n\xb4\xa6\xf0\\P2\x83h\x00\xc3\xacq\x8bm\n\xa0\xb4\xb7\xb6\xd2\x16\x88\x05\xb4dsolcC\x00\x08\r\x003" )
-                 </output>
-                 <callStack>
-                   ListItem ( <callState>-fragment ... ... <id>
-                     728815563385977040452943777879061427756277306518
-                   </id> <caller>
-                     CALLER_ID:Int
-                   </caller> <callData>
-                     b"\n\x92T\xe4"
-                   </callData> <callValue>
-                     0
-                   </callValue> <wordStack>
-                     ( 193 : ( selector ( "setUp()" ) : .WordStack ) )
-                   </wordStack> <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`@Qa\x02z8\x03\x80a\x02z\x839\x81\x01`@\x81\x90Ra\x00/\x91a\x00TV[`\x00\x80T`\x01`\x01`\xa0\x1b\x03\x19\x16`\x01`\x01`\xa0\x1b\x03\x92\x90\x92\x16\x91\x90\x91\x17\x90Ua\x00\x84V[`\x00` \x82\x84\x03\x12\x15a\x00fW`\x00\x80\xfd[\x81Q`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x00}W`\x00\x80\xfd[\x93\x92PPPV[a\x01\xe7\x80a\x00\x93`\x009`\x00\xf3\xfe`\x80`@R`\x046\x10a\x00CW`\x005`\xe0\x1c\x80c\f\x11\xde\xdd\x14a\x00OW\x80c'\xe25\xe3\x14a\x00uW\x80cp\xa0\x821\x14a\x00\xa2W\x80c\xfc\fTj\x14a\x00\xd8W`\x00\x80\xfd[6a\x00JW\x00[`\x00\x80\xfd[a\x00ba\x00]6`\x04a\x01[V[a\x01\x10V[`@Q\x90\x81R` \x01[`@Q\x80\x91\x03\x90\xf3[4\x80\x15a\x00\x81W`\x00\x80\xfd[Pa\x00ba\x00\x906`\x04a\x01[V[`\x01` R`\x00\x90\x81R`@\x90 T\x81V[4\x80\x15a\x00\xaeW`\x00\x80\xfd[Pa\x00ba\x00\xbd6`\x04a\x01[V[`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[4\x80\x15a\x00\xe4W`\x00\x80\xfd[P`\x00Ta\x00\xf8\x90`\x01`\x01`\xa0\x1b\x03\x16\x81V[`@Q`\x01`\x01`\xa0\x1b\x03\x90\x91\x16\x81R` \x01a\x00lV[`\x01`\x01`\xa0\x1b\x03\x81\x16`\x00\x90\x81R`\x01` R`@\x81 \x80T4\x91\x90\x83\x90a\x01:\x90\x84\x90a\x01\x8bV[\x90\x91UPPP`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[`\x00` \x82\x84\x03\x12\x15a\x01mW`\x00\x80\xfd[\x815`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x01\x84W`\x00\x80\xfd[\x93\x92PPPV[`\x00\x82\x19\x82\x11\x15a\x01\xacWcNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[P\x01\x90V\xfe\xa2dipfsX\"\x12 \xa2\xe1\xe3\x00(\x01\xe6\n\xb4\xa6\xf0\\P2\x83h\x00\xc3\xacq\x8bm\n\xa0\xb4\xb7\xb6\xd2\x16\x88\x05\xb4dsolcC\x00\x08\r\x003\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"
-                   </localMem> ... ... <memoryUsed>
-                     25
-                   </memoryUsed> <callGas>
-                     #gas ( #allBut64th ( ( VGAS:Int +Int -32419 ) ) )
-                   </callGas> <static>
-                     false
-                   </static> <callDepth>
-                     0
-                   </callDepth> </callState>-fragment )
+                     </callGas>
+                     <static>
+                       false
+                     </static>
+                     <callDepth>
+                       0
+                     </callDepth>
+                   </callState> ) )
                  </callStack>
                  <interimStates>
-                   ListItem ( { <accounts>-fragment ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
+                   ( .List => ListItem ( { <accounts>
+                     ( <account>
+                       <acctID>
+                         645326474426547203313410069153905908525362434349
+                       </acctID>
+                       <balance>
+                         0
+                       </balance>
+                       ...
+                       <storage>
+                         .Map
+                       </storage>
+                       <origStorage>
+                         .Map
+                       </origStorage>
+                       <nonce>
+                         0
+                       </nonce>
+                     </account>
+                     <account>
+                       <acctID>
+                         728815563385977040452943777879061427756277306518
+                       </acctID>
+                       <balance>
+                         0
+                       </balance>
+                       ...
+                       <storage>
+                         .Map
+                       </storage>
+                       <origStorage>
+                         .Map
+                       </origStorage>
+                       <nonce>
+                         2
+                       </nonce>
+                     </account> )
+                   </accounts> | <substate>
+                     <selfDestruct>
+                       SELFDESTRUCT_CELL:Set
+                     </selfDestruct>
+                     <log>
+                       .List
+                     </log>
+                     <refund>
                        0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       2
-                     </nonce>
-                   </account> ) </accounts>-fragment | <substate>-fragment <selfDestruct>
-                     SELFDESTRUCT_CELL:Set
-                   </selfDestruct> <log>
-                     .List
-                   </log> <refund>
-                     REFUND_CELL:Int
-                   </refund> <accessedAccounts>
-                     SetItem ( 491460923342184218035706888008750043977755113263 )
-                   </accessedAccounts> <accessedStorage>
-                     .Map
-                   </accessedStorage> </substate>-fragment } )
+                     </refund>
+                     <accessedAccounts>
+                       SetItem ( 491460923342184218035706888008750043977755113263 )
+                     </accessedAccounts>
+                     <accessedStorage>
+                       .Map
+                     </accessedStorage>
+                   </substate> } ) )
                  </interimStates>
                  <touchedAccounts>
-                   _TOUCHEDACCOUNTS_CELL |Set SetItem ( 728815563385977040452943777879061427756277306518 ) |Set SetItem ( 491460923342184218035706888008750043977755113263 )
+                   ( TOUCHEDACCOUNTS_CELL:Set => TOUCHEDACCOUNTS_CELL:Set |Set SetItem ( 728815563385977040452943777879061427756277306518 ) |Set SetItem ( 491460923342184218035706888008750043977755113263 ) )
                  </touchedAccounts>
                  <callState>
                    ...
                    ...
                    <id>
-                     491460923342184218035706888008750043977755113263
+                     ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 )
                    </id>
                    <caller>
-                     728815563385977040452943777879061427756277306518
+                     ( CALLER_ID:Int => 728815563385977040452943777879061427756277306518 )
                    </caller>
                    <callData>
-                     b""
+                     ( b"\n\x92T\xe4" => b"" )
                    </callData>
                    <callValue>
                      0
@@ -535,12 +229,12 @@
                      .WordStack
                    </wordStack>
                    <localMem>
-                     ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xa0\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" => b"`\x80`@R`\x046\x10a\x00CW`\x005`\xe0\x1c\x80c\f\x11\xde\xdd\x14a\x00OW\x80c'\xe25\xe3\x14a\x00uW\x80cp\xa0\x821\x14a\x00\xa2W\x80c\xfc\fTj\x14a\x00\xd8W`\x00\x80\xfd[6a\x00JW\x00[`\x00\x80\xfd[a\x00ba\x00]6`\x04a\x01[V[a\x01\x10V[`@Q\x90\x81R` \x01[`@Q\x80\x91\x03\x90\xf3[4\x80\x15a\x00\x81W`\x00\x80\xfd[Pa\x00ba\x00\x906`\x04a\x01[V[`\x01` R`\x00\x90\x81R`@\x90 T\x81V[4\x80\x15a\x00\xaeW`\x00\x80\xfd[Pa\x00ba\x00\xbd6`\x04a\x01[V[`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[4\x80\x15a\x00\xe4W`\x00\x80\xfd[P`\x00Ta\x00\xf8\x90`\x01`\x01`\xa0\x1b\x03\x16\x81V[`@Q`\x01`\x01`\xa0\x1b\x03\x90\x91\x16\x81R` \x01a\x00lV[`\x01`\x01`\xa0\x1b\x03\x81\x16`\x00\x90\x81R`\x01` R`@\x81 \x80T4\x91\x90\x83\x90a\x01:\x90\x84\x90a\x01\x8bV[\x90\x91UPPP`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[`\x00` \x82\x84\x03\x12\x15a\x01mW`\x00\x80\xfd[\x815`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x01\x84W`\x00\x80\xfd[\x93\x92PPPV[`\x00\x82\x19\x82\x11\x15a\x01\xacWcNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[P\x01\x90V\xfe\xa2dipfsX\"\x12 \xa2\xe1\xe3\x00(\x01\xe6\n\xb4\xa6\xf0\\P2\x83h\x00\xc3\xacq\x8bm\n\xa0\xb4\xb7\xb6\xd2\x16\x88\x05\xb4dsolcC\x00\x08\r\x003" )
+                     ( b"" => b"`\x80`@R`\x046\x10a\x00CW`\x005`\xe0\x1c\x80c\f\x11\xde\xdd\x14a\x00OW\x80c'\xe25\xe3\x14a\x00uW\x80cp\xa0\x821\x14a\x00\xa2W\x80c\xfc\fTj\x14a\x00\xd8W`\x00\x80\xfd[6a\x00JW\x00[`\x00\x80\xfd[a\x00ba\x00]6`\x04a\x01[V[a\x01\x10V[`@Q\x90\x81R` \x01[`@Q\x80\x91\x03\x90\xf3[4\x80\x15a\x00\x81W`\x00\x80\xfd[Pa\x00ba\x00\x906`\x04a\x01[V[`\x01` R`\x00\x90\x81R`@\x90 T\x81V[4\x80\x15a\x00\xaeW`\x00\x80\xfd[Pa\x00ba\x00\xbd6`\x04a\x01[V[`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[4\x80\x15a\x00\xe4W`\x00\x80\xfd[P`\x00Ta\x00\xf8\x90`\x01`\x01`\xa0\x1b\x03\x16\x81V[`@Q`\x01`\x01`\xa0\x1b\x03\x90\x91\x16\x81R` \x01a\x00lV[`\x01`\x01`\xa0\x1b\x03\x81\x16`\x00\x90\x81R`\x01` R`@\x81 \x80T4\x91\x90\x83\x90a\x01:\x90\x84\x90a\x01\x8bV[\x90\x91UPPP`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[`\x00` \x82\x84\x03\x12\x15a\x01mW`\x00\x80\xfd[\x815`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x01\x84W`\x00\x80\xfd[\x93\x92PPPV[`\x00\x82\x19\x82\x11\x15a\x01\xacWcNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[P\x01\x90V\xfe\xa2dipfsX\"\x12 \xa2\xe1\xe3\x00(\x01\xe6\n\xb4\xa6\xf0\\P2\x83h\x00\xc3\xacq\x8bm\n\xa0\xb4\xb7\xb6\xd2\x16\x88\x05\xb4dsolcC\x00\x08\r\x003" )
                    </localMem>
                    ...
                    ...
                    <memoryUsed>
-                     ( 5 => 16 )
+                     0
                    </memoryUsed>
                    <callGas>
                      0
@@ -549,7 +243,7 @@
                      false
                    </static>
                    <callDepth>
-                     1
+                     ( 0 => 1 )
                    </callDepth>
                  </callState>
                  <substate>
@@ -560,13 +254,13 @@
                      .List
                    </log>
                    <refund>
-                     REFUND_CELL:Int
+                     0
                    </refund>
                    <accessedAccounts>
-                     ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
+                     ( .Set => ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) )
                    </accessedAccounts>
                    <accessedStorage>
-                     ( 491460923342184218035706888008750043977755113263 |-> SetItem ( 0 ) )
+                     ( .Map => ( 491460923342184218035706888008750043977755113263 |-> SetItem ( 0 ) ) )
                    </accessedStorage>
                  </substate>
                  <origin>
@@ -584,7 +278,7 @@
                  <accounts>
                    ( <account>
                      <acctID>
-                       491460923342184218035706888008750043977755113263
+                       ( 645326474426547203313410069153905908525362434349 => 491460923342184218035706888008750043977755113263 )
                      </acctID>
                      <balance>
                        0
@@ -597,10 +291,27 @@
                        .Map
                      </origStorage>
                      <nonce>
-                       1
+                       ( 0 => 1 )
                      </nonce>
                    </account>
                    ( <account>
+                     <acctID>
+                       728815563385977040452943777879061427756277306518
+                     </acctID>
+                     <balance>
+                       0
+                     </balance>
+                     ...
+                     <storage>
+                       .Map
+                     </storage>
+                     <origStorage>
+                       .Map
+                     </origStorage>
+                     <nonce>
+                       1
+                     </nonce>
+                   </account> => ( <account>
                      <acctID>
                        645326474426547203313410069153905908525362434349
                      </acctID>
@@ -635,7 +346,7 @@
                      <nonce>
                        2
                      </nonce>
-                   </account> ) )
+                   </account> ) ) )
                  </accounts>
                  ...
                </network>
@@ -719,9 +430,9 @@
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
                ))))))
-      [label(BASIC-BLOCK-3-TO-4)]
+      [label(BASIC-BLOCK-1-TO-3)]
     
-    rule [BASIC-BLOCK-4-TO-5]: <foundry>
+    rule [BASIC-BLOCK-3-TO-4]: <foundry>
            <kevm>
              <k>
                ( #end EVMC_SUCCESS => #halt )
@@ -738,6 +449,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -747,75 +461,98 @@
                    ( _STATUSCODE => EVMC_SUCCESS )
                  </statusCode>
                  <callStack>
-                   ListItem ( <callState>-fragment ... ... <id>
-                     728815563385977040452943777879061427756277306518
-                   </id> <caller>
-                     CALLER_ID:Int
-                   </caller> <callData>
-                     b"\n\x92T\xe4"
-                   </callData> <callValue>
-                     0
-                   </callValue> <wordStack>
-                     ( 193 : ( selector ( "setUp()" ) : .WordStack ) )
-                   </wordStack> <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`@Qa\x02z8\x03\x80a\x02z\x839\x81\x01`@\x81\x90Ra\x00/\x91a\x00TV[`\x00\x80T`\x01`\x01`\xa0\x1b\x03\x19\x16`\x01`\x01`\xa0\x1b\x03\x92\x90\x92\x16\x91\x90\x91\x17\x90Ua\x00\x84V[`\x00` \x82\x84\x03\x12\x15a\x00fW`\x00\x80\xfd[\x81Q`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x00}W`\x00\x80\xfd[\x93\x92PPPV[a\x01\xe7\x80a\x00\x93`\x009`\x00\xf3\xfe`\x80`@R`\x046\x10a\x00CW`\x005`\xe0\x1c\x80c\f\x11\xde\xdd\x14a\x00OW\x80c'\xe25\xe3\x14a\x00uW\x80cp\xa0\x821\x14a\x00\xa2W\x80c\xfc\fTj\x14a\x00\xd8W`\x00\x80\xfd[6a\x00JW\x00[`\x00\x80\xfd[a\x00ba\x00]6`\x04a\x01[V[a\x01\x10V[`@Q\x90\x81R` \x01[`@Q\x80\x91\x03\x90\xf3[4\x80\x15a\x00\x81W`\x00\x80\xfd[Pa\x00ba\x00\x906`\x04a\x01[V[`\x01` R`\x00\x90\x81R`@\x90 T\x81V[4\x80\x15a\x00\xaeW`\x00\x80\xfd[Pa\x00ba\x00\xbd6`\x04a\x01[V[`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[4\x80\x15a\x00\xe4W`\x00\x80\xfd[P`\x00Ta\x00\xf8\x90`\x01`\x01`\xa0\x1b\x03\x16\x81V[`@Q`\x01`\x01`\xa0\x1b\x03\x90\x91\x16\x81R` \x01a\x00lV[`\x01`\x01`\xa0\x1b\x03\x81\x16`\x00\x90\x81R`\x01` R`@\x81 \x80T4\x91\x90\x83\x90a\x01:\x90\x84\x90a\x01\x8bV[\x90\x91UPPP`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[`\x00` \x82\x84\x03\x12\x15a\x01mW`\x00\x80\xfd[\x815`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x01\x84W`\x00\x80\xfd[\x93\x92PPPV[`\x00\x82\x19\x82\x11\x15a\x01\xacWcNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[P\x01\x90V\xfe\xa2dipfsX\"\x12 \xa2\xe1\xe3\x00(\x01\xe6\n\xb4\xa6\xf0\\P2\x83h\x00\xc3\xacq\x8bm\n\xa0\xb4\xb7\xb6\xd2\x16\x88\x05\xb4dsolcC\x00\x08\r\x003\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"
-                   </localMem> ... ... <memoryUsed>
-                     25
-                   </memoryUsed> <callGas>
-                     #gas ( #allBut64th ( ( VGAS:Int +Int -32419 ) ) )
-                   </callGas> <static>
-                     false
-                   </static> <callDepth>
-                     0
-                   </callDepth> </callState>-fragment )
-                 </callStack>
-                 <interimStates>
-                   ListItem ( { <accounts>-fragment ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
+                   ListItem ( <callState>
                      ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
+                     ...
+                     <id>
                        728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
+                     </id>
+                     <caller>
+                       CALLER_ID:Int
+                     </caller>
+                     <callData>
+                       b"\n\x92T\xe4"
+                     </callData>
+                     <callValue>
                        0
-                     </balance>
+                     </callValue>
+                     <wordStack>
+                       ( 193 : ( selector ( "setUp()" ) : .WordStack ) )
+                     </wordStack>
+                     <localMem>
+                       b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`@Qa\x02z8\x03\x80a\x02z\x839\x81\x01`@\x81\x90Ra\x00/\x91a\x00TV[`\x00\x80T`\x01`\x01`\xa0\x1b\x03\x19\x16`\x01`\x01`\xa0\x1b\x03\x92\x90\x92\x16\x91\x90\x91\x17\x90Ua\x00\x84V[`\x00` \x82\x84\x03\x12\x15a\x00fW`\x00\x80\xfd[\x81Q`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x00}W`\x00\x80\xfd[\x93\x92PPPV[a\x01\xe7\x80a\x00\x93`\x009`\x00\xf3\xfe`\x80`@R`\x046\x10a\x00CW`\x005`\xe0\x1c\x80c\f\x11\xde\xdd\x14a\x00OW\x80c'\xe25\xe3\x14a\x00uW\x80cp\xa0\x821\x14a\x00\xa2W\x80c\xfc\fTj\x14a\x00\xd8W`\x00\x80\xfd[6a\x00JW\x00[`\x00\x80\xfd[a\x00ba\x00]6`\x04a\x01[V[a\x01\x10V[`@Q\x90\x81R` \x01[`@Q\x80\x91\x03\x90\xf3[4\x80\x15a\x00\x81W`\x00\x80\xfd[Pa\x00ba\x00\x906`\x04a\x01[V[`\x01` R`\x00\x90\x81R`@\x90 T\x81V[4\x80\x15a\x00\xaeW`\x00\x80\xfd[Pa\x00ba\x00\xbd6`\x04a\x01[V[`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[4\x80\x15a\x00\xe4W`\x00\x80\xfd[P`\x00Ta\x00\xf8\x90`\x01`\x01`\xa0\x1b\x03\x16\x81V[`@Q`\x01`\x01`\xa0\x1b\x03\x90\x91\x16\x81R` \x01a\x00lV[`\x01`\x01`\xa0\x1b\x03\x81\x16`\x00\x90\x81R`\x01` R`@\x81 \x80T4\x91\x90\x83\x90a\x01:\x90\x84\x90a\x01\x8bV[\x90\x91UPPP`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[`\x00` \x82\x84\x03\x12\x15a\x01mW`\x00\x80\xfd[\x815`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x01\x84W`\x00\x80\xfd[\x93\x92PPPV[`\x00\x82\x19\x82\x11\x15a\x01\xacWcNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[P\x01\x90V\xfe\xa2dipfsX\"\x12 \xa2\xe1\xe3\x00(\x01\xe6\n\xb4\xa6\xf0\\P2\x83h\x00\xc3\xacq\x8bm\n\xa0\xb4\xb7\xb6\xd2\x16\x88\x05\xb4dsolcC\x00\x08\r\x003\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"
+                     </localMem>
                      ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       2
-                     </nonce>
-                   </account> ) </accounts>-fragment | <substate>-fragment <selfDestruct>
-                     SELFDESTRUCT_CELL:Set
-                   </selfDestruct> <log>
-                     .List
-                   </log> <refund>
-                     REFUND_CELL:Int
-                   </refund> <accessedAccounts>
-                     SetItem ( 491460923342184218035706888008750043977755113263 )
-                   </accessedAccounts> <accessedStorage>
-                     .Map
-                   </accessedStorage> </substate>-fragment } )
+                     ...
+                     <memoryUsed>
+                       0
+                     </memoryUsed>
+                     <callGas>
+                       0
+                     </callGas>
+                     <static>
+                       false
+                     </static>
+                     <callDepth>
+                       0
+                     </callDepth>
+                   </callState> )
+                 </callStack>
+                 <interimStates>
+                   ListItem ( { <accounts>
+                     ( <account>
+                       <acctID>
+                         645326474426547203313410069153905908525362434349
+                       </acctID>
+                       <balance>
+                         0
+                       </balance>
+                       ...
+                       <storage>
+                         .Map
+                       </storage>
+                       <origStorage>
+                         .Map
+                       </origStorage>
+                       <nonce>
+                         0
+                       </nonce>
+                     </account>
+                     <account>
+                       <acctID>
+                         728815563385977040452943777879061427756277306518
+                       </acctID>
+                       <balance>
+                         0
+                       </balance>
+                       ...
+                       <storage>
+                         .Map
+                       </storage>
+                       <origStorage>
+                         .Map
+                       </origStorage>
+                       <nonce>
+                         2
+                       </nonce>
+                     </account> )
+                   </accounts> | <substate>
+                     <selfDestruct>
+                       SELFDESTRUCT_CELL:Set
+                     </selfDestruct>
+                     <log>
+                       .List
+                     </log>
+                     <refund>
+                       0
+                     </refund>
+                     <accessedAccounts>
+                       SetItem ( 491460923342184218035706888008750043977755113263 )
+                     </accessedAccounts>
+                     <accessedStorage>
+                       .Map
+                     </accessedStorage>
+                   </substate> } )
                  </interimStates>
                  <touchedAccounts>
                    _TOUCHEDACCOUNTS_CELL |Set SetItem ( 728815563385977040452943777879061427756277306518 ) |Set SetItem ( 491460923342184218035706888008750043977755113263 )
@@ -844,7 +581,7 @@
                    ...
                    ...
                    <memoryUsed>
-                     16
+                     0
                    </memoryUsed>
                    <callGas>
                      0
@@ -864,7 +601,7 @@
                      .List
                    </log>
                    <refund>
-                     REFUND_CELL:Int
+                     0
                    </refund>
                    <accessedAccounts>
                      ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
@@ -1023,9 +760,9 @@
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
                ))))))
-      [label(BASIC-BLOCK-4-TO-5)]
+      [label(BASIC-BLOCK-3-TO-4)]
     
-    rule [BASIC-BLOCK-5-TO-6]: <foundry>
+    rule [BASIC-BLOCK-4-TO-5]: <foundry>
            <kevm>
              <k>
                #halt
@@ -1042,6 +779,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1051,75 +791,98 @@
                    EVMC_SUCCESS
                  </statusCode>
                  <callStack>
-                   ListItem ( <callState>-fragment ... ... <id>
-                     728815563385977040452943777879061427756277306518
-                   </id> <caller>
-                     CALLER_ID:Int
-                   </caller> <callData>
-                     b"\n\x92T\xe4"
-                   </callData> <callValue>
-                     0
-                   </callValue> <wordStack>
-                     ( 193 : ( selector ( "setUp()" ) : .WordStack ) )
-                   </wordStack> <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`@Qa\x02z8\x03\x80a\x02z\x839\x81\x01`@\x81\x90Ra\x00/\x91a\x00TV[`\x00\x80T`\x01`\x01`\xa0\x1b\x03\x19\x16`\x01`\x01`\xa0\x1b\x03\x92\x90\x92\x16\x91\x90\x91\x17\x90Ua\x00\x84V[`\x00` \x82\x84\x03\x12\x15a\x00fW`\x00\x80\xfd[\x81Q`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x00}W`\x00\x80\xfd[\x93\x92PPPV[a\x01\xe7\x80a\x00\x93`\x009`\x00\xf3\xfe`\x80`@R`\x046\x10a\x00CW`\x005`\xe0\x1c\x80c\f\x11\xde\xdd\x14a\x00OW\x80c'\xe25\xe3\x14a\x00uW\x80cp\xa0\x821\x14a\x00\xa2W\x80c\xfc\fTj\x14a\x00\xd8W`\x00\x80\xfd[6a\x00JW\x00[`\x00\x80\xfd[a\x00ba\x00]6`\x04a\x01[V[a\x01\x10V[`@Q\x90\x81R` \x01[`@Q\x80\x91\x03\x90\xf3[4\x80\x15a\x00\x81W`\x00\x80\xfd[Pa\x00ba\x00\x906`\x04a\x01[V[`\x01` R`\x00\x90\x81R`@\x90 T\x81V[4\x80\x15a\x00\xaeW`\x00\x80\xfd[Pa\x00ba\x00\xbd6`\x04a\x01[V[`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[4\x80\x15a\x00\xe4W`\x00\x80\xfd[P`\x00Ta\x00\xf8\x90`\x01`\x01`\xa0\x1b\x03\x16\x81V[`@Q`\x01`\x01`\xa0\x1b\x03\x90\x91\x16\x81R` \x01a\x00lV[`\x01`\x01`\xa0\x1b\x03\x81\x16`\x00\x90\x81R`\x01` R`@\x81 \x80T4\x91\x90\x83\x90a\x01:\x90\x84\x90a\x01\x8bV[\x90\x91UPPP`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[`\x00` \x82\x84\x03\x12\x15a\x01mW`\x00\x80\xfd[\x815`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x01\x84W`\x00\x80\xfd[\x93\x92PPPV[`\x00\x82\x19\x82\x11\x15a\x01\xacWcNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[P\x01\x90V\xfe\xa2dipfsX\"\x12 \xa2\xe1\xe3\x00(\x01\xe6\n\xb4\xa6\xf0\\P2\x83h\x00\xc3\xacq\x8bm\n\xa0\xb4\xb7\xb6\xd2\x16\x88\x05\xb4dsolcC\x00\x08\r\x003\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"
-                   </localMem> ... ... <memoryUsed>
-                     25
-                   </memoryUsed> <callGas>
-                     #gas ( #allBut64th ( ( VGAS:Int +Int -32419 ) ) )
-                   </callGas> <static>
-                     false
-                   </static> <callDepth>
-                     0
-                   </callDepth> </callState>-fragment )
-                 </callStack>
-                 <interimStates>
-                   ListItem ( { <accounts>-fragment ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
+                   ListItem ( <callState>
                      ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
+                     ...
+                     <id>
                        728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
+                     </id>
+                     <caller>
+                       CALLER_ID:Int
+                     </caller>
+                     <callData>
+                       b"\n\x92T\xe4"
+                     </callData>
+                     <callValue>
                        0
-                     </balance>
+                     </callValue>
+                     <wordStack>
+                       ( 193 : ( selector ( "setUp()" ) : .WordStack ) )
+                     </wordStack>
+                     <localMem>
+                       b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`@Qa\x02z8\x03\x80a\x02z\x839\x81\x01`@\x81\x90Ra\x00/\x91a\x00TV[`\x00\x80T`\x01`\x01`\xa0\x1b\x03\x19\x16`\x01`\x01`\xa0\x1b\x03\x92\x90\x92\x16\x91\x90\x91\x17\x90Ua\x00\x84V[`\x00` \x82\x84\x03\x12\x15a\x00fW`\x00\x80\xfd[\x81Q`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x00}W`\x00\x80\xfd[\x93\x92PPPV[a\x01\xe7\x80a\x00\x93`\x009`\x00\xf3\xfe`\x80`@R`\x046\x10a\x00CW`\x005`\xe0\x1c\x80c\f\x11\xde\xdd\x14a\x00OW\x80c'\xe25\xe3\x14a\x00uW\x80cp\xa0\x821\x14a\x00\xa2W\x80c\xfc\fTj\x14a\x00\xd8W`\x00\x80\xfd[6a\x00JW\x00[`\x00\x80\xfd[a\x00ba\x00]6`\x04a\x01[V[a\x01\x10V[`@Q\x90\x81R` \x01[`@Q\x80\x91\x03\x90\xf3[4\x80\x15a\x00\x81W`\x00\x80\xfd[Pa\x00ba\x00\x906`\x04a\x01[V[`\x01` R`\x00\x90\x81R`@\x90 T\x81V[4\x80\x15a\x00\xaeW`\x00\x80\xfd[Pa\x00ba\x00\xbd6`\x04a\x01[V[`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[4\x80\x15a\x00\xe4W`\x00\x80\xfd[P`\x00Ta\x00\xf8\x90`\x01`\x01`\xa0\x1b\x03\x16\x81V[`@Q`\x01`\x01`\xa0\x1b\x03\x90\x91\x16\x81R` \x01a\x00lV[`\x01`\x01`\xa0\x1b\x03\x81\x16`\x00\x90\x81R`\x01` R`@\x81 \x80T4\x91\x90\x83\x90a\x01:\x90\x84\x90a\x01\x8bV[\x90\x91UPPP`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[`\x00` \x82\x84\x03\x12\x15a\x01mW`\x00\x80\xfd[\x815`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x01\x84W`\x00\x80\xfd[\x93\x92PPPV[`\x00\x82\x19\x82\x11\x15a\x01\xacWcNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[P\x01\x90V\xfe\xa2dipfsX\"\x12 \xa2\xe1\xe3\x00(\x01\xe6\n\xb4\xa6\xf0\\P2\x83h\x00\xc3\xacq\x8bm\n\xa0\xb4\xb7\xb6\xd2\x16\x88\x05\xb4dsolcC\x00\x08\r\x003\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"
+                     </localMem>
                      ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       2
-                     </nonce>
-                   </account> ) </accounts>-fragment | <substate>-fragment <selfDestruct>
-                     SELFDESTRUCT_CELL:Set
-                   </selfDestruct> <log>
-                     .List
-                   </log> <refund>
-                     REFUND_CELL:Int
-                   </refund> <accessedAccounts>
-                     SetItem ( 491460923342184218035706888008750043977755113263 )
-                   </accessedAccounts> <accessedStorage>
-                     .Map
-                   </accessedStorage> </substate>-fragment } )
+                     ...
+                     <memoryUsed>
+                       0
+                     </memoryUsed>
+                     <callGas>
+                       0
+                     </callGas>
+                     <static>
+                       false
+                     </static>
+                     <callDepth>
+                       0
+                     </callDepth>
+                   </callState> )
+                 </callStack>
+                 <interimStates>
+                   ListItem ( { <accounts>
+                     ( <account>
+                       <acctID>
+                         645326474426547203313410069153905908525362434349
+                       </acctID>
+                       <balance>
+                         0
+                       </balance>
+                       ...
+                       <storage>
+                         .Map
+                       </storage>
+                       <origStorage>
+                         .Map
+                       </origStorage>
+                       <nonce>
+                         0
+                       </nonce>
+                     </account>
+                     <account>
+                       <acctID>
+                         728815563385977040452943777879061427756277306518
+                       </acctID>
+                       <balance>
+                         0
+                       </balance>
+                       ...
+                       <storage>
+                         .Map
+                       </storage>
+                       <origStorage>
+                         .Map
+                       </origStorage>
+                       <nonce>
+                         2
+                       </nonce>
+                     </account> )
+                   </accounts> | <substate>
+                     <selfDestruct>
+                       SELFDESTRUCT_CELL:Set
+                     </selfDestruct>
+                     <log>
+                       .List
+                     </log>
+                     <refund>
+                       0
+                     </refund>
+                     <accessedAccounts>
+                       SetItem ( 491460923342184218035706888008750043977755113263 )
+                     </accessedAccounts>
+                     <accessedStorage>
+                       .Map
+                     </accessedStorage>
+                   </substate> } )
                  </interimStates>
                  <touchedAccounts>
                    _TOUCHEDACCOUNTS_CELL |Set SetItem ( 728815563385977040452943777879061427756277306518 ) |Set SetItem ( 491460923342184218035706888008750043977755113263 )
@@ -1148,7 +911,7 @@
                    ...
                    ...
                    <memoryUsed>
-                     16
+                     0
                    </memoryUsed>
                    <callGas>
                      0
@@ -1168,7 +931,7 @@
                      .List
                    </log>
                    <refund>
-                     REFUND_CELL:Int
+                     0
                    </refund>
                    <accessedAccounts>
                      ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
@@ -1327,9 +1090,9 @@
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
                ))))))
-      [label(BASIC-BLOCK-5-TO-6)]
+      [label(BASIC-BLOCK-4-TO-5)]
     
-    rule [BASIC-BLOCK-6-TO-7]: <foundry>
+    rule [BASIC-BLOCK-5-TO-6]: <foundry>
            <kevm>
              <k>
                ( #halt
@@ -1345,6 +1108,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1354,75 +1120,98 @@
                    EVMC_SUCCESS
                  </statusCode>
                  <callStack>
-                   ( ListItem ( <callState>-fragment ... ... <id>
-                     728815563385977040452943777879061427756277306518
-                   </id> <caller>
-                     CALLER_ID:Int
-                   </caller> <callData>
-                     b"\n\x92T\xe4"
-                   </callData> <callValue>
-                     0
-                   </callValue> <wordStack>
-                     ( 193 : ( selector ( "setUp()" ) : .WordStack ) )
-                   </wordStack> <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`@Qa\x02z8\x03\x80a\x02z\x839\x81\x01`@\x81\x90Ra\x00/\x91a\x00TV[`\x00\x80T`\x01`\x01`\xa0\x1b\x03\x19\x16`\x01`\x01`\xa0\x1b\x03\x92\x90\x92\x16\x91\x90\x91\x17\x90Ua\x00\x84V[`\x00` \x82\x84\x03\x12\x15a\x00fW`\x00\x80\xfd[\x81Q`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x00}W`\x00\x80\xfd[\x93\x92PPPV[a\x01\xe7\x80a\x00\x93`\x009`\x00\xf3\xfe`\x80`@R`\x046\x10a\x00CW`\x005`\xe0\x1c\x80c\f\x11\xde\xdd\x14a\x00OW\x80c'\xe25\xe3\x14a\x00uW\x80cp\xa0\x821\x14a\x00\xa2W\x80c\xfc\fTj\x14a\x00\xd8W`\x00\x80\xfd[6a\x00JW\x00[`\x00\x80\xfd[a\x00ba\x00]6`\x04a\x01[V[a\x01\x10V[`@Q\x90\x81R` \x01[`@Q\x80\x91\x03\x90\xf3[4\x80\x15a\x00\x81W`\x00\x80\xfd[Pa\x00ba\x00\x906`\x04a\x01[V[`\x01` R`\x00\x90\x81R`@\x90 T\x81V[4\x80\x15a\x00\xaeW`\x00\x80\xfd[Pa\x00ba\x00\xbd6`\x04a\x01[V[`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[4\x80\x15a\x00\xe4W`\x00\x80\xfd[P`\x00Ta\x00\xf8\x90`\x01`\x01`\xa0\x1b\x03\x16\x81V[`@Q`\x01`\x01`\xa0\x1b\x03\x90\x91\x16\x81R` \x01a\x00lV[`\x01`\x01`\xa0\x1b\x03\x81\x16`\x00\x90\x81R`\x01` R`@\x81 \x80T4\x91\x90\x83\x90a\x01:\x90\x84\x90a\x01\x8bV[\x90\x91UPPP`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[`\x00` \x82\x84\x03\x12\x15a\x01mW`\x00\x80\xfd[\x815`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x01\x84W`\x00\x80\xfd[\x93\x92PPPV[`\x00\x82\x19\x82\x11\x15a\x01\xacWcNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[P\x01\x90V\xfe\xa2dipfsX\"\x12 \xa2\xe1\xe3\x00(\x01\xe6\n\xb4\xa6\xf0\\P2\x83h\x00\xc3\xacq\x8bm\n\xa0\xb4\xb7\xb6\xd2\x16\x88\x05\xb4dsolcC\x00\x08\r\x003\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"
-                   </localMem> ... ... <memoryUsed>
-                     25
-                   </memoryUsed> <callGas>
-                     #gas ( #allBut64th ( ( VGAS:Int +Int -32419 ) ) )
-                   </callGas> <static>
-                     false
-                   </static> <callDepth>
-                     0
-                   </callDepth> </callState>-fragment ) => .List )
-                 </callStack>
-                 <interimStates>
-                   ( ListItem ( { <accounts>-fragment ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
+                   ( ListItem ( <callState>
                      ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
+                     ...
+                     <id>
                        728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
+                     </id>
+                     <caller>
+                       CALLER_ID:Int
+                     </caller>
+                     <callData>
+                       b"\n\x92T\xe4"
+                     </callData>
+                     <callValue>
                        0
-                     </balance>
+                     </callValue>
+                     <wordStack>
+                       ( 193 : ( selector ( "setUp()" ) : .WordStack ) )
+                     </wordStack>
+                     <localMem>
+                       b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`@Qa\x02z8\x03\x80a\x02z\x839\x81\x01`@\x81\x90Ra\x00/\x91a\x00TV[`\x00\x80T`\x01`\x01`\xa0\x1b\x03\x19\x16`\x01`\x01`\xa0\x1b\x03\x92\x90\x92\x16\x91\x90\x91\x17\x90Ua\x00\x84V[`\x00` \x82\x84\x03\x12\x15a\x00fW`\x00\x80\xfd[\x81Q`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x00}W`\x00\x80\xfd[\x93\x92PPPV[a\x01\xe7\x80a\x00\x93`\x009`\x00\xf3\xfe`\x80`@R`\x046\x10a\x00CW`\x005`\xe0\x1c\x80c\f\x11\xde\xdd\x14a\x00OW\x80c'\xe25\xe3\x14a\x00uW\x80cp\xa0\x821\x14a\x00\xa2W\x80c\xfc\fTj\x14a\x00\xd8W`\x00\x80\xfd[6a\x00JW\x00[`\x00\x80\xfd[a\x00ba\x00]6`\x04a\x01[V[a\x01\x10V[`@Q\x90\x81R` \x01[`@Q\x80\x91\x03\x90\xf3[4\x80\x15a\x00\x81W`\x00\x80\xfd[Pa\x00ba\x00\x906`\x04a\x01[V[`\x01` R`\x00\x90\x81R`@\x90 T\x81V[4\x80\x15a\x00\xaeW`\x00\x80\xfd[Pa\x00ba\x00\xbd6`\x04a\x01[V[`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[4\x80\x15a\x00\xe4W`\x00\x80\xfd[P`\x00Ta\x00\xf8\x90`\x01`\x01`\xa0\x1b\x03\x16\x81V[`@Q`\x01`\x01`\xa0\x1b\x03\x90\x91\x16\x81R` \x01a\x00lV[`\x01`\x01`\xa0\x1b\x03\x81\x16`\x00\x90\x81R`\x01` R`@\x81 \x80T4\x91\x90\x83\x90a\x01:\x90\x84\x90a\x01\x8bV[\x90\x91UPPP`\x01`\x01`\xa0\x1b\x03\x16`\x00\x90\x81R`\x01` R`@\x90 T\x90V[`\x00` \x82\x84\x03\x12\x15a\x01mW`\x00\x80\xfd[\x815`\x01`\x01`\xa0\x1b\x03\x81\x16\x81\x14a\x01\x84W`\x00\x80\xfd[\x93\x92PPPV[`\x00\x82\x19\x82\x11\x15a\x01\xacWcNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[P\x01\x90V\xfe\xa2dipfsX\"\x12 \xa2\xe1\xe3\x00(\x01\xe6\n\xb4\xa6\xf0\\P2\x83h\x00\xc3\xacq\x8bm\n\xa0\xb4\xb7\xb6\xd2\x16\x88\x05\xb4dsolcC\x00\x08\r\x003\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"
+                     </localMem>
                      ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       2
-                     </nonce>
-                   </account> ) </accounts>-fragment | <substate>-fragment <selfDestruct>
-                     SELFDESTRUCT_CELL:Set
-                   </selfDestruct> <log>
-                     .List
-                   </log> <refund>
-                     REFUND_CELL:Int
-                   </refund> <accessedAccounts>
-                     SetItem ( 491460923342184218035706888008750043977755113263 )
-                   </accessedAccounts> <accessedStorage>
-                     .Map
-                   </accessedStorage> </substate>-fragment } ) => .List )
+                     ...
+                     <memoryUsed>
+                       0
+                     </memoryUsed>
+                     <callGas>
+                       0
+                     </callGas>
+                     <static>
+                       false
+                     </static>
+                     <callDepth>
+                       0
+                     </callDepth>
+                   </callState> ) => .List )
+                 </callStack>
+                 <interimStates>
+                   ( ListItem ( { <accounts>
+                     ( <account>
+                       <acctID>
+                         645326474426547203313410069153905908525362434349
+                       </acctID>
+                       <balance>
+                         0
+                       </balance>
+                       ...
+                       <storage>
+                         .Map
+                       </storage>
+                       <origStorage>
+                         .Map
+                       </origStorage>
+                       <nonce>
+                         0
+                       </nonce>
+                     </account>
+                     <account>
+                       <acctID>
+                         728815563385977040452943777879061427756277306518
+                       </acctID>
+                       <balance>
+                         0
+                       </balance>
+                       ...
+                       <storage>
+                         .Map
+                       </storage>
+                       <origStorage>
+                         .Map
+                       </origStorage>
+                       <nonce>
+                         2
+                       </nonce>
+                     </account> )
+                   </accounts> | <substate>
+                     <selfDestruct>
+                       SELFDESTRUCT_CELL:Set
+                     </selfDestruct>
+                     <log>
+                       .List
+                     </log>
+                     <refund>
+                       0
+                     </refund>
+                     <accessedAccounts>
+                       SetItem ( 491460923342184218035706888008750043977755113263 )
+                     </accessedAccounts>
+                     <accessedStorage>
+                       .Map
+                     </accessedStorage>
+                   </substate> } ) => .List )
                  </interimStates>
                  <touchedAccounts>
                    _TOUCHEDACCOUNTS_CELL |Set SetItem ( 728815563385977040452943777879061427756277306518 ) |Set SetItem ( 491460923342184218035706888008750043977755113263 )
@@ -1451,10 +1240,10 @@
                    ...
                    ...
                    <memoryUsed>
-                     ( 16 => 25 )
+                     0
                    </memoryUsed>
                    <callGas>
-                     ( 0 => #gas ( #allBut64th ( ( VGAS:Int +Int -32419 ) ) ) )
+                     0
                    </callGas>
                    <static>
                      false
@@ -1471,7 +1260,7 @@
                      .List
                    </log>
                    <refund>
-                     REFUND_CELL:Int
+                     0
                    </refund>
                    <accessedAccounts>
                      ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
@@ -1631,9 +1420,9 @@
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
                ))))))
-      [label(BASIC-BLOCK-6-TO-7)]
+      [label(BASIC-BLOCK-5-TO-6)]
     
-    rule [BASIC-BLOCK-7-TO-8]: <foundry>
+    rule [BASIC-BLOCK-6-TO-7]: <foundry>
            <kevm>
              <k>
                ( #end EVMC_SUCCESS => #halt )
@@ -1647,6 +1436,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1688,10 +1480,10 @@
                    ...
                    ...
                    <memoryUsed>
-                     25
+                     0
                    </memoryUsed>
                    <callGas>
-                     #gas ( #allBut64th ( ( VGAS:Int +Int -32419 ) ) )
+                     0
                    </callGas>
                    <static>
                      false
@@ -1704,6 +1496,9 @@
                    <log>
                      .List
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
                    </accessedAccounts>
@@ -1863,9 +1658,9 @@
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
                ))))))
-      [label(BASIC-BLOCK-7-TO-8)]
+      [label(BASIC-BLOCK-6-TO-7)]
     
-    rule [BASIC-BLOCK-8-TO-9]: <foundry>
+    rule [BASIC-BLOCK-7-TO-8]: <foundry>
            <kevm>
              <k>
                #halt
@@ -1879,6 +1674,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1920,10 +1718,10 @@
                    ...
                    ...
                    <memoryUsed>
-                     25
+                     0
                    </memoryUsed>
                    <callGas>
-                     #gas ( #allBut64th ( ( VGAS:Int +Int -32419 ) ) )
+                     0
                    </callGas>
                    <static>
                      false
@@ -1936,6 +1734,9 @@
                    <log>
                      .List
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
                    </accessedAccounts>
@@ -2095,9 +1896,9 @@
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
                ))))))
-      [label(BASIC-BLOCK-8-TO-9)]
+      [label(BASIC-BLOCK-7-TO-8)]
     
-    rule [BASIC-BLOCK-9-TO-10]: <foundry>
+    rule [BASIC-BLOCK-8-TO-9]: <foundry>
            <kevm>
              <k>
                ( #halt => #execute )
@@ -2109,6 +1910,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -2150,10 +1954,10 @@
                    ...
                    ...
                    <memoryUsed>
-                     ( 25 => 0 )
+                     0
                    </memoryUsed>
                    <callGas>
-                     ( #gas ( #allBut64th ( ( VGAS:Int +Int -32419 ) ) ) => ?_CALLGAS_CELL )
+                     0
                    </callGas>
                    <static>
                      false
@@ -2166,6 +1970,9 @@
                    <log>
                      .List
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      ( ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) => .Set )
                    </accessedAccounts>
@@ -2325,9 +2132,9 @@
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
                ))))))
-      [label(BASIC-BLOCK-9-TO-10)]
+      [label(BASIC-BLOCK-8-TO-9)]
     
-    rule [BASIC-BLOCK-10-TO-12]: <foundry>
+    rule [BASIC-BLOCK-9-TO-11]: <foundry>
            <kevm>
              <k>
                ( .K => #end EVMC_SUCCESS
@@ -2341,6 +2148,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -2373,8 +2183,11 @@
                    ...
                    ...
                    <memoryUsed>
-                     ( 0 => 3 )
+                     0
                    </memoryUsed>
+                   <callGas>
+                     0
+                   </callGas>
                    <static>
                      false
                    </static>
@@ -2387,6 +2200,9 @@
                    <log>
                      .List
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      ( .Set => SetItem ( 491460923342184218035706888008750043977755113263 ) )
                    </accessedAccounts>
@@ -2529,9 +2345,9 @@
              </whitelist>
            </cheatcodes>
          </foundry>
-      [label(BASIC-BLOCK-10-TO-12)]
+      [label(BASIC-BLOCK-9-TO-11)]
     
-    rule [BASIC-BLOCK-12-TO-13]: <foundry>
+    rule [BASIC-BLOCK-11-TO-12]: <foundry>
            <kevm>
              <k>
                ( #end EVMC_SUCCESS => #halt )
@@ -2545,6 +2361,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -2580,8 +2399,11 @@
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
+                   <callGas>
+                     0
+                   </callGas>
                    <static>
                      false
                    </static>
@@ -2594,6 +2416,9 @@
                    <log>
                      .List
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      SetItem ( 491460923342184218035706888008750043977755113263 )
                    </accessedAccounts>
@@ -2736,9 +2561,9 @@
              </whitelist>
            </cheatcodes>
          </foundry>
-      [label(BASIC-BLOCK-12-TO-13)]
+      [label(BASIC-BLOCK-11-TO-12)]
     
-    rule [BASIC-BLOCK-13-TO-14]: <foundry>
+    rule [BASIC-BLOCK-12-TO-13]: <foundry>
            <kevm>
              <k>
                #halt
@@ -2752,6 +2577,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -2787,8 +2615,11 @@
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
+                   <callGas>
+                     0
+                   </callGas>
                    <static>
                      false
                    </static>
@@ -2801,6 +2632,9 @@
                    <log>
                      .List
                    </log>
+                   <refund>
+                     0
+                   </refund>
                    <accessedAccounts>
                      SetItem ( 491460923342184218035706888008750043977755113263 )
                    </accessedAccounts>
@@ -2943,7 +2777,7 @@
              </whitelist>
            </cheatcodes>
          </foundry>
-      [label(BASIC-BLOCK-13-TO-14)]
+      [label(BASIC-BLOCK-12-TO-13)]
 
 endmodule
 0 Failure nodes. (0 pending and 0 failing)
diff --git a/src/tests/integration/test_foundry_prove.py b/src/tests/integration/test_foundry_prove.py
index 9184f5338..124a63f5c 100644
--- a/src/tests/integration/test_foundry_prove.py
+++ b/src/tests/integration/test_foundry_prove.py
@@ -157,7 +157,7 @@ def test_foundry_prove(
     # Then
     assert_pass(test_id, single(prove_res))
 
-    if test_id not in SHOW_TESTS or not no_use_booster:
+    if test_id not in SHOW_TESTS:
         return
 
     # And when
@@ -206,7 +206,7 @@ def test_foundry_fail(
     # Then
     assert_fail(test_id, single(prove_res))
 
-    if test_id not in SHOW_TESTS or not no_use_booster:
+    if test_id not in SHOW_TESTS:
         return
 
     # And when
@@ -336,9 +336,6 @@ def test_foundry_auto_abstraction(
         ),
     )
 
-    if not no_use_booster:
-        return
-
     show_res = foundry_show(
         foundry,
         test=test_id,
diff --git a/test_summary.md b/test_summary.md
new file mode 100644
index 000000000..1c6e37307
--- /dev/null
+++ b/test_summary.md
@@ -0,0 +1,391 @@
+foundry-prove-all that are not skipped on booster
+
+AccountParamsTest.testDealConcrete()
+  - deal cheatcode with concrete value sets balance correctly
+AccountParamsTest.testDealSymbolic(uint256)
+  - deal cheatcode with symbolic value sets balance correctly
+AccountParamsTest.testEtchConcrete()
+  - etch cheatcode with concrete value sets code correctly
+AccountParamsTest.testFail_GetNonce_true()
+  - getNonce cheatcode, account nonce of 0 address is not 10
+AccountParamsTest.test_GetNonce_true()
+  - getNonce cheatcode the current account nonce is 1
+AccountParamsTest.test_getNonce_unknownSymbolic(address)
+  - getNonce cheatcode, the nonce of a symbolic account not in the configuration is 0
+AccountParamsTest.test_Nonce_ExistentAddress()
+  - getNonce and setNonce cheatcode, can set and get nonce of account in configuration
+AccountParamsTest.test_Nonce_NonExistentAddress()
+  - getNonce and setNonce cheatcode, can set and get nonce of new account not in configuration
+AccountParamsTest.testNonceSymbolic(uint64)
+  - getNonce and setNonce cheatcode, can set and get a symbolic account nonce value
+
+AddrTest.test_addr_true()
+  - addr cheatcode, computes address correctly
+AddrTest.test_builtInAddresses()
+  - contract account and VM contract account have the correct address
+AddrTest.test_notBuiltinAddress_concrete()
+  - notBuiltinAddress cheatcode, not equal to concrete address value
+AddrTest.test_notBuiltinAddress_symbolic(address)
+  - notBuiltinAddress cheatcode, not equal to symbolic address value
+
+AllowChangesTest.testAllow()
+  - allowCallsToAddress and allowChangesToStorage cheatcodes, allows changing contract values externally
+AllowChangesTest.testFailAllowCallsToAddress()
+  - allowCallsToAddress and allowChangesToStorage cheatcodes, values cannot be changed calling cheatcode on wrong address
+AllowChangesTest.testFailAllowChangesToStorage()
+  - allowCallsToAddress and allowChangesToStorage cheatcodes, values cannot be changed calling cheatcode on wrong storage slot
+
+ArithmeticTest.test_max1(uint256,uint256)
+  - custom max function, test with symbolic values, assume one is geq to the other
+ArithmeticTest.test_max2(uint256,uint256)
+  - custom max function, test with symbolic values, assert result is geq to both inputs
+AssertTest.test_assert_true()
+  - assert true
+AssertTest.test_assert_true_branch(uint256)
+  - set number relative to symbolic input on two different branches and assert relation to input
+AssertTest.checkFail_assert_false()
+  - assert false
+
+AssumeTest.test_assume_staticCall(bool)
+  - assume a symbolic boolean value inside a static call and then assert that same value
+AssumeTest.test_assume_true(uint256,uint256)
+  - assume and then assert two variables are equal
+AssumeTest.testFail_assume_true(uint256,uint256)
+  - assume and two variables are not equal and assert that they are
+AssumeTest.test_multi_assume(address,address)
+  - make multiple assumptions about inputs not being equal to various addresses
+
+BlockParamsTest.testBlockNumber()
+  - assert current block number is nonnegative
+BlockParamsTest.testChainId(uint256)
+  - use cheatcode to set chainID to a symbolic value
+BlockParamsTest.testCoinBase()
+  - use cheatcode to set coinBase to a concrete value
+BlockParamsTest.testFee(uint256)
+  - use cheatcode to set fee to a symbolic value
+BlockParamsTest.testRoll(uint256)
+  - use roll cheatcode to roll to a symbolic new block number
+BlockParamsTest.testWarp(uint256)
+  - use warp cheatcode to set timestamp to a symbolic value
+  
+BMCLoopsTest.test_countdown_concrete()
+  - count down with a loop from a concrete value of 3
+BMCLoopsTest.test_countdown_symbolic(uint256)
+  - count down with a loop from a concrete value, assumed to be leq 3
+
+BytesTypeTest.test_bytes4(bytes4)
+  - assert symbolic bytes4 value converted to uint32 is leq maximum uint32 value
+BytesTypeTest.test_bytes4_fail(bytes4)
+  - assert symbolic bytes4 value converted to uint32 is greater than maximum uint32 value
+
+CounterTest.testIncrement()
+  - test creation of Counter contract and both its functions
+CounterTest.testSetNumber(uint256)
+  - test creation of Counter contract and set its number to a symbolic value
+
+EmitContractTest.testExpectEmit()
+  - test expectEmit cheatcode
+EmitContractTest.testExpectEmitCheckEmitter()
+  - test expectEmit cheatcode, additionally check emitter address is correct
+EmitContractTest.testExpectEmitDoNotCheckData()
+  - test expectEmit cheatcode with divergent data, but specify not to check data
+
+ExpectCallTest.testExpectRegularCall()
+  - test expectRegularCall cheatcode
+ExpectCallTest.testExpectStaticCall()
+  - test expectStaticCall cheatcode
+
+ExpectRevertTest.test_ExpectRevert_increasedDepth()
+  - test expectRevert cheatcode catches revert on nested function calls
+ExpectRevertTest.test_expectRevert_message()
+  - test expectRevert cheatcode, asserts correct revert message is retained
+ExpectRevertTest.test_expectRevert_returnValue()
+  - test expectRevert cheatcode, default values are returned if function reverts
+ExpectRevertTest.test_expectRevert_true()
+  - test expectRevert cheatcode, basic
+ExpectRevertTest.testFail_expectRevert_empty()
+  - test expectRevert cheatcode, fails because no revert
+ExpectRevertTest.testFail_ExpectRevert_failAndSuccess()
+  - test expectRevert cheatcode, fails because one no revert and one successful expected revert
+ExpectRevertTest.testFail_expectRevert_false()
+  - test expectRevert cheatcode, fails because one no revert
+ExpectRevertTest.testFail_expectRevert_multipleReverts()
+  - test expectRevert cheatcode, fails because more reverts than expected
+
+GasTest.testSetGas()
+  - test setGas cheatcode, set gas and then check it goes doesn after some operation
+
+LabelTest.testLabel()
+  - set address label using label cheatcode
+
+LoopsTest.sum_N(uint256)
+  - generic symbolic loop sum, uses circularity lemma
+LoopsTest.test_sum_10()
+  - call sum_N on value of 10
+
+MethodDisambiguateTest.test_method_call()
+  - test that it is possible to disambiguate method calls based on argument types
+
+PlainPrankTest.testFail_startPrank_internalCall()
+  - test startPrank cheatcode on same contract function
+PlainPrankTest.test_prank_zeroAddress_true()
+  - test prank cheatcode as address 0
+PlainPrankTest.test_startPrank_true()
+  - startPrank and stopPrank, basic
+PlainPrankTest.test_startPrankWithOrigin_true()
+  - startPrank and stopPrank, also set origin field for startPrank
+PlainPrankTest.test_startPrank_zeroAddress_true()
+  - startPrank and stopPrank cheatcodes as address 0
+PlainPrankTest.test_stopPrank_notExistent()
+  - stopPrank with no corresponding startPrank
+
+Setup2Test.testFail_setup()
+  - test setUp method runs and sets fields to other value
+Setup2Test.test_setup()
+  - test setUp method runs and sets fields to value
+
+SetUpDeployTest.test_extcodesize()
+  - test contract deployed in setup has positive extcodesize
+
+StoreTest.testGasLoadColdVM()
+StoreTest.testGasLoadWarmUp()
+StoreTest.testGasStoreColdVM()
+StoreTest.testGasStoreWarmUp()
+StoreTest.testLoadNonExistent()
+StoreTest.testStoreLoad()
+StoreTest.testStoreLoadNonExistent()
+SymbolicStorageTest.testEmptyInitialStorage(uint256)
+SymbolicStorageTest.testFail_SymbolicStorage(uint256)
+SymbolicStorageTest.testFail_SymbolicStorage1(uint256)
+UintTypeTest.test_uint256(uint256)
+StructTypeTest.test_vars((uint8,uint32,bytes32))
+
+Skipped tests:
+
+AccountParamsTest.testEtchSymbolic(bytes)
+AccountParamsTest.testFail_GetNonce_false()
+AccountParamsTest.test_GetNonce_false()
+AddrTest.test_addr_false()
+AddrTest.test_addr_symbolic(uint256)
+AddrTest.testFail_addr_false()
+AddrTest.testFail_addr_true()
+AllowChangesTest.test()
+AllowChangesTest.testAllow_fail()
+ArithmeticTest.test_decreasing_div(uint256,uint256)
+ArithmeticTest.test_max1_broken(uint256,uint256)
+ArithmeticTest.test_wdiv_rounding(uint256,uint256)
+ArithmeticTest.test_wmul_increasing(uint256,uint256)
+ArithmeticTest.test_wmul_increasing_gt_one(uint256,uint256)
+ArithmeticTest.test_wmul_increasing_overflow(uint256,uint256)
+ArithmeticTest.test_wmul_increasing_positive(uint256,uint256)
+ArithmeticTest.test_wmul_rounding(uint256,uint256)
+ArithmeticTest.test_wmul_wdiv_inverse(uint256,uint256)
+ArithmeticTest.test_wmul_wdiv_inverse_underflow(uint256,uint256)
+ArithmeticTest.test_wmul_weakly_increasing_positive(uint256,uint256)
+AssertTest.test_assert_false()
+AssertTest.testFail_assert_true()
+AssertTest.testFail_expect_revert()
+AssertTest.test_failing_branch(uint256)
+AssertTest.test_revert_branch(uint256,uint256)
+AssumeTest.test_assume_false(uint256,uint256)
+AssumeTest.testFail_assume_false(uint256,uint256)
+BroadcastTest.testDeploy()
+BytesTypeTest.test_bytes32_fail(bytes32)
+BytesTypeTest.test_bytes4_fail(bytes4)
+BytesTypeTest.testFail_bytes32(bytes32)
+BytesTypeTest.testFail_bytes4(bytes4)
+ContractBTest.testCannotSubtract43()
+ContractBTest.testFailSubtract43()
+ContractBTest.testNumberIs42()
+ContractTest.testExample()
+EnvTest.testEnvAddress()
+EnvTest.testEnvAddresseArray()
+EnvTest.testEnvBool()
+EnvTest.testEnvBoolArray()
+EnvTest.testEnvBytes()
+EnvTest.testEnvBytes32()
+EnvTest.testEnvBytes32Array()
+EnvTest.testEnvBytesArray()
+EnvTest.testEnvInt()
+EnvTest.testEnvIntArray()
+EnvTest.testEnvString()
+EnvTest.testEnvStringArray()
+EnvTest.testEnvUInt()
+EnvTest.testEnvUIntArray()
+ExpectRevertTest.test_expectRevert_bytes4()
+ExpectRevertTest.test_expectRevert_encodedSymbolic(address)
+ExpectRevertTest.test_expectRevert_internalCall()
+ExpectRevertTest.testFail_expectRevert_bytes4()
+FfiTest.testffi()
+FfiTest.testFFIFOO()
+FfiTest.testFFIScript()
+FfiTest.testFFIScript2()
+FilesTest.testFailRemoveFile()
+FilesTest.testReadWriteFile()
+FilesTest.testReadWriteLine()
+ForkTest.testActiveFork()
+ForkTest.testAllRPCUrl()
+ForkTest.testCreateFork()
+ForkTest.testCreateForkBlock()
+ForkTest.testCreateSelectFork()
+ForkTest.testCreateSelectForkBlock()
+ForkTest.testRollFork()
+ForkTest.testRollForkId()
+ForkTest.testRPCUrl()
+ForkTest.testRPCUrlRevert()
+GasTest.testInfiniteGas()
+GetCodeTest.testGetCode()
+LoopsTest.testIsNotPrime(uint256)
+LoopsTest.testIsPrime(uint256,uint256)
+LoopsTest.testIsPrimeBroken(uint256,uint256)
+LoopsTest.testIsPrimeOpt(uint256)
+LoopsTest.testMax(uint256[])
+LoopsTest.testMaxBroken(uint256[])
+LoopsTest.testNthPrime(uint256,uint256)
+LoopsTest.testSort(uint256[])
+LoopsTest.testSortBroken(uint256[])
+LoopsTest.testSqrt(uint256)
+LoopsTest.test_sum_100()
+LoopsTest.test_sum_1000()
+LoopsTest.testSumToN(uint256)
+LoopsTest.testSumToNBroken(uint256)
+MockCallTest.testMockCall()
+MockCallTest.testMockCalls()
+MockCallTest.testMockCallValue()
+OwnerUpOnlyTest.testFailIncrementAsNotOwner()
+OwnerUpOnlyTest.testIncrementAsNotOwner()
+OwnerUpOnlyTest.testIncrementAsOwner()
+PlainPrankTest.testFail_startPrank_existingAlready()
+PrankTest.testAddAsOwner(uint256)
+PrankTest.testAddStartPrank(uint256)
+PrankTest.testFailAddPrank(uint256)
+PrankTest.testSubtractAsTxOrigin(uint256,uint256)
+PrankTest.testSubtractFail(uint256)
+PrankTest.testSubtractStartPrank(uint256,uint256)
+RecordLogsTest.testRecordLogs()
+SafeTest.testWithdraw()
+SafeTest.testWithdrawFuzz(uint96)
+SetUpTest.testSetUpCalled()
+SetUpTest.testSetUpCalledSymbolic(uint256)
+SignTest.testSign()
+SignTest.testSign_symbolic(uint256)
+SnapshotTest.testSnapshot()
+StoreTest.testAccesses()
+StoreTest.testGasLoadWarmVM()
+StoreTest.testGasStoreWarmVM()
+ToStringTest.testAddressToString()
+ToStringTest.testBoolToString()
+ToStringTest.testBytes32ToString()
+ToStringTest.testBytesToString()
+ToStringTest.testIntToString()
+ToStringTest.testUint256ToString()
+UintTypeTest.testFail_uint104(uint104)
+UintTypeTest.testFail_uint112(uint112)
+UintTypeTest.testFail_uint120(uint120)
+UintTypeTest.testFail_uint128(uint128)
+UintTypeTest.testFail_uint136(uint136)
+UintTypeTest.testFail_uint144(uint144)
+UintTypeTest.testFail_uint152(uint152)
+UintTypeTest.testFail_uint16(uint16)
+UintTypeTest.testFail_uint160(uint160)
+UintTypeTest.testFail_uint168(uint168)
+UintTypeTest.testFail_uint176(uint176)
+UintTypeTest.testFail_uint184(uint184)
+UintTypeTest.testFail_uint192(uint192)
+UintTypeTest.testFail_uint200(uint200)
+UintTypeTest.testFail_uint208(uint208)
+UintTypeTest.testFail_uint216(uint216)
+UintTypeTest.testFail_uint224(uint224)
+UintTypeTest.testFail_uint232(uint232)
+UintTypeTest.testFail_uint24(uint24)
+UintTypeTest.testFail_uint240(uint240)
+UintTypeTest.testFail_uint248(uint248)
+UintTypeTest.testFail_uint256(uint256)
+UintTypeTest.testFail_uint32(uint32)
+UintTypeTest.testFail_uint40(uint40)
+UintTypeTest.testFail_uint48(uint48)
+UintTypeTest.testFail_uint56(uint56)
+UintTypeTest.testFail_uint64(uint64)
+UintTypeTest.testFail_uint72(uint72)
+UintTypeTest.testFail_uint8(uint8)
+UintTypeTest.testFail_uint80(uint80)
+UintTypeTest.testFail_uint88(uint88)
+UintTypeTest.testFail_uint96(uint96)
+UintTypeTest.test_uint104(uint104)
+UintTypeTest.test_uint104_fail(uint104)
+UintTypeTest.test_uint112(uint112)
+UintTypeTest.test_uint112_fail(uint112)
+UintTypeTest.test_uint120(uint120)
+UintTypeTest.test_uint120_fail(uint120)
+UintTypeTest.test_uint128(uint128)
+UintTypeTest.test_uint128_fail(uint128)
+UintTypeTest.test_uint136(uint136)
+UintTypeTest.test_uint136_fail(uint136)
+UintTypeTest.test_uint144(uint144)
+UintTypeTest.test_uint144_fail(uint144)
+UintTypeTest.test_uint152(uint152)
+UintTypeTest.test_uint152_fail(uint152)
+UintTypeTest.test_uint16(uint16)
+UintTypeTest.test_uint160(uint160)
+UintTypeTest.test_uint160_fail(uint160)
+UintTypeTest.test_uint168(uint168)
+UintTypeTest.test_uint168_fail(uint168)
+UintTypeTest.test_uint16_fail(uint16)
+UintTypeTest.test_uint176(uint176)
+UintTypeTest.test_uint176_fail(uint176)
+UintTypeTest.test_uint184(uint184)
+UintTypeTest.test_uint184_fail(uint184)
+UintTypeTest.test_uint192(uint192)
+UintTypeTest.test_uint192_fail(uint192)
+UintTypeTest.test_uint200(uint200)
+UintTypeTest.test_uint200_fail(uint200)
+UintTypeTest.test_uint208(uint208)
+UintTypeTest.test_uint208_fail(uint208)
+UintTypeTest.test_uint216(uint216)
+UintTypeTest.test_uint216_fail(uint216)
+UintTypeTest.test_uint224(uint224)
+UintTypeTest.test_uint224_fail(uint224)
+UintTypeTest.test_uint232(uint232)
+UintTypeTest.test_uint232_fail(uint232)
+UintTypeTest.test_uint24(uint24)
+UintTypeTest.test_uint240(uint240)
+UintTypeTest.test_uint240_fail(uint240)
+UintTypeTest.test_uint248(uint248)
+UintTypeTest.test_uint248_fail(uint248)
+UintTypeTest.test_uint24_fail(uint24)
+UintTypeTest.test_uint256_fail(uint256)
+UintTypeTest.test_uint32(uint32)
+UintTypeTest.test_uint32_fail(uint32)
+UintTypeTest.test_uint40(uint40)
+UintTypeTest.test_uint40_fail(uint40)
+UintTypeTest.test_uint48(uint48)
+UintTypeTest.test_uint48_fail(uint48)
+UintTypeTest.test_uint56(uint56)
+UintTypeTest.test_uint56_fail(uint56)
+UintTypeTest.test_uint64(uint64)
+UintTypeTest.test_uint64_fail(uint64)
+UintTypeTest.test_uint72(uint72)
+UintTypeTest.test_uint72_fail(uint72)
+UintTypeTest.test_uint8(uint8)
+UintTypeTest.test_uint80(uint80)
+UintTypeTest.test_uint80_fail(uint80)
+UintTypeTest.test_uint88(uint88)
+UintTypeTest.test_uint88_fail(uint88)
+UintTypeTest.test_uint8_fail(uint8)
+UintTypeTest.test_uint96(uint96)
+UintTypeTest.test_uint96_fail(uint96)
+IntTypeTest.testFail_int128(uint128)
+IntTypeTest.testFail_int256(uint256)
+IntTypeTest.testFail_int64(uint64)
+IntTypeTest.test_int128(uint128)
+IntTypeTest.test_int128_fail(uint128)
+IntTypeTest.test_int256(uint256)
+IntTypeTest.test_int256_fail(uint256)
+IntTypeTest.test_int64(uint64)
+IntTypeTest.test_int64_fail(uint64)
+
+
+- Remove duplicate/unneccesary tests
+- Check test functions do not exist which are not in the test list
+- Check all tests in `test_foundry_prove.py` that they properly use booster backend
+- Check updated expected output after switching file comparison tests to booster