Skip to content
This repository was archived by the owner on Apr 25, 2024. It is now read-only.

Commit 36477fb

Browse files
committed
proof/reachability: remove redundant check for is_covered in pending sets
1 parent 65cbe13 commit 36477fb

1 file changed

Lines changed: 2 additions & 11 deletions

File tree

src/pyk/proof/reachability.py

Lines changed: 2 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -65,11 +65,7 @@ def terminal(self) -> list[KCFG.Node]:
6565

6666
@property
6767
def pending(self) -> list[KCFG.Node]:
68-
return [
69-
nd
70-
for nd in self.kcfg.leaves
71-
if not (self.is_terminal(nd.id) or self.kcfg.is_covered(nd.id) or self.is_target(nd.id))
72-
]
68+
return [nd for nd in self.kcfg.leaves if not (self.is_terminal(nd.id) or self.is_target(nd.id))]
7369

7470
def is_terminal(self, node_id: NodeIdLike) -> bool:
7571
return self.kcfg._resolve(node_id) in (nd.id for nd in self.terminal)
@@ -200,12 +196,7 @@ def pending(self) -> list[KCFG.Node]:
200196
return [
201197
nd
202198
for nd in self.kcfg.leaves
203-
if not (
204-
self.is_terminal(nd.id)
205-
or self.is_bounded(nd.id)
206-
or self.kcfg.is_covered(nd.id)
207-
or self.is_target(nd.id)
208-
)
199+
if not (self.is_terminal(nd.id) or self.is_bounded(nd.id) or self.is_target(nd.id))
209200
]
210201

211202
def is_bounded(self, node_id: NodeIdLike) -> bool:

0 commit comments

Comments
 (0)