Merge remote-tracking branch 'origin/master' into georgy-retry-smt-in-booster

Author: geo2a

booster/library/Booster/Pattern/Rewrite.hs

@@ -361,10 +361,10 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu
             failRewrite $
                 RuleConditionUnclear rule . coerce . foldl1 AndTerm $
                     map coerce unclearRequires
-
     case mbSolver of
         Just solver -> do
-            checkAllRequires <- SMT.checkPredicates solver prior mempty (Set.fromList unclearRequires)
+            checkAllRequires <-
+                SMT.checkPredicates solver prior mempty (Set.fromList unclearRequires)
 
             case checkAllRequires of
                 Left SMT.SMTSolverUnknown{} ->

booster/library/Booster/SMT/Interface.hs

@@ -57,9 +57,6 @@ throwSMT = throw . GeneralSMTError
 throwSMT' :: String -> a
 throwSMT' = throwSMT . pack
 
-throwUnknown :: Text -> Set Predicate -> Set Predicate -> a
-throwUnknown reason premises preds = throw $ SMTSolverUnknown reason premises preds
-
 smtTranslateError :: Text -> a
 smtTranslateError = throw . SMTTranslationError
 
@@ -401,7 +398,7 @@ checkPredicates ctxt givenPs givenSubst psToCheck
     failBecauseUnknown :: ExceptT SMTError (SMT io) (Maybe Bool)
     failBecauseUnknown =
         smtRun GetReasonUnknown >>= \case
-            ReasonUnknown reason -> throwUnknown reason givenPs psToCheck
+            ReasonUnknown reason -> throwE $ SMTSolverUnknown reason givenPs psToCheck
             other -> throwSMT' $ "Unexpected result while calling ':reason-unknown': " <> show other
 
     interactWihtSolver ::