add mlEqualsTrue

runtimeverification · Dec 3, 2024 · 5784068 · 5784068
1 parent d2c69f4
commit 5784068
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
@@ -151,7 +151,7 @@ def custom_step(self, cterm: CTerm) -> KCFGExtendResult | None:
             print('snd', snd_term)
             print('operator', operator)
             assert type(operator) is KToken
-            eq = KApply(_operators[int(operator.token)],fst_term, snd_term)
+            eq = mlEqualsTrue( KApply(_operators[int(operator.token)],fst_term, snd_term))
             print('kapply',eq)
             print('cterms', cterm.constraints)
             print(eq in cterm.constraints)