kevm-pyk/{utils,__main__}: KCFG.replace_node returns new node id and preserves cover data

Author: ehildenb

kevm-pyk/src/kevm_pyk/__main__.py

@@ -353,8 +353,8 @@ def _write_cfg(_cfg: KCFG, _cfgpath: Path) -> None:
                 init_term = foundry.simplify(CTerm(init_term))
                 _LOGGER.info(f'Simplifying target state for test: {test}')
                 target_term = foundry.simplify(CTerm(target_term))
-            cfg = KCFG__replace_node(cfg, cfg.get_unique_init().id, CTerm(init_term))
-            cfg = KCFG__replace_node(cfg, cfg.get_unique_target().id, CTerm(target_term))
+            cfg, _ = KCFG__replace_node(cfg, cfg.get_unique_init().id, CTerm(init_term))
+            cfg, _ = KCFG__replace_node(cfg, cfg.get_unique_target().id, CTerm(target_term))
             kcfgs[test] = (cfg, kcfg_file)
             _write_cfg(cfg, kcfg_file)
         else:

kevm-pyk/src/kevm_pyk/utils.py

@@ -1,4 +1,4 @@
-from typing import Collection, Iterable, List
+from typing import Collection, Iterable, List, Tuple
 
 from pyk.cterm import CTerm
 from pyk.kast.inner import KApply, KInner, KRewrite, KVariable
@@ -36,7 +36,7 @@ def _expand_macros(_term: KInner) -> KInner:
     return term
 
 
-def KCFG__replace_node(cfg: KCFG, node_id: str, new_cterm: CTerm) -> KCFG:  # noqa: N802
+def KCFG__replace_node(cfg: KCFG, node_id: str, new_cterm: CTerm) -> Tuple[KCFG, str]:  # noqa: N802
 
     # Remove old node, record data
     node = cfg.node(node_id)
@@ -57,9 +57,9 @@ def KCFG__replace_node(cfg: KCFG, node_id: str, new_cterm: CTerm) -> KCFG:  # no
     for out_edge in out_edges:
         cfg.create_edge(new_node.id, out_edge.target.id, out_edge.condition, out_edge.depth)
     for in_cover in in_covers:
-        cfg.create_cover(in_cover.source.id, new_node.id)
+        cfg.create_cover(in_cover.source.id, new_node.id, subst=in_cover.subst, constraint=in_cover.constraint)
     for out_cover in out_covers:
-        cfg.create_cover(new_node.id, out_cover.target.id)
+        cfg.create_cover(new_node.id, out_cover.target.id, subst=in_cover.subst, constraint=in_cover.constraint)
     if init:
         cfg.add_init(new_node.id)
     if target:
@@ -70,7 +70,7 @@ def KCFG__replace_node(cfg: KCFG, node_id: str, new_cterm: CTerm) -> KCFG:  # no
         if in_expanded[nid]:
             cfg.add_expanded(nid)
 
-    return cfg
+    return (cfg, new_node.id)
 
 
 def KPrint_make_unparsing(_self: KPrint, extra_modules: Iterable[KFlatModule] = ()) -> KPrint:  # noqa: N802