diff --git a/kore/src/Kore/Rewrite/SMT/Evaluator.hs b/kore/src/Kore/Rewrite/SMT/Evaluator.hs index 103a9cacb2..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 @@ -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