kontrol/foundry: use new CSubst.pred instead of Subst.pred

runtimeverification · Sep 5, 2024 · 523ee6b · 523ee6b
1 parent 028c8ff
commit 523ee6b
Showing 1 changed file with 8 additions and 2 deletions.
diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
@@ -1131,8 +1131,14 @@ def check_cells_equal(cell: str, nodes: Iterable[KCFG.Node]) -> bool:
     anti_unification = nodes[0].cterm
     for node in nodes[1:]:
         anti_unification, csubst1, csubst2 = anti_unification.anti_unify(node.cterm, kdef=foundry.kevm.definition)
-        constraint1 = andBool([csubst1.subst.pred] + list(map(ml_pred_to_bool, csubst1.constraints)))
-        constraint2 = andBool([csubst2.subst.pred] + list(map(ml_pred_to_bool, csubst2.constraints)))
+        constraint1 = andBool(
+            [csubst1.pred(constraints=False, sort_with=foundry.kevm.definition)]
+            + list(map(ml_pred_to_bool, csubst1.constraints))
+        )
+        constraint2 = andBool(
+            [csubst2.pred(constraints=False, sort_with=foundry.kevm.definition)]
+            + list(map(ml_pred_to_bool, csubst2.constraints))
+        )
         anti_unification.add_constraint(mlEqualsTrue(orBool([constraint1, constraint2])))
 
     new_node = apr_proof.kcfg.create_node(anti_unification)