fix: bv_decide benchmarks

tests/bench/bv_decide_inequality.lean

@@ -28,26 +28,24 @@ 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 →
     (0#64 < addr + 1#64 - addr ∧ 0#64 < addr + 1#64 + n - addr)
     ∧ 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 →
     b2 - b1 = 18446744073709551615#64 ∨ c2 - b1 ≤ b2 - b1 ∧ c1 - b1 ≤ c2 - b1 →
     ((a2 - a1 < c1 - a1 ∧ a2 - a1 < c2 - a1)
     ∧ c2 - c1 < a1 - c1)
     ∧ c2 - c1 < a2 - c1 := by
-  bv_decide
+  bv_decide (config := { timeout := 120 })

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 })