diff --git a/deps/k_release b/deps/k_release
index 65f6d2bc1..773066585 100644
--- a/deps/k_release
+++ b/deps/k_release
@@ -1 +1 @@
-6.1.60
+6.1.71
diff --git a/deps/kevm_release b/deps/kevm_release
index 302d5deb2..a0b345325 100644
--- a/deps/kevm_release
+++ b/deps/kevm_release
@@ -1 +1 @@
-1.0.397
+1.0.405
diff --git a/flake.lock b/flake.lock
index 16675c477..0a918aba7 100644
--- a/flake.lock
+++ b/flake.lock
@@ -72,17 +72,17 @@
         ]
       },
       "locked": {
-        "lastModified": 1702465848,
-        "narHash": "sha256-pikJMY8bJqbO+kTKGZiPRzspHcGJ6lFk/JytCUrm1yk=",
+        "lastModified": 1703078812,
+        "narHash": "sha256-Un3MXYKEm2tlOMbk8LSI98lQQIzp+LJFvXv8pyypcGU=",
         "owner": "runtimeverification",
         "repo": "hs-backend-booster",
-        "rev": "6e29375d4cbcfdeddf99e98f2ba7577db0cbf963",
+        "rev": "c6edfad1aa4c085e2cc2978c6d7cdc885157b0fb",
         "type": "github"
       },
       "original": {
         "owner": "runtimeverification",
         "repo": "hs-backend-booster",
-        "rev": "6e29375d4cbcfdeddf99e98f2ba7577db0cbf963",
+        "rev": "c6edfad1aa4c085e2cc2978c6d7cdc885157b0fb",
         "type": "github"
       }
     },
@@ -238,17 +238,17 @@
         "z3": "z3"
       },
       "locked": {
-        "lastModified": 1701950567,
-        "narHash": "sha256-e4A4dTW8GYQ0KPHcAb1PVaLXqGpKUJuQNJLlM7HO74Y=",
+        "lastModified": 1703063258,
+        "narHash": "sha256-wL5kFsbs6RS+bsrf+SDq85DDKce/sZZ7VQDtJZA5JS0=",
         "owner": "runtimeverification",
         "repo": "haskell-backend",
-        "rev": "a5847301404583e16d55cd4d051b8e605d704fbc",
+        "rev": "ca05f14b7957fec9f2a5ab3444cae01c5a76f12f",
         "type": "github"
       },
       "original": {
         "owner": "runtimeverification",
         "repo": "haskell-backend",
-        "rev": "a5847301404583e16d55cd4d051b8e605d704fbc",
+        "rev": "ca05f14b7957fec9f2a5ab3444cae01c5a76f12f",
         "type": "github"
       }
     },
@@ -284,16 +284,16 @@
         "rv-utils": "rv-utils"
       },
       "locked": {
-        "lastModified": 1702579377,
-        "narHash": "sha256-SM7WOVRO15OabLdeYZjVf4feRv1LK6Hm/nhCUuJc48Q=",
+        "lastModified": 1703095402,
+        "narHash": "sha256-3Szh7B8Ui8/kGXMWywrbaARFJ5okvdE8vBJix3nsW6s=",
         "owner": "runtimeverification",
         "repo": "k",
-        "rev": "0b4353c62f018a46736dc6b512414b77ab81523d",
+        "rev": "3f547d5459b244c5e258231362c467d3ef50beb6",
         "type": "github"
       },
       "original": {
         "owner": "runtimeverification",
-        "ref": "v6.1.60",
+        "ref": "v6.1.71",
         "repo": "k",
         "type": "github"
       }
@@ -337,16 +337,16 @@
         ]
       },
       "locked": {
-        "lastModified": 1702661104,
-        "narHash": "sha256-tiTfnsicKHPvJdp9pKPbAuN4OrgWQQeD6evCdF7n054=",
+        "lastModified": 1703166093,
+        "narHash": "sha256-bqfoBC/4IddlaDl8HnrtDR4ueOAQ4YrbRaXqXEJlKvY=",
         "owner": "runtimeverification",
         "repo": "evm-semantics",
-        "rev": "1349ef9203534b80bd52577637060ceb5d4e0d24",
+        "rev": "2382ef6ad179f72691283d8d3c048d30829eadcc",
         "type": "github"
       },
       "original": {
         "owner": "runtimeverification",
-        "ref": "v1.0.397",
+        "ref": "v1.0.405",
         "repo": "evm-semantics",
         "type": "github"
       }
@@ -388,11 +388,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1702393410,
-        "narHash": "sha256-YbfXAIj/qax/o9G5dhGAiJOvvOQrtMPoi3KDCfOPOms=",
+        "lastModified": 1703090628,
+        "narHash": "sha256-uYF53yhj4XlelzSEpjVu4nElkyx6CWndfGUjcBt0yfs=",
         "owner": "runtimeverification",
         "repo": "llvm-backend",
-        "rev": "14c372e93bf6133b2c780868dcda8bb2abbe6d8b",
+        "rev": "136dc466528f3cd9e157351cb85909716c3ed9b2",
         "type": "github"
       },
       "original": {
@@ -543,16 +543,16 @@
         "poetry2nix": "poetry2nix"
       },
       "locked": {
-        "lastModified": 1702643479,
-        "narHash": "sha256-umKe3kkRGP3CB/Meujbc51hu6+aM/xDgEk8dRhezrH8=",
+        "lastModified": 1703157822,
+        "narHash": "sha256-VJDAnQ3RjutL0Wils8b62fFB++wMZnZJKUiWZdKbR/8=",
         "owner": "runtimeverification",
         "repo": "pyk",
-        "rev": "c397bba169e7e3f46ea403452a5f44c4cfa9eab0",
+        "rev": "3a91f68cfe2145562eae3c57187338b06317bfaa",
         "type": "github"
       },
       "original": {
         "owner": "runtimeverification",
-        "ref": "v0.1.549",
+        "ref": "v0.1.563",
         "repo": "pyk",
         "type": "github"
       }
diff --git a/flake.nix b/flake.nix
index 4e46451b9..c760c369e 100644
--- a/flake.nix
+++ b/flake.nix
@@ -2,7 +2,7 @@
   description = "Kontrol";
 
   inputs = {
-    kevm.url = "github:runtimeverification/evm-semantics/v1.0.397";
+    kevm.url = "github:runtimeverification/evm-semantics/v1.0.405";
     nixpkgs.follows = "kevm/nixpkgs";
     nixpkgs-pyk.follows = "kevm/nixpkgs-pyk";
     k-framework.follows = "kevm/k-framework";
diff --git a/package/version b/package/version
index 91c96fdf8..5950146bb 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.102
+0.1.103
diff --git a/poetry.lock b/poetry.lock
index dc4a8f59f..6080437e7 100644
--- a/poetry.lock
+++ b/poetry.lock
@@ -156,63 +156,63 @@ cron = ["capturer (>=2.4)"]
 
 [[package]]
 name = "coverage"
-version = "7.3.3"
+version = "7.3.4"
 description = "Code coverage measurement for Python"
 optional = false
 python-versions = ">=3.8"
 files = [
-    {file = "coverage-7.3.3-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:d874434e0cb7b90f7af2b6e3309b0733cde8ec1476eb47db148ed7deeb2a9494"},
-    {file = "coverage-7.3.3-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:ee6621dccce8af666b8c4651f9f43467bfbf409607c604b840b78f4ff3619aeb"},
-    {file = "coverage-7.3.3-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:1367aa411afb4431ab58fd7ee102adb2665894d047c490649e86219327183134"},
-    {file = "coverage-7.3.3-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:1f0f8f0c497eb9c9f18f21de0750c8d8b4b9c7000b43996a094290b59d0e7523"},
-    {file = "coverage-7.3.3-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:db0338c4b0951d93d547e0ff8d8ea340fecf5885f5b00b23be5aa99549e14cfd"},
-    {file = "coverage-7.3.3-cp310-cp310-musllinux_1_1_aarch64.whl", hash = "sha256:d31650d313bd90d027f4be7663dfa2241079edd780b56ac416b56eebe0a21aab"},
-    {file = "coverage-7.3.3-cp310-cp310-musllinux_1_1_i686.whl", hash = "sha256:9437a4074b43c177c92c96d051957592afd85ba00d3e92002c8ef45ee75df438"},
-    {file = "coverage-7.3.3-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:9e17d9cb06c13b4f2ef570355fa45797d10f19ca71395910b249e3f77942a837"},
-    {file = "coverage-7.3.3-cp310-cp310-win32.whl", hash = "sha256:eee5e741b43ea1b49d98ab6e40f7e299e97715af2488d1c77a90de4a663a86e2"},
-    {file = "coverage-7.3.3-cp310-cp310-win_amd64.whl", hash = "sha256:593efa42160c15c59ee9b66c5f27a453ed3968718e6e58431cdfb2d50d5ad284"},
-    {file = "coverage-7.3.3-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:8c944cf1775235c0857829c275c777a2c3e33032e544bcef614036f337ac37bb"},
-    {file = "coverage-7.3.3-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:eda7f6e92358ac9e1717ce1f0377ed2b9320cea070906ece4e5c11d172a45a39"},
-    {file = "coverage-7.3.3-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:3c854c1d2c7d3e47f7120b560d1a30c1ca221e207439608d27bc4d08fd4aeae8"},
-    {file = "coverage-7.3.3-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:222b038f08a7ebed1e4e78ccf3c09a1ca4ac3da16de983e66520973443b546bc"},
-    {file = "coverage-7.3.3-cp311-cp311-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:ff4800783d85bff132f2cc7d007426ec698cdce08c3062c8d501ad3f4ea3d16c"},
-    {file = "coverage-7.3.3-cp311-cp311-musllinux_1_1_aarch64.whl", hash = "sha256:fc200cec654311ca2c3f5ab3ce2220521b3d4732f68e1b1e79bef8fcfc1f2b97"},
-    {file = "coverage-7.3.3-cp311-cp311-musllinux_1_1_i686.whl", hash = "sha256:307aecb65bb77cbfebf2eb6e12009e9034d050c6c69d8a5f3f737b329f4f15fb"},
-    {file = "coverage-7.3.3-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:ffb0eacbadb705c0a6969b0adf468f126b064f3362411df95f6d4f31c40d31c1"},
-    {file = "coverage-7.3.3-cp311-cp311-win32.whl", hash = "sha256:79c32f875fd7c0ed8d642b221cf81feba98183d2ff14d1f37a1bbce6b0347d9f"},
-    {file = "coverage-7.3.3-cp311-cp311-win_amd64.whl", hash = "sha256:243576944f7c1a1205e5cd658533a50eba662c74f9be4c050d51c69bd4532936"},
-    {file = "coverage-7.3.3-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:a2ac4245f18057dfec3b0074c4eb366953bca6787f1ec397c004c78176a23d56"},
-    {file = "coverage-7.3.3-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:f9191be7af41f0b54324ded600e8ddbcabea23e1e8ba419d9a53b241dece821d"},
-    {file = "coverage-7.3.3-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:31c0b1b8b5a4aebf8fcd227237fc4263aa7fa0ddcd4d288d42f50eff18b0bac4"},
-    {file = "coverage-7.3.3-cp312-cp312-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:ee453085279df1bac0996bc97004771a4a052b1f1e23f6101213e3796ff3cb85"},
-    {file = "coverage-7.3.3-cp312-cp312-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:1191270b06ecd68b1d00897b2daddb98e1719f63750969614ceb3438228c088e"},
-    {file = "coverage-7.3.3-cp312-cp312-musllinux_1_1_aarch64.whl", hash = "sha256:007a7e49831cfe387473e92e9ff07377f6121120669ddc39674e7244350a6a29"},
-    {file = "coverage-7.3.3-cp312-cp312-musllinux_1_1_i686.whl", hash = "sha256:af75cf83c2d57717a8493ed2246d34b1f3398cb8a92b10fd7a1858cad8e78f59"},
-    {file = "coverage-7.3.3-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:811ca7373da32f1ccee2927dc27dc523462fd30674a80102f86c6753d6681bc6"},
-    {file = "coverage-7.3.3-cp312-cp312-win32.whl", hash = "sha256:733537a182b5d62184f2a72796eb6901299898231a8e4f84c858c68684b25a70"},
-    {file = "coverage-7.3.3-cp312-cp312-win_amd64.whl", hash = "sha256:e995efb191f04b01ced307dbd7407ebf6e6dc209b528d75583277b10fd1800ee"},
-    {file = "coverage-7.3.3-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:fbd8a5fe6c893de21a3c6835071ec116d79334fbdf641743332e442a3466f7ea"},
-    {file = "coverage-7.3.3-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:50c472c1916540f8b2deef10cdc736cd2b3d1464d3945e4da0333862270dcb15"},
-    {file = "coverage-7.3.3-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:2e9223a18f51d00d3ce239c39fc41410489ec7a248a84fab443fbb39c943616c"},
-    {file = "coverage-7.3.3-cp38-cp38-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:f501e36ac428c1b334c41e196ff6bd550c0353c7314716e80055b1f0a32ba394"},
-    {file = "coverage-7.3.3-cp38-cp38-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:475de8213ed95a6b6283056d180b2442eee38d5948d735cd3d3b52b86dd65b92"},
-    {file = "coverage-7.3.3-cp38-cp38-musllinux_1_1_aarch64.whl", hash = "sha256:afdcc10c01d0db217fc0a64f58c7edd635b8f27787fea0a3054b856a6dff8717"},
-    {file = "coverage-7.3.3-cp38-cp38-musllinux_1_1_i686.whl", hash = "sha256:fff0b2f249ac642fd735f009b8363c2b46cf406d3caec00e4deeb79b5ff39b40"},
-    {file = "coverage-7.3.3-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:a1f76cfc122c9e0f62dbe0460ec9cc7696fc9a0293931a33b8870f78cf83a327"},
-    {file = "coverage-7.3.3-cp38-cp38-win32.whl", hash = "sha256:757453848c18d7ab5d5b5f1827293d580f156f1c2c8cef45bfc21f37d8681069"},
-    {file = "coverage-7.3.3-cp38-cp38-win_amd64.whl", hash = "sha256:ad2453b852a1316c8a103c9c970db8fbc262f4f6b930aa6c606df9b2766eee06"},
-    {file = "coverage-7.3.3-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:3b15e03b8ee6a908db48eccf4e4e42397f146ab1e91c6324da44197a45cb9132"},
-    {file = "coverage-7.3.3-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:89400aa1752e09f666cc48708eaa171eef0ebe3d5f74044b614729231763ae69"},
-    {file = "coverage-7.3.3-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:c59a3e59fb95e6d72e71dc915e6d7fa568863fad0a80b33bc7b82d6e9f844973"},
-    {file = "coverage-7.3.3-cp39-cp39-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:9ede881c7618f9cf93e2df0421ee127afdfd267d1b5d0c59bcea771cf160ea4a"},
-    {file = "coverage-7.3.3-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:f3bfd2c2f0e5384276e12b14882bf2c7621f97c35320c3e7132c156ce18436a1"},
-    {file = "coverage-7.3.3-cp39-cp39-musllinux_1_1_aarch64.whl", hash = "sha256:7f3bad1a9313401ff2964e411ab7d57fb700a2d5478b727e13f156c8f89774a0"},
-    {file = "coverage-7.3.3-cp39-cp39-musllinux_1_1_i686.whl", hash = "sha256:65d716b736f16e250435473c5ca01285d73c29f20097decdbb12571d5dfb2c94"},
-    {file = "coverage-7.3.3-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:a702e66483b1fe602717020a0e90506e759c84a71dbc1616dd55d29d86a9b91f"},
-    {file = "coverage-7.3.3-cp39-cp39-win32.whl", hash = "sha256:7fbf3f5756e7955174a31fb579307d69ffca91ad163467ed123858ce0f3fd4aa"},
-    {file = "coverage-7.3.3-cp39-cp39-win_amd64.whl", hash = "sha256:cad9afc1644b979211989ec3ff7d82110b2ed52995c2f7263e7841c846a75348"},
-    {file = "coverage-7.3.3-pp38.pp39.pp310-none-any.whl", hash = "sha256:d299d379b676812e142fb57662a8d0d810b859421412b4d7af996154c00c31bb"},
-    {file = "coverage-7.3.3.tar.gz", hash = "sha256:df04c64e58df96b4427db8d0559e95e2df3138c9916c96f9f6a4dd220db2fdb7"},
+    {file = "coverage-7.3.4-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:aff2bd3d585969cc4486bfc69655e862028b689404563e6b549e6a8244f226df"},
+    {file = "coverage-7.3.4-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:e4353923f38d752ecfbd3f1f20bf7a3546993ae5ecd7c07fd2f25d40b4e54571"},
+    {file = "coverage-7.3.4-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:ea473c37872f0159294f7073f3fa72f68b03a129799f3533b2bb44d5e9fa4f82"},
+    {file = "coverage-7.3.4-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:5214362abf26e254d749fc0c18af4c57b532a4bfde1a057565616dd3b8d7cc94"},
+    {file = "coverage-7.3.4-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:f99b7d3f7a7adfa3d11e3a48d1a91bb65739555dd6a0d3fa68aa5852d962e5b1"},
+    {file = "coverage-7.3.4-cp310-cp310-musllinux_1_1_aarch64.whl", hash = "sha256:74397a1263275bea9d736572d4cf338efaade2de9ff759f9c26bcdceb383bb49"},
+    {file = "coverage-7.3.4-cp310-cp310-musllinux_1_1_i686.whl", hash = "sha256:f154bd866318185ef5865ace5be3ac047b6d1cc0aeecf53bf83fe846f4384d5d"},
+    {file = "coverage-7.3.4-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:e0d84099ea7cba9ff467f9c6f747e3fc3906e2aadac1ce7b41add72e8d0a3712"},
+    {file = "coverage-7.3.4-cp310-cp310-win32.whl", hash = "sha256:3f477fb8a56e0c603587b8278d9dbd32e54bcc2922d62405f65574bd76eba78a"},
+    {file = "coverage-7.3.4-cp310-cp310-win_amd64.whl", hash = "sha256:c75738ce13d257efbb6633a049fb2ed8e87e2e6c2e906c52d1093a4d08d67c6b"},
+    {file = "coverage-7.3.4-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:997aa14b3e014339d8101b9886063c5d06238848905d9ad6c6eabe533440a9a7"},
+    {file = "coverage-7.3.4-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:8a9c5bc5db3eb4cd55ecb8397d8e9b70247904f8eca718cc53c12dcc98e59fc8"},
+    {file = "coverage-7.3.4-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:27ee94f088397d1feea3cb524e4313ff0410ead7d968029ecc4bc5a7e1d34fbf"},
+    {file = "coverage-7.3.4-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:8ce03e25e18dd9bf44723e83bc202114817f3367789052dc9e5b5c79f40cf59d"},
+    {file = "coverage-7.3.4-cp311-cp311-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:85072e99474d894e5df582faec04abe137b28972d5e466999bc64fc37f564a03"},
+    {file = "coverage-7.3.4-cp311-cp311-musllinux_1_1_aarch64.whl", hash = "sha256:a877810ef918d0d345b783fc569608804f3ed2507bf32f14f652e4eaf5d8f8d0"},
+    {file = "coverage-7.3.4-cp311-cp311-musllinux_1_1_i686.whl", hash = "sha256:9ac17b94ab4ca66cf803f2b22d47e392f0977f9da838bf71d1f0db6c32893cb9"},
+    {file = "coverage-7.3.4-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:36d75ef2acab74dc948d0b537ef021306796da551e8ac8b467810911000af66a"},
+    {file = "coverage-7.3.4-cp311-cp311-win32.whl", hash = "sha256:47ee56c2cd445ea35a8cc3ad5c8134cb9bece3a5cb50bb8265514208d0a65928"},
+    {file = "coverage-7.3.4-cp311-cp311-win_amd64.whl", hash = "sha256:11ab62d0ce5d9324915726f611f511a761efcca970bd49d876cf831b4de65be5"},
+    {file = "coverage-7.3.4-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:33e63c578f4acce1b6cd292a66bc30164495010f1091d4b7529d014845cd9bee"},
+    {file = "coverage-7.3.4-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:782693b817218169bfeb9b9ba7f4a9f242764e180ac9589b45112571f32a0ba6"},
+    {file = "coverage-7.3.4-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:7c4277ddaad9293454da19121c59f2d850f16bcb27f71f89a5c4836906eb35ef"},
+    {file = "coverage-7.3.4-cp312-cp312-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:3d892a19ae24b9801771a5a989fb3e850bd1ad2e2b6e83e949c65e8f37bc67a1"},
+    {file = "coverage-7.3.4-cp312-cp312-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:3024ec1b3a221bd10b5d87337d0373c2bcaf7afd86d42081afe39b3e1820323b"},
+    {file = "coverage-7.3.4-cp312-cp312-musllinux_1_1_aarch64.whl", hash = "sha256:a1c3e9d2bbd6f3f79cfecd6f20854f4dc0c6e0ec317df2b265266d0dc06535f1"},
+    {file = "coverage-7.3.4-cp312-cp312-musllinux_1_1_i686.whl", hash = "sha256:e91029d7f151d8bf5ab7d8bfe2c3dbefd239759d642b211a677bc0709c9fdb96"},
+    {file = "coverage-7.3.4-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:6879fe41c60080aa4bb59703a526c54e0412b77e649a0d06a61782ecf0853ee1"},
+    {file = "coverage-7.3.4-cp312-cp312-win32.whl", hash = "sha256:fd2f8a641f8f193968afdc8fd1697e602e199931012b574194052d132a79be13"},
+    {file = "coverage-7.3.4-cp312-cp312-win_amd64.whl", hash = "sha256:d1d0ce6c6947a3a4aa5479bebceff2c807b9f3b529b637e2b33dea4468d75fc7"},
+    {file = "coverage-7.3.4-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:36797b3625d1da885b369bdaaa3b0d9fb8865caed3c2b8230afaa6005434aa2f"},
+    {file = "coverage-7.3.4-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:bfed0ec4b419fbc807dec417c401499ea869436910e1ca524cfb4f81cf3f60e7"},
+    {file = "coverage-7.3.4-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:f97ff5a9fc2ca47f3383482858dd2cb8ddbf7514427eecf5aa5f7992d0571429"},
+    {file = "coverage-7.3.4-cp38-cp38-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:607b6c6b35aa49defaebf4526729bd5238bc36fe3ef1a417d9839e1d96ee1e4c"},
+    {file = "coverage-7.3.4-cp38-cp38-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:a8e258dcc335055ab59fe79f1dec217d9fb0cdace103d6b5c6df6b75915e7959"},
+    {file = "coverage-7.3.4-cp38-cp38-musllinux_1_1_aarch64.whl", hash = "sha256:a02ac7c51819702b384fea5ee033a7c202f732a2a2f1fe6c41e3d4019828c8d3"},
+    {file = "coverage-7.3.4-cp38-cp38-musllinux_1_1_i686.whl", hash = "sha256:b710869a15b8caf02e31d16487a931dbe78335462a122c8603bb9bd401ff6fb2"},
+    {file = "coverage-7.3.4-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:c6a23ae9348a7a92e7f750f9b7e828448e428e99c24616dec93a0720342f241d"},
+    {file = "coverage-7.3.4-cp38-cp38-win32.whl", hash = "sha256:758ebaf74578b73f727acc4e8ab4b16ab6f22a5ffd7dd254e5946aba42a4ce76"},
+    {file = "coverage-7.3.4-cp38-cp38-win_amd64.whl", hash = "sha256:309ed6a559bc942b7cc721f2976326efbfe81fc2b8f601c722bff927328507dc"},
+    {file = "coverage-7.3.4-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:aefbb29dc56317a4fcb2f3857d5bce9b881038ed7e5aa5d3bcab25bd23f57328"},
+    {file = "coverage-7.3.4-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:183c16173a70caf92e2dfcfe7c7a576de6fa9edc4119b8e13f91db7ca33a7923"},
+    {file = "coverage-7.3.4-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:4a4184dcbe4f98d86470273e758f1d24191ca095412e4335ff27b417291f5964"},
+    {file = "coverage-7.3.4-cp39-cp39-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:93698ac0995516ccdca55342599a1463ed2e2d8942316da31686d4d614597ef9"},
+    {file = "coverage-7.3.4-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:fb220b3596358a86361139edce40d97da7458412d412e1e10c8e1970ee8c09ab"},
+    {file = "coverage-7.3.4-cp39-cp39-musllinux_1_1_aarch64.whl", hash = "sha256:d5b14abde6f8d969e6b9dd8c7a013d9a2b52af1235fe7bebef25ad5c8f47fa18"},
+    {file = "coverage-7.3.4-cp39-cp39-musllinux_1_1_i686.whl", hash = "sha256:610afaf929dc0e09a5eef6981edb6a57a46b7eceff151947b836d869d6d567c1"},
+    {file = "coverage-7.3.4-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:d6ed790728fb71e6b8247bd28e77e99d0c276dff952389b5388169b8ca7b1c28"},
+    {file = "coverage-7.3.4-cp39-cp39-win32.whl", hash = "sha256:c15fdfb141fcf6a900e68bfa35689e1256a670db32b96e7a931cab4a0e1600e5"},
+    {file = "coverage-7.3.4-cp39-cp39-win_amd64.whl", hash = "sha256:38d0b307c4d99a7aca4e00cad4311b7c51b7ac38fb7dea2abe0d182dd4008e05"},
+    {file = "coverage-7.3.4-pp38.pp39.pp310-none-any.whl", hash = "sha256:b1e0f25ae99cf247abfb3f0fac7ae25739e4cd96bf1afa3537827c576b4847e5"},
+    {file = "coverage-7.3.4.tar.gz", hash = "sha256:020d56d2da5bc22a0e00a5b0d54597ee91ad72446fa4cf1b97c35022f6b6dbf0"},
 ]
 
 [package.dependencies]
@@ -431,7 +431,7 @@ colors = ["colorama (>=0.4.6)"]
 
 [[package]]
 name = "kevm-pyk"
-version = "1.0.397"
+version = "1.0.405"
 description = ""
 optional = false
 python-versions = "^3.10"
@@ -440,14 +440,14 @@ develop = false
 
 [package.dependencies]
 pathos = "*"
-pyk = {git = "https://github.com/runtimeverification/pyk.git", tag = "v0.1.549"}
+pyk = {git = "https://github.com/runtimeverification/pyk.git", tag = "v0.1.563"}
 tomlkit = "^0.11.6"
 
 [package.source]
 type = "git"
 url = "https://github.com/runtimeverification/evm-semantics.git"
-reference = "v1.0.397"
-resolved_reference = "1349ef9203534b80bd52577637060ceb5d4e0d24"
+reference = "v1.0.405"
+resolved_reference = "2382ef6ad179f72691283d8d3c048d30829eadcc"
 subdirectory = "kevm-pyk"
 
 [[package]]
@@ -567,38 +567,38 @@ dill = ">=0.3.7"
 
 [[package]]
 name = "mypy"
-version = "1.7.1"
+version = "1.8.0"
 description = "Optional static typing for Python"
 optional = false
 python-versions = ">=3.8"
 files = [
-    {file = "mypy-1.7.1-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:12cce78e329838d70a204293e7b29af9faa3ab14899aec397798a4b41be7f340"},
-    {file = "mypy-1.7.1-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:1484b8fa2c10adf4474f016e09d7a159602f3239075c7bf9f1627f5acf40ad49"},
-    {file = "mypy-1.7.1-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:31902408f4bf54108bbfb2e35369877c01c95adc6192958684473658c322c8a5"},
-    {file = "mypy-1.7.1-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:f2c2521a8e4d6d769e3234350ba7b65ff5d527137cdcde13ff4d99114b0c8e7d"},
-    {file = "mypy-1.7.1-cp310-cp310-win_amd64.whl", hash = "sha256:fcd2572dd4519e8a6642b733cd3a8cfc1ef94bafd0c1ceed9c94fe736cb65b6a"},
-    {file = "mypy-1.7.1-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:4b901927f16224d0d143b925ce9a4e6b3a758010673eeded9b748f250cf4e8f7"},
-    {file = "mypy-1.7.1-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:2f7f6985d05a4e3ce8255396df363046c28bea790e40617654e91ed580ca7c51"},
-    {file = "mypy-1.7.1-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:944bdc21ebd620eafefc090cdf83158393ec2b1391578359776c00de00e8907a"},
-    {file = "mypy-1.7.1-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:9c7ac372232c928fff0645d85f273a726970c014749b924ce5710d7d89763a28"},
-    {file = "mypy-1.7.1-cp311-cp311-win_amd64.whl", hash = "sha256:f6efc9bd72258f89a3816e3a98c09d36f079c223aa345c659622f056b760ab42"},
-    {file = "mypy-1.7.1-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:6dbdec441c60699288adf051f51a5d512b0d818526d1dcfff5a41f8cd8b4aaf1"},
-    {file = "mypy-1.7.1-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:4fc3d14ee80cd22367caaaf6e014494415bf440980a3045bf5045b525680ac33"},
-    {file = "mypy-1.7.1-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:2c6e4464ed5f01dc44dc9821caf67b60a4e5c3b04278286a85c067010653a0eb"},
-    {file = "mypy-1.7.1-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:d9b338c19fa2412f76e17525c1b4f2c687a55b156320acb588df79f2e6fa9fea"},
-    {file = "mypy-1.7.1-cp312-cp312-win_amd64.whl", hash = "sha256:204e0d6de5fd2317394a4eff62065614c4892d5a4d1a7ee55b765d7a3d9e3f82"},
-    {file = "mypy-1.7.1-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:84860e06ba363d9c0eeabd45ac0fde4b903ad7aa4f93cd8b648385a888e23200"},
-    {file = "mypy-1.7.1-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:8c5091ebd294f7628eb25ea554852a52058ac81472c921150e3a61cdd68f75a7"},
-    {file = "mypy-1.7.1-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:40716d1f821b89838589e5b3106ebbc23636ffdef5abc31f7cd0266db936067e"},
-    {file = "mypy-1.7.1-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:5cf3f0c5ac72139797953bd50bc6c95ac13075e62dbfcc923571180bebb662e9"},
-    {file = "mypy-1.7.1-cp38-cp38-win_amd64.whl", hash = "sha256:78e25b2fd6cbb55ddfb8058417df193f0129cad5f4ee75d1502248e588d9e0d7"},
-    {file = "mypy-1.7.1-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:75c4d2a6effd015786c87774e04331b6da863fc3fc4e8adfc3b40aa55ab516fe"},
-    {file = "mypy-1.7.1-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:2643d145af5292ee956aa0a83c2ce1038a3bdb26e033dadeb2f7066fb0c9abce"},
-    {file = "mypy-1.7.1-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:75aa828610b67462ffe3057d4d8a4112105ed211596b750b53cbfe182f44777a"},
-    {file = "mypy-1.7.1-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:ee5d62d28b854eb61889cde4e1dbc10fbaa5560cb39780c3995f6737f7e82120"},
-    {file = "mypy-1.7.1-cp39-cp39-win_amd64.whl", hash = "sha256:72cf32ce7dd3562373f78bd751f73c96cfb441de147cc2448a92c1a308bd0ca6"},
-    {file = "mypy-1.7.1-py3-none-any.whl", hash = "sha256:f7c5d642db47376a0cc130f0de6d055056e010debdaf0707cd2b0fc7e7ef30ea"},
-    {file = "mypy-1.7.1.tar.gz", hash = "sha256:fcb6d9afb1b6208b4c712af0dafdc650f518836065df0d4fb1d800f5d6773db2"},
+    {file = "mypy-1.8.0-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:485a8942f671120f76afffff70f259e1cd0f0cfe08f81c05d8816d958d4577d3"},
+    {file = "mypy-1.8.0-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:df9824ac11deaf007443e7ed2a4a26bebff98d2bc43c6da21b2b64185da011c4"},
+    {file = "mypy-1.8.0-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:2afecd6354bbfb6e0160f4e4ad9ba6e4e003b767dd80d85516e71f2e955ab50d"},
+    {file = "mypy-1.8.0-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:8963b83d53ee733a6e4196954502b33567ad07dfd74851f32be18eb932fb1cb9"},
+    {file = "mypy-1.8.0-cp310-cp310-win_amd64.whl", hash = "sha256:e46f44b54ebddbeedbd3d5b289a893219065ef805d95094d16a0af6630f5d410"},
+    {file = "mypy-1.8.0-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:855fe27b80375e5c5878492f0729540db47b186509c98dae341254c8f45f42ae"},
+    {file = "mypy-1.8.0-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:4c886c6cce2d070bd7df4ec4a05a13ee20c0aa60cb587e8d1265b6c03cf91da3"},
+    {file = "mypy-1.8.0-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:d19c413b3c07cbecf1f991e2221746b0d2a9410b59cb3f4fb9557f0365a1a817"},
+    {file = "mypy-1.8.0-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:9261ed810972061388918c83c3f5cd46079d875026ba97380f3e3978a72f503d"},
+    {file = "mypy-1.8.0-cp311-cp311-win_amd64.whl", hash = "sha256:51720c776d148bad2372ca21ca29256ed483aa9a4cdefefcef49006dff2a6835"},
+    {file = "mypy-1.8.0-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:52825b01f5c4c1c4eb0db253ec09c7aa17e1a7304d247c48b6f3599ef40db8bd"},
+    {file = "mypy-1.8.0-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:f5ac9a4eeb1ec0f1ccdc6f326bcdb464de5f80eb07fb38b5ddd7b0de6bc61e55"},
+    {file = "mypy-1.8.0-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:afe3fe972c645b4632c563d3f3eff1cdca2fa058f730df2b93a35e3b0c538218"},
+    {file = "mypy-1.8.0-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:42c6680d256ab35637ef88891c6bd02514ccb7e1122133ac96055ff458f93fc3"},
+    {file = "mypy-1.8.0-cp312-cp312-win_amd64.whl", hash = "sha256:720a5ca70e136b675af3af63db533c1c8c9181314d207568bbe79051f122669e"},
+    {file = "mypy-1.8.0-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:028cf9f2cae89e202d7b6593cd98db6759379f17a319b5faf4f9978d7084cdc6"},
+    {file = "mypy-1.8.0-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:4e6d97288757e1ddba10dd9549ac27982e3e74a49d8d0179fc14d4365c7add66"},
+    {file = "mypy-1.8.0-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:7f1478736fcebb90f97e40aff11a5f253af890c845ee0c850fe80aa060a267c6"},
+    {file = "mypy-1.8.0-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:42419861b43e6962a649068a61f4a4839205a3ef525b858377a960b9e2de6e0d"},
+    {file = "mypy-1.8.0-cp38-cp38-win_amd64.whl", hash = "sha256:2b5b6c721bd4aabaadead3a5e6fa85c11c6c795e0c81a7215776ef8afc66de02"},
+    {file = "mypy-1.8.0-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:5c1538c38584029352878a0466f03a8ee7547d7bd9f641f57a0f3017a7c905b8"},
+    {file = "mypy-1.8.0-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:4ef4be7baf08a203170f29e89d79064463b7fc7a0908b9d0d5114e8009c3a259"},
+    {file = "mypy-1.8.0-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:7178def594014aa6c35a8ff411cf37d682f428b3b5617ca79029d8ae72f5402b"},
+    {file = "mypy-1.8.0-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:ab3c84fa13c04aeeeabb2a7f67a25ef5d77ac9d6486ff33ded762ef353aa5592"},
+    {file = "mypy-1.8.0-cp39-cp39-win_amd64.whl", hash = "sha256:99b00bc72855812a60d253420d8a2eae839b0afa4938f09f4d2aa9bb4654263a"},
+    {file = "mypy-1.8.0-py3-none-any.whl", hash = "sha256:538fd81bb5e430cc1381a443971c0475582ff9f434c16cd46d2c66763ce85d9d"},
+    {file = "mypy-1.8.0.tar.gz", hash = "sha256:6ff8b244d7085a0b425b56d327b480c3b29cafbd2eff27316a004f9a7391ae07"},
 ]
 
 [package.dependencies]
@@ -810,7 +810,7 @@ windows-terminal = ["colorama (>=0.4.6)"]
 
 [[package]]
 name = "pyk"
-version = "0.1.549"
+version = "0.1.563"
 description = ""
 optional = false
 python-versions = "^3.10"
@@ -831,8 +831,8 @@ xdg-base-dirs = "^6.0.1"
 [package.source]
 type = "git"
 url = "https://github.com/runtimeverification/pyk.git"
-reference = "v0.1.549"
-resolved_reference = "c397bba169e7e3f46ea403452a5f44c4cfa9eab0"
+reference = "v0.1.563"
+resolved_reference = "3a91f68cfe2145562eae3c57187338b06317bfaa"
 
 [[package]]
 name = "pyperclip"
@@ -1082,4 +1082,4 @@ testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "p
 [metadata]
 lock-version = "2.0"
 python-versions = "^3.10"
-content-hash = "2c6a4cf888cf5961dc58a2969d1fd69cf532bdc3003683d8673cef1533f4c161"
+content-hash = "4d4bc05145fd87e870e86485d16e0514c66c716181c24ce8bbf2eea6a0846c6e"
diff --git a/pyproject.toml b/pyproject.toml
index 3ad52f660..7bbc6aeb8 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.102"
+version = "0.1.103"
 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 f6b5570fd..b76a15e04 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.102'
+VERSION: Final = '0.1.103'
diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py
index f21e39fe0..b74e551d4 100644
--- a/src/kontrol/__main__.py
+++ b/src/kontrol/__main__.py
@@ -229,6 +229,7 @@ def exec_prove(
     fail_fast: bool = False,
     port: int | None = None,
     maude_port: int | None = None,
+    use_gas: bool = False,
     **kwargs: Any,
 ) -> None:
     _ignore_arg(kwargs, 'main_module', f'--main-module: {kwargs["main_module"]}')
@@ -258,6 +259,7 @@ def exec_prove(
         max_iterations=max_iterations,
         run_constructor=run_constructor,
         fail_fast=fail_fast,
+        use_gas=use_gas,
     )
 
     rpc_options = RPCOptions(
@@ -724,6 +726,9 @@ def _parse_test_version_tuple(value: str) -> tuple[str, int | None]:
         action='store_true',
         help='Include the contract constructor in the test execution.',
     )
+    prove_args.add_argument(
+        '--use-gas', dest='use_gas', default=False, action='store_true', help='Enables gas computation in KEVM.'
+    )
 
     show_args = command_parser.add_parser(
         'show',
diff --git a/src/kontrol/options.py b/src/kontrol/options.py
index 7f472078a..1762be1f6 100644
--- a/src/kontrol/options.py
+++ b/src/kontrol/options.py
@@ -24,6 +24,7 @@ class ProveOptions:
     run_constructor: bool
     fail_fast: bool
     reinit: bool
+    use_gas: bool
 
     def __init__(
         self,
@@ -41,6 +42,7 @@ def __init__(
         run_constructor: bool = False,
         fail_fast: bool = True,
         reinit: bool = False,
+        use_gas: bool = False,
     ) -> None:
         object.__setattr__(self, 'auto_abstract_gas', auto_abstract_gas)
         object.__setattr__(self, 'bug_report', bug_report)
@@ -55,6 +57,7 @@ def __init__(
         object.__setattr__(self, 'run_constructor', run_constructor)
         object.__setattr__(self, 'fail_fast', fail_fast)
         object.__setattr__(self, 'reinit', reinit)
+        object.__setattr__(self, 'use_gas', use_gas)
 
 
 @dataclass(frozen=True)
diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index 6d9dcd0c8..0e9885310 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -12,8 +12,8 @@
 from pyk.kast.manip import flatten_label, set_cell
 from pyk.kcfg import KCFG
 from pyk.prelude.k import GENERATED_TOP_CELL
-from pyk.prelude.kbool import FALSE, notBool
-from pyk.prelude.kint import intToken, leInt, eqInt
+from pyk.prelude.kbool import FALSE, TRUE, notBool
+from pyk.prelude.kint import intToken, eqInt
 from pyk.prelude.ml import mlEqualsTrue
 from pyk.proof.proof import Proof
 from pyk.proof.reachability import APRBMCProof, APRProof
@@ -204,6 +204,7 @@ def init_and_run_proof(test: FoundryTest) -> Proof:
                 kcfg_explore=kcfg_explore,
                 bmc_depth=prove_options.bmc_depth,
                 run_constructor=prove_options.run_constructor,
+                use_gas=prove_options.use_gas,
             )
 
             run_prover(
@@ -238,6 +239,7 @@ def method_to_apr_proof(
     kcfg_explore: KCFGExplore,
     bmc_depth: int | None = None,
     run_constructor: bool = False,
+    use_gas: bool = False,
 ) -> APRProof | APRBMCProof:
     if Proof.proof_data_exists(test.id, foundry.proofs_dir):
         apr_proof = foundry.get_apr_proof(test.id)
@@ -259,6 +261,7 @@ def method_to_apr_proof(
         test=test,
         kcfg_explore=kcfg_explore,
         setup_proof=setup_proof,
+        use_gas=use_gas,
     )
 
     if bmc_depth is not None:
@@ -299,6 +302,7 @@ def _method_to_initialized_cfg(
     kcfg_explore: KCFGExplore,
     *,
     setup_proof: APRProof | None = None,
+    use_gas: bool = False,
 ) -> tuple[KCFG, int, int]:
     _LOGGER.info(f'Initializing KCFG for test: {test.id}')
 
@@ -308,6 +312,7 @@ def _method_to_initialized_cfg(
         test.contract,
         test.method,
         setup_proof,
+        use_gas,
     )
 
     for node_id in new_node_ids:
@@ -336,6 +341,7 @@ def _method_to_cfg(
     contract: Contract,
     method: Contract.Method | Contract.Constructor,
     setup_proof: APRProof | None,
+    use_gas: bool,
 ) -> tuple[KCFG, list[int], int, int]:
     calldata = None
     callvalue = None
@@ -357,6 +363,7 @@ def _method_to_cfg(
         calldata=calldata,
         is_calldata_symbolic=is_calldata_symbolic,
         callvalue=callvalue,
+        use_gas=use_gas,
     )
     new_node_ids = []
 
@@ -422,6 +429,7 @@ def _init_cterm(
     empty_config: KInner,
     contract_name: str,
     program: KInner,
+    use_gas: bool,
     *,
     setup_cterm: CTerm | None = None,
     calldata: KInner | None = None,
@@ -438,6 +446,7 @@ def _init_cterm(
     )
     init_subst = {
         'MODE_CELL': KApply('NORMAL'),
+        'USEGAS_CELL': TRUE if use_gas else FALSE,
         'SCHEDULE_CELL': KApply('SHANGHAI_EVM'),
         'STATUSCODE_CELL': KVariable('STATUSCODE'),
         'CALLSTACK_CELL': KApply('.List'),
diff --git a/src/tests/integration/test-data/foundry-prove-with-gas b/src/tests/integration/test-data/foundry-prove-with-gas
new file mode 100644
index 000000000..e65ddea40
--- /dev/null
+++ b/src/tests/integration/test-data/foundry-prove-with-gas
@@ -0,0 +1,8 @@
+GasTest.testInfiniteGas()
+GasTest.testSetGas()
+StoreTest.testGasLoadColdVM()
+StoreTest.testGasLoadWarmUp()
+StoreTest.testGasLoadWarmVM()
+StoreTest.testGasStoreColdVM()
+StoreTest.testGasStoreWarmUp()
+StoreTest.testGasStoreWarmVM()
\ No newline at end of file
diff --git a/src/tests/integration/test-data/gas-abstraction.expected b/src/tests/integration/test-data/gas-abstraction.expected
index 51cea1ec7..cfa779311 100644
--- a/src/tests/integration/test-data/gas-abstraction.expected
+++ b/src/tests/integration/test-data/gas-abstraction.expected
@@ -103,6 +103,9 @@ Node 6:
       <schedule>
         SHANGHAI
       </schedule>
+      <useGas>
+        true
+      </useGas>
       <ethereum>
         <evm>
           <output>
@@ -408,6 +411,9 @@ Node 6:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               true
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -614,6 +620,9 @@ Node 6:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               true
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -823,6 +832,9 @@ Node 6:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               true
+             </useGas>
              <ethereum>
                <evm>
                  <output>
diff --git a/src/tests/integration/test-data/show/AssertTest.testFail_assert_false().expected b/src/tests/integration/test-data/show/AssertTest.testFail_assert_false().expected
index 4fb341571..99dcdd49e 100644
--- a/src/tests/integration/test-data/show/AssertTest.testFail_assert_false().expected
+++ b/src/tests/integration/test-data/show/AssertTest.testFail_assert_false().expected
@@ -5,7 +5,7 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (272 steps)
+│  (179 steps)
 ├─ 3
 │   k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
 │   pc: 317
@@ -33,7 +33,7 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (376 steps)
+│  (244 steps)
 ├─ 8
 │   k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K
 │   pc: 2984
@@ -81,6 +81,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -116,7 +119,7 @@
                    ...
                    ...
                    <memoryUsed>
-                     ( 0 => 3 )
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -286,6 +289,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -324,7 +330,7 @@
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -494,6 +500,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -532,7 +541,7 @@
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -700,6 +709,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -738,7 +750,7 @@
                    ...
                    ...
                    <memoryUsed>
-                     ( 3 => 0 )
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -908,6 +920,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -940,7 +955,7 @@
                    ...
                    ...
                    <memoryUsed>
-                     ( 0 => 3 )
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -1094,6 +1109,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1129,7 +1147,7 @@
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -1283,6 +1301,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1318,7 +1339,7 @@
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
diff --git a/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected b/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected
index 4967d3c24..93b9b49bd 100644
--- a/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected
+++ b/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected
@@ -5,7 +5,7 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (272 steps)
+│  (179 steps)
 ├─ 3
 │   k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
 │   pc: 317
@@ -33,7 +33,7 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (303 steps)
+│  (200 steps)
 ├─ 8
 │   k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
 │   pc: 317
@@ -77,6 +77,9 @@ Node 10:
       <schedule>
         SHANGHAI
       </schedule>
+      <useGas>
+        false
+      </useGas>
       <ethereum>
         <evm>
           <output>
@@ -108,7 +111,7 @@ Node 10:
               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"
             </localMem>
             <memoryUsed>
-              3
+              0
             </memoryUsed>
             <static>
               false
@@ -267,6 +270,9 @@ Node 10:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -302,7 +308,7 @@ Node 10:
                    ...
                    ...
                    <memoryUsed>
-                     ( 0 => 3 )
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -472,6 +478,9 @@ Node 10:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -510,7 +519,7 @@ Node 10:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -680,6 +689,9 @@ Node 10:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -718,7 +730,7 @@ Node 10:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -886,6 +898,9 @@ Node 10:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -924,7 +939,7 @@ Node 10:
                    ...
                    ...
                    <memoryUsed>
-                     ( 3 => 0 )
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -1094,6 +1109,9 @@ Node 10:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1126,7 +1144,7 @@ Node 10:
                    ...
                    ...
                    <memoryUsed>
-                     ( 0 => 3 )
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -1280,6 +1298,9 @@ Node 10:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1315,7 +1336,7 @@ Node 10:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -1469,6 +1490,9 @@ Node 10:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1504,7 +1528,7 @@ Node 10:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
diff --git a/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected b/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected
index 786e4e74a..9003b03d8 100644
--- a/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected
+++ b/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected
@@ -5,7 +5,7 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (272 steps)
+│  (179 steps)
 ├─ 3
 │   k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
 │   pc: 317
@@ -33,9 +33,9 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (641 steps)
+│  (416 steps)
 ├─ 8
-│   k: CALL ( VGAS:Int +Int -2951 ) 645326474426547203313410069153905908525362434349 0  ...
+│   k: CALL VGAS:Int 645326474426547203313410069153905908525362434349 0 128 4 128 0 ~>  ...
 │   pc: 800
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
@@ -47,9 +47,9 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (365 steps)
+│  (228 steps)
 ├─ 10
-│   k: STATICCALL ( VGAS:Int +Int -5792 ) 728815563385977040452943777879061427756277306 ...
+│   k: STATICCALL VGAS:Int 728815563385977040452943777879061427756277306518 128 4 128 0 ...
 │   pc: 881
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
@@ -61,7 +61,7 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (505 steps)
+│  (338 steps)
 ├─ 12
 │   k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> #return 128 0 ~> #pc [ STATICC ...
 │   pc: 2984
@@ -84,12 +84,12 @@
 │
 │  (1 step)
 ├─ 15
-│   k: #popCallStack ~> #popWorldState ~> 0 ~> #push ~> #refund #gas ( ( Cgascap ( SHAN ...
+│   k: #popCallStack ~> #popWorldState ~> 0 ~> #push ~> #refund #gas ( VGAS:Int ) ~> #s ...
 │   pc: 2984
 │   callDepth: 1
 │   statusCode: EVMC_REVERT
 │
-│  (150 steps)
+│  (95 steps)
 ├─ 16
 │   k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
 │   pc: 317
@@ -133,6 +133,9 @@ Node 18:
       <schedule>
         SHANGHAI
       </schedule>
+      <useGas>
+        false
+      </useGas>
       <ethereum>
         <evm>
           <output>
@@ -167,11 +170,8 @@ Node 18:
               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\xf3\xad0#\x00\x00\x00\x00\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>
-              5
+              0
             </memoryUsed>
-            <callGas>
-              #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) )
-            </callGas>
             <static>
               false
             </static>
@@ -185,7 +185,7 @@ Node 18:
               .List
             </log>
             <accessedAccounts>
-              ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
+              .Set
             </accessedAccounts>
             <accessedStorage>
               .Map
@@ -334,6 +334,9 @@ Node 18:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -369,7 +372,7 @@ Node 18:
                    ...
                    ...
                    <memoryUsed>
-                     ( 0 => 3 )
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -539,6 +542,9 @@ Node 18:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -577,7 +583,7 @@ Node 18:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -747,6 +753,9 @@ Node 18:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -785,7 +794,7 @@ Node 18:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -953,6 +962,9 @@ Node 18:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -991,7 +1003,7 @@ Node 18:
                    ...
                    ...
                    <memoryUsed>
-                     ( 3 => 0 )
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -1150,7 +1162,7 @@ Node 18:
     rule [BASIC-BLOCK-6-TO-8]: <foundry>
            <kevm>
              <k>
-               ( .K => CALL ( VGAS:Int +Int -2951 ) 645326474426547203313410069153905908525362434349 0 128 4 128 0
+               ( .K => CALL VGAS:Int 645326474426547203313410069153905908525362434349 0 128 4 128 0
                ~> #pc [ CALL ] )
                ~> #execute
                ~> _CONTINUATION
@@ -1161,6 +1173,9 @@ Node 18:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <callStack>
@@ -1190,11 +1205,8 @@ Node 18:
                    ...
                    ...
                    <memoryUsed>
-                     ( 0 => 5 )
+                     0
                    </memoryUsed>
-                   <callGas>
-                     ( _CALLGAS_CELL => #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -2951 ) , ( VGAS:Int +Int -2951 ) , 100 ) ) )
-                   </callGas>
                    <static>
                      false
                    </static>
@@ -1208,7 +1220,7 @@ Node 18:
                      .List
                    </log>
                    <accessedAccounts>
-                     ( .Set => SetItem ( 645326474426547203313410069153905908525362434349 ) )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -1336,7 +1348,7 @@ Node 18:
     rule [BASIC-BLOCK-8-TO-9]: <foundry>
            <kevm>
              <k>
-               ( CALL ( VGAS:Int +Int -2951 ) 645326474426547203313410069153905908525362434349 0 128 4 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0
+               ( CALL VGAS:Int 645326474426547203313410069153905908525362434349 0 128 4 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0
                ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"\xf4\x84H\x14" false
                ~> #return 128 0 )
                ~> #pc [ CALL ]
@@ -1349,6 +1361,9 @@ Node 18:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <callStack>
@@ -1378,11 +1393,8 @@ Node 18:
                    ...
                    ...
                    <memoryUsed>
-                     5
+                     0
                    </memoryUsed>
-                   <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -2951 ) , ( VGAS:Int +Int -2951 ) , 100 ) )
-                   </callGas>
                    <static>
                      false
                    </static>
@@ -1396,7 +1408,7 @@ Node 18:
                      .List
                    </log>
                    <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -1527,7 +1539,7 @@ Node 18:
                ( #checkCall 728815563385977040452943777879061427756277306518 0
                ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"\xf4\x84H\x14" false
                ~> #return 128 0
-               ~> #pc [ CALL ] => STATICCALL ( VGAS:Int +Int -5792 ) 728815563385977040452943777879061427756277306518 128 4 128 0
+               ~> #pc [ CALL ] => STATICCALL VGAS:Int 728815563385977040452943777879061427756277306518 128 4 128 0
                ~> #pc [ STATICCALL ]
                ~> #checkRevert
                ~> #updateRevertOutput 128 0 )
@@ -1540,6 +1552,9 @@ Node 18:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1572,11 +1587,8 @@ Node 18:
                    ...
                    ...
                    <memoryUsed>
-                     5
+                     0
                    </memoryUsed>
-                   <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int ( -2951 => -5792 ) ) , ( VGAS:Int +Int ( -2951 => -5792 ) ) , 100 ) )
-                   </callGas>
                    <static>
                      false
                    </static>
@@ -1590,7 +1602,7 @@ Node 18:
                      .List
                    </log>
                    <accessedAccounts>
-                     ( SetItem ( 645326474426547203313410069153905908525362434349 ) => ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -1723,7 +1735,7 @@ Node 18:
     rule [BASIC-BLOCK-10-TO-11]: <foundry>
            <kevm>
              <k>
-               ( STATICCALL ( VGAS:Int +Int -5792 ) 728815563385977040452943777879061427756277306518 128 4 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0
+               ( STATICCALL VGAS:Int 728815563385977040452943777879061427756277306518 128 4 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0
                ~> #call 728815563385977040452943777879061427756277306518 728815563385977040452943777879061427756277306518 728815563385977040452943777879061427756277306518 0 0 b"\xf3\xad0#" true
                ~> #return 128 0 )
                ~> #pc [ STATICCALL ]
@@ -1738,6 +1750,9 @@ Node 18:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1770,11 +1785,8 @@ Node 18:
                    ...
                    ...
                    <memoryUsed>
-                     5
+                     0
                    </memoryUsed>
-                   <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) )
-                   </callGas>
                    <static>
                      false
                    </static>
@@ -1788,7 +1800,7 @@ Node 18:
                      .List
                    </log>
                    <accessedAccounts>
-                     ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -1938,6 +1950,9 @@ Node 18:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1957,9 +1972,9 @@ Node 18:
                    </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\xf3\xad0#\x00\x00\x00\x00\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>
-                     5
+                     0
                    </memoryUsed> <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) )
+                     CALLGAS_CELL:Gas
                    </callGas> <static>
                      false
                    </static> <callDepth>
@@ -2009,7 +2024,7 @@ Node 18:
                    </log> <refund>
                      REFUND_CELL:Int
                    </refund> <accessedAccounts>
-                     ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
+                     .Set
                    </accessedAccounts> <accessedStorage>
                      .Map
                    </accessedStorage> </substate>-fragment } ) )
@@ -2041,10 +2056,10 @@ Node 18:
                    ...
                    ...
                    <memoryUsed>
-                     ( 5 => 3 )
+                     0
                    </memoryUsed>
                    <callGas>
-                     ( #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) ) => 0 )
+                     CALLGAS_CELL:Gas
                    </callGas>
                    <static>
                      ( false => true )
@@ -2064,7 +2079,7 @@ Node 18:
                      REFUND_CELL:Int
                    </refund>
                    <accessedAccounts>
-                     ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
+                     ( .Set => SetItem ( 728815563385977040452943777879061427756277306518 ) )
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -2212,6 +2227,9 @@ Node 18:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -2232,9 +2250,9 @@ Node 18:
                    </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\xf3\xad0#\x00\x00\x00\x00\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>
-                     5
+                     0
                    </memoryUsed> <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) )
+                     CALLGAS_CELL:Gas
                    </callGas> <static>
                      false
                    </static> <callDepth>
@@ -2284,7 +2302,7 @@ Node 18:
                    </log> <refund>
                      REFUND_CELL:Int
                    </refund> <accessedAccounts>
-                     ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
+                     .Set
                    </accessedAccounts> <accessedStorage>
                      .Map
                    </accessedStorage> </substate>-fragment } )
@@ -2316,10 +2334,10 @@ Node 18:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <callGas>
-                     0
+                     CALLGAS_CELL:Gas
                    </callGas>
                    <static>
                      true
@@ -2339,7 +2357,7 @@ Node 18:
                      REFUND_CELL:Int
                    </refund>
                    <accessedAccounts>
-                     ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
+                     SetItem ( 728815563385977040452943777879061427756277306518 )
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -2487,6 +2505,9 @@ Node 18:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -2507,9 +2528,9 @@ Node 18:
                    </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\xf3\xad0#\x00\x00\x00\x00\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>
-                     5
+                     0
                    </memoryUsed> <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) )
+                     CALLGAS_CELL:Gas
                    </callGas> <static>
                      false
                    </static> <callDepth>
@@ -2559,7 +2580,7 @@ Node 18:
                    </log> <refund>
                      REFUND_CELL:Int
                    </refund> <accessedAccounts>
-                     ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
+                     .Set
                    </accessedAccounts> <accessedStorage>
                      .Map
                    </accessedStorage> </substate>-fragment } )
@@ -2591,10 +2612,10 @@ Node 18:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <callGas>
-                     0
+                     CALLGAS_CELL:Gas
                    </callGas>
                    <static>
                      true
@@ -2614,7 +2635,7 @@ Node 18:
                      REFUND_CELL:Int
                    </refund>
                    <accessedAccounts>
-                     ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
+                     SetItem ( 728815563385977040452943777879061427756277306518 )
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -2751,7 +2772,7 @@ Node 18:
                ~> #popWorldState
                ~> 0
                ~> #push
-               ~> #refund #gas ( ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) +Int -290 ) )
+               ~> #refund #gas ( VGAS:Int )
                ~> #setLocalMem 128 0 b"NH{q\x00\x00\x00\x00\x00\x00\x00\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" )
                ~> #pc [ STATICCALL ]
                ~> #checkRevert
@@ -2765,6 +2786,9 @@ Node 18:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -2785,9 +2809,9 @@ Node 18:
                    </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\xf3\xad0#\x00\x00\x00\x00\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>
-                     5
+                     0
                    </memoryUsed> <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) )
+                     CALLGAS_CELL:Gas
                    </callGas> <static>
                      false
                    </static> <callDepth>
@@ -2837,7 +2861,7 @@ Node 18:
                    </log> <refund>
                      REFUND_CELL:Int
                    </refund> <accessedAccounts>
-                     ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
+                     .Set
                    </accessedAccounts> <accessedStorage>
                      .Map
                    </accessedStorage> </substate>-fragment } )
@@ -2869,10 +2893,10 @@ Node 18:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <callGas>
-                     0
+                     CALLGAS_CELL:Gas
                    </callGas>
                    <static>
                      true
@@ -2892,7 +2916,7 @@ Node 18:
                      REFUND_CELL:Int
                    </refund>
                    <accessedAccounts>
-                     ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
+                     SetItem ( 728815563385977040452943777879061427756277306518 )
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -3028,7 +3052,7 @@ Node 18:
                ~> #popWorldState
                ~> 0
                ~> #push
-               ~> #refund #gas ( ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) +Int -290 ) )
+               ~> #refund #gas ( VGAS:Int )
                ~> #setLocalMem 128 0 b"NH{q\x00\x00\x00\x00\x00\x00\x00\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"
                ~> #pc [ STATICCALL ]
                ~> #checkRevert
@@ -3043,6 +3067,9 @@ Node 18:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -3065,9 +3092,9 @@ Node 18:
                    </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\xf3\xad0#\x00\x00\x00\x00\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>
-                     5
+                     0
                    </memoryUsed> <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) )
+                     CALLGAS_CELL:Gas
                    </callGas> <static>
                      false
                    </static> <callDepth>
@@ -3117,7 +3144,7 @@ Node 18:
                    </log> <refund>
                      REFUND_CELL:Int
                    </refund> <accessedAccounts>
-                     ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
+                     .Set
                    </accessedAccounts> <accessedStorage>
                      .Map
                    </accessedStorage> </substate>-fragment } ) => .List )
@@ -3149,10 +3176,10 @@ Node 18:
                    ...
                    ...
                    <memoryUsed>
-                     ( 3 => 5 )
+                     0
                    </memoryUsed>
                    <callGas>
-                     ( 0 => #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) ) )
+                     CALLGAS_CELL:Gas
                    </callGas>
                    <static>
                      ( true => false )
@@ -3172,7 +3199,7 @@ Node 18:
                      REFUND_CELL:Int
                    </refund>
                    <accessedAccounts>
-                     ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
+                     ( SetItem ( 728815563385977040452943777879061427756277306518 ) => .Set )
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -3315,6 +3342,9 @@ Node 18:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -3353,11 +3383,8 @@ Node 18:
                    ...
                    ...
                    <memoryUsed>
-                     5
+                     0
                    </memoryUsed>
-                   <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) )
-                   </callGas>
                    <static>
                      false
                    </static>
@@ -3371,7 +3398,7 @@ Node 18:
                      .List
                    </log>
                    <accessedAccounts>
-                     ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -3515,6 +3542,9 @@ Node 18:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -3553,11 +3583,8 @@ Node 18:
                    ...
                    ...
                    <memoryUsed>
-                     5
+                     0
                    </memoryUsed>
-                   <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) )
-                   </callGas>
                    <static>
                      false
                    </static>
@@ -3571,7 +3598,7 @@ Node 18:
                      .List
                    </log>
                    <accessedAccounts>
-                     ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
diff --git a/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected b/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected
index 3dc16681d..972f95ae5 100644
--- a/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected
+++ b/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected
@@ -5,7 +5,7 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (272 steps)
+│  (179 steps)
 ├─ 3
 │   k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
 │   pc: 317
@@ -33,7 +33,7 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (469 steps)
+│  (307 steps)
 ├─ 8
 │   k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K
 │   pc: 2984
@@ -77,6 +77,9 @@ Node 10:
       <schedule>
         SHANGHAI
       </schedule>
+      <useGas>
+        false
+      </useGas>
       <ethereum>
         <evm>
           <output>
@@ -108,7 +111,7 @@ Node 10:
               b"NH{q\x00\x00\x00\x00\x00\x00\x00\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\x80"
             </localMem>
             <memoryUsed>
-              3
+              0
             </memoryUsed>
             <static>
               false
@@ -267,6 +270,9 @@ Node 10:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -302,7 +308,7 @@ Node 10:
                    ...
                    ...
                    <memoryUsed>
-                     ( 0 => 3 )
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -472,6 +478,9 @@ Node 10:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -510,7 +519,7 @@ Node 10:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -680,6 +689,9 @@ Node 10:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -718,7 +730,7 @@ Node 10:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -886,6 +898,9 @@ Node 10:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -924,7 +939,7 @@ Node 10:
                    ...
                    ...
                    <memoryUsed>
-                     ( 3 => 0 )
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -1094,6 +1109,9 @@ Node 10:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1126,7 +1144,7 @@ Node 10:
                    ...
                    ...
                    <memoryUsed>
-                     ( 0 => 3 )
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -1280,6 +1298,9 @@ Node 10:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1315,7 +1336,7 @@ Node 10:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -1469,6 +1490,9 @@ Node 10:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1504,7 +1528,7 @@ Node 10:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
diff --git a/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected b/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected
index 9dda7ff30..25d7ea272 100644
--- a/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected
+++ b/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected
@@ -5,7 +5,7 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (272 steps)
+│  (179 steps)
 ├─ 3
 │   k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
 │   pc: 317
@@ -33,7 +33,7 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (396 steps)
+│  (263 steps)
 ├─ 8
 │   k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
 │   pc: 317
@@ -81,6 +81,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -116,7 +119,7 @@
                    ...
                    ...
                    <memoryUsed>
-                     ( 0 => 3 )
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -286,6 +289,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -324,7 +330,7 @@
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -494,6 +500,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -532,7 +541,7 @@
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -700,6 +709,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -738,7 +750,7 @@
                    ...
                    ...
                    <memoryUsed>
-                     ( 3 => 0 )
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -908,6 +920,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -940,7 +955,7 @@
                    ...
                    ...
                    <memoryUsed>
-                     ( 0 => 3 )
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -1094,6 +1109,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1129,7 +1147,7 @@
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -1283,6 +1301,9 @@
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1318,7 +1339,7 @@
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
diff --git a/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected b/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected
index 98e4e2c88..316b4222e 100644
--- a/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected
+++ b/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected
@@ -5,7 +5,7 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (272 steps)
+│  (179 steps)
 ├─ 3
 │   k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
 │   pc: 317
@@ -33,7 +33,7 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (543 steps)
+│  (360 steps)
 ├─ 8 (split)
 │   k: JUMPI 1113 bool2Word ( 100 <=Int VV0_x_114b9705:Int ) ~> #pc [ JUMPI ] ~> #execu ...
 │   pc: 1105
@@ -49,7 +49,7 @@
 ┃  │   callDepth: 0
 ┃  │   statusCode: STATUSCODE:StatusCode
 ┃  │
-┃  │  (64 steps)
+┃  │  (39 steps)
 ┃  ├─ 11
 ┃  │   k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
 ┃  │   pc: 317
@@ -86,7 +86,7 @@
    │   callDepth: 0
    │   statusCode: STATUSCODE:StatusCode
    │
-   │  (102 steps)
+   │  (63 steps)
    ├─ 12
    │   k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K
    │   pc: 2984
@@ -124,6 +124,9 @@ Node 16:
       <schedule>
         SHANGHAI
       </schedule>
+      <useGas>
+        false
+      </useGas>
       <ethereum>
         <evm>
           <output>
@@ -155,7 +158,7 @@ Node 16:
               b"NH{q\x00\x00\x00\x00\x00\x00\x00\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\x80"
             </localMem>
             <memoryUsed>
-              3
+              0
             </memoryUsed>
             <static>
               false
@@ -317,6 +320,9 @@ Node 16:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -352,7 +358,7 @@ Node 16:
                    ...
                    ...
                    <memoryUsed>
-                     ( 0 => 3 )
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -522,6 +528,9 @@ Node 16:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -560,7 +569,7 @@ Node 16:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -730,6 +739,9 @@ Node 16:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -768,7 +780,7 @@ Node 16:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -936,6 +948,9 @@ Node 16:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -974,7 +989,7 @@ Node 16:
                    ...
                    ...
                    <memoryUsed>
-                     ( 3 => 0 )
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -1147,6 +1162,9 @@ Node 16:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <callStack>
@@ -1176,7 +1194,7 @@ Node 16:
                    ...
                    ...
                    <memoryUsed>
-                     ( 0 => 3 )
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -1334,6 +1352,9 @@ Node 16:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1366,7 +1387,7 @@ Node 16:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -1525,6 +1546,9 @@ Node 16:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1557,7 +1581,7 @@ Node 16:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -1716,6 +1740,9 @@ Node 16:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1751,7 +1778,7 @@ Node 16:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -1909,6 +1936,9 @@ Node 16:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1944,7 +1974,7 @@ Node 16:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -2102,6 +2132,9 @@ Node 16:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -2137,7 +2170,7 @@ Node 16:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -2295,6 +2328,9 @@ Node 16:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -2330,7 +2366,7 @@ Node 16:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
diff --git a/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected b/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected
index e1dab288e..bd27726f3 100644
--- a/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected
+++ b/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected
@@ -5,7 +5,7 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (272 steps)
+│  (179 steps)
 ├─ 3
 │   k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
 │   pc: 317
@@ -33,7 +33,7 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (580 steps)
+│  (387 steps)
 ├─ 8 (split)
 │   k: JUMPI 1583 bool2Word ( VV1_y_114b9705:Int <=Int VV0_x_114b9705:Int ) ~> #pc [ JU ...
 │   pc: 1579
@@ -49,7 +49,7 @@
 ┃  │   callDepth: 0
 ┃  │   statusCode: STATUSCODE:StatusCode
 ┃  │
-┃  │  (116 steps)
+┃  │  (72 steps)
 ┃  ├─ 11
 ┃  │   k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K
 ┃  │   pc: 2984
@@ -78,7 +78,7 @@
    │   callDepth: 0
    │   statusCode: STATUSCODE:StatusCode
    │
-   │  (62 steps)
+   │  (37 steps)
    ├─ 12
    │   k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
    │   pc: 317
@@ -124,6 +124,9 @@ Node 15:
       <schedule>
         SHANGHAI
       </schedule>
+      <useGas>
+        false
+      </useGas>
       <ethereum>
         <evm>
           <output>
@@ -155,7 +158,7 @@ Node 15:
               b"NH{q\x00\x00\x00\x00\x00\x00\x00\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\x80"
             </localMem>
             <memoryUsed>
-              3
+              0
             </memoryUsed>
             <static>
               false
@@ -319,6 +322,9 @@ Node 15:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -354,7 +360,7 @@ Node 15:
                    ...
                    ...
                    <memoryUsed>
-                     ( 0 => 3 )
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -524,6 +530,9 @@ Node 15:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -562,7 +571,7 @@ Node 15:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -732,6 +741,9 @@ Node 15:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -770,7 +782,7 @@ Node 15:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -938,6 +950,9 @@ Node 15:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -976,7 +991,7 @@ Node 15:
                    ...
                    ...
                    <memoryUsed>
-                     ( 3 => 0 )
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -1151,6 +1166,9 @@ Node 15:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <callStack>
@@ -1180,7 +1198,7 @@ Node 15:
                    ...
                    ...
                    <memoryUsed>
-                     ( 0 => 3 )
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -1340,6 +1358,9 @@ Node 15:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1372,7 +1393,7 @@ Node 15:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -1533,6 +1554,9 @@ Node 15:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1565,7 +1589,7 @@ Node 15:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -1726,6 +1750,9 @@ Node 15:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1761,7 +1788,7 @@ Node 15:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -1921,6 +1948,9 @@ Node 15:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1956,7 +1986,7 @@ Node 15:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -2116,6 +2146,9 @@ Node 15:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -2151,7 +2184,7 @@ Node 15:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
@@ -2311,6 +2344,9 @@ Node 15:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -2346,7 +2382,7 @@ Node 15:
                    ...
                    ...
                    <memoryUsed>
-                     3
+                     0
                    </memoryUsed>
                    <static>
                      false
diff --git a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected
index 8efd6d73d..f0cc0c4c4 100644
--- a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected
+++ b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected
@@ -5,9 +5,9 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (875 steps)
+│  (560 steps)
 ├─ 3
-│   k: STATICCALL ( VGAS:Int +Int -3048 ) 645326474426547203313410069153905908525362434 ...
+│   k: STATICCALL VGAS:Int 645326474426547203313410069153905908525362434349 128 36 128  ...
 │   pc: 563
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
@@ -19,7 +19,7 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (299 steps)
+│  (189 steps)
 ├─ 5
 │   k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
 │   pc: 281
@@ -63,6 +63,9 @@ Node 7:
       <schedule>
         SHANGHAI
       </schedule>
+      <useGas>
+        false
+      </useGas>
       <ethereum>
         <evm>
           <output>
@@ -97,11 +100,8 @@ Node 7:
               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\x00\x00\x00\x00\x00\x00\x00\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"
             </localMem>
             <memoryUsed>
-              6
+              0
             </memoryUsed>
-            <callGas>
-              #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3048 ) , ( VGAS:Int +Int -3048 ) , 100 ) )
-            </callGas>
             <static>
               false
             </static>
@@ -115,7 +115,7 @@ Node 7:
               .List
             </log>
             <accessedAccounts>
-              SetItem ( 645326474426547203313410069153905908525362434349 )
+              .Set
             </accessedAccounts>
             <accessedStorage>
               .Map
@@ -266,7 +266,7 @@ Node 7:
     rule [BASIC-BLOCK-1-TO-3]: <foundry>
            <kevm>
              <k>
-               ( .K => STATICCALL ( VGAS:Int +Int -3048 ) 645326474426547203313410069153905908525362434349 128 36 128 0
+               ( .K => STATICCALL VGAS:Int 645326474426547203313410069153905908525362434349 128 36 128 0
                ~> #pc [ STATICCALL ] )
                ~> #execute
                ~> _CONTINUATION
@@ -277,6 +277,9 @@ Node 7:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <callStack>
@@ -309,24 +312,22 @@ Node 7:
                    ...
                    ...
                    <memoryUsed>
-                     ( 0 => 6 )
+                     0
                    </memoryUsed>
-                   <callGas>
-                     ( _CALLGAS_CELL => #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3048 ) , ( VGAS:Int +Int -3048 ) , 100 ) ) )
-                   </callGas>
                    <static>
                      false
                    </static>
                    <callDepth>
                      0
                    </callDepth>
+                   ...
                  </callState>
                  <substate>
                    <log>
                      .List
                    </log>
                    <accessedAccounts>
-                     ( .Set => SetItem ( 645326474426547203313410069153905908525362434349 ) )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -474,7 +475,7 @@ Node 7:
     rule [BASIC-BLOCK-3-TO-4]: <foundry>
            <kevm>
              <k>
-               ( STATICCALL ( VGAS:Int +Int -3048 ) 645326474426547203313410069153905908525362434349 128 36 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0
+               ( STATICCALL VGAS:Int 645326474426547203313410069153905908525362434349 128 36 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0
                ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) ) true
                ~> #return 128 0 )
                ~> #pc [ STATICCALL ]
@@ -487,6 +488,9 @@ Node 7:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <callStack>
@@ -519,24 +523,22 @@ Node 7:
                    ...
                    ...
                    <memoryUsed>
-                     6
+                     0
                    </memoryUsed>
-                   <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3048 ) , ( VGAS:Int +Int -3048 ) , 100 ) )
-                   </callGas>
                    <static>
                      false
                    </static>
                    <callDepth>
                      0
                    </callDepth>
+                   ...
                  </callState>
                  <substate>
                    <log>
                      .List
                    </log>
                    <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -698,6 +700,9 @@ Node 7:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -733,24 +738,22 @@ Node 7:
                    ...
                    ...
                    <memoryUsed>
-                     6
+                     0
                    </memoryUsed>
-                   <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3048 ) , ( VGAS:Int +Int -3048 ) , 100 ) )
-                   </callGas>
                    <static>
                      false
                    </static>
                    <callDepth>
                      0
                    </callDepth>
+                   ...
                  </callState>
                  <substate>
                    <log>
                      .List
                    </log>
                    <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -910,6 +913,9 @@ Node 7:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -948,24 +954,22 @@ Node 7:
                    ...
                    ...
                    <memoryUsed>
-                     6
+                     0
                    </memoryUsed>
-                   <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3048 ) , ( VGAS:Int +Int -3048 ) , 100 ) )
-                   </callGas>
                    <static>
                      false
                    </static>
                    <callDepth>
                      0
                    </callDepth>
+                   ...
                  </callState>
                  <substate>
                    <log>
                      .List
                    </log>
                    <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -1123,6 +1127,9 @@ Node 7:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1161,24 +1168,22 @@ Node 7:
                    ...
                    ...
                    <memoryUsed>
-                     6
+                     0
                    </memoryUsed>
-                   <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3048 ) , ( VGAS:Int +Int -3048 ) , 100 ) )
-                   </callGas>
                    <static>
                      false
                    </static>
                    <callDepth>
                      0
                    </callDepth>
+                   ...
                  </callState>
                  <substate>
                    <log>
                      .List
                    </log>
                    <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
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 af163d093..91e37f62c 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
@@ -5,9 +5,9 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (890 steps)
+│  (570 steps)
 ├─ 3
-│   k: STATICCALL ( VGAS:Int +Int -3061 ) 645326474426547203313410069153905908525362434 ...
+│   k: STATICCALL VGAS:Int 645326474426547203313410069153905908525362434349 128 36 128  ...
 │   pc: 563
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
@@ -21,48 +21,41 @@
 │
 │  (1000 steps)
 ├─ 5
-│   k: #gas [ MSTORE , MSTORE 192 46308022326495007027972728677917914892729792999299745 ...
-│   pc: 3667
+│   k: #gas [ ISZERO , ISZERO 1 ] ~> ISZERO 1 ~> #pc [ ISZERO ] ~> #execute ~> CONTINUA ...
+│   pc: 4206
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (1000 steps)
+│  (825 steps)
 ├─ 6
-│   k: #next [ DUP ( 2 ) ] ~> #execute ~> CONTINUATION:K
-│   pc: 4451
-│   callDepth: 0
-│   statusCode: STATUSCODE:StatusCode
-│
-│  (797 steps)
-├─ 7
-│   k: CALL ( VGAS:Int +Int -10173 ) 645326474426547203313410069153905908525362434349 0 ...
+│   k: CALL VGAS:Int 645326474426547203313410069153905908525362434349 0 388 100 388 0 ~ ...
 │   pc: 3785
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
 │  (1 step)
-├─ 8
+├─ 7
 │   k: #checkCall 728815563385977040452943777879061427756277306518 0 ~> #call 728815563 ...
 │   pc: 3785
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
-│  (387 steps)
-├─ 9
+│  (241 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 (leaf, terminal)
+└─ 10 (leaf, terminal)
     k: #halt ~> CONTINUATION:K
     pc: 281
     callDepth: 0
@@ -76,7 +69,7 @@
 │   statusCode: STATUSCODE_FINAL:StatusCode
 
 
-Node 11:
+Node 10:
 
 ( <generatedTop>
   <foundry>
@@ -91,6 +84,9 @@ Node 11:
       <schedule>
         SHANGHAI
       </schedule>
+      <useGas>
+        false
+      </useGas>
       <ethereum>
         <evm>
           <output>
@@ -125,11 +121,8 @@ Node 11:
               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>
-              17
+              0
             </memoryUsed>
-            <callGas>
-              #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -10173 ) , ( VGAS:Int +Int -10173 ) , 100 ) )
-            </callGas>
             <static>
               false
             </static>
@@ -146,7 +139,7 @@ Node 11:
               SetItem ( 645326474426547203313410069153905908525362434349 )
             </accessedAccounts>
             <accessedStorage>
-              ( 728815563385977040452943777879061427756277306518 |-> SetItem ( 7 ) )
+              .Map
             </accessedStorage>
             ...
           </substate>
@@ -297,7 +290,7 @@ Node 11:
     rule [BASIC-BLOCK-1-TO-3]: <foundry>
            <kevm>
              <k>
-               ( .K => STATICCALL ( VGAS:Int +Int -3061 ) 645326474426547203313410069153905908525362434349 128 36 128 0
+               ( .K => STATICCALL VGAS:Int 645326474426547203313410069153905908525362434349 128 36 128 0
                ~> #pc [ STATICCALL ] )
                ~> #execute
                ~> _CONTINUATION
@@ -308,6 +301,9 @@ Node 11:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <callStack>
@@ -340,24 +336,22 @@ Node 11:
                    ...
                    ...
                    <memoryUsed>
-                     ( 0 => 6 )
+                     0
                    </memoryUsed>
-                   <callGas>
-                     ( _CALLGAS_CELL => #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3061 ) , ( VGAS:Int +Int -3061 ) , 100 ) ) )
-                   </callGas>
                    <static>
                      false
                    </static>
                    <callDepth>
                      0
                    </callDepth>
+                   ...
                  </callState>
                  <substate>
                    <log>
                      .List
                    </log>
                    <accessedAccounts>
-                     ( .Set => SetItem ( 645326474426547203313410069153905908525362434349 ) )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -505,7 +499,7 @@ Node 11:
     rule [BASIC-BLOCK-3-TO-4]: <foundry>
            <kevm>
              <k>
-               ( STATICCALL ( VGAS:Int +Int -3061 ) 645326474426547203313410069153905908525362434349 128 36 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0
+               ( STATICCALL VGAS:Int 645326474426547203313410069153905908525362434349 128 36 128 0 => #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 ]
@@ -518,6 +512,9 @@ Node 11:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <callStack>
@@ -550,24 +547,22 @@ Node 11:
                    ...
                    ...
                    <memoryUsed>
-                     6
+                     0
                    </memoryUsed>
-                   <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3061 ) , ( VGAS:Int +Int -3061 ) , 100 ) )
-                   </callGas>
                    <static>
                      false
                    </static>
                    <callDepth>
                      0
                    </callDepth>
+                   ...
                  </callState>
                  <substate>
                    <log>
                      .List
                    </log>
                    <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -718,9 +713,9 @@ Node 11:
                ( #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 ] => #gas [ ISZERO , ISZERO 1 ]
+               ~> ISZERO 1
+               ~> #pc [ ISZERO ] )
                ~> #execute
                ~> _CONTINUATION
              </k>
@@ -730,6 +725,9 @@ Node 11:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -757,32 +755,30 @@ Node 11:
                      0
                    </callValue>
                    <wordStack>
-                     ( ( 164 => 128 ) : ( ( selector ( "assume(bool)" ) => 645326474426547203313410069153905908525362434349 ) : ( ( 645326474426547203313410069153905908525362434349 => 594 ) : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( ( 280 => 594 ) : ( ( selector ( "test_assume_false(uint256,uint256)" ) => VV1_b_114b9705:Int ) : ( .WordStack => ( VV0_a_114b9705:Int : ( 280 : ( selector ( "test_assume_false(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) ) ) )
+                     ( ( 164 => 64 ) : ( ( selector ( "assume(bool)" ) => 160 ) : ( ( 645326474426547203313410069153905908525362434349 => 292 ) : ( ( VV1_b_114b9705:Int => 96 ) : ( ( VV0_a_114b9705:Int => 4586 ) : ( ( 280 => 96 ) : ( ( selector ( "test_assume_false(uint256,uint256)" ) => 0 ) : ( .WordStack => ( 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 ( "test_assume_false(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 -3061 ) , ( VGAS:Int +Int -3061 ) , 100 ) )
-                   </callGas>
                    <static>
                      false
                    </static>
                    <callDepth>
                      0
                    </callDepth>
+                   ...
                  </callState>
                  <substate>
                    <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>
                    <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -933,9 +929,10 @@ Node 11:
     rule [BASIC-BLOCK-5-TO-6]: <foundry>
            <kevm>
              <k>
-               ( #gas [ MSTORE , MSTORE 192 46308022326495007027972728677917914892729792999299745830475596687180801507328 ]
-               ~> MSTORE 192 46308022326495007027972728677917914892729792999299745830475596687180801507328
-               ~> #pc [ MSTORE ] => #next [ DUP ( 2 ) ] )
+               ( #gas [ ISZERO , ISZERO 1 ]
+               ~> ISZERO 1
+               ~> #pc [ ISZERO ] => CALL VGAS:Int 645326474426547203313410069153905908525362434349 0 388 100 388 0
+               ~> #pc [ CALL ] )
                ~> #execute
                ~> _CONTINUATION
              </k>
@@ -945,6 +942,9 @@ Node 11:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -972,32 +972,30 @@ Node 11:
                      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 ( "test_assume_false(uint256,uint256)" ) => VV1_b_114b9705:Int ) : ( .WordStack => ( VV0_a_114b9705:Int : ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 280 : ( selector ( "test_assume_false(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
+                     ( ( 64 => 488 ) : ( ( 160 => 645326474426547203313410069153905908525362434349 ) : ( ( 292 => 0 ) : ( ( 96 => 594 ) : ( ( 4586 => VV1_b_114b9705:Int ) : ( ( 96 => VV0_a_114b9705:Int ) : ( ( 0 => 594 ) : ( ( 288 => VV1_b_114b9705:Int ) : ( ( 128 => VV0_a_114b9705:Int ) : ( ( 51016057639858100040180367130768047423658391221723556551037572491782395555780 => 280 ) : ( ( 3745 => selector ( "test_assume_false(uint256,uint256)" ) ) : ( ( 645326474426547203313410069153905908525362434349 : ( 0 : ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 280 : ( selector ( "test_assume_false(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 -3061 ) , ( VGAS:Int +Int -3061 ) , 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 )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -1147,220 +1145,7 @@ Node 11:
     rule [BASIC-BLOCK-6-TO-7]: <foundry>
            <kevm>
              <k>
-               ( #next [ DUP ( 2 ) ] => CALL ( VGAS:Int +Int -10173 ) 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"\xe4\x1b\xef\xb4" +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 ( "test_assume_false(uint256,uint256)" ) ) : ( ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 280 : ( selector ( "test_assume_false(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 ( -3061 => -10173 ) ) , ( VGAS:Int +Int ( -3061 => -10173 ) ) , 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 -10173 ) 645326474426547203313410069153905908525362434349 0 388 100 388 0 => #checkCall 728815563385977040452943777879061427756277306518 0
+               ( CALL VGAS:Int 645326474426547203313410069153905908525362434349 0 388 100 388 0 => #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 ]
@@ -1373,6 +1158,9 @@ Node 11:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1408,24 +1196,22 @@ Node 11:
                    ...
                    ...
                    <memoryUsed>
-                     17
+                     0
                    </memoryUsed>
-                   <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -10173 ) , ( VGAS:Int +Int -10173 ) , 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 )
+                     .Set
                    </accessedAccounts>
                    <accessedStorage>
                      .Map
@@ -1570,9 +1356,9 @@ Node 11:
        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
@@ -1589,6 +1375,9 @@ Node 11:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1624,27 +1413,25 @@ Node 11:
                    ...
                    ...
                    <memoryUsed>
-                     17
+                     0
                    </memoryUsed>
-                   <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -10173 ) , ( VGAS:Int +Int -10173 ) , 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 )
+                     ( .Set => SetItem ( 645326474426547203313410069153905908525362434349 ) )
                    </accessedAccounts>
                    <accessedStorage>
-                     ( .Map => ( 728815563385977040452943777879061427756277306518 |-> SetItem ( 7 ) ) )
+                     .Map
                    </accessedStorage>
                    ...
                  </substate>
@@ -1786,9 +1573,9 @@ Node 11:
        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 )
@@ -1802,6 +1589,9 @@ Node 11:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -1840,17 +1630,15 @@ Node 11:
                    ...
                    ...
                    <memoryUsed>
-                     17
+                     0
                    </memoryUsed>
-                   <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -10173 ) , ( VGAS:Int +Int -10173 ) , 100 ) )
-                   </callGas>
                    <static>
                      false
                    </static>
                    <callDepth>
                      0
                    </callDepth>
+                   ...
                  </callState>
                  <substate>
                    <log>
@@ -1860,7 +1648,7 @@ Node 11:
                      SetItem ( 645326474426547203313410069153905908525362434349 )
                    </accessedAccounts>
                    <accessedStorage>
-                     ( 728815563385977040452943777879061427756277306518 |-> SetItem ( 7 ) )
+                     .Map
                    </accessedStorage>
                    ...
                  </substate>
@@ -2002,9 +1790,9 @@ Node 11:
        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
@@ -2018,6 +1806,9 @@ Node 11:
              <schedule>
                SHANGHAI
              </schedule>
+             <useGas>
+               false
+             </useGas>
              <ethereum>
                <evm>
                  <output>
@@ -2056,17 +1847,15 @@ Node 11:
                    ...
                    ...
                    <memoryUsed>
-                     17
+                     0
                    </memoryUsed>
-                   <callGas>
-                     #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -10173 ) , ( VGAS:Int +Int -10173 ) , 100 ) )
-                   </callGas>
                    <static>
                      false
                    </static>
                    <callDepth>
                      0
                    </callDepth>
+                   ...
                  </callState>
                  <substate>
                    <log>
@@ -2076,7 +1865,7 @@ Node 11:
                      SetItem ( 645326474426547203313410069153905908525362434349 )
                    </accessedAccounts>
                    <accessedStorage>
-                     ( 728815563385977040452943777879061427756277306518 |-> SetItem ( 7 ) )
+                     .Map
                    </accessedStorage>
                    ...
                  </substate>
@@ -2218,14 +2007,14 @@ Node 11:
        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
 1 Failure nodes. (0 pending and 1 failing)
 
 Failing nodes:
 
-  Node id: 11
+  Node id: 10
   Failure reason:
     Implication check failed, the following is the remaining implication:
     ( ( { true #Equals 0 <=Int CALLER_ID:Int }
diff --git a/src/tests/integration/test_foundry_prove.py b/src/tests/integration/test_foundry_prove.py
index 52bf0aad8..eb88d799a 100644
--- a/src/tests/integration/test_foundry_prove.py
+++ b/src/tests/integration/test_foundry_prove.py
@@ -121,6 +121,7 @@ def assert_or_update_k_output(k_file: Path, expected_file: Path, *, update: bool
 ALL_PROVE_TESTS: Final = tuple((TEST_DATA_DIR / 'foundry-prove-all').read_text().splitlines())
 SKIPPED_PROVE_TESTS: Final = set((TEST_DATA_DIR / 'foundry-prove-skip').read_text().splitlines())
 SKIPPED_LEGACY_TESTS: Final = set((TEST_DATA_DIR / 'foundry-prove-skip-legacy').read_text().splitlines())
+GAS_TESTS: Final = set((TEST_DATA_DIR / 'foundry-prove-with-gas').read_text().splitlines())
 
 SHOW_TESTS = set((TEST_DATA_DIR / 'foundry-show').read_text().splitlines())
 
@@ -141,14 +142,13 @@ def test_foundry_prove(
     ):
         pytest.skip()
 
+    prove_options = ProveOptions(counterexample_info=True, bug_report=bug_report, use_gas=test_id in GAS_TESTS)
+
     # When
     prove_res = foundry_prove(
         foundry,
         tests=[(test_id, None)],
-        prove_options=ProveOptions(
-            counterexample_info=True,
-            bug_report=bug_report,
-        ),
+        prove_options=prove_options,
         rpc_options=RPCOptions(
             port=server.port,
         ),
@@ -329,6 +329,7 @@ def test_foundry_auto_abstraction(
         prove_options=ProveOptions(
             auto_abstract_gas=True,
             bug_report=bug_report,
+            use_gas=True,
         ),
         rpc_options=RPCOptions(
             port=server.port,