Fix

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

@@ -171,6 +171,8 @@ decidePredicate onUnknown sideCondition predicates =
             debugEvaluateConditionResult result
             case result of
                 Unsat -> do
+                    return False
+                Sat -> do
                     heuristicResult <- queryWithHeuristic predicates
                     case heuristicResult of
                         Unsat -> return False
@@ -186,7 +188,6 @@ decidePredicate onUnknown sideCondition predicates =
                                     SMT.reinit
                                 _ -> pure ()
                             empty
-                Sat -> empty
                 Unknown -> do
                     limit <- SMT.withSolver SMT.askRetryLimit
                     -- depending on the value of `onUnknown`, this call will either log a warning
@@ -228,7 +229,7 @@ decidePredicate onUnknown sideCondition predicates =
                             preds'
                     traverse_ SMT.assert predicates'
                     SMT.check
-        hoistMaybe (find SimpleSMT.isSat results)
+        hoistMaybe (find SimpleSMT.isUnSat results)
 
     applyHeuristic :: Predicate variable -> LogicT m (Predicate variable)
     applyHeuristic (Predicate.PredicateNot (Predicate.PredicateExists var child)) = do

kore/src/SMT/SimpleSMT.hs

@@ -61,7 +61,7 @@ module SMT.SimpleSMT (
     assert,
     check,
     Result (..),
-    isSat,
+    isUnSat,
     getExprs,
     getExpr,
     getConsts,
@@ -261,9 +261,9 @@ data Result
       Unknown
     deriving stock (Eq, Show)
 
-isSat :: Result -> Bool
-isSat Sat = True
-isSat _ = False
+isUnSat :: Result -> Bool
+isUnSat Sat = True
+isUnSat _ = False
 
 -- | Common values returned by SMT solvers.
 data Value