Merge remote-tracking branch 'origin/develop'

runtimeverification · Feb 3, 2025 · 7798d97 · 7798d97
2 parents 54b7a9c + db556c8
commit 7798d97
Showing 1 changed file with 3 additions and 1 deletion.
diff --git 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