Skip to content

Commit 40c912b

Browse files
committed
Do not retry SMT query when WarnDecidePredicateUnknown
1 parent bcbbca6 commit 40c912b

File tree

1 file changed

+5
-1
lines changed

1 file changed

+5
-1
lines changed

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

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -169,7 +169,11 @@ decidePredicate ::
169169
decidePredicate onUnknown sideCondition predicates =
170170
whileDebugEvaluateCondition predicates $
171171
do
172-
result <- query >>= whenUnknown retry
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
173177
debugEvaluateConditionResult result
174178
case result of
175179
Unsat -> return False

0 commit comments

Comments
 (0)