diff --git a/deps/k_release b/deps/k_release
index f889afac18..c6a0785c7b 100644
--- a/deps/k_release
+++ b/deps/k_release
@@ -1 +1 @@
-6.0.67
+6.0.69
diff --git a/deps/pyk_release b/deps/pyk_release
index 6187db8f0b..1a64f848ce 100644
--- a/deps/pyk_release
+++ b/deps/pyk_release
@@ -1 +1 @@
-v0.1.425
+v0.1.431
diff --git a/flake.lock b/flake.lock
index 88a3a02a3c..d1002dc07a 100644
--- a/flake.lock
+++ b/flake.lock
@@ -547,11 +547,11 @@
         "systems": "systems_2"
       },
       "locked": {
-        "lastModified": 1689068808,
-        "narHash": "sha256-6ixXo3wt24N/melDWjq70UuHQLxGV8jZvooRanIHXw0=",
+        "lastModified": 1692799911,
+        "narHash": "sha256-3eihraek4qL744EvQXsK1Ha6C3CR7nnT8X2qWap4RNk=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "919d646de7be200f3bf08cb76ae1f09402b6f9b4",
+        "rev": "f9e7cf818399d17d347f847525c5a5a8032e4e44",
         "type": "github"
       },
       "original": {
@@ -1076,16 +1076,16 @@
         "rv-utils": "rv-utils"
       },
       "locked": {
-        "lastModified": 1692732310,
-        "narHash": "sha256-gcBd/kMS8XDSB148ttYpUxvSk+361Fx4+knc3ZQU3wk=",
+        "lastModified": 1692817190,
+        "narHash": "sha256-rwMLR1F4U+m6XbxO3KQ2Y1EUqQC0EtOBCBnHmO7CvKE=",
         "owner": "runtimeverification",
         "repo": "k",
-        "rev": "9045d43f9a900e79eeb5303e88d009fc371db464",
+        "rev": "645ffc4d6e3c34de3d85574a93604c9507af222e",
         "type": "github"
       },
       "original": {
         "owner": "runtimeverification",
-        "ref": "v6.0.67",
+        "ref": "v6.0.69",
         "repo": "k",
         "type": "github"
       }
@@ -1139,11 +1139,11 @@
         "utils": "utils_2"
       },
       "locked": {
-        "lastModified": 1692267154,
-        "narHash": "sha256-8jeSucCQ/1XPlDBIEfXcy+OHNXn/bVeY0ux8uWTqe3M=",
+        "lastModified": 1692815027,
+        "narHash": "sha256-oydxYW0oLxlmEsohMWg0IEryob9R1VCLmpbMRwKhdIg=",
         "owner": "runtimeverification",
         "repo": "llvm-backend",
-        "rev": "7a964b819d16e7b651f581271798b40d152cb2d6",
+        "rev": "2cd7199d67842439504e26776efab88f719e6e41",
         "type": "github"
       },
       "original": {
@@ -1735,16 +1735,16 @@
         "poetry2nix": "poetry2nix"
       },
       "locked": {
-        "lastModified": 1692801807,
-        "narHash": "sha256-4UwTosCoYspT9Jww3L+gQW4GChv4spJSkGtP7BP2hp0=",
+        "lastModified": 1693330087,
+        "narHash": "sha256-gHc4wrk0nw070fYlJoup5scKM3Wx0I5NFp5RHi0T820=",
         "owner": "runtimeverification",
         "repo": "pyk",
-        "rev": "c292c4610183acec2ae44d8f68973ebf3cb4cd1e",
+        "rev": "a18d76df9419194acf1f9d159d8fa697e0471bd9",
         "type": "github"
       },
       "original": {
         "owner": "runtimeverification",
-        "ref": "v0.1.425",
+        "ref": "v0.1.431",
         "repo": "pyk",
         "type": "github"
       }
@@ -1863,11 +1863,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1692863432,
-        "narHash": "sha256-IKDrCwbSY7+9wQkRlH31UygyXSpSeo44DqraBh2UeLo=",
+        "lastModified": 1692871473,
+        "narHash": "sha256-2eLQOPBzQomQfcC8wQdYekccvl1KtYCqkDdw7oPeOiU=",
         "owner": "hellwolf",
         "repo": "solc.nix",
-        "rev": "d87ead250023a730633f30620dec95d97b9b3e7f",
+        "rev": "fbbe5553a7fc52f2d423afac81316023a183e72c",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index 42fbd9b6d0..f18aea326c 100644
--- a/flake.nix
+++ b/flake.nix
@@ -3,7 +3,7 @@
 
   inputs = {
     nixpkgs.url = "github:NixOS/nixpkgs/b01f185e4866de7c5b5a82f833ca9ea3c3f72fc4";
-    k-framework.url = "github:runtimeverification/k/v6.0.67";
+    k-framework.url = "github:runtimeverification/k/v6.0.69";
     k-framework.inputs.nixpkgs.follows = "nixpkgs";
     #nixpkgs.follows = "k-framework/nixpkgs";
     flake-utils.follows = "k-framework/flake-utils";
@@ -17,7 +17,7 @@
     ethereum-legacytests.url = "github:ethereum/legacytests/d7abc42a7b352a7b44b1f66b58aca54e4af6a9d7";
     ethereum-legacytests.flake = false;
     haskell-backend.follows = "k-framework/haskell-backend";
-    pyk.url = "github:runtimeverification/pyk/v0.1.425";
+    pyk.url = "github:runtimeverification/pyk/v0.1.431";
     pyk.inputs.flake-utils.follows = "k-framework/flake-utils";
     pyk.inputs.nixpkgs.follows = "k-framework/nixpkgs";
     foundry.url = "github:shazow/foundry.nix/monthly"; # Use monthly branch for permanent releases
diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock
index 95a0f083fb..3d8857bf0c 100644
--- a/kevm-pyk/poetry.lock
+++ b/kevm-pyk/poetry.lock
@@ -1,10 +1,9 @@
-# This file is automatically @generated by Poetry 1.4.2 and should not be changed by hand.
+# This file is automatically @generated by Poetry 1.6.1 and should not be changed by hand.
 
 [[package]]
 name = "attrs"
 version = "23.1.0"
 description = "Classes Without Boilerplate"
-category = "main"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -23,7 +22,6 @@ tests-no-zope = ["cloudpickle", "hypothesis", "mypy (>=1.1.1)", "pympler", "pyte
 name = "autoflake"
 version = "2.2.0"
 description = "Removes unused imports and unused variables"
-category = "dev"
 optional = false
 python-versions = ">=3.8"
 files = [
@@ -39,7 +37,6 @@ tomli = {version = ">=2.0.1", markers = "python_version < \"3.11\""}
 name = "black"
 version = "23.7.0"
 description = "The uncompromising code formatter."
-category = "dev"
 optional = false
 python-versions = ">=3.8"
 files = [
@@ -85,7 +82,6 @@ uvloop = ["uvloop (>=0.15.2)"]
 name = "classify-imports"
 version = "4.2.0"
 description = "Utilities for refactoring imports in python-like syntax."
-category = "dev"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -97,7 +93,6 @@ files = [
 name = "click"
 version = "8.1.7"
 description = "Composable command line interface toolkit"
-category = "dev"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -112,7 +107,6 @@ colorama = {version = "*", markers = "platform_system == \"Windows\""}
 name = "cmd2"
 version = "2.4.3"
 description = "cmd2 - quickly build feature-rich and user-friendly interactive command line applications in Python"
-category = "main"
 optional = false
 python-versions = ">=3.6"
 files = [
@@ -135,7 +129,6 @@ validate = ["flake8", "mypy", "types-pkg-resources"]
 name = "colorama"
 version = "0.4.6"
 description = "Cross-platform colored terminal text."
-category = "dev"
 optional = false
 python-versions = "!=3.0.*,!=3.1.*,!=3.2.*,!=3.3.*,!=3.4.*,!=3.5.*,!=3.6.*,>=2.7"
 files = [
@@ -147,7 +140,6 @@ files = [
 name = "coloredlogs"
 version = "15.0.1"
 description = "Colored terminal output for Python's logging module"
-category = "main"
 optional = false
 python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*, !=3.4.*"
 files = [
@@ -165,7 +157,6 @@ cron = ["capturer (>=2.4)"]
 name = "coverage"
 version = "7.3.0"
 description = "Code coverage measurement for Python"
-category = "dev"
 optional = false
 python-versions = ">=3.8"
 files = [
@@ -233,7 +224,6 @@ toml = ["tomli"]
 name = "dill"
 version = "0.3.7"
 description = "serialize all of Python"
-category = "main"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -248,7 +238,6 @@ graph = ["objgraph (>=1.7.2)"]
 name = "exceptiongroup"
 version = "1.1.3"
 description = "Backport of PEP 654 (exception groups)"
-category = "dev"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -263,7 +252,6 @@ test = ["pytest (>=6)"]
 name = "execnet"
 version = "2.0.2"
 description = "execnet: rapid multi-Python deployment"
-category = "dev"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -276,25 +264,26 @@ testing = ["hatch", "pre-commit", "pytest", "tox"]
 
 [[package]]
 name = "filelock"
-version = "3.12.2"
+version = "3.12.3"
 description = "A platform independent file lock."
-category = "main"
 optional = false
-python-versions = ">=3.7"
+python-versions = ">=3.8"
 files = [
-    {file = "filelock-3.12.2-py3-none-any.whl", hash = "sha256:cbb791cdea2a72f23da6ac5b5269ab0a0d161e9ef0100e653b69049a7706d1ec"},
-    {file = "filelock-3.12.2.tar.gz", hash = "sha256:002740518d8aa59a26b0c76e10fb8c6e15eae825d34b6fdf670333fd7b938d81"},
+    {file = "filelock-3.12.3-py3-none-any.whl", hash = "sha256:f067e40ccc40f2b48395a80fcbd4728262fab54e232e090a4063ab804179efeb"},
+    {file = "filelock-3.12.3.tar.gz", hash = "sha256:0ecc1dd2ec4672a10c8550a8182f1bd0c0a5088470ecd5a125e45f49472fac3d"},
 ]
 
+[package.dependencies]
+typing-extensions = {version = ">=4.7.1", markers = "python_version < \"3.11\""}
+
 [package.extras]
-docs = ["furo (>=2023.5.20)", "sphinx (>=7.0.1)", "sphinx-autodoc-typehints (>=1.23,!=1.23.4)"]
-testing = ["covdefaults (>=2.3)", "coverage (>=7.2.7)", "diff-cover (>=7.5)", "pytest (>=7.3.1)", "pytest-cov (>=4.1)", "pytest-mock (>=3.10)", "pytest-timeout (>=2.1)"]
+docs = ["furo (>=2023.7.26)", "sphinx (>=7.1.2)", "sphinx-autodoc-typehints (>=1.24)"]
+testing = ["covdefaults (>=2.3)", "coverage (>=7.3)", "diff-cover (>=7.7)", "pytest (>=7.4)", "pytest-cov (>=4.1)", "pytest-mock (>=3.11.1)", "pytest-timeout (>=2.1)"]
 
 [[package]]
 name = "flake8"
 version = "6.1.0"
 description = "the modular source code checker: pep8 pyflakes and co"
-category = "dev"
 optional = false
 python-versions = ">=3.8.1"
 files = [
@@ -311,7 +300,6 @@ pyflakes = ">=3.1.0,<3.2.0"
 name = "flake8-bugbear"
 version = "23.7.10"
 description = "A plugin for flake8 finding likely bugs and design problems in your program. Contains warnings that don't belong in pyflakes and pycodestyle."
-category = "dev"
 optional = false
 python-versions = ">=3.8.1"
 files = [
@@ -330,7 +318,6 @@ dev = ["coverage", "hypothesis", "hypothesmith (>=0.2)", "pre-commit", "pytest",
 name = "flake8-comprehensions"
 version = "3.14.0"
 description = "A flake8 plugin to help you write better list/set/dict comprehensions."
-category = "dev"
 optional = false
 python-versions = ">=3.8"
 files = [
@@ -345,7 +332,6 @@ flake8 = ">=3.0,<3.2.0 || >3.2.0"
 name = "flake8-quotes"
 version = "3.3.2"
 description = "Flake8 lint for quotes."
-category = "dev"
 optional = false
 python-versions = "*"
 files = [
@@ -359,7 +345,6 @@ flake8 = "*"
 name = "flake8-type-checking"
 version = "2.4.1"
 description = "A flake8 plugin for managing type-checking imports & forward references"
-category = "dev"
 optional = false
 python-versions = ">=3.8"
 files = [
@@ -375,7 +360,6 @@ flake8 = "*"
 name = "graphviz"
 version = "0.20.1"
 description = "Simple Python interface for Graphviz"
-category = "main"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -392,7 +376,6 @@ test = ["coverage", "mock (>=4)", "pytest (>=7)", "pytest-cov", "pytest-mock (>=
 name = "humanfriendly"
 version = "10.0"
 description = "Human friendly output for text interfaces using Python"
-category = "main"
 optional = false
 python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*, !=3.4.*"
 files = [
@@ -407,7 +390,6 @@ pyreadline3 = {version = "*", markers = "sys_platform == \"win32\" and python_ve
 name = "importlib-metadata"
 version = "6.8.0"
 description = "Read metadata from Python packages"
-category = "main"
 optional = false
 python-versions = ">=3.8"
 files = [
@@ -427,7 +409,6 @@ testing = ["flufl.flake8", "importlib-resources (>=1.3)", "packaging", "pyfakefs
 name = "iniconfig"
 version = "2.0.0"
 description = "brain-dead simple config-ini parsing"
-category = "dev"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -439,7 +420,6 @@ files = [
 name = "isort"
 version = "5.12.0"
 description = "A Python utility / library to sort Python imports."
-category = "dev"
 optional = false
 python-versions = ">=3.8.0"
 files = [
@@ -457,7 +437,6 @@ requirements-deprecated-finder = ["pip-api", "pipreqs"]
 name = "linkify-it-py"
 version = "2.0.2"
 description = "Links recognition library with FULL unicode support."
-category = "main"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -478,7 +457,6 @@ test = ["coverage", "pytest", "pytest-cov"]
 name = "markdown-it-py"
 version = "2.2.0"
 description = "Python port of markdown-it. Markdown parsing, done right!"
-category = "main"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -505,7 +483,6 @@ testing = ["coverage", "pytest", "pytest-cov", "pytest-regressions"]
 name = "mccabe"
 version = "0.7.0"
 description = "McCabe checker, plugin for flake8"
-category = "dev"
 optional = false
 python-versions = ">=3.6"
 files = [
@@ -517,7 +494,6 @@ files = [
 name = "mdit-py-plugins"
 version = "0.4.0"
 description = "Collection of plugins for markdown-it-py"
-category = "main"
 optional = false
 python-versions = ">=3.8"
 files = [
@@ -537,7 +513,6 @@ testing = ["coverage", "pytest", "pytest-cov", "pytest-regressions"]
 name = "mdurl"
 version = "0.1.2"
 description = "Markdown URL utilities"
-category = "main"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -549,7 +524,6 @@ files = [
 name = "multiprocess"
 version = "0.70.15"
 description = "better multiprocessing and multithreading in Python"
-category = "main"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -578,7 +552,6 @@ dill = ">=0.3.7"
 name = "mypy"
 version = "1.5.1"
 description = "Optional static typing for Python"
-category = "dev"
 optional = false
 python-versions = ">=3.8"
 files = [
@@ -625,7 +598,6 @@ reports = ["lxml"]
 name = "mypy-extensions"
 version = "1.0.0"
 description = "Type system extensions for programs checked with the mypy type checker."
-category = "dev"
 optional = false
 python-versions = ">=3.5"
 files = [
@@ -637,7 +609,6 @@ files = [
 name = "packaging"
 version = "23.1"
 description = "Core utilities for Python packages"
-category = "dev"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -649,7 +620,6 @@ files = [
 name = "pathos"
 version = "0.3.1"
 description = "parallel graph management and execution in heterogeneous computing"
-category = "main"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -667,7 +637,6 @@ ppft = ">=1.7.6.7"
 name = "pathspec"
 version = "0.11.2"
 description = "Utility library for gitignore style pattern matching of file paths."
-category = "dev"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -679,7 +648,6 @@ files = [
 name = "pep8-naming"
 version = "0.13.3"
 description = "Check PEP-8 naming conventions, plugin for flake8"
-category = "dev"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -694,7 +662,6 @@ flake8 = ">=5.0.0"
 name = "platformdirs"
 version = "3.10.0"
 description = "A small Python package for determining appropriate platform-specific dirs, e.g. a \"user data dir\"."
-category = "dev"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -710,7 +677,6 @@ test = ["appdirs (==1.4.4)", "covdefaults (>=2.3)", "pytest (>=7.4)", "pytest-co
 name = "pluggy"
 version = "1.3.0"
 description = "plugin and hook calling mechanisms for python"
-category = "dev"
 optional = false
 python-versions = ">=3.8"
 files = [
@@ -726,7 +692,6 @@ testing = ["pytest", "pytest-benchmark"]
 name = "pox"
 version = "0.3.3"
 description = "utilities for filesystem exploration and automated builds"
-category = "main"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -738,7 +703,6 @@ files = [
 name = "ppft"
 version = "1.7.6.7"
 description = "distributed and parallel Python"
-category = "main"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -753,7 +717,6 @@ dill = ["dill (>=0.3.7)"]
 name = "psutil"
 version = "5.9.5"
 description = "Cross-platform lib for process and system monitoring in Python."
-category = "main"
 optional = false
 python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*"
 files = [
@@ -780,7 +743,6 @@ test = ["enum34", "ipaddress", "mock", "pywin32", "wmi"]
 name = "pybind11"
 version = "2.11.1"
 description = "Seamless operability between C++11 and Python"
-category = "main"
 optional = false
 python-versions = ">=3.6"
 files = [
@@ -795,7 +757,6 @@ global = ["pybind11-global (==2.11.1)"]
 name = "pycodestyle"
 version = "2.11.0"
 description = "Python style guide checker"
-category = "dev"
 optional = false
 python-versions = ">=3.8"
 files = [
@@ -807,7 +768,6 @@ files = [
 name = "pyflakes"
 version = "3.1.0"
 description = "passive checker of Python programs"
-category = "dev"
 optional = false
 python-versions = ">=3.8"
 files = [
@@ -819,7 +779,6 @@ files = [
 name = "pygments"
 version = "2.16.1"
 description = "Pygments is a syntax highlighting package written in Python."
-category = "main"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -832,9 +791,8 @@ plugins = ["importlib-metadata"]
 
 [[package]]
 name = "pyk"
-version = "0.1.425"
+version = "0.1.431"
 description = ""
-category = "main"
 optional = false
 python-versions = "^3.10"
 files = []
@@ -853,14 +811,13 @@ tomli = "^2.0.1"
 [package.source]
 type = "git"
 url = "https://github.com/runtimeverification/pyk.git"
-reference = "v0.1.425"
-resolved_reference = "c292c4610183acec2ae44d8f68973ebf3cb4cd1e"
+reference = "v0.1.431"
+resolved_reference = "a18d76df9419194acf1f9d159d8fa697e0471bd9"
 
 [[package]]
 name = "pyperclip"
 version = "1.8.2"
 description = "A cross-platform clipboard module for Python. (Only handles plain text for now.)"
-category = "main"
 optional = false
 python-versions = "*"
 files = [
@@ -871,7 +828,6 @@ files = [
 name = "pyreadline3"
 version = "3.4.1"
 description = "A python implementation of GNU readline."
-category = "main"
 optional = false
 python-versions = "*"
 files = [
@@ -883,7 +839,6 @@ files = [
 name = "pytest"
 version = "7.4.0"
 description = "pytest: simple powerful testing with Python"
-category = "dev"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -906,7 +861,6 @@ testing = ["argcomplete", "attrs (>=19.2.0)", "hypothesis (>=3.56)", "mock", "no
 name = "pytest-cov"
 version = "4.1.0"
 description = "Pytest plugin for measuring coverage."
-category = "dev"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -925,7 +879,6 @@ testing = ["fields", "hunter", "process-tests", "pytest-xdist", "six", "virtuale
 name = "pytest-mock"
 version = "3.11.1"
 description = "Thin-wrapper around the mock package for easier use with pytest"
-category = "dev"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -943,7 +896,6 @@ dev = ["pre-commit", "pytest-asyncio", "tox"]
 name = "pytest-xdist"
 version = "3.3.1"
 description = "pytest xdist plugin for distributed testing, most importantly across multiple CPUs"
-category = "dev"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -964,7 +916,6 @@ testing = ["filelock"]
 name = "pyupgrade"
 version = "3.10.1"
 description = "A tool to automatically upgrade syntax for newer versions."
-category = "dev"
 optional = false
 python-versions = ">=3.8.1"
 files = [
@@ -979,7 +930,6 @@ tokenize-rt = ">=5.2.0"
 name = "rich"
 version = "13.5.2"
 description = "Render rich text, tables, progress bars, syntax highlighting, markdown and more to the terminal"
-category = "main"
 optional = false
 python-versions = ">=3.7.0"
 files = [
@@ -998,7 +948,6 @@ jupyter = ["ipywidgets (>=7.5.1,<9)"]
 name = "textual"
 version = "0.27.0"
 description = "Modern Text User Interface framework"
-category = "main"
 optional = false
 python-versions = ">=3.7,<4.0"
 files = [
@@ -1019,7 +968,6 @@ dev = ["aiohttp (>=3.8.1)", "click (>=8.1.2)", "msgpack (>=1.0.3)"]
 name = "tokenize-rt"
 version = "5.2.0"
 description = "A wrapper around the stdlib `tokenize` which roundtrips."
-category = "dev"
 optional = false
 python-versions = ">=3.8"
 files = [
@@ -1031,7 +979,6 @@ files = [
 name = "tomli"
 version = "2.0.1"
 description = "A lil' TOML parser"
-category = "main"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -1043,7 +990,6 @@ files = [
 name = "tomlkit"
 version = "0.11.8"
 description = "Style preserving TOML library"
-category = "main"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -1055,7 +1001,6 @@ files = [
 name = "typing-extensions"
 version = "4.7.1"
 description = "Backported and Experimental Type Hints for Python 3.7+"
-category = "main"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -1067,7 +1012,6 @@ files = [
 name = "uc-micro-py"
 version = "1.0.2"
 description = "Micro subset of unicode data files for linkify-it-py projects."
-category = "main"
 optional = false
 python-versions = ">=3.7"
 files = [
@@ -1082,7 +1026,6 @@ test = ["coverage", "pytest", "pytest-cov"]
 name = "wcwidth"
 version = "0.2.6"
 description = "Measures the displayed width of unicode strings in a terminal"
-category = "main"
 optional = false
 python-versions = "*"
 files = [
@@ -1094,7 +1037,6 @@ files = [
 name = "zipp"
 version = "3.16.2"
 description = "Backport of pathlib-compatible object wrapper for zip files"
-category = "main"
 optional = false
 python-versions = ">=3.8"
 files = [
@@ -1109,4 +1051,4 @@ testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "p
 [metadata]
 lock-version = "2.0"
 python-versions = "^3.10"
-content-hash = "7a6eba6fae9c636c5f96e42d56b7f5cf5033f59481f4dd9e0344e3efe231b03b"
+content-hash = "52c02013a3aa448f371fadb4d9e4c27249a355e1591b7257fe9af57e44e0a524"
diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
index e0db37e984..1ff05c2d4e 100644
--- a/kevm-pyk/pyproject.toml
+++ b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.284"
+version = "1.0.285"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
@@ -17,7 +17,7 @@ packages = [
 [tool.poetry.dependencies]
 python = "^3.10"
 pathos = "*"
-pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.425" }
+pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.431" }
 tomlkit = "^0.11.6"
 
 [tool.poetry.group.dev.dependencies]
diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py
index f3e8b6ba12..35e20011e4 100644
--- a/kevm-pyk/src/kevm_pyk/__main__.py
+++ b/kevm-pyk/src/kevm_pyk/__main__.py
@@ -15,7 +15,7 @@
 from pyk.kore.tools import PrintOutput, kore_print
 from pyk.ktool.kompile import LLVMKompileType
 from pyk.ktool.krun import KRunOutput
-from pyk.prelude.ml import is_bottom, is_top
+from pyk.prelude.ml import is_top, mlOr
 from pyk.proof import APRProof
 from pyk.proof.equality import EqualityProof
 from pyk.proof.show import APRProofShow
@@ -164,8 +164,9 @@ def exec_prove_legacy(
         branching_allowed=branching_allowed,
         haskell_backend_args=haskell_backend_args,
     )
-    print(kevm.pretty_print(final_state))
-    if not is_top(final_state):
+    final_kast = mlOr([state.kast for state in final_state])
+    print(kevm.pretty_print(final_kast))
+    if not is_top(final_kast):
         raise SystemExit(1)
 
 
@@ -277,24 +278,22 @@ def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]:
 
                     if simplify_init:
                         _LOGGER.info(f'Simplifying initial and target node: {claim.label}')
-                        _new_init, _ = kcfg_explore.cterm_simplify(new_init)
-                        _new_target, _ = kcfg_explore.cterm_simplify(new_target)
-                        if is_bottom(_new_init):
+                        new_init, _ = kcfg_explore.cterm_simplify(new_init)
+                        new_target, _ = kcfg_explore.cterm_simplify(new_target)
+                        if CTerm._is_bottom(new_init.kast):
                             raise ValueError(
                                 'Simplifying initial node led to #Bottom, are you sure your LHS is defined?'
                             )
-                        if is_bottom(_new_target):
+                        if CTerm._is_top(new_target.kast):
                             raise ValueError(
                                 'Simplifying target node led to #Bottom, are you sure your RHS is defined?'
                             )
-                        new_init = CTerm.from_kast(_new_init)
-                        new_target = CTerm.from_kast(_new_target)
 
                     kcfg.replace_node(init_node_id, new_init)
                     kcfg.replace_node(target_node_id, new_target)
 
                     proof_problem = APRProof(
-                        claim.label, kcfg, init_node_id, target_node_id, {}, proof_dir=save_directory
+                        claim.label, kcfg, [], init_node_id, target_node_id, {}, proof_dir=save_directory
                     )
 
             passed = kevm_prove(
@@ -374,7 +373,7 @@ def exec_prune_proof(
     )
 
     apr_proof = APRProof.read_proof_data(save_directory, claim.label)
-    node_ids = apr_proof.prune_from(node)
+    node_ids = apr_proof.prune(node)
     _LOGGER.info(f'Pruned nodes: {node_ids}')
     apr_proof.write_proof_data()
 
diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py
index e370cf0edc..e806c4ed64 100644
--- a/kevm-pyk/src/kevm_pyk/kevm.py
+++ b/kevm-pyk/src/kevm_pyk/kevm.py
@@ -195,14 +195,18 @@ class Sorts:
         KEVM_CELL: Final = KSort('KevmCell')
 
     def short_info(self, cterm: CTerm) -> list[str]:
-        k_cell = self.pretty_print(cterm.cell('K_CELL')).replace('\n', ' ')
-        if len(k_cell) > 80:
-            k_cell = k_cell[0:80] + ' ...'
-        k_str = f'k: {k_cell}'
-        ret_strs = [k_str]
-        for cell, name in [('PC_CELL', 'pc'), ('CALLDEPTH_CELL', 'callDepth'), ('STATUSCODE_CELL', 'statusCode')]:
-            if cell in cterm.cells:
-                ret_strs.append(f'{name}: {self.pretty_print(cterm.cell(cell))}')
+        k_cell = cterm.try_cell('K_CELL')
+        if k_cell is not None:
+            pretty_cell = self.pretty_print(k_cell).replace('\n', ' ')
+            if len(pretty_cell) > 80:
+                pretty_cell = pretty_cell[0:80] + ' ...'
+            k_str = f'k: {pretty_cell}'
+            ret_strs = [k_str]
+            for cell, name in [('PC_CELL', 'pc'), ('CALLDEPTH_CELL', 'callDepth'), ('STATUSCODE_CELL', 'statusCode')]:
+                if cell in cterm.cells:
+                    ret_strs.append(f'{name}: {self.pretty_print(cterm.cell(cell))}')
+        else:
+            ret_strs = ['(empty configuration)']
         return ret_strs
 
     @staticmethod
@@ -416,7 +420,7 @@ def prove_legacy(
         max_counterexamples: int | None = None,
         branching_allowed: int | None = None,
         haskell_backend_args: Iterable[str] = (),
-    ) -> KInner:
+    ) -> list[CTerm]:
         md_selector = 'k & ! node'
         args: list[str] = []
         haskell_args: list[str] = []
diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py
index 35a8879b7b..b85f875514 100644
--- a/kevm-pyk/src/kevm_pyk/utils.py
+++ b/kevm-pyk/src/kevm_pyk/utils.py
@@ -174,11 +174,8 @@ def print_failure_info(proof: Proof, kcfg_explore: KCFGExplore, counterexample_i
                 res_lines.append('')
                 res_lines.append(f'  Node id: {str(node.id)}')
 
-                simplified_node, _ = kcfg_explore.cterm_simplify(node.cterm)
-                simplified_target, _ = kcfg_explore.cterm_simplify(target.cterm)
-
-                node_cterm = CTerm.from_kast(simplified_node)
-                target_cterm = CTerm.from_kast(simplified_target)
+                node_cterm, _ = kcfg_explore.cterm_simplify(node.cterm)
+                target_cterm, _ = kcfg_explore.cterm_simplify(target.cterm)
 
                 res_lines.append('  Failure reason:')
                 _, reason = kcfg_explore.implication_failure_reason(node_cterm, target_cterm)
diff --git a/kevm-pyk/src/kontrol/foundry.py b/kevm-pyk/src/kontrol/foundry.py
index 470aa8386a..8fdb8b711b 100644
--- a/kevm-pyk/src/kontrol/foundry.py
+++ b/kevm-pyk/src/kontrol/foundry.py
@@ -264,7 +264,7 @@ def short_info_for_contract(self, contract_name: str, cterm: CTerm) -> list[str]
 
     def custom_view(self, contract_name: str, element: KCFGElem) -> Iterable[str]:
         if type(element) is KCFG.Node:
-            pc_cell = element.cterm.cell('PC_CELL')
+            pc_cell = element.cterm.try_cell('PC_CELL')
             if type(pc_cell) is KToken and pc_cell.sort == INT:
                 return self.solidity_src(contract_name, int(pc_cell.token))
         return ['NO DATA']
@@ -904,7 +904,7 @@ def foundry_remove_node(foundry_root: Path, test: str, node: NodeIdLike, id: str
     foundry = Foundry(foundry_root)
     test_id = foundry.get_test_id(test, id)
     apr_proof = foundry.get_apr_proof(test_id)
-    node_ids = apr_proof.prune_from(node)
+    node_ids = apr_proof.prune(node)
     _LOGGER.info(f'Pruned nodes: {node_ids}')
     apr_proof.write_proof_data()
 
@@ -943,9 +943,9 @@ def foundry_simplify_node(
     ) as kcfg_explore:
         new_term, _ = kcfg_explore.cterm_simplify(cterm)
     if replace:
-        apr_proof.kcfg.replace_node(node, CTerm.from_kast(new_term))
+        apr_proof.kcfg.replace_node(node, new_term)
         apr_proof.write_proof_data()
-    res_term = minimize_term(new_term) if minimize else new_term
+    res_term = minimize_term(new_term.kast) if minimize else new_term.kast
     return foundry.kevm.pretty_print(res_term, unalias=False, sort_collections=sort_collections)
 
 
@@ -961,9 +961,11 @@ def check_cells_equal(cell: str, nodes: Iterable[KCFG.Node]) -> bool:
         nodes = list(nodes)
         if len(nodes) < 2:
             return True
-        cell_value = nodes[0].cterm.cell(cell)
+        cell_value = nodes[0].cterm.try_cell(cell)
+        if cell_value is None:
+            return False
         for node in nodes[1:]:
-            if cell_value != node.cterm.cell(cell):
+            if node.cterm.try_cell(cell) is None or cell_value != node.cterm.cell(cell):
                 return False
         return True
 
@@ -1209,6 +1211,7 @@ def _method_to_apr_proof(
             apr_proof = APRBMCProof(
                 test_id,
                 kcfg,
+                [],
                 init_node_id,
                 target_node_id,
                 {},
@@ -1216,7 +1219,7 @@ def _method_to_apr_proof(
                 proof_dir=save_directory,
             )
         else:
-            apr_proof = APRProof(test_id, kcfg, init_node_id, target_node_id, {}, proof_dir=save_directory)
+            apr_proof = APRProof(test_id, kcfg, [], init_node_id, target_node_id, {}, proof_dir=save_directory)
 
     apr_proof.write_proof_data()
     return apr_proof
@@ -1434,7 +1437,7 @@ def __init__(self, foundry: Foundry, contract_name: str):
 
     def print_node(self, kcfg: KCFG, node: KCFG.Node) -> list[str]:
         ret_strs = super().print_node(kcfg, node)
-        _pc = node.cterm.cell('PC_CELL')
+        _pc = node.cterm.try_cell('PC_CELL')
         if type(_pc) is KToken and _pc.sort == INT:
             srcmap_data = self.foundry.srcmap_data(self.contract_name, int(_pc.token))
             if srcmap_data is not None:
diff --git a/kevm-pyk/src/tests/integration/test-data/gas-abstraction.expected b/kevm-pyk/src/tests/integration/test-data/gas-abstraction.expected
index 53f9095a0d..aef9b60a97 100644
--- a/kevm-pyk/src/tests/integration/test-data/gas-abstraction.expected
+++ b/kevm-pyk/src/tests/integration/test-data/gas-abstraction.expected
@@ -1,9 +1,9 @@
 
 ┌─ 1 (root, init)
-│   k: #execute ~> CONTINUATION:K
+│   k: #execute ~> CONTINUATION
 │   pc: 0
 │   callDepth: 0
-│   statusCode: STATUSCODE:StatusCode
+│   statusCode: STATUSCODE
 │
 │  (511 steps)
 ├─ 3
@@ -92,10 +92,10 @@
 
 
 ┌─ 2 (root, leaf, target)
-│   k: #halt ~> CONTINUATION:K
-│   pc: PC_CELL_5d410f2a:Int
-│   callDepth: CALLDEPTH_CELL_5d410f2a:Int
-│   statusCode: STATUSCODE_FINAL:StatusCode
+│   k: #halt ~> CONTINUATION
+│   pc: PC_CELL_5d410f2a
+│   callDepth: CALLDEPTH_CELL_5d410f2a
+│   statusCode: STATUSCODE_FINAL
 
 
 Node 8:
@@ -407,10 +407,11 @@ Node 8:
     rule [BASIC-BLOCK-1-TO-3]: <foundry>
            <kevm>
              <k>
-               ( .K => CALL 9223372036854772946 645326474426547203313410069153905908525362434349 0 128 4 128 0
-               ~> #pc [ CALL ] )
+               ( #execute
+               ~> CONTINUATION => CALL 9223372036854772946 645326474426547203313410069153905908525362434349 0 128 4 128 0
+               ~> #pc [ CALL ]
                ~> #execute
-               ~> _CONTINUATION
+               ~> CONTINUATION:K )
              </k>
              <mode>
                NORMAL
@@ -433,10 +434,10 @@ Node 8:
                      728815563385977040452943777879061427756277306518
                    </id>
                    <caller>
-                     CALLER_ID:Int
+                     CALLER_ID
                    </caller>
                    <callData>
-                     b"c\xfe\xc36"
+                     ( S2KGasTest . S2KtestInfiniteGas ( ) => b"c\xfe\xc36" )
                    </callData>
                    <callValue>
                      0
@@ -445,7 +446,7 @@ Node 8:
                      ( .WordStack => ( 132 : ( selector ( "infiniteGas()" ) : ( 645326474426547203313410069153905908525362434349 : ( 167 : ( selector ( "testInfiniteGas()" ) : .WordStack ) ) ) ) ) )
                    </wordStack>
                    <localMem>
-                     ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\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\xed\x9fsS\x00\x00\x00\x00\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 => 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\xed\x9fsS\x00\x00\x00\x00\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>
                    ...
                    ...
@@ -475,11 +476,11 @@ Node 8:
                    ...
                  </substate>
                  <origin>
-                   ORIGIN_ID:Int
+                   ORIGIN_ID
                  </origin>
                  <block>
                    <number>
-                     NUMBER_CELL:Int
+                     NUMBER_CELL
                    </number>
                    ...
                  </block>
@@ -568,7 +569,7 @@ Node 8:
                  0
                </expectedValue>
                <expectedData>
-                 b""
+                 ( .Bytes => b"" )
                </expectedData>
                <opcodeType>
                  .OpcodeType
@@ -599,7 +600,19 @@ Node 8:
              </whitelist>
            </cheatcodes>
          </foundry>
-      requires ( 0 <=Int CALLER_ID:Int
+      requires ( 0 <=Int CALLER_ID
+       andBool ( CALLER_ID <Int pow160
+       andBool ( 0 <=Int ORIGIN_ID
+       andBool ( ORIGIN_ID <Int pow160
+       andBool ( 0 <=Int NUMBER_CELL
+       andBool ( NUMBER_CELL <=Int maxSInt256
+       andBool ( lengthBytes ( S2KGasTest . S2KtestInfiniteGas ( ) ) <Int pow128
+       andBool ( 0 <=Int maxSInt64
+       andBool ( maxSInt64 <Int pow256
+       andBool ( 0 <=Int 728815563385977040452943777879061427756277306518
+       andBool ( 728815563385977040452943777879061427756277306518 <Int pow160
+               )))))))))))
+       ensures ( 0 <=Int CALLER_ID:Int
        andBool ( 0 <=Int ORIGIN_ID:Int
        andBool ( 0 <=Int NUMBER_CELL:Int
        andBool ( CALLER_ID:Int <Int pow160
diff --git a/kevm-pyk/src/tests/integration/test_foundry_prove.py b/kevm-pyk/src/tests/integration/test_foundry_prove.py
index ec2a9885c3..bc3cfd348b 100644
--- a/kevm-pyk/src/tests/integration/test_foundry_prove.py
+++ b/kevm-pyk/src/tests/integration/test_foundry_prove.py
@@ -257,6 +257,7 @@ def test_foundry_auto_abstraction(
         tests=[(test_id, None)],
         auto_abstract_gas=True,
         port=server.port,
+        simplify_init=False,
     )
 
     if use_booster:
@@ -278,7 +279,7 @@ def test_foundry_auto_abstraction(
     assert_or_update_show_output(show_res, TEST_DATA_DIR / 'gas-abstraction.expected', update=update_expected_output)
 
 
-def test_foundry_remove_node(foundry_root: Path, update_expected_output: bool) -> None:
+def test_foundry_remove_node(foundry_root: Path, update_expected_output: bool, server: KoreServer) -> None:
     test = 'AssertTest.test_assert_true()'
 
     foundry = Foundry(foundry_root)
@@ -286,8 +287,7 @@ def test_foundry_remove_node(foundry_root: Path, update_expected_output: bool) -
     prove_res = foundry_prove(
         foundry_root,
         tests=[(test, None)],
-        smt_timeout=300,
-        smt_retry_limit=10,
+        port=server.port,
     )
     assert_pass(test, prove_res)
 
@@ -304,8 +304,7 @@ def test_foundry_remove_node(foundry_root: Path, update_expected_output: bool) -
     prove_res = foundry_prove(
         foundry_root,
         tests=[(test, None)],
-        smt_timeout=300,
-        smt_retry_limit=10,
+        port=server.port,
     )
     assert_pass(test, prove_res)
 
diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py
index 34e28c5e6a..46b34f3ed5 100644
--- a/kevm-pyk/src/tests/integration/test_prove.py
+++ b/kevm-pyk/src/tests/integration/test_prove.py
@@ -5,7 +5,7 @@
 from typing import TYPE_CHECKING, NamedTuple
 
 import pytest
-from pyk.prelude.ml import mlTop
+from pyk.cterm import CTerm
 
 from kevm_pyk import config
 from kevm_pyk.__main__ import exec_prove
@@ -301,4 +301,5 @@ def test_legacy_prove(
         log_file.write_text(caplog.text)
 
     # Then
-    assert actual == mlTop('K')
+    assert len(actual) == 1
+    assert CTerm._is_top(actual[0].kast)
diff --git a/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.setUp()/proof.json b/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.setUp()/proof.json
index 95363edf63..a957f62725 100644
--- a/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.setUp()/proof.json
+++ b/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.setUp()/proof.json
@@ -1 +1 @@
-{"id": "AssertTest.setUp:c795c796f72d2e6aaa4d26a190f8855a2d9432cb510e944378ac2cf4cafae346", "subproof_ids": [], "admitted": false, "type": "APRProof", "init": 1, "target": 2, "terminal_nodes": [5], "node_refutations": {}, "circularity": false, "logs": {"3": [], "4": [], "5": []}}
\ No newline at end of file
+{"id": "AssertTest.setUp:c795c796f72d2e6aaa4d26a190f8855a2d9432cb510e944378ac2cf4cafae346", "subproof_ids": [], "admitted": false, "type": "APRProof", "init": 1, "target": 2, "terminal": [5], "node_refutations": {}, "circularity": false, "logs": {"3": [], "4": [], "5": []}}
diff --git a/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.testFail_assert_false():0/proof.json b/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.testFail_assert_false():0/proof.json
index f79e5c7bb2..7dc3479c4d 100644
--- a/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.testFail_assert_false():0/proof.json
+++ b/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.testFail_assert_false():0/proof.json
@@ -1 +1 @@
-{"id": "AssertTest.testFail_assert_false:b5202d1b3fe2344c79708f9a3a2c67d446fb9d70c920a623ad408a2e224215b1", "subproof_ids": [], "admitted": false, "type": "APRProof", "init": 1, "target": 2, "terminal_nodes": [5], "node_refutations": {}, "circularity": false, "logs": {"3": [], "4": [], "5": []}}
\ No newline at end of file
+{"id": "AssertTest.testFail_assert_false:b5202d1b3fe2344c79708f9a3a2c67d446fb9d70c920a623ad408a2e224215b1", "subproof_ids": [], "admitted": false, "type": "APRProof", "init": 1, "target": 2, "terminal": [5], "node_refutations": {}, "circularity": false, "logs": {"3": [], "4": [], "5": []}}
diff --git a/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.testFail_assert_true():0/proof.json b/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.testFail_assert_true():0/proof.json
index 40e2fefa58..faaeead7a2 100644
--- a/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.testFail_assert_true():0/proof.json
+++ b/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.testFail_assert_true():0/proof.json
@@ -1 +1 @@
-{"id": "AssertTest.testFail_assert_true:242f699b1574032456e9e771ae766945b79d19d3ef23d383a5a46634800e924d", "subproof_ids": [], "admitted": false, "type": "APRProof", "init": 1, "target": 2, "terminal_nodes": [5], "node_refutations": {}, "circularity": false, "logs": {"3": [], "4": [], "5": []}}
\ No newline at end of file
+{"id": "AssertTest.testFail_assert_true:242f699b1574032456e9e771ae766945b79d19d3ef23d383a5a46634800e924d", "subproof_ids": [], "admitted": false, "type": "APRProof", "init": 1, "target": 2, "terminal": [5], "node_refutations": {}, "circularity": false, "logs": {"3": [], "4": [], "5": []}}
diff --git a/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.test_assert_false():0/proof.json b/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.test_assert_false():0/proof.json
index f04a3664c5..b6d6caef50 100644
--- a/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.test_assert_false():0/proof.json
+++ b/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.test_assert_false():0/proof.json
@@ -1 +1 @@
-{"id": "AssertTest.test_assert_false:6cbc877ca7d55dff8601da29b45e21f589afa4bb6200a47e7de1e24a74ee755c", "subproof_ids": [], "admitted": false, "type": "APRProof", "init": 1, "target": 2, "terminal_nodes": [5], "node_refutations": {}, "circularity": false, "logs": {"3": [], "4": [], "5": []}}
\ No newline at end of file
+{"id": "AssertTest.test_assert_false:6cbc877ca7d55dff8601da29b45e21f589afa4bb6200a47e7de1e24a74ee755c", "subproof_ids": [], "admitted": false, "type": "APRProof", "init": 1, "target": 2, "terminal": [5], "node_refutations": {}, "circularity": false, "logs": {"3": [], "4": [], "5": []}}
diff --git a/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.test_assert_true():0/proof.json b/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.test_assert_true():0/proof.json
index 34574cf2e5..f3945dab6d 100644
--- a/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.test_assert_true():0/proof.json
+++ b/kevm-pyk/src/tests/unit/test-data/foundry-list/apr_proofs/AssertTest.test_assert_true():0/proof.json
@@ -1 +1 @@
-{"id": "AssertTest.test_assert_true:49ed4957b0e11abe41ead027d5e5e0895d082b39dfa5694297dd0e87741d6a49", "subproof_ids": [], "admitted": false, "type": "APRProof", "init": 1, "target": 2, "terminal_nodes": [5], "node_refutations": {}, "circularity": false, "logs": {"3": [], "4": [], "5": []}}
\ No newline at end of file
+{"id": "AssertTest.test_assert_true:49ed4957b0e11abe41ead027d5e5e0895d082b39dfa5694297dd0e87741d6a49", "subproof_ids": [], "admitted": false, "type": "APRProof", "init": 1, "target": 2, "terminal": [5], "node_refutations": {}, "circularity": false, "logs": {"3": [], "4": [], "5": []}}
diff --git a/package/debian/changelog b/package/debian/changelog
index 4c841274ad..38a60b153d 100644
--- a/package/debian/changelog
+++ b/package/debian/changelog
@@ -1,4 +1,4 @@
-kevm (1.0.284) unstable; urgency=medium
+kevm (1.0.285) unstable; urgency=medium
 
   * Initial Release.
 
diff --git a/package/version b/package/version
index e9034ea560..cff7ecca0a 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-1.0.284
+1.0.285