diff --git a/Arm/Memory/MemoryProofs.lean b/Arm/Memory/MemoryProofs.lean
index 3d53b9d1..4c743772 100644
--- a/Arm/Memory/MemoryProofs.lean
+++ b/Arm/Memory/MemoryProofs.lean
@@ -7,7 +7,7 @@ import Arm.FromMathlib
 import Arm.State
 import Arm.Memory.Separate
 import Arm.Memory.SeparateProofs
-
+import Tactics.BvOmegaBench
 -- In this file, we have memory (non-)interference proofs.
 
 ----------------------------------------------------------------------
@@ -321,7 +321,7 @@ private theorem mem_subset_neq_first_addr_small_second_region
       omega
     simp only [l1, Nat.lt_irrefl] at h1
   · rename_i h
-    bv_omega
+    bv_omega_bench
     done
 
 private theorem write_mem_bytes_of_write_mem_bytes_shadow_general_n2_lt
@@ -756,7 +756,7 @@ private theorem mem_legal_lemma (h0 : 0 < n) (h1 : n < 2^64)
   revert h0 h1 h2
   have : 2^64 = 18446744073709551616 := by decide
   simp_all [mem_legal]
-  bv_omega
+  bv_omega_bench
 
 private theorem addr_diff_upper_bound_lemma (h0 : 0 < n1) (h1 : n1 ≤ 2 ^ 64)
   (h2 : 0 < n2) (h3 : n2 < 2^64)
@@ -768,7 +768,7 @@ private theorem addr_diff_upper_bound_lemma (h0 : 0 < n1) (h1 : n1 ≤ 2 ^ 64)
   have _ : 2^64 = 18446744073709551616 := by decide
   have _ : 2^64 - 1 = 18446744073709551615 := by decide
   simp_all [mem_subset, mem_legal]
-  bv_omega
+  bv_omega_bench
 
 private theorem read_mem_bytes_of_write_mem_bytes_subset_n2_lt
   (h0 : 0 < n1) (h1 : n1 <= 2^64) (h2 : 0 < n2) (h3 : n2 < 2^64)
@@ -850,7 +850,7 @@ theorem entire_memory_subset_of_only_itself
   have : 2^64 = 18446744073709551616 := by decide
   unfold my_pow at *
   simp_all [mem_subset, BitVec.add_sub_self_left_64]
-  bv_omega
+  bv_omega_bench
 
 theorem entire_memory_subset_legal_regions_eq_addr
   (h1 : mem_subset addr2 (addr2 + (BitVec.ofNat 64 (my_pow 2 64 - 1))) addr1 (addr1 + (BitVec.ofNat 64 (my_pow 2 64 - 1))))
@@ -860,7 +860,7 @@ theorem entire_memory_subset_legal_regions_eq_addr
   have : 2^64-1 = 18446744073709551615 := by decide
   unfold my_pow at *
   simp_all [mem_subset, mem_legal]
-  bv_omega
+  bv_omega_bench
 
 private theorem read_mem_bytes_of_write_mem_bytes_subset_n2_eq_alt
   (h0 : 0 < n1) (h1 : n1 <= my_pow 2 64) (h2 : 0 < n2) (h3 : n2 = my_pow 2 64)
diff --git a/Arm/Memory/Separate.lean b/Arm/Memory/Separate.lean
index a05cc413..99c6bdcc 100644
--- a/Arm/Memory/Separate.lean
+++ b/Arm/Memory/Separate.lean
@@ -5,7 +5,7 @@ Author(s): Shilpi Goel, Siddharth Bhat
 -/
 import Arm.State
 import Arm.BitVec
-
+import Tactics.BvOmegaBench
 section Separate
 
 open BitVec
@@ -137,7 +137,7 @@ theorem lt_or_gt_of_mem_separate_of_mem_legal_of_mem_legal (h : mem_separate a1
   · by_cases h₆ : a1.toNat > b2.toNat
     · simp only  [BitVec.val_bitvec_lt, gt_iff_lt, h₆, or_true]
     · exfalso
-      bv_omega
+      bv_omega_bench
 
 /--
 Given two legal memory regions `[a1, a2]` and `[b1, b2]`,
@@ -153,7 +153,7 @@ theorem mem_separate_of_lt_or_gt_of_mem_legal_of_mem_legal (h : a2 < b1 ∨ a1 >
   unfold mem_legal at ha hb
   simp only [decide_eq_true_eq] at ha hb
   rw [BitVec.le_def] at ha hb
-  bv_omega
+  bv_omega_bench
 
 /--
 Given two legal memory regions `[a1, a2]` and `[b1, b2]`,
@@ -183,7 +183,7 @@ theorem add_lt_of_mem_legal_of_lt
   by_cases hadd : a.toNat + n.toNat < 2^64
   · assumption
   · exfalso
-    bv_omega
+    bv_omega_bench
 
 /--
 If we express a memory region as `[a..(a+n)]` for `(n : Nat)`,
@@ -274,7 +274,7 @@ theorem mem_legal_of_mem_legal' (h : mem_legal' a n) :
   simp only [mem_legal', mem_legal, BitVec.le_def] at h ⊢
   rw [BitVec.toNat_add_eq_toNat_add_toNat]
   simp only [BitVec.toNat_ofNat, Nat.reducePow, Nat.le_add_right, decide_True]
-  bv_omega
+  bv_omega_bench
 
 /--
 Legal in the new sense implies legal in the old sense.
@@ -283,7 +283,7 @@ Note that the subtraction could also have been written as `(b - a).toNat + 1`
 theorem mem_legal'_of_mem_legal (h: mem_legal a b) : mem_legal' a (b.toNat - a.toNat + 1) := by
   simp only [mem_legal, decide_eq_true_eq] at h
   rw [mem_legal']
-  bv_omega
+  bv_omega_bench
 
 def mem_legal'_of_mem_legal'_of_lt (h : mem_legal' a n) (m : Nat) (hm : m ≤ n) :
     mem_legal' a m := by
@@ -304,7 +304,7 @@ theorem mem_legal_iff_mem_legal' : mem_legal a b ↔
   · intros h
     simp only [mem_legal'] at h
     simp only [mem_legal, BitVec.le_def, decide_eq_true_eq]
-    bv_omega
+    bv_omega_bench
 
 /--
 `mem_separate' a an b bn` asserts that two memory regions [a..an) and [b..bn) are separate.
@@ -449,7 +449,7 @@ theorem mem_subset'_refl (h : mem_legal' a an) : mem_subset' a an a an where
 theorem mem_separate'.symm (h : mem_separate' addr₁ n₁ addr₂ n₂) : mem_separate' addr₂ n₂ addr₁ n₁ := by
   have := h.omega_def
   apply mem_separate'.of_omega
-  bv_omega
+  bv_omega_bench
 
 theorem mem_separate'.of_subset'_of_subset'
   (h : mem_separate' addr₁ n₁ addr₂ n₂)
@@ -460,7 +460,7 @@ theorem mem_separate'.of_subset'_of_subset'
   have := h₁.omega_def
   have := h₂.omega_def
   apply mem_separate'.of_omega
-  bv_omega
+  bv_omega_bench
 
 /--
 If `[a'..a'+an')` begins at least where `[a..an)` begins,
@@ -522,8 +522,8 @@ theorem mem_subset_of_mem_subset' (h : mem_subset' a an b bn) (han : an > 0) (hb
   simp only [bitvec_rules, minimal_theory]
   by_cases hb : bn = 2^64
   · left
-    bv_omega
-  · bv_omega
+    bv_omega_bench
+  · bv_omega_bench
 
 /- value of read_mem_bytes when separate from the write. -/
 theorem Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate'
@@ -541,7 +541,7 @@ theorem Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate'
   simp only [decide_True, ite_eq_left_iff, Bool.true_and]
   intros h₁
   intros h₂
-  bv_omega
+  bv_omega_bench
 
 /- value of `read_mem_bytes'` when subset of the write. -/
 theorem Memory.read_bytes_write_bytes_eq_of_mem_subset'
@@ -619,17 +619,17 @@ theorem Memory.read_bytes_eq_extractLsBytes_sub_of_mem_subset'
     have ⟨h1, h2, h3, h4⟩ := hsubset.omega_def
     apply BitVec.eq_of_extractLsByte_eq
     intros i
-    rw [extractLsByte_read_bytes (by bv_omega)]
+    rw [extractLsByte_read_bytes (by bv_omega_bench)]
     rw [BitVec.extractLsByte_extractLsBytes]
     by_cases h : i < an
     · simp only [h, ↓reduceIte]
       apply BitVec.eq_of_getLsbD_eq
       intros j
       rw [← hread]
-      rw [extractLsByte_read_bytes (by bv_omega)]
-      simp only [show a.toNat - b.toNat + i < bn by bv_omega, if_true]
+      rw [extractLsByte_read_bytes (by bv_omega_bench)]
+      simp only [show a.toNat - b.toNat + i < bn by bv_omega_bench, if_true]
       congr 2
-      bv_omega
+      bv_omega_bench
     · simp only [h, ↓reduceIte]
 
 /-- A region of memory, given by (base pointer, length) -/
diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean
index 29ac674c..5efa5763 100644
--- a/Arm/Memory/SeparateAutomation.lean
+++ b/Arm/Memory/SeparateAutomation.lean
@@ -20,10 +20,10 @@ import Lean.Meta.Tactic.Rewrites
 import Lean.Elab.Tactic.Conv
 import Lean.Elab.Tactic.Conv.Basic
 import Tactics.Simp
+import Tactics.BvOmegaBench
 
 open Lean Meta Elab Tactic
 
-
 /-! ## Memory Separation Automation
 
 ##### A Note on Notation
@@ -431,7 +431,7 @@ def omega : SimpMemM Unit := do
   -- https://leanprover.zulipchat.com/#narrow/stream/326056-ICERM22-after-party/topic/Regression.20tests/near/290131280
   -- @bollu: TODO: understand what precisely we are recovering from.
   withoutRecover do
-    evalTactic (← `(tactic| bv_omega))
+    evalTactic (← `(tactic| bv_omega_bench))
 
 section Hypotheses
 
diff --git a/Arm/Memory/SeparateProofs.lean b/Arm/Memory/SeparateProofs.lean
index c9439cbb..e1e91f65 100644
--- a/Arm/Memory/SeparateProofs.lean
+++ b/Arm/Memory/SeparateProofs.lean
@@ -6,6 +6,7 @@ Author(s): Shilpi Goel
 import Arm.State
 import Arm.Memory.Separate
 import Std.Tactic.BVDecide
+import Tactics.BvOmegaBench
 
 ----------------------------------------------------------------------
 
@@ -30,45 +31,45 @@ theorem n_minus_1_lt_2_64_1 (n : Nat)
 -- (FIXME) Prove for all bitvector widths.
 theorem BitVec.add_sub_self_left_64 (a m : BitVec 64) :
   a + m - a = m := by
-  bv_omega
+  bv_omega_bench
 
 -- (FIXME) Prove for all bitvector widths.
 theorem BitVec.add_sub_self_right_64 (a m : BitVec 64) :
   a + m - m = a := by
-  bv_omega
+  bv_omega_bench
 
 -- (FIXME) Prove for all bitvector widths.
 theorem BitVec.add_sub_add_left (a m n : BitVec 64) :
   a + m - (a + n) = m - n := by
-  bv_omega
+  bv_omega_bench
 
 -- (FIXME) Prove for all bitvector widths, using general assoc/comm
 -- BitVec lemmas.
 theorem BitVec.sub_of_add_is_sub_sub (a b c : BitVec 64) :
   (a - (b + c)) = a - b - c := by
-  bv_omega
+  bv_omega_bench
 
 -- (FIXME) Prove for all bitvector widths, using general assoc/comm
 -- BitVec lemmas.
 theorem BitVec.add_of_sub_sub_of_add (a b c : BitVec 64) :
   (a + b - c) = a - c + b := by
-  bv_omega
+  bv_omega_bench
 
 theorem nat_bitvec_sub1 (x y : BitVec 64)
   (_h : y.toNat <= x.toNat) :
   (x - y).toNat = (x.toNat - y.toNat) % 2^64 := by
-  bv_omega
+  bv_omega_bench
 
 theorem nat_bitvec_sub2 (x y : Nat)
   (h : y <= x) (xub : x < 2^64) :
   BitVec.ofNat 64 (x - y) =
   (BitVec.ofNat 64 x) - (BitVec.ofNat 64 y) := by
-  bv_omega
+  bv_omega_bench
 
 theorem addr_add_one_add_m_sub_one  (n : Nat) (addr : BitVec 64)
   (h_lb : Nat.succ 0 ≤ n) (h_ub : n + 1 ≤ 2 ^ 64) :
   (addr + 1#64 + (BitVec.ofNat 64 (n - 1))) = addr + (BitVec.ofNat 64 n) := by
-  bv_omega
+  bv_omega_bench
 
 ----------------------------------------------------------------------
 ---- mem_subset ----
@@ -124,7 +125,7 @@ theorem first_address_add_one_is_subset_of_region (n : Nat) (addr : BitVec 64)
   mem_subset (addr + 1#64) (addr + (BitVec.ofNat 64 n)) addr (addr + (BitVec.ofNat 64 n)) := by
   simp [mem_subset]
   apply first_address_add_one_is_subset_of_region_helper
-  bv_omega
+  bv_omega_bench
 
 private theorem first_addresses_add_one_is_subset_of_region_general_helper
   (n m addr1 addr2 : BitVec 64) (h0 : 0#64 < m) :
@@ -146,7 +147,7 @@ theorem first_addresses_add_one_is_subset_of_region_general
   revert h3
   simp [mem_subset]
   apply first_addresses_add_one_is_subset_of_region_general_helper
-  bv_omega
+  bv_omega_bench
 
 private theorem first_addresses_add_one_preserves_subset_same_addr_helper (h1l : 0#64 < m) :
   m - 1#64 ≤ (BitVec.ofNat 64 (2^64 - 1)) - 1#64 := by
@@ -208,9 +209,9 @@ theorem mem_subset_one_addr_region_lemma (addr1 addr2 : BitVec 64) (h : n1 <= 2
   mem_subset addr1 (addr1 + (BitVec.ofNat 64 n1) - 1#64) addr2 addr2 → (n1 = 1) ∧ (addr1 = addr2) := by
   simp [mem_subset]
   have h0 := mem_subset_one_addr_region_lemma_helper (BitVec.ofNat 64 n1) addr1 addr2
-  have h1 : 0#64 ≠ 18446744073709551615#64 := by bv_omega
+  have h1 : 0#64 ≠ 18446744073709551615#64 := by bv_omega_bench
   simp_all only [ofNat_eq_ofNat, and_imp, ne_eq, false_or]
-  have h2 : (BitVec.ofNat 64 n1) = 1#64 → n1 = 1 := by bv_omega
+  have h2 : (BitVec.ofNat 64 n1) = 1#64 → n1 = 1 := by bv_omega_bench
   intro h₀ h₁
   simp_all only [true_implies, BitVec.sub_self, and_self]
 
@@ -218,16 +219,16 @@ theorem mem_subset_one_addr_region_lemma_alt (addr1 addr2 : BitVec 64)
   (h : n1 < 2 ^ 64) :
   mem_subset addr1 (addr1 + (BitVec.ofNat 64 n1)) addr2 addr2 → (n1 = 0) ∧ (addr1 = addr2) := by
   simp only [mem_subset, bitvec_rules, minimal_theory]
-  have h1 : 0#64 ≠ 18446744073709551615#64 := by bv_omega
+  have h1 : 0#64 ≠ 18446744073709551615#64 := by bv_omega_bench
   simp_all only [ne_eq, false_or, and_imp]
-  bv_omega
+  bv_omega_bench
 
 theorem mem_subset_same_region_lemma
   (h0 : 0 < n)
   (h1 : Nat.succ n ≤ 2 ^ 64) :
   mem_subset (addr + 1#64) (addr + 1#64 + (BitVec.ofNat 64 (n - 1))) addr (addr + (BitVec.ofNat 64 (Nat.succ n - 1))) := by
   simp [mem_subset]
-  bv_omega
+  bv_omega_bench
   done
 
 theorem mem_subset_trans
@@ -281,7 +282,7 @@ theorem mem_separate_contiguous_regions_one_address (addr : BitVec 64) (h : n' <
   mem_separate addr addr (addr + 1#64) (addr + 1#64 + (BitVec.ofNat 64 (n' - 1))) := by
   simp [mem_separate, mem_overlap]
   have h' : (BitVec.ofNat 64 (n' - 1)) < 0xffffffffffffffff#64 := by
-    bv_omega
+    bv_omega_bench
   apply mem_separate_contiguous_regions_one_address_helper
   assumption
 
diff --git a/Proofs/Experiments/AddLoop/AddLoop.lean b/Proofs/Experiments/AddLoop/AddLoop.lean
index 732f21d6..eb647fd0 100644
--- a/Proofs/Experiments/AddLoop/AddLoop.lean
+++ b/Proofs/Experiments/AddLoop/AddLoop.lean
@@ -11,6 +11,7 @@ import Arm
 import Tactics.StepThms
 import Tactics.Sym
 import Correctness.ArmSpec
+import Tactics.BvOmegaBench
 
 namespace AddLoop
 
@@ -523,18 +524,18 @@ private theorem loop_inv_x0_le (x y : BitVec 64)
   (h_assert_x0 : x ≤ y)
   (h_assert_x0_nz : ¬x = 0x0#64) :
   x - 0x1#64 ≤ y := by
-  bv_omega
+  bv_omega_bench
 
 private theorem AddWithCarry.add_one_64 (x : BitVec 64) :
   (AddWithCarry x 0x1#64 0x0#1).fst = x + 0x1#64 := by
   simp only [AddWithCarry, bitvec_rules]
-  bv_omega
+  bv_omega_bench
 
 private theorem crock_lemma (x y z : BitVec 64) :
   x + (y - z) + 1#64 = x + (y - (z - 1#64)) := by
-  -- (FIXME) Without this apply below, bv_omega crashes my editor.
+  -- (FIXME) Without this apply below, bv_omega_bench crashes my editor.
   apply BitVec.eq_sub_iff_add_eq.mp
-  bv_omega
+  bv_omega_bench
 
 theorem partial_correctness :
   PartialCorrectness ArmState := by
diff --git a/Proofs/Experiments/AddLoop/AddLoopTandem.lean b/Proofs/Experiments/AddLoop/AddLoopTandem.lean
index ac58b4d9..a5aa02d6 100644
--- a/Proofs/Experiments/AddLoop/AddLoopTandem.lean
+++ b/Proofs/Experiments/AddLoop/AddLoopTandem.lean
@@ -12,6 +12,7 @@ import Tactics.CSE
 import Tactics.Sym
 import Tactics.StepThms
 import Correctness.ArmSpec
+import Tactics.BvOmegaBench
 
 namespace AddLoopTandem
 
@@ -123,7 +124,7 @@ instance : Spec' ArmState where
 private theorem AddWithCarry.add_one_64 (x : BitVec 64) :
   (AddWithCarry x 0x1#64 0x0#1).fst = x + 0x1#64 := by
   simp only [AddWithCarry, bitvec_rules]
-  bv_omega
+  bv_omega_bench
 
 private theorem AddWithCarry.sub_one_64 (x : BitVec 64) :
   (AddWithCarry x 0xfffffffffffffffe#64 0x1#1).fst = x - 1#64 := by
@@ -317,14 +318,14 @@ private theorem non_one_bit_is_zero {x : BitVec 1}
 
 private theorem crock_lemma (x y z : BitVec 64) :
   x + (y - z) + 1#64 = x + (y - (z - 1#64)) := by
-  -- (FIXME) Without this apply below, bv_omega crashes my editor.
+  -- (FIXME) Without this apply below, bv_omega_bench crashes my editor.
   apply BitVec.eq_sub_iff_add_eq.mp
-  bv_omega
+  bv_omega_bench
 
 private theorem loop_inv_x0_helper_lemma {x y : BitVec 64} (h1 : x ≤ y)
   (h2 : ¬(x = 0#64)) :
   x - 0x1#64 ≤ y := by
-  bv_omega
+  bv_omega_bench
 
 -------------------------------------------------------------------------------
 
@@ -340,17 +341,17 @@ def loop_clock (x0 : BitVec 64) : Nat :=
     1
   else
     have : x0 - 0x1#64 < x0 := by
-     bv_omega
+     bv_omega_bench
     4 + loop_clock (x0 - 1)
   termination_by x0.toNat
 
 theorem loop_clock_inv_lemma (h : ¬x = 0x0#64) :
   loop_clock (x - 0x1#64) < loop_clock x := by
   generalize h_xn : x.toNat = xn
-  have h_xn_ge_1 : 1 ≤ xn := by bv_omega
+  have h_xn_ge_1 : 1 ≤ xn := by bv_omega_bench
   induction xn, h_xn_ge_1 using Nat.le_induction generalizing x
   case base =>
-    have h_x_eq_1 : x = 1#64 := by bv_omega
+    have h_x_eq_1 : x = 1#64 := by bv_omega_bench
     unfold loop_clock
     simp only [h_x_eq_1, BitVec.sub_self, BitVec.ofNat_eq_ofNat,
                reduceDIte, gt_iff_lt, BitVec.reduceEq]
@@ -359,8 +360,8 @@ theorem loop_clock_inv_lemma (h : ¬x = 0x0#64) :
     rename_i xn' h_xn' h_inv
     unfold loop_clock
     simp only [BitVec.ofNat_eq_ofNat, dite_eq_ite, gt_iff_lt]
-    have h1 : ¬ x - 0x1#64 = 0x0#64 := by bv_omega
-    have h2 : (x - 0x1#64).toNat = xn' := by bv_omega
+    have h1 : ¬ x - 0x1#64 = 0x0#64 := by bv_omega_bench
+    have h2 : (x - 0x1#64).toNat = xn' := by bv_omega_bench
     simp only [h, h1, h2, h_inv,
                reduceIte, Nat.add_lt_add_iff_left, not_false_eq_true]
   done
diff --git a/Proofs/Experiments/Max/MaxTandem.lean b/Proofs/Experiments/Max/MaxTandem.lean
index f8aac756..e75925a0 100644
--- a/Proofs/Experiments/Max/MaxTandem.lean
+++ b/Proofs/Experiments/Max/MaxTandem.lean
@@ -164,7 +164,7 @@ theorem program.stepi_0x894_cut (s sn : ArmState)
   | apply Aligned_AddWithCarry_64_4'
   repeat solve
   | decide
-  | bv_omega
+  | bv_omega_bench
   | assumption
 
 /--
diff --git a/Proofs/Experiments/Memcpy/MemCpyVCG.lean b/Proofs/Experiments/Memcpy/MemCpyVCG.lean
index e12f2b2b..4b4a7ce1 100644
--- a/Proofs/Experiments/Memcpy/MemCpyVCG.lean
+++ b/Proofs/Experiments/Memcpy/MemCpyVCG.lean
@@ -464,7 +464,7 @@ theorem Memcpy.extracted_2 (s0 si : ArmState)
       (Memory.write_bytes 16 (s0.x2 + 0x10#64 * (s0.x0 - si.x0))
         (Memory.read_bytes 16 (s0.x1 + 0x10#64 * (s0.x0 - si.x0)) si.mem) si.mem) =
     Memory.read_bytes n addr s0.mem := by
-  have h_le : (s0.x0 - (si.x0 - 0x1#64)).toNat ≤ s0.x0.toNat := by bv_omega
+  have h_le : (s0.x0 - (si.x0 - 0x1#64)).toNat ≤ s0.x0.toNat := by bv_omega_bench
   have h_upper_bound := hsep.hb.omega_def
   have h_upper_bound₂ := h_pre_1.hb.omega_def
   have h_upper_bound₃ := hsep.ha.omega_def
@@ -476,7 +476,7 @@ theorem Memcpy.extracted_2 (s0 si : ArmState)
     apply mem_separate'.symm
     apply mem_separate'.of_subset'_of_subset' hsep
     · apply mem_subset'.of_omega
-      skip_proof refine ⟨?_, ?_, ?_, ?_⟩ <;> skip_proof bv_omega
+      skip_proof refine ⟨?_, ?_, ?_, ?_⟩ <;> skip_proof bv_omega_bench
     · apply mem_subset'_refl hsep.hb
 
 -- set_option skip_proof.skip true in
@@ -519,9 +519,9 @@ theorem Memcpy.extracted_0 (s0 si : ArmState)
       skip_proof simp_mem
     have h_subset_1 : mem_subset' (s0.x1 + 0x10#64 * (s0.x0 - si.x0)) 16 s0.x1 (s0.x0.toNat * 16) := by
       skip_proof simp_mem
-    have icases : i = s0.x0 - si.x0 ∨ i < s0.x0 - si.x0 := by skip_proof bv_omega
+    have icases : i = s0.x0 - si.x0 ∨ i < s0.x0 - si.x0 := by skip_proof bv_omega_bench
     have s2_sum_inbounds := h_pre_1.hb.omega_def
-    have i_sub_x0_mul_16 : 16 * i.toNat < 16 * s0.x0.toNat := by skip_proof bv_omega
+    have i_sub_x0_mul_16 : 16 * i.toNat < 16 * s0.x0.toNat := by skip_proof bv_omega_bench
 
     rcases icases with hi | hi
     · subst hi
@@ -541,13 +541,13 @@ theorem Memcpy.extracted_0 (s0 si : ArmState)
           -- proof states.
           skip_proof {
             have s2_sum_inbounds := h_pre_1.hb.omega_def
-            have i_sub_x0_mul_16 : 16 * i.toNat < 16 * s0.x0.toNat := by skip_proof bv_omega
-            rw [BitVec.toNat_add_eq_toNat_add_toNat (by bv_omega)]
-            rw [BitVec.toNat_add_eq_toNat_add_toNat (by bv_omega)]
-            rw [BitVec.toNat_mul_of_lt (by bv_omega)]
-            rw [BitVec.toNat_mul_of_lt (by bv_omega)]
-            rw [BitVec.toNat_sub_of_lt (by bv_omega)]
-            bv_omega
+            have i_sub_x0_mul_16 : 16 * i.toNat < 16 * s0.x0.toNat := by skip_proof bv_omega_bench
+            rw [BitVec.toNat_add_eq_toNat_add_toNat (by bv_omega_bench)]
+            rw [BitVec.toNat_add_eq_toNat_add_toNat (by bv_omega_bench)]
+            rw [BitVec.toNat_mul_of_lt (by bv_omega_bench)]
+            rw [BitVec.toNat_mul_of_lt (by bv_omega_bench)]
+            rw [BitVec.toNat_sub_of_lt (by bv_omega_bench)]
+            bv_omega_bench
           }
   · intros n addr hsep
     apply Memcpy.extracted_2 <;> assumption
@@ -741,19 +741,19 @@ theorem partial_correctness :
           apply zero_iff_z_eq_one
         simp only [h_s5_z]
 
-        simp only [show s5.x0 ≤ s0.x0 by bv_omega, true_and]
+        simp only [show s5.x0 ≤ s0.x0 by bv_omega_bench, true_and]
         rw [h_s5_x0, h_s5_x1, h_si_x1]
         have h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64)) := by
-          rw [show s0.x0 - (si.x0 - 0x1#64) = (s0.x0 - si.x0) + 0x1#64 by skip_proof bv_omega,
+          rw [show s0.x0 - (si.x0 - 0x1#64) = (s0.x0 - si.x0) + 0x1#64 by skip_proof bv_omega_bench,
             BitVec.BitVec.mul_add,
             BitVec.add_assoc, BitVec.mul_one]
         simp only [h_s0_x1, true_and]
 
         rw [h_s5_x2, h_si_x2]
         have h_s0_x2 : s0.x2 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x2 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64)) := by
-          rw [show s0.x0 - (si.x0 - 0x1#64) = (s0.x0 - si.x0) + 0x1#64 by skip_proof bv_omega,
+          rw [show s0.x0 - (si.x0 - 0x1#64) = (s0.x0 - si.x0) + 0x1#64 by skip_proof bv_omega_bench,
             BitVec.BitVec.mul_add]
-          skip_proof bv_omega
+          skip_proof bv_omega_bench
         simp only [h_s0_x2, true_and]
         simp only [step_8f0_8f4.h_err,
           step_8f0_8f4.h_program,
diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean
index a357172c..30065890 100644
--- a/Proofs/Experiments/MemoryAliasing.lean
+++ b/Proofs/Experiments/MemoryAliasing.lean
@@ -200,7 +200,7 @@ theorem mem_automation_test_4
   simp only [memory_rules]
   simp_mem
   congr 1
-  bv_omega -- TODO: address normalization.
+  bv_omega_bench -- TODO: address normalization.
 
 /-- info: 'mem_automation_test_4' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms mem_automation_test_4
@@ -229,7 +229,7 @@ theorem overlapping_read_test_2 {out : BitVec (16 * 8)}
   simp_mem
   · congr
     -- ⊢ (src_addr + 6).toNat - src_addr.toNat = 6
-    bv_omega
+    bv_omega_bench
 /--
 info: 'ReadOverlappingRead.overlapping_read_test_2' depends on axioms: [propext, Classical.choice, Quot.sound]
 -/
@@ -248,13 +248,13 @@ theorem overlapping_read_test_3
   simp_mem
   · congr
     -- ⊢ (src_addr + 6).toNat - src_addr.toNat = 6
-    bv_omega
+    bv_omega_bench
 /--
 info: 'ReadOverlappingRead.overlapping_read_test_3' depends on axioms: [propext, Classical.choice, Quot.sound]
 -/
 #guard_msgs in #print axioms overlapping_read_test_3
 
-/- TODO(@bollu): This test case hangs at `bv_omega`. This is to be debugged.
+/- TODO(@bollu): This test case hangs at `bv_omega_bench`. This is to be debugged.
 /-- A read in the goal state overlaps with a read in the
 right hand side of the hypotheis `h`.
 -/
@@ -268,7 +268,7 @@ theorem overlapping_read_test_4
   simp_mem
   · congr
     -- ⊢ (src_addr + 6).toNat - src_addr.toNat = 6
-    bv_omega -- TODO: Lean gets stuck here?
+    bv_omega_bench -- TODO: Lean gets stuck here?
 
 #guard_msgs in #print axioms overlapping_read_test_4
 -/
@@ -290,7 +290,7 @@ theorem test_2 {val : BitVec _}
     Memory.read_bytes 6 (src_addr + 10) (Memory.write_bytes 16 src_addr val mem) =
     val.extractLsBytes 10 6 := by
   simp_mem
-  have : ((src_addr + 10).toNat - src_addr.toNat) = 10 := by bv_omega
+  have : ((src_addr + 10).toNat - src_addr.toNat) = 10 := by bv_omega_bench
   rw [this]
 
 /--
diff --git a/Tactics/Attr.lean b/Tactics/Attr.lean
index e6b682e8..6f4e8095 100644
--- a/Tactics/Attr.lean
+++ b/Tactics/Attr.lean
@@ -27,3 +27,31 @@ initialize
       generally not set this option, unless they are reporting a bug with \
       `sym_n`"
   }
+
+  -- enable extra checks for debugging `sym_n`,
+  -- see `AxEffects.validate` for more detail on what is being type-checked
+
+  register_option Tactic.bv_omega_bench.filePath : String := {
+    defValue := "/tmp/omega-bench.txt"
+    descr := "File path that `omega-bench` writes its results to."
+  }
+
+  register_option Tactic.bv_omega_bench.enabled : Bool := {
+    defValue := true,
+    descr := "Enable `bv_omega_bench`'s logging, which writes benchmarking data to `Tactic.bv_omega_bench.filePath`."
+  }
+
+  register_option Tactic.bv_omega_bench.minMs : Nat := {
+    defValue := 1000,
+    descr := "Log into `Tactic.bv_omega_bench.filePath` if the time spent in milliseconds is greater than or equal to `Tactic.bv_omega_bench.minMs`."
+  }
+
+def getBvOmegaBenchFilePath [Monad m] [MonadOptions m] : m String := do
+  return Tactic.bv_omega_bench.filePath.get (← getOptions)
+
+
+def getBvOmegaBenchIsEnabled [Monad m] [MonadOptions m] : m Bool := do
+  return Tactic.bv_omega_bench.enabled.get (← getOptions)
+
+def getBvOmegaBenchMinMs [Monad m] [MonadOptions m] : m Nat := do
+  return Tactic.bv_omega_bench.minMs.get (← getOptions)
diff --git a/Tactics/BvOmegaBench.lean b/Tactics/BvOmegaBench.lean
new file mode 100644
index 00000000..1505335c
--- /dev/null
+++ b/Tactics/BvOmegaBench.lean
@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Siddharth Bhat
+-/
+/-
+This module implements `bv_omega_bench`, which writes benchmarking results of `bv_omega`
+into a user-defined file. This is used for extracting out calls to `bv_omega` that are slow,
+and allows us to send bug reports to the Lean developers.
+-/
+import Tactics.Attr
+import Lean
+open Lean Elab Meta Tactic
+
+namespace BvOmegaBench
+
+/--
+Run bv_omega, gather the results, and then store them at the value that is given by the option.
+By default, it's stored at `pwd`, with filename `omega-bench`. The file is appended to,
+with the goal state that is being run, and the time elapsed to solve the goal is written.
+-/
+def run : TacticM Unit := do
+  let minMs ← getBvOmegaBenchMinMs
+  let goal ← getMainGoal
+  let goalStr ← ppGoal goal
+  let startTime ← IO.monoMsNow
+  try
+    withMainContext do
+      withoutRecover do
+        evalTactic (← `(tactic| bv_omega))
+        if !(← getBvOmegaBenchIsEnabled) then
+          return ()
+        let endTime ← IO.monoMsNow
+        let delta := endTime - startTime
+        let filePath ← getBvOmegaBenchFilePath
+        IO.FS.withFile filePath IO.FS.Mode.append fun h => do
+          if delta >= minMs then
+            h.putStrLn "\n---\n"
+            h.putStrLn s!"time"
+            h.putStrLn s!"{delta}"
+            h.putStrLn s!"endtime"
+            h.putStrLn s!"goal"
+            h.putStrLn goalStr.pretty
+            h.putStrLn s!"endgoal"
+  catch e =>
+    throw e
+  return ()
+
+end BvOmegaBench
+
+syntax (name := bvOmegaBenchTac) "bv_omega_bench" : tactic
+
+@[tactic bvOmegaBenchTac]
+def bvOmegaBenchImpl : Tactic
+| `(tactic| bv_omega_bench) =>
+   BvOmegaBench.run
+| _ => throwUnsupportedSyntax