From eebe4e9fd9dd6c606b37a384dbbfecca85943a38 Mon Sep 17 00:00:00 2001 From: Samuel Balco Date: Thu, 2 Nov 2023 09:50:05 +0000 Subject: [PATCH] Catch IOError when a query times out and retry correctly (#3692) This (hopefully) fixes https://github.com/runtimeverification/k/issues/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 | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) 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