Skip to content

Commit

Permalink
revert last commit
Browse files Browse the repository at this point in the history
  • Loading branch information
goodlyrottenapple committed Nov 1, 2023
1 parent b541e4e commit 58a101d
Showing 1 changed file with 1 addition and 6 deletions.
7 changes: 1 addition & 6 deletions kore/src/Kore/Rewrite/SMT/Evaluator.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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' <-
Expand All @@ -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
Expand Down

0 comments on commit 58a101d

Please sign in to comment.