From 416e7fe3ad69af6d642be430714e6701935bc625 Mon Sep 17 00:00:00 2001
From: Ana Pantilie <ana.pantilie95@gmail.com>
Date: Tue, 21 Feb 2023 18:02:39 +0200
Subject: [PATCH] Fix

---
 kore/src/Kore/Rewrite/SMT/Evaluator.hs | 5 +++--
 kore/src/SMT/SimpleSMT.hs              | 8 ++++----
 2 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/kore/src/Kore/Rewrite/SMT/Evaluator.hs b/kore/src/Kore/Rewrite/SMT/Evaluator.hs
index 8292f42a8e..f20414eef6 100644
--- a/kore/src/Kore/Rewrite/SMT/Evaluator.hs
+++ b/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
diff --git a/kore/src/SMT/SimpleSMT.hs b/kore/src/SMT/SimpleSMT.hs
index 8d826b111b..7aff990df8 100644
--- a/kore/src/SMT/SimpleSMT.hs
+++ b/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