Make WarnDecidePredicateUnknown an error (#1939)

* Redo everything

* Add renamed module

* Stylish

Author: andreiburdusa

kore/src/Kore/Log/WarnDecidePredicateUnknown.hs renamed to kore/src/Kore/Log/ErrorDecidePredicateUnknown.hs

@@ -4,9 +4,9 @@ License     : NCSA
 
 -}
 
-module Kore.Log.WarnDecidePredicateUnknown
-    ( WarnDecidePredicateUnknown (..)
-    , warnDecidePredicateUnknown
+module Kore.Log.ErrorDecidePredicateUnknown
+    ( ErrorDecidePredicateUnknown (..)
+    , errorDecidePredicateUnknown
     ) where
 
 import Prelude.Kore
@@ -27,14 +27,14 @@ import Pretty
     )
 import qualified Pretty
 
-newtype WarnDecidePredicateUnknown =
-    WarnDecidePredicateUnknown
+newtype ErrorDecidePredicateUnknown =
+    ErrorDecidePredicateUnknown
         { predicates :: NonEmpty (Predicate VariableName)
         }
     deriving (Show)
 
-instance Pretty WarnDecidePredicateUnknown where
-    pretty WarnDecidePredicateUnknown { predicates } =
+instance Pretty ErrorDecidePredicateUnknown where
+    pretty ErrorDecidePredicateUnknown { predicates } =
         Pretty.vsep
         ( ["Failed to decide predicate:", Pretty.indent 4 (unparse predicate)]
         ++ do
@@ -44,16 +44,17 @@ instance Pretty WarnDecidePredicateUnknown where
       where
        predicate :| sideConditions = predicates
 
-instance Entry WarnDecidePredicateUnknown where
-    entrySeverity _ = Warning
-    helpDoc _ = "warn when the solver cannot decide satisfiability of a formula"
+instance Entry ErrorDecidePredicateUnknown where
+    entrySeverity _ = Error
+    helpDoc _ =
+        "errors raised when the solver cannot decide satisfiability of a formula"
 
-warnDecidePredicateUnknown
+errorDecidePredicateUnknown
     :: MonadLog log
     => InternalVariable variable
     => NonEmpty (Predicate variable)
     -> log ()
-warnDecidePredicateUnknown predicates' =
-    logEntry WarnDecidePredicateUnknown { predicates }
+errorDecidePredicateUnknown predicates' =
+    logEntry ErrorDecidePredicateUnknown { predicates }
   where
     predicates = Predicate.mapVariables (pure toVariableName) <$> predicates'

kore/src/Kore/Log/Registry.hs

@@ -65,6 +65,9 @@ import Kore.Log.DebugUnification
 import Kore.Log.ErrorBottomTotalFunction
     ( ErrorBottomTotalFunction
     )
+import Kore.Log.ErrorDecidePredicateUnknown
+    ( ErrorDecidePredicateUnknown
+    )
 import Kore.Log.ErrorException
     ( ErrorException
     )
@@ -80,9 +83,6 @@ import Kore.Log.InfoAttemptUnification
 import Kore.Log.InfoReachability
     ( InfoReachability
     )
-import Kore.Log.WarnDecidePredicateUnknown
-    ( WarnDecidePredicateUnknown
-    )
 import Kore.Log.WarnFunctionWithoutEvaluators
     ( WarnFunctionWithoutEvaluators
     )
@@ -132,7 +132,7 @@ entryHelpDocs :: [Pretty.Doc ()]
     , mk $ Proxy @DebugAppliedRewriteRules
     , mk $ Proxy @DebugSubstitutionSimplifier
     , mk $ Proxy @ErrorBottomTotalFunction
-    , mk $ Proxy @WarnDecidePredicateUnknown
+    , mk $ Proxy @ErrorDecidePredicateUnknown
     , mk $ Proxy @WarnFunctionWithoutEvaluators
     , mk $ Proxy @WarnSymbolSMTRepresentation
     , mk $ Proxy @DebugEvaluateCondition

kore/src/Kore/Step/SMT/Evaluator.hs

@@ -66,8 +66,8 @@ import Kore.Log.DebugEvaluateCondition
     ( debugEvaluateConditionResult
     , whileDebugEvaluateCondition
     )
-import Kore.Log.WarnDecidePredicateUnknown
-    ( warnDecidePredicateUnknown
+import Kore.Log.ErrorDecidePredicateUnknown
+    ( errorDecidePredicateUnknown
     )
 import qualified Kore.Profiler.Profile as Profile
     ( smtDecision
@@ -191,7 +191,7 @@ decidePredicate predicates =
             Unsat -> return False
             Sat -> empty
             Unknown -> do
-                warnDecidePredicateUnknown predicates
+                errorDecidePredicateUnknown predicates
                 empty
 
 translatePredicate