refactor a better way for as_rules

runtimeverification · Aug 27, 2024 · de9cb1f · de9cb1f
1 parent 4c44997
commit de9cb1f
Showing 1 changed file with 7 additions and 2 deletions.
diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py
@@ -26,7 +26,7 @@
     from pathlib import Path
     from typing import Any, Final, TypeVar
 
-    from ..kast.outer import KClaim, KDefinition, KFlatModuleList
+    from ..kast.outer import KClaim, KDefinition, KFlatModuleList, KRuleLike
     from ..kcfg import KCFGExplore
     from ..kcfg.explore import KCFGExtendResult
     from ..kcfg.kcfg import CSubst, NodeIdLike
@@ -444,7 +444,12 @@ def as_rules(self, priority: int = 20, direct_rule: bool = False) -> list[KRule]
             or (self.admitted and not self.kcfg.predecessors(self.target))
         ):
             return [self.as_rule(priority=priority)]
-        return [rule for rule in self.kcfg.to_rules(self.rule_id, priority=priority) if isinstance(rule, KRule)]
+
+        def _return_rule(r: KRuleLike) -> KRule:
+            assert isinstance(r, KRule)
+            return r
+
+        return [_return_rule(rule) for rule in self.kcfg.to_rules(self.rule_id, priority=priority)]
 
     def as_rule(self, priority: int = 20) -> KRule:
         _edge = KCFG.Edge(self.kcfg.node(self.init), self.kcfg.node(self.target), depth=0, rules=())