Skip to content

Commit deb6870

Browse files
geo2arv-jenkins
andauthored
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]>
1 parent 912cbe6 commit deb6870

File tree

1 file changed

+1
-5
lines changed

1 file changed

+1
-5
lines changed

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

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -169,11 +169,7 @@ decidePredicate ::
169169
decidePredicate onUnknown sideCondition predicates =
170170
whileDebugEvaluateCondition predicates $
171171
do
172-
result <- case onUnknown of
173-
-- do not retry the query on Unknown if the use-case is "soft", i.e. applying simplifications
174-
WarnDecidePredicateUnknown _ _ -> query
175-
-- if Unknown leads to a hard error, retry the query with scaled timeouts
176-
ErrorDecidePredicateUnknown _ _ -> query >>= whenUnknown retry
172+
result <- query >>= whenUnknown retry
177173
debugEvaluateConditionResult result
178174
case result of
179175
Unsat -> return False

0 commit comments

Comments
 (0)