Scale SMT timeout as powers of two

Author: geo2a

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

@@ -206,10 +206,8 @@ decidePredicate onUnknown sideCondition predicates =
 retryWithScaledTimeout :: MonadSMT m => m Result -> m Result
 retryWithScaledTimeout q = do
     SMT.RetryLimit limit <- SMT.askRetryLimit
-    -- Use the same timeout for the first retry, since sometimes z3
-    -- decides it doesn't want to work today and all we need is to
-    -- retry it once.
-    let timeoutScales = takeWithin limit [1 ..]
+    -- the timeout is doubled for every retry
+    let timeoutScales = takeWithin limit . map (2 ^) $ [1 :: Integer ..]
         retryActions = map (retryOnceWithScaledTimeout q) timeoutScales
         combineRetries [] = pure $ Unknown "retry limit is 0"
         combineRetries [r] = r