From db556c810a1042c1d928b46441324370cf8fb3e1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 3 Feb 2025 18:03:06 +0100 Subject: [PATCH] Generate binders for variables in definedness constraints (#4751) This PR fixes a bug in the generator where a variable is not declared in the signature of a `Rewrites` constructor if it only occurs in a definedness constraint. --- pyk/src/pyk/klean/k2lean4.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/klean/k2lean4.py b/pyk/src/pyk/klean/k2lean4.py index 6fd83cfadf..c7aa03ca18 100644 --- a/pyk/src/pyk/klean/k2lean4.py +++ b/pyk/src/pyk/klean/k2lean4.py @@ -326,7 +326,9 @@ def _rewrite_ctor(self, rule: RewriteRule) -> Ctor: # Step 3: create binders binders: list[Binder] = [] - binders.extend(self._free_binders(pattern)) # Binders of the form {x y : SortInt} + binders.extend( + self._free_binders(And(SortApp('Foo'), (pattern,) + tuple(defs.values()))) + ) # Binders of the form {x y : SortInt} binders.extend(self._def_binders(defs)) # Binders of the form (def_y : foo x = some y) # Step 4: transform patterns