diff --git a/Arm/Memory/Separate.lean b/Arm/Memory/Separate.lean
index a05cc413..a236326c 100644
--- a/Arm/Memory/Separate.lean
+++ b/Arm/Memory/Separate.lean
@@ -230,12 +230,12 @@ theorem mem_legal'.omega_def (h : mem_legal' a n) : a.toNat + n ≤ 2^64 := h
 
 /-- The linear constraint is equivalent to `mem_legal'`. -/
 theorem mem_legal'.iff_omega (a : BitVec 64) (n : Nat) :
-    (a.toNat + n ≤ 2^64) ↔ mem_legal' a n := by
+    mem_legal' a n ↔ (a.toNat + n ≤ 2^64)  := by
   constructor
-  · intros h
-    apply mem_legal'.of_omega h
   · intros h
     apply h.omega_def
+  · intros h
+    apply mem_legal'.of_omega h
 
 instance : Decidable (mem_legal' a n) :=
   if h : a.toNat + n ≤ 2^64 then
@@ -341,14 +341,15 @@ theorem mem_separate'.of_omega
 
 /-- The linear constraint is equivalent to `mem_separate'`. -/
 theorem mem_separate'.iff_omega (a : BitVec 64) (an : Nat) (b : BitVec 64) (bn : Nat) :
+    mem_separate' a an b bn ↔
     (a.toNat + an ≤ 2^64 ∧
     b.toNat + bn ≤ 2^64 ∧
-    (a.toNat + an ≤ b.toNat ∨ a.toNat ≥ b.toNat + bn)) ↔ mem_separate' a an b bn := by
+    (a.toNat + an ≤ b.toNat ∨ a.toNat ≥ b.toNat + bn)) := by
   constructor
-  · intros h
-    apply mem_separate'.of_omega h
   · intros h
     apply h.omega_def
+  · intros h
+    apply mem_separate'.of_omega h
 
 instance : Decidable (mem_separate' a an b bn) :=
   if h : (a.toNat + an ≤ 2^64 ∧ b.toNat + bn ≤ 2^64 ∧ (a.toNat + an ≤ b.toNat ∨ a.toNat ≥ b.toNat + bn)) then
@@ -424,15 +425,16 @@ constructor
 
 /-- The linear constraint is equivalent to `mem_subset'`. -/
 theorem mem_subset'.iff_omega (a : BitVec 64) (an : Nat) (b : BitVec 64) (bn : Nat) :
+    mem_subset' a an b bn ↔
     (a.toNat + an ≤ 2^64 ∧
     b.toNat + bn ≤ 2^64 ∧
     b.toNat ≤ a.toNat ∧
-    a.toNat + an ≤ b.toNat + bn) ↔ mem_subset' a an b bn := by
+    a.toNat + an ≤ b.toNat + bn) := by
   constructor
-  · intros h
-    apply mem_subset'.of_omega h
   · intros h
     apply h.omega_def
+  · intros h
+    apply mem_subset'.of_omega h
 
 instance : Decidable (mem_subset' a an b bn) :=
   if h : (a.toNat + an ≤ 2^64 ∧ b.toNat + bn ≤ 2^64 ∧ b.toNat ≤ a.toNat ∧ a.toNat + an ≤ b.toNat + bn) then
diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean
index 1e5c13ba..ed8a1367 100644
--- a/Arm/Memory/SeparateAutomation.lean
+++ b/Arm/Memory/SeparateAutomation.lean
@@ -433,38 +433,34 @@ def simpAndIntroDef (name : String) (hdefVal : Expr) : TacticM FVarId  := do
 attribute [bv_toNat] BitVec.le_def
 -- bv_omega' := (try simp only [bv_toNat, BitVec.le_def] at *) <;> omega)
 -- #check Lean.Elab.Tactic.Omega.omega
--- #check Lean.Elab.Tactic.Omega.bvOmega
+-- #check Lean.Elab.Tactic.Omega.
 -- simpTargetStar
 
 
+    -- let proof  := localDecl.toExpr
+
+    -- let simpTheorems ← ctx.simpTheorems.addTheorem (.fvar h) proof
+    -- ctx := { ctx with simpTheorems }
+
 /-- SimpMemM's omega invoker -/
 def omega : TacticM Unit := do
-  let g ← getMainGoal
+  let g ← match ← (← getMainGoal).falseOrByContra with
+    | none =>
+      trace[simp_mem] "omega converting goal to false/contra *closed* goal."
+      return ()
+    | some g' =>
+      pure g'
+  replaceMainGoal [g]
   let (simpCtx, simprocs) ← LNSymSimpContext
-      (config := {})
-      (simp_attrs := #[`bv_toNat]) (useDefaultSimprocs := false) (simprocs := #[])
-  let (result, stats) ← simpTargetStar g simpCtx simprocs
-  trace[simp_mem] "simp stats: {stats.usedTheorems.toArray.map Origin.key}"
-  if let .closed := result then
-    trace[simp_mem] "omega preprocessor *closed* goal."
-    replaceMainGoal []
-    return ()
-  else
-    let g :=
-      match result with
-      | .modified g' => g'
-      | .noChange | .closed => g
-    -- Step 2: prove goal with omega.
-    let g ←
-      match ← g.falseOrByContra with
-      | none =>
-        trace[simp_mem] "omega converting goal to false/contra *closed* goal."
-        return ()
-      | some g' =>
-        pure g'
-    trace[simp_mem] "omega goal: {g}"
-    replaceMainGoal [g]
-    g.withContext (do Lean.Elab.Tactic.Omega.omega (← getLocalHyps).toList g {})
+      (config := { failIfUnchanged := false })
+      (simp_attrs := #[`bv_toNat])
+      (useDefaultSimprocs := false)
+      (thms := #[``mem_legal'.iff_omega, ``mem_separate'.iff_omega, ``mem_subset'.iff_omega, ``BitVec.le_def])
+      (simprocs := #[])
+  let _ ← simpLocation simpCtx simprocs (loc := Location.wildcard)
+  let g ← getMainGoal
+  trace[simp_mem] "omega goal: {g}"
+  g.withContext (do Lean.Elab.Tactic.Omega.omega (← getLocalHyps).toList g {})
 
 section Hypotheses
 
@@ -1016,23 +1012,23 @@ partial def SimpMemM.closeGoal (g : MVarId) (hyps : Array Hypothesis) : SimpMemM
       withTraceNode m!"Matched on ⊢ {e}. Proving..." do
         if let .some proof ← proveWithOmega? e hyps then
           g.assign proof.h
-    else if (← getConfig).useOmegaToClose then
-      withTraceNode m!"Unknown memory expression ⊢ {gt}. Trying reduction to omega (`config.useOmegaToClose = true`):" do
-        let oldGoals := (← getGoals)
-        try
-          let gproof ← mkFreshExprMVar (type? := gt)
-          setGoals (gproof.mvarId! :: (← getGoals))
-          SimpMemM.withMainContext do
-          let _ ← Hypothesis.addOmegaFactsOfHyps hyps.toList #[]
-          trace[simp_mem.info] m!"Executing `omega` to close {gt}"
-          SimpMemM.withTraceNode m!"goal (Note: can be large)" do
-            trace[simp_mem.info] "{← getMainGoal}"
-          omega
-          trace[simp_mem.info] "{checkEmoji} `omega` succeeded."
-          g.assign gproof
-        catch e =>
-          trace[simp_mem.info]  "{crossEmoji} `omega` failed with error:\n{e.toMessageData}"
-          setGoals oldGoals
+    -- else if false && (← getConfig).useOmegaToClose then
+    --   withTraceNode m!"Unknown memory expression ⊢ {gt}. Trying reduction to omega (`config.useOmegaToClose = true`):" do
+    --     let oldGoals := (← getGoals)
+    --     try
+    --       let gproof ← mkFreshExprMVar (type? := gt)
+    --       setGoals (gproof.mvarId! :: (← getGoals))
+    --       SimpMemM.withMainContext do
+    --       let _ ← Hypothesis.addOmegaFactsOfHyps hyps.toList #[]
+    --       trace[simp_mem.info] m!"Executing `omega` to close {gt}"
+    --       SimpMemM.withTraceNode m!"goal (Note: can be large)" do
+    --         trace[simp_mem.info] "{← getMainGoal}"
+    --       omega
+    --       trace[simp_mem.info] "{checkEmoji} `omega` succeeded."
+    --       g.assign gproof
+    --     catch e =>
+    --       trace[simp_mem.info]  "{crossEmoji} `omega` failed with error:\n{e.toMessageData}"
+    --       setGoals oldGoals
   return ← g.isAssigned
 
 
@@ -1068,9 +1064,9 @@ partial def SimpMemM.simplifyLoop : SimpMemM Unit := do
       for (i, h) in foundHyps.toList.enum do
         trace[simp_mem.info] m!"{i+1}) {h}"
 
-    if ← SimpMemM.closeGoal g foundHyps then
-      trace[simp_mem.info] "{checkEmoji} goal closed."
-      return ()
+    -- if ← SimpMemM.closeGoal g foundHyps then
+    --   trace[simp_mem.info] "{checkEmoji} goal closed."
+    --   return ()
 
     -- goal was not closed, try and improve.
     let mut changedInAnyIter? := false
diff --git a/Proofs/Experiments/Max/MaxTandem.lean b/Proofs/Experiments/Max/MaxTandem.lean
index f8aac756..0971e68a 100644
--- a/Proofs/Experiments/Max/MaxTandem.lean
+++ b/Proofs/Experiments/Max/MaxTandem.lean
@@ -626,7 +626,7 @@ theorem partial_correctness :
       -- 2/15
       name h_s1_run : s2 := run 1 s1
       obtain ⟨h_s2_cut, h_s2_pc, h_s2_err, h_s2_program, h_s2_read_sp_8, h_s2_read_sp_12, h_s2_x0, h_s2_x1, h_s2_sp, h_s2_sp_aligned⟩ :=
-        program.stepi_0x898_cut s1 s2 h_s1_program h_s1_pc h_s1_err h_s1_sp_aligned (by simp_mem) h_s1_run.symm
+        program.stepi_0x898_cut s1 s2 h_s1_program h_s1_pc h_s1_err h_s1_sp_aligned (by mem_omega) h_s1_run.symm
       rw [Correctness.snd_cassert_of_not_cut h_s2_cut]; -- try rw [Correctness.snd_cassert_of_cut h_cut];
       simp [show Sys.next s2 = run 1 s2 by rfl]
       replace h_s2_sp : s2.sp = (s0.sp - 32#64) := by simp_all
@@ -637,7 +637,7 @@ theorem partial_correctness :
 
       -- 3/15
       name h_run : s3 := run 1 s2
-      obtain h := program.stepi_0x89c_cut s2 s3 h_s2_program h_s2_pc h_s2_err h_s2_sp_aligned (by simp_mem) h_run.symm
+      obtain h := program.stepi_0x89c_cut s2 s3 h_s2_program h_s2_pc h_s2_err h_s2_sp_aligned (by mem_omega) h_run.symm
       obtain ⟨h_s3_cut, h_s3_read_sp_8, h_s3_read_sp_12, h_s3_x0, h_s3_x1, h_s3_sp, h_s3_pc, h_s3_err, h_s3_program, h_s3_sp_aligned⟩ := h
       rw [Correctness.snd_cassert_of_not_cut h_s3_cut]; -- try rw [Correctness.snd_cassert_of_cut h_cut];
       simp [show Sys.next s3 = run 1 s3 by rfl]
diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean
index 1bcd64de..93aaf1ae 100644
--- a/Proofs/Experiments/MemoryAliasing.lean
+++ b/Proofs/Experiments/MemoryAliasing.lean
@@ -10,16 +10,16 @@ import Arm.Memory.MemoryProofs
 import Arm.BitVec
 import Arm.Memory.SeparateAutomation
 
-set_option trace.simp_mem true
-set_option trace.simp_mem.info true
-set_option trace.Tactic.addressNormalization true
+-- set_option trace.simp_mem true
+-- set_option trace.simp_mem.info true
+-- set_option trace.Tactic.addressNormalization true
 
 namespace MemLegal
 /-- Show reflexivity of legality. -/
 theorem legal_1 (l : mem_legal' a 16) : mem_legal' a 16 := by
-  simp_mem
+  mem_omega
 
-/-- info: 'MemLegal.legal_1' depends on axioms: [propext] -/
+/-- info: 'MemLegal.legal_1' depends on axioms: [propext, Quot.sound] -/
 #guard_msgs in #print axioms legal_1
 
 end MemLegal
@@ -27,28 +27,28 @@ end MemLegal
 namespace MemSubset
 /-- Reflexivity. -/
 theorem subset_1 (l : mem_subset' a 16 b 16) : mem_subset' a 16 b 16 := by
-  simp_mem
+  mem_omega
 
 /-- info: 'MemSubset.subset_1' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms subset_1
 
 /-- Show that smaller subsets are also subsets. -/
 theorem subset_2 (l : mem_subset' a 16 b 16) : mem_subset' a 10 b 16 := by
-  simp_mem
+  mem_omega
 
 /-- info: 'MemSubset.subset_2' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms subset_2
 
 /-- Show that smaller subsets are also subsets, even when moving base pointer. -/
 theorem subset_3 (l : mem_subset' a 16 b 16) : mem_subset' (a+6) 10 b 16 := by
-  simp_mem
+  mem_omega
 
 /-- info: 'MemSubset.subset_3' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms subset_3
 
 /-- Show that we can perform address arithmetic based on subset constraints. -/
 theorem subset_4 (l : mem_subset' a 16 b 16) : a = b := by
-  simp_mem
+  mem_omega
 
 /-- Show that we can perform address arithmetic based on subset constraints.
 Only two configurations possible:
@@ -60,7 +60,7 @@ a0 a1 a2 ..
 b0 b1 b2 b3
 -/
 theorem subset_5 (l : mem_subset' a 3 b 4) : a ≤ b + 1 := by
-  simp_mem
+  mem_omega
 
 end MemSubset
 
@@ -68,7 +68,7 @@ namespace MemSeparate
 
 /-- Reflexivity. -/
 theorem separate_1 (l : mem_separate' a 16 b 16) : mem_separate' a 16 b 16 := by
-  simp_mem
+  mem_omega
 
 /-- info: 'MemSeparate.separate_1' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms separate_1
@@ -76,14 +76,14 @@ theorem separate_1 (l : mem_separate' a 16 b 16) : mem_separate' a 16 b 16 := by
 
 /-- Symmetry. -/
 theorem separate_2 (l : mem_separate' a 16 b 16) : mem_separate' b 16 a 16 := by
-  simp_mem
+  mem_omega
 
 /-- info: 'MemSeparate.separate_2' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms separate_2
 
 /-- Smaller subsets. -/
 theorem separate_3 (l : mem_separate' a 16 b 16) : mem_separate' b 10 a 10 := by
-  simp_mem
+  mem_omega
 
 /-- info: 'MemSeparate.separate_3' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms separate_3
@@ -91,7 +91,7 @@ theorem separate_3 (l : mem_separate' a 16 b 16) : mem_separate' b 10 a 10 := by
 /-- sliding subset to the right. -/
 theorem separate_4 (l : mem_separate' a 16 b 16) (hab : a < b) :
     mem_separate' a 17 (b+1) 15 := by
-  simp_mem
+  mem_omega
 
 /-- info: 'MemSeparate.separate_4' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms separate_4
@@ -100,7 +100,7 @@ theorem separate_4 (l : mem_separate' a 16 b 16) (hab : a < b) :
 theorem separate_5 {n : Nat} (hn : n ≠ 0)
     (l : mem_separate' a (n <<< 4) b (n <<< 4))  :
     mem_separate' a 16 b 16 := by
-  simp_mem
+  mem_omega
 
 /-- info: 'MemSeparate.separate_5' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms separate_5
@@ -109,7 +109,7 @@ theorem separate_5 {n : Nat} (hn : n ≠ 0)
 theorem separate_6 {n : Nat} (hn : n ≠ 0)
     (l : mem_separate' a (n <<< 4) b (n <<< 4))  :
     mem_separate' a (n <<< 3 + 8) b (n <<< 4) := by
-  simp_mem
+  mem_omega
 
 /-- info: 'MemSeparate.separate_6' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms separate_6
@@ -127,15 +127,38 @@ theorem separate_6 {n : Nat} (hn : n ≠ 0)
     (l : mem_separate' a 100 b m)
     (l : mem_separate' (a+100) 100 b m)  :
     mem_separate' a 200 b m := by
-  simp_mem
+  mem_omega
+  done
   trace_state
 
-/-- error: ❌️ simp_mem failed to make any progress. -/
+/--
+error: unsolved goals
+m : Nat
+a b : BitVec 64
+n : Nat
+hn : n ≠ 0
+hm : m ≠ 0
+hlegal : mem_legal' a (2 * n)
+l✝ : mem_separate' a n b m
+l : mem_separate' (a + ↑n) n b m
+⊢ mem_separate' a (2 * n) b m
+---
+info: m : Nat
+a b : BitVec 64
+n : Nat
+hn : n ≠ 0
+hm : m ≠ 0
+hlegal : mem_legal' a (2 * n)
+l✝ : mem_separate' a n b m
+l : mem_separate' (a + ↑n) n b m
+⊢ mem_separate' a (2 * n) b m
+-/
 #guard_msgs in theorem separate_8 {n : Nat} (hn : n ≠ 0) (hm : m ≠ 0)
+    (hlegal : mem_legal' a (2*n))
     (l : mem_separate' a n b m)
     (l : mem_separate' (a+n) n b m)  :
     mem_separate' a (2*n) b m := by
-  simp_mem
+  mem_omega
   trace_state
 
 /--
@@ -143,7 +166,7 @@ Check that we can close address relationship goals that require
 us to exploit memory separateness properties.
 -/
 theorem mem_separate_9  (h : mem_separate' a 100 b 100)
-  (hab : a < b) : a + 50 ≤ b := by simp_mem
+  (hab : a < b) : a + 50 ≤ b := by mem_omega
 
 end MemSeparate
 
@@ -190,8 +213,6 @@ theorem mem_automation_test_3
   simp_mem
   rfl
 
-
-
 /-- info: 'mem_automation_test_3' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms mem_automation_test_3
 
@@ -208,7 +229,7 @@ theorem mem_automation_test_4
   simp only [memory_rules]
   simp_mem
   congr 1
-  bv_omega' -- TODO: address normalization.
+  mem_omega
 
 /-- info: 'mem_automation_test_4' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms mem_automation_test_4
@@ -223,8 +244,11 @@ theorem overlapping_read_test_1 {out : BitVec (16 * 8)}
     read_mem_bytes 16 src_addr s = out := by
   simp only [memory_rules] at h ⊢
   simp_mem
+  simp [BitVec.extractLsBytes_eq_self]
 
-/-- info: 'ReadOverlappingRead.overlapping_read_test_1' depends on axioms: [propext, Quot.sound] -/
+/--
+info: 'ReadOverlappingRead.overlapping_read_test_1' depends on axioms: [propext, Classical.choice, Quot.sound]
+-/
 #guard_msgs in #print axioms overlapping_read_test_1
 
 /-- A read overlapping with another read. -/
@@ -236,7 +260,7 @@ theorem overlapping_read_test_2 {out : BitVec (16 * 8)}
   simp_mem
   · congr
     -- ⊢ (src_addr + 6).toNat - src_addr.toNat = 6
-    bv_omega'
+    mem_omega
 /--
 info: 'ReadOverlappingRead.overlapping_read_test_2' depends on axioms: [propext, Classical.choice, Quot.sound]
 -/
@@ -255,7 +279,7 @@ theorem overlapping_read_test_3
   simp_mem
   · congr
     -- ⊢ (src_addr + 6).toNat - src_addr.toNat = 6
-    bv_omega'
+    mem_omega
 /--
 info: 'ReadOverlappingRead.overlapping_read_test_3' depends on axioms: [propext, Classical.choice, Quot.sound]
 -/
@@ -384,7 +408,7 @@ proving generic properties about our definitions of `mem_legal'`,
 -/
 
 /-! ### mem_subset is a partial order. -/
-theorem mem_subset_refl (h : mem_legal' a an) : mem_subset' a an a an := by simp_mem
+theorem mem_subset_refl (h : mem_legal' a an) : mem_subset' a an a an := by mem_omega
 /-
 TODO(@bollu): In such a scenario, we should call `omega` directly on the goal,
 and see if it can solve it.
@@ -393,20 +417,20 @@ theorem mem_subset_asymm (h : mem_subset' a an b bn) (h' : mem_subset' b bn a an
   simp_mem
 -/
 theorem mem_subset_trans (h : mem_subset' a an b bn) (h' : mem_subset' b bn c cn) :
-  mem_subset' a an c cn := by simp_mem
+  mem_subset' a an c cn := by mem_omega
 
 /-! ### mem_separate relationship to arithmetic -/
 
-theorem mem_separate_comm (h : mem_separate' a an b bn) : mem_separate' b bn a an := by simp_mem
+theorem mem_separate_comm (h : mem_separate' a an b bn) : mem_separate' b bn a an := by mem_omega
 /-- if `[a..an)⟂[b..bn)`, then `[a+δ..an-δ)⟂[b..bn)`-/
 theorem mem_separate_of_lt_of_lt_sub (h : mem_separate' a an b bn) (hab : a < b)
-  (hδ : δ < b - a): mem_separate' (a + δ) (an - δ.toNat) b bn := by simp_mem
+  (hδ : δ < b - a): mem_separate' (a + δ) (an - δ.toNat) b bn := by mem_omega
 /-- If `[a..an)⟂[b..bn)`, and `a ≤ b`, then `[a'..an+(a-a'))⟂[b..bn)`.
 This lets us increase the size of the left memory region.
 -/
 theorem mem_separate_move_of_lt_of_le  (h : mem_separate' a an b bn)
   (hab : a < b)
-  (hlegal : a' ≤ a) : mem_separate' a' (an + (a - a').toNat) b bn := by simp_mem
+  (hlegal : a' ≤ a) : mem_separate' a' (an + (a - a').toNat) b bn := by mem_omega
 
 end MathProperties
 
@@ -416,12 +440,12 @@ section PairwiseSeparate
   /- Check that a direct implication of the pairwise separation is proven. -/
   theorem pairwise_direct (h : Memory.Region.pairwiseSeparate [⟨a, 100⟩, ⟨b, 200⟩, ⟨c, 300⟩, ⟨d, 400⟩]) :
     mem_separate' a 100 b 200 := by
-    simp_mem
+    mem_omega
 
   /- Check that a direct implication of the pairwise separation is proven. -/
   theorem pairwise_subset (h : Memory.Region.pairwiseSeparate [⟨a, 100⟩, ⟨b, 200⟩, ⟨c, 300⟩, ⟨d, 400⟩]) :
     mem_separate' a 80 b 100 := by
-    simp_mem
+    mem_omega
 
 end PairwiseSeparate
 
@@ -435,14 +459,6 @@ error: unsolved goals
 ---
 info: [simp_mem.info] Searching for Hypotheses
 [simp_mem.info] Summary: Found 0 hypotheses
-[simp_mem.info] ⚙️ Matching on ⊢ False
-[simp_mem.info] Unknown memory expression ⊢ False. Trying reduction to omega (`config.useOmegaToClose = true`):
-  [simp_mem.info] Adding omega facts from hypotheses
-  [simp_mem.info] Executing `omega` to close False
-  [simp_mem.info] goal (Note: can be large)
-    [simp_mem.info] ⊢ False
-  [simp_mem.info] ❌️ `omega` failed with error:
-      simp_all made no progress
 [simp_mem.info] Performing Rewrite At Main Goal
   [simp_mem.info] Simplifying goal.
 [simp_mem.info] ❌️ No progress made in this iteration. halting.
@@ -460,14 +476,6 @@ error: ❌️ simp_mem failed to make any progress.
 ---
 info: [simp_mem.info] Searching for Hypotheses
 [simp_mem.info] Summary: Found 0 hypotheses
-[simp_mem.info] ⚙️ Matching on ⊢ False
-[simp_mem.info] Unknown memory expression ⊢ False. Trying reduction to omega (`config.useOmegaToClose = true`):
-  [simp_mem.info] Adding omega facts from hypotheses
-  [simp_mem.info] Executing `omega` to close False
-  [simp_mem.info] goal (Note: can be large)
-    [simp_mem.info] ⊢ False
-  [simp_mem.info] ❌️ `omega` failed with error:
-      simp_all made no progress
 [simp_mem.info] Performing Rewrite At Main Goal
   [simp_mem.info] Simplifying goal.
 [simp_mem.info] ❌️ No progress made in this iteration. halting.