Skip to content

Commit

Permalink
Assume definedness of current configuration in HB when falling back (#…
Browse files Browse the repository at this point in the history
…421)

When falling back to Kore, take advantage of the fact initial rewriting
state is defined, the fact that Booster preserves definiteness and a new
feature in `kore-rpc` that assumes definedness of the execution state
(see runtimeverification/haskell-backend#3705).

---------

Co-authored-by: Jost Berthold <[email protected]>
  • Loading branch information
geo2a and jberthold authored Jan 11, 2024
1 parent beab5ee commit c3436ba
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions tools/booster/Proxy.hs
Original file line number Diff line number Diff line change
Expand Up @@ -277,6 +277,7 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
r
{ state = execStateToKoreJson simplifiedBoosterState
, maxDepth = Just $ Depth 1
, assumeStateDefined = Just True
}
)
when (isJust statsVar) $ do
Expand Down

0 comments on commit c3436ba

Please sign in to comment.