From deb68707d2498fc992e7ba7958b118b582700b41 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 28 May 2024 02:04:45 +0200 Subject: [PATCH] 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 40c912bf769b3bf7cfae8552e0faf698ac727920. Co-authored-by: rv-jenkins --- kore/src/Kore/Rewrite/SMT/Evaluator.hs | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/kore/src/Kore/Rewrite/SMT/Evaluator.hs b/kore/src/Kore/Rewrite/SMT/Evaluator.hs index 87afc8aef8..df714b656c 100644 --- 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