Skip to content

Commit

Permalink
Catch IOError when a query times out and retry correctly
Browse files Browse the repository at this point in the history
  • Loading branch information
goodlyrottenapple committed Nov 1, 2023
1 parent 1458a72 commit b541e4e
Showing 1 changed file with 6 additions and 1 deletion.
7 changes: 6 additions & 1 deletion kore/src/Kore/Rewrite/SMT/Evaluator.hs
Original file line number Diff line number Diff line change
Expand Up @@ -92,6 +92,8 @@ 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.
Expand Down Expand Up @@ -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' <-
Expand All @@ -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
Expand Down

0 comments on commit b541e4e

Please sign in to comment.