From d12df6c2ad83aa461e34bcb0ef60d27281eb9e87 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sat, 9 Nov 2024 12:18:33 +0100
Subject: [PATCH] fix: bv_decide benchmarks (#6017)

This PR fixes the nightly build after bv_decide changed its options
---
 tests/bench/bv_decide_inequality.lean | 6 ++----
 tests/bench/bv_decide_mod.lean        | 3 +--
 2 files changed, 3 insertions(+), 6 deletions(-)

diff --git a/tests/bench/bv_decide_inequality.lean b/tests/bench/bv_decide_inequality.lean
index 023de494a5f2..5019811af116 100644
--- a/tests/bench/bv_decide_inequality.lean
+++ b/tests/bench/bv_decide_inequality.lean
@@ -28,13 +28,12 @@ example :
     → (0#64 < c - a ∧ 0#64 < d - a) ∧ d - c < a - c := by
   bv_decide
 
-set_option sat.timeout 120 in
 example :
     n < 18446744073709551615#64 - k →
     ((a + k - a < a + k + 1#64 - a ∧ a + k - a < a + k + 1#64 + n - a) ∧
         a + k + 1#64 + n - (a + k + 1#64) < a - (a + k + 1#64)) ∧
       a + k + 1#64 + n - (a + k + 1#64) < a + k - (a + k + 1#64) := by
-  bv_decide
+  bv_decide (config := { timeout := 120 })
 
 example :
     n < 18446744073709551615 →
@@ -42,7 +41,6 @@ example :
     ∧ addr + 1#64 + n - (addr + 1#64) < addr - (addr + 1#64) := by
   bv_decide
 
-set_option sat.timeout 120 in
 example :
     a2 - a1 < b1 - a1 → a2 - a1 < b2 - a1 →
     b2 - b1 < a1 - b1 → b2 - b1 < a2 - b1 →
@@ -50,4 +48,4 @@ example :
     ((a2 - a1 < c1 - a1 ∧ a2 - a1 < c2 - a1)
     ∧ c2 - c1 < a1 - c1)
     ∧ c2 - c1 < a2 - c1 := by
-  bv_decide
+  bv_decide (config := { timeout := 120 })
diff --git a/tests/bench/bv_decide_mod.lean b/tests/bench/bv_decide_mod.lean
index 9792e29e16eb..8a1dd142b137 100644
--- a/tests/bench/bv_decide_mod.lean
+++ b/tests/bench/bv_decide_mod.lean
@@ -32,8 +32,7 @@ def opt (state : BitVec 32) : BitVec 32 :=
 --set_option trace.Meta.Tactic.bv true in
 --set_option trace.Meta.Tactic.sat true in
 --set_option trace.profiler true in
-set_option sat.timeout 120 in
 theorem lehmer_correct (state : BitVec 32) (h1 : state > 0) (h2 : state < 0x7fffffff) :
     naive state = opt state := by
   unfold naive opt
-  bv_decide
+  bv_decide (config := { timeout := 120 })