From c3436bafff8ae1e5b5a66ea178f5a9ff076c44b2 Mon Sep 17 00:00:00 2001
From: Georgy Lukyanov <georgiylukjanov@gmail.com>
Date: Thu, 11 Jan 2024 16:24:47 +0100
Subject: [PATCH] Assume definedness of current configuration in HB when
 falling back  (#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 https://github.com/runtimeverification/haskell-backend/pull/3705).

---------

Co-authored-by: Jost Berthold <jost.berthold@runtimeverification.com>
---
 tools/booster/Proxy.hs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tools/booster/Proxy.hs b/tools/booster/Proxy.hs
index 07d1d9f31..bb0c50ed2 100644
--- a/tools/booster/Proxy.hs
+++ b/tools/booster/Proxy.hs
@@ -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