diff --git a/deps/kevm_release b/deps/kevm_release index 17237ed68..3683b00b3 100644 --- a/deps/kevm_release +++ b/deps/kevm_release @@ -1 +1 @@ -1.0.763 +1.0.764 diff --git a/flake.lock b/flake.lock index 731c2a6e5..aa8135939 100644 --- a/flake.lock +++ b/flake.lock @@ -435,16 +435,16 @@ ] }, "locked": { - "lastModified": 1734420381, - "narHash": "sha256-Kd0WG5vWW5Lj6263/uVP4AWvRRSf39zeWK9TGW/B3Lo=", + "lastModified": 1734436934, + "narHash": "sha256-NHLy0zJQ2qVuV0tWnbv5hbqSuWhqp89zxYWSa5rJlks=", "owner": "runtimeverification", "repo": "evm-semantics", - "rev": "022eda8085a78c0cb063f382a24885616a21ecf2", + "rev": "a53872bf553c29259b025aeb14d027da16b4fc43", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v1.0.763", + "ref": "v1.0.764", "repo": "evm-semantics", "type": "github" } diff --git a/flake.nix b/flake.nix index 9ef948fd6..62b34e09c 100644 --- a/flake.nix +++ b/flake.nix @@ -2,7 +2,7 @@ description = "Kontrol"; inputs = { - kevm.url = "github:runtimeverification/evm-semantics/v1.0.763"; + kevm.url = "github:runtimeverification/evm-semantics/v1.0.764"; nixpkgs.follows = "kevm/nixpkgs"; k-framework.follows = "kevm/k-framework"; flake-utils.follows = "kevm/flake-utils"; diff --git a/poetry.lock b/poetry.lock index a0acf3318..a6fb22eb3 100644 --- a/poetry.lock +++ b/poetry.lock @@ -707,7 +707,7 @@ colors = ["colorama (>=0.4.6)"] [[package]] name = "kevm-pyk" -version = "1.0.763" +version = "1.0.764" description = "" optional = false python-versions = "^3.10" @@ -722,8 +722,8 @@ tomlkit = "^0.11.6" [package.source] type = "git" url = "https://github.com/runtimeverification/evm-semantics.git" -reference = "v1.0.763" -resolved_reference = "022eda8085a78c0cb063f382a24885616a21ecf2" +reference = "v1.0.764" +resolved_reference = "a53872bf553c29259b025aeb14d027da16b4fc43" subdirectory = "kevm-pyk" [[package]] @@ -1517,4 +1517,4 @@ type = ["pytest-mypy"] [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "30d57aefe9fc1fe2f9e1361483e627f3cc50aac3c73951db44356f70e3740782" +content-hash = "2ff9fc14ea4cf20e1febfe4a2eb6636f6ee68fd5c1eefb637fa5aac830978c82" diff --git a/pyproject.toml b/pyproject.toml index 6000de643..8138d5ac4 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -12,7 +12,7 @@ authors = [ [tool.poetry.dependencies] python = "^3.10" -kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.763", subdirectory = "kevm-pyk" } +kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.764", subdirectory = "kevm-pyk" } eth-utils = "^4.1.1" pycryptodome = "^3.20.0" pyevmasm = "^0.2.3" diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 56ff8f9c2..a9169b5a1 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -475,6 +475,7 @@ def create_kcfg_explore() -> KCFGExplore: maintenance_rate=options.maintenance_rate, assume_defined=options.assume_defined, extra_module=extra_lemmas_module, + optimize_kcfg=options.optimize_kcfg, ) if progress is not None and task is not None: