Skip to content

Commit 0d98bc9

Browse files
Prune #Bottom states when branching (#3650)
Fix for change introduced by #3637, wherein branching could contain bottom states which were not being pruned. (see runtimeverification/pyk#634 (comment))
1 parent 1da6c43 commit 0d98bc9

File tree

2 files changed

+10
-4
lines changed

2 files changed

+10
-4
lines changed

cabal.project.freeze

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@ constraints: any.Cabal ==3.6.3.0,
1111
aeson -cffi +ordered-keymap,
1212
any.aeson-pretty ==0.8.9,
1313
aeson-pretty -lib-only,
14-
any.alex ==3.2.7.4,
1514
any.ansi-terminal ==0.11.4,
1615
ansi-terminal -example +win32-2-13-1,
1716
any.ansi-wl-pprint ==0.6.9,
@@ -109,7 +108,6 @@ constraints: any.Cabal ==3.6.3.0,
109108
any.gitrev ==1.3.1,
110109
any.graphviz ==2999.20.1.0,
111110
graphviz -test-parsing,
112-
any.happy ==1.20.1.1,
113111
any.hashable ==1.4.2.0,
114112
hashable +integer-gmp -random-initial-seed,
115113
any.hashtables ==1.3.1,

kore/src/Kore/Exec.hs

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -557,8 +557,16 @@ rpcExec
557557
Rewritten _ -> GraphTraversal.Continuing next'
558558
Remaining _ -> GraphTraversal.Stuck next'
559559
Kore.Rewrite.Bottom -> GraphTraversal.Vacuous prior
560-
toTransitionResult prior (s : ss) =
561-
GraphTraversal.Branch prior $ fmap fst (s :| ss)
560+
toTransitionResult prior rs =
561+
case filter
562+
( \(RpcExecState{rpcProgState}, _) -> case rpcProgState of
563+
Kore.Rewrite.Bottom -> False
564+
_ -> True
565+
)
566+
rs of
567+
(s : ss) -> GraphTraversal.Branch prior $ fmap fst (s :| ss)
568+
-- either empty or single result
569+
other -> toTransitionResult prior other
562570

563571
setTraces ::
564572
Seq (RewriteRule v, Seq SimplifierTrace) -> Seq RuleTrace -> RpcExecState v -> RpcExecState v

0 commit comments

Comments
 (0)