Catch IOError when a query times out and retry correctly (#3692)

This (hopefully) fixes
runtimeverification/k#3729, specifially the
error below, thrown
[here](https://github.com/runtimeverification/haskell-backend/blob/58a101d279efb64e7042bab2968a22f27a9e2706/kore/src/SMT/SimpleSMT.hs#L444-L450)
```
kore-exec: [41516716] Error (ErrorException):
    user error (Unexpected result from the SMT solver:
      Command: (push 1 )
      Expected: success
      Result: (error "line 178 column 8: push canceled" )
    )
```

This error occurs when smt-limit is low and we send an assert query to
the solver. When this happens, we want to re-try instead of letting the
error bubble up, as it currently does.

I have tested this and confirmed that at a threshold level of
`smt-timeout` where Z3 fails intermittently, with this change, we re-try
the specified number of times before failing fully.

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
@@ -186,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' <-
@@ -196,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