cterm/cterm: do not include identity substiutions in CSubst.pred

runtimeverification · Sep 6, 2024 · 8757594 · 8757594
1 parent 5d00f3c
commit 8757594
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/pyk/src/pyk/cterm/cterm.py b/pyk/src/pyk/cterm/cterm.py
@@ -323,7 +323,7 @@ def pred(self, sort_with: KDefinition | None = None, subst: bool = True, constra
         """Return an ML predicate representing this substitution."""
         _preds: list[KInner] = []
         if subst:
-            for k, v in self.subst.items():
+            for k, v in self.subst.minimize().items():
                 sort = K if not (sort_with and sort_with.sort(v)) else not_none(sort_with.sort(v))
                 _preds.append(mlEquals(KVariable(k, sort=sort), v, arg_sort=sort))
         if constraints:

diff --git a/pyk/src/tests/unit/test_cterm.py b/pyk/src/tests/unit/test_cterm.py
@@ -192,6 +192,7 @@ def test_from_kast(test_id: str, kast: KInner, expected: CTerm) -> None:
 ML_PRED_TEST_DATA: Final = (
     ('empty', CSubst(Subst({})), mlTop()),
     ('singleton', CSubst(Subst({'X': TRUE})), mlEquals(KVariable('X', sort=K), TRUE, arg_sort=K)),
+    ('identity', CSubst(Subst({'X': KVariable('X')})), mlTop()),
     (
         'double',
         CSubst(Subst({'X': TRUE, 'Y': intToken(4)})),