From 58a101d279efb64e7042bab2968a22f27a9e2706 Mon Sep 17 00:00:00 2001 From: Sam Balco Date: Wed, 1 Nov 2023 15:03:30 +0000 Subject: [PATCH] revert last commit --- kore/src/Kore/Rewrite/SMT/Evaluator.hs | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/kore/src/Kore/Rewrite/SMT/Evaluator.hs b/kore/src/Kore/Rewrite/SMT/Evaluator.hs index 40f31ec12e..103a9cacb2 100644 --- a/kore/src/Kore/Rewrite/SMT/Evaluator.hs +++ b/kore/src/Kore/Rewrite/SMT/Evaluator.hs @@ -92,8 +92,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. @@ -188,7 +186,7 @@ decidePredicate onUnknown sideCondition predicates = & runMaybeT where query :: MaybeT Simplifier Result - query = onErrorUnknown $ SMT.withSolver . evalTranslator $ do + query = SMT.withSolver . evalTranslator $ do tools <- Simplifier.askMetadataTools Morph.hoist SMT.liftSMT $ do predicates' <- @@ -198,9 +196,6 @@ 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