Update merge-nodes to function for non-leaf nodes (#444)

* Update merge-nodes to function for non-leaf nodes * Set Version: 0.1.200 * Add suggested change Co-authored-by: Everett Hildenbrandt <[email protected]> * Set Version: 0.1.201 * Update expected output * Set Version: 0.1.202 * Reduce iterations for faster execution * Set Version: 0.1.203 * Set Version: 0.1.204 --------- Co-authored-by: devops <[email protected]> Co-authored-by: Everett Hildenbrandt <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
runtimeverification · Mar 14, 2024 · 3af182c · 3af182c
1 parent ab19284
commit 3af182c
Show file tree

Hide file tree

Showing 6 changed files with 2,781 additions and 4 deletions.
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.203
+0.1.204
diff --git a/pyproject.toml b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.203"
+version = "0.1.204"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git 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.203'
+VERSION: Final = '0.1.204'
diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
@@ -915,7 +915,12 @@ def check_cells_equal(cell: str, nodes: Iterable[KCFG.Node]) -> bool:
         anti_unification, _, _ = anti_unification.anti_unify(node.cterm, keep_values=True, kdef=foundry.kevm.definition)
     new_node = apr_proof.kcfg.create_node(anti_unification)
     for node in nodes:
-        apr_proof.kcfg.create_cover(node.id, new_node.id)
+        succ = apr_proof.kcfg.successors(node.id)
+        if len(succ) == 0:
+            apr_proof.kcfg.create_cover(node.id, new_node.id)
+        else:
+            apr_proof.prune(node.id, keep_nodes=[node.id])
+            apr_proof.kcfg.create_cover(node.id, new_node.id)
 
     apr_proof.write_proof_data()