Revert "Do not retry SMT query when WarnDecidePredicateUnknown" (#3901)

Some `kasmer` proof rely heavily on simplifications and start failing when we stop applying them. This reverts commit 40c912b. Co-authored-by: rv-jenkins <[email protected]>
runtimeverification · May 28, 2024 · deb6870 · deb6870
1 parent 912cbe6
commit deb6870
Showing 1 changed file with 1 addition and 5 deletions.
diff --git a/kore/src/Kore/Rewrite/SMT/Evaluator.hs b/kore/src/Kore/Rewrite/SMT/Evaluator.hs
@@ -169,11 +169,7 @@ decidePredicate ::
 decidePredicate onUnknown sideCondition predicates =
     whileDebugEvaluateCondition predicates $
         do
-            result <- case onUnknown of
-                -- do not retry the query on Unknown if the use-case is "soft", i.e. applying simplifications
-                WarnDecidePredicateUnknown _ _ -> query
-                -- if Unknown leads to a hard error, retry the query with scaled timeouts
-                ErrorDecidePredicateUnknown _ _ -> query >>= whenUnknown retry
+            result <- query >>= whenUnknown retry
             debugEvaluateConditionResult result
             case result of
                 Unsat -> return False