From f3b9af31536e08155d69cf1ad373f7f9da2582ae Mon Sep 17 00:00:00 2001
From: Sam Balco <goodlyrottenapple@gmail.com>
Date: Wed, 1 Nov 2023 14:51:27 +0000
Subject: [PATCH 1/2] Catch IOError when a query times out and retry correctly

---
 kore/src/Kore/Rewrite/SMT/Evaluator.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/kore/src/Kore/Rewrite/SMT/Evaluator.hs b/kore/src/Kore/Rewrite/SMT/Evaluator.hs
index 40f31ec12e..ec082655c5 100644
--- a/kore/src/Kore/Rewrite/SMT/Evaluator.hs
+++ b/kore/src/Kore/Rewrite/SMT/Evaluator.hs
@@ -19,7 +19,9 @@ import Control.Error (
     MaybeT (..),
     runMaybeT,
  )
+import Control.Exception (IOException)
 import Control.Lens qualified as Lens
+import Control.Monad.Catch qualified as Exception
 import Control.Monad.Counter qualified as Counter
 import Control.Monad.Morph qualified as Morph
 import Control.Monad.State.Strict qualified as State
@@ -92,8 +94,6 @@ import SMT (
  )
 import SMT qualified
 import SMT.SimpleSMT qualified as SimpleSMT
-import Control.Monad.Catch qualified as Exception
-import Control.Exception (IOException)
 
 {- | Attempt to evaluate the 'Predicate' argument with an optional side
  condition using an external SMT solver.

From 281d02128f6f4b669743c055a50abc4833b5d798 Mon Sep 17 00:00:00 2001
From: Sam Balco <goodlyrottenapple@gmail.com>
Date: Wed, 1 Nov 2023 15:07:05 +0000
Subject: [PATCH 2/2] Catch IOError when a query times out and retry correctly

---
 kore/src/Kore/Rewrite/SMT/Evaluator.hs | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/kore/src/Kore/Rewrite/SMT/Evaluator.hs b/kore/src/Kore/Rewrite/SMT/Evaluator.hs
index 3e7f79e425..ec082655c5 100644
--- a/kore/src/Kore/Rewrite/SMT/Evaluator.hs
+++ b/kore/src/Kore/Rewrite/SMT/Evaluator.hs
@@ -188,7 +188,7 @@ decidePredicate onUnknown sideCondition predicates =
             & runMaybeT
   where
     query :: MaybeT Simplifier Result
-    query = SMT.withSolver . evalTranslator $ do
+    query = onErrorUnknown $ SMT.withSolver . evalTranslator $ do
         tools <- Simplifier.askMetadataTools
         Morph.hoist SMT.liftSMT $ do
             predicates' <-
@@ -198,6 +198,9 @@ decidePredicate onUnknown sideCondition predicates =
             traverse_ SMT.assert predicates'
             SMT.check >>= maybe empty return
 
+    onErrorUnknown action =
+        action `Exception.catch` \(_ :: IOException) -> pure Unknown
+
     retry = retryWithScaledTimeout $ query <* debugRetrySolverQuery predicates
 
 retryWithScaledTimeout :: MonadSMT m => m Result -> m Result