diff --git a/Arm/Memory/Attr.lean b/Arm/Memory/Attr.lean
index b95cd9c4..810a65ec 100644
--- a/Arm/Memory/Attr.lean
+++ b/Arm/Memory/Attr.lean
@@ -23,3 +23,20 @@ register_simp_attr memory_omega
 
 -- Simprocs for address normalization
 register_simp_attr address_normalization
+
+register_option simp_mem.omegaTimeoutMs : Nat := {
+  defValue := 1000
+  descr := "maximum amount of time per omega invocation in milliseconds before `simp_mem` times out. `0` for no timeout."
+}
+
+register_option simp_mem.omegaNumIgnoredTimeouts: Nat := {
+  defValue := 0
+  descr := "number of times omega is allowed to timeout before an error is thrown."
+}
+
+
+def getOmegaTimeoutMs [Monad m] [MonadOptions m] : m Nat := do
+  return simp_mem.omegaTimeoutMs.get (← getOptions)
+
+def getOmegaNumIgnoredTimeouts [Monad m] [MonadOptions m] : m Nat := do
+  return simp_mem.omegaNumIgnoredTimeouts.get (← getOptions)
diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean
index 88b3c8da..2a37e6fe 100644
--- a/Arm/Memory/SeparateAutomation.lean
+++ b/Arm/Memory/SeparateAutomation.lean
@@ -15,6 +15,8 @@ import Arm.BitVec
 import Arm.Memory.Attr
 import Arm.Memory.AddressNormalization
 import Lean
+import Lean.Meta.ForEachExpr
+import Lean.Meta.ExprTraverse
 import Lean.Meta.Tactic.Rewrite
 import Lean.Meta.Tactic.Rewrites
 import Lean.Elab.Tactic.Conv
@@ -101,22 +103,12 @@ end BvOmega
 namespace SeparateAutomation
 
 structure SimpMemConfig where
+  /-- Locally turn on tracing for this particular invocation of 'simp_mem'. -/
+  trace : Bool := false
   /-- number of times rewrites must be performed. -/
   rewriteFuel : Nat := 1000
   /-- whether an error should be thrown if the tactic makes no progress. -/
   failIfUnchanged : Bool := true
-  /-- whether `simp_mem` should always try to use `omega` to close the goal,
-    even if goal state is not recognized as one of the blessed states.
-    This is useful when one is trying to establish some numerical invariant
-    about addresses based on knowledge of memory.
-    e.g.
-    ```
-    h : mem_separate' a 10 b 10
-    hab : a < b
-    ⊢ a + 5 < b
-    ```
-  -/
-  useOmegaToClose : Bool := false
 
 /-- Context for the `SimpMemM` monad, containing the user configurable options. -/
 structure Context where
@@ -343,14 +335,22 @@ instance : ToMessageData Hypothesis where
 structure State where
   hypotheses : Array Hypothesis := #[]
   rewriteFuel : Nat
+  changed : Bool := false
+  /-- Times taken by the `omega` tactic. -/
+  omegaTimingsMs : Array Nat := #[]
+  /-- Number of times omega has timed out. -/
+  omegaNumTimeouts : Nat := 0
 
 def State.init (cfg : SimpMemConfig) : State :=
   { rewriteFuel := cfg.rewriteFuel}
 
 abbrev SimpMemM := StateRefT State (ReaderT Context TacticM)
 
-def SimpMemM.run (m : SimpMemM α) (cfg : SimpMemConfig) : TacticM α :=
-  m.run' (State.init cfg) |>.run (Context.init cfg)
+def SimpMemM.run (m : SimpMemM α) (cfg : SimpMemConfig) : TacticM α := do
+  let insertTraceIfEnabled := fun (opts : Options) =>
+    if cfg.trace then opts.insert `simp_mem.trace.info true else opts
+  withOptions insertTraceIfEnabled do
+    m.run' (State.init cfg) |>.run (Context.init cfg)
 
 /-- Add a `Hypothesis` to our hypothesis cache. -/
 def SimpMemM.addHypothesis (h : Hypothesis) : SimpMemM Unit :=
@@ -421,17 +421,34 @@ def simpAndIntroDef (name : String) (hdefVal : Expr) : SimpMemM FVarId  := do
     let hdefVal ← simpResult.mkCast hdefVal
     let hdefTy ← inferType hdefVal
 
-    let goal ← goal.define name hdefTy hdefVal
+    let goal ← goal.assert name hdefTy hdefVal
     let (fvar, goal) ← goal.intro1P
     replaceMainGoal [goal]
     return fvar
 
+def pushOmegaTiming (goal : MVarId) (ms : Nat) : SimpMemM Unit := do
+  let s ← get
+  modify fun s => { s with omegaTimingsMs := s.omegaTimingsMs.push ms  }
+  if ms ≥ (← getOmegaTimeoutMs) then
+    let numTimeouts := s.omegaNumTimeouts + 1
+    modify fun s => { s with omegaNumTimeouts := numTimeouts }
+    if numTimeouts ≤ (← getOmegaNumIgnoredTimeouts) then
+      trace[simp_mem.info] m!"[simp_mem] 🚫 omega tactic took too long ({ms}ms) to run, but this is a permitted failure at occurrence {numTimeouts}. Goal: {indentD goal}"
+    else
+      throwError m!"[simp_mem] omega tactic took too long ({ms}ms) at occurrence {numTimeouts}. Goal: {indentD goal}"
+
+
 /-- SimpMemM's omega invoker -/
 def omega : SimpMemM Unit := do
+  let g ← getMainGoal
   -- https://leanprover.zulipchat.com/#narrow/stream/326056-ICERM22-after-party/topic/Regression.20tests/near/290131280
   -- @bollu: TODO: understand what precisely we are recovering from.
+  let startTime ← IO.monoMsNow
   withoutRecover do
+    -- TODO: replace this with filling in an MVar, sure, but not like this.
     evalTactic (← `(tactic| bv_omega))
+  let endTime ← IO.monoMsNow
+  pushOmegaTiming g (endTime - startTime)
 
 section Hypotheses
 
@@ -793,7 +810,7 @@ def proveWithOmega?  {α : Type} [ToMessageData α] [OmegaReducible α] (e : α)
     trace[simp_mem.info] "{checkEmoji} `omega` succeeded."
     return (.some <| Proof.mk (← instantiateMVars factProof))
   catch e =>
-    trace[simp_mem.info]  "{crossEmoji} `omega` failed with error:\n{e.toMessageData}"
+    trace[simp_mem.info]  "{crossEmoji} `omega` failed with error:{indentD e.toMessageData}"
     setGoals oldGoals
     return none
   end ReductionToOmega
@@ -813,6 +830,44 @@ def SimpMemM.rewriteWithEquality (rw : Expr) (msg : MessageData) : SimpMemM Unit
         throwError m!"{crossEmoji} internal error: expected rewrite to produce no side conditions. Produced {result.mvarIds}"
       replaceMainGoal [mvarId']
 
+-- /--
+-- Rewrites `e` via some `eq`, producing a proof `e = e'` for some `e'`.
+
+-- Rewrites with a fresh metavariable as the ambient goal.
+-- Fails if the rewrite produces any subgoals.
+-- -/
+-- -- source: https://github.com/leanprover-community/mathlib4/blob/b35703fe5a80f1fa74b82a2adc22f3631316a5b3/Mathlib/Lean/Expr/Basic.lean#L476-L477
+-- private def rewrite (e eq : Expr) : MetaM Expr := do
+--   let ⟨_, eq', []⟩ ← (← mkFreshExprMVar none).mvarId!.rewrite e eq
+--     | throwError "Expr.rewrite may not produce subgoals."
+--   return eq'
+
+-- /--
+-- Rewrites the type of `e` via some `eq`, then moves `e` into the new type via `Eq.mp`.
+
+-- Rewrites with a fresh metavariable as the ambient goal.
+-- Fails if the rewrite produces any subgoals.
+-- -/
+-- -- source: https://github.com/leanprover-community/mathlib4/blob/b35703fe5a80f1fa74b82a2adc22f3631316a5b3/Mathlib/Lean/Expr/Basic.lean#L476-L477
+-- private def rewriteType (e eq : Expr) : MetaM Expr := do
+--   mkEqMP (← rewrite (← inferType e) eq) e
+
+-- def ppExprWithInfos (ctx : PPContext) (e : Expr) (msg : MessageData) : MetaM FormatWithInfos := do
+--   let out : FormatWithInfos := {
+--     fmt := format (toString e),
+--     infos := RBMap.empty.insert 0 (.ofTermInfo { expr := e, lctx := ← getLCtx })
+--   }
+--   return out
+
+-- def SimpMemM.rewriteWithEqualityAtTarget (rw : Expr) (targetExpr : Expr) (msg : MessageData) : SimpMemM Expr := do
+--   withTraceNode msg do
+--     withMainContext do
+--       withTraceNode m!"rewrite (Note: can be large)" do
+--         trace[simp_mem.info] "{← inferType rw}"
+--       let targetExpr' ← rewriteType targetExpr rw
+--       return targetExpr'
+
+
 /--
 info: Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate' {x : BitVec 64} {xn : Nat} {y : BitVec 64} {yn : Nat}
   {mem : Memory} (hsep : mem_separate' x xn y yn) (val : BitVec (yn * 8)) :
@@ -872,6 +927,11 @@ def SimpMemM.rewriteReadOfSubsetWrite
       ew.val]
   SimpMemM.rewriteWithEquality call m!"rewriting read({er})⊆write({ew})"
 
+
+structure SimplifyExprResult where
+  e : Expr
+  changed : Bool
+
 mutual
 
 /--
@@ -879,7 +939,13 @@ Pattern match for memory patterns, and simplify them.
 Close memory side conditions with `simplifyGoal`.
 Returns if progress was made.
 -/
-partial def SimpMemM.simplifyExpr (e : Expr) (hyps : Array Hypothesis) : SimpMemM Bool := do
+partial def SimpMemM.simplifyExpr
+  (e : Expr)
+  (hyps : Array Hypothesis)
+  (useSeparate : Bool := false)
+  (useSubset : Bool := false)
+  (useOverlappingRead : Bool := false)
+  : SimpMemM Bool := do
   consumeRewriteFuel
   if ← outofRewriteFuel? then
     trace[simp_mem.info] "out of fuel for rewriting, stopping."
@@ -890,75 +956,71 @@ partial def SimpMemM.simplifyExpr (e : Expr) (hyps : Array Hypothesis) : SimpMem
     return false
 
   if let .some er := ReadBytesExpr.ofExpr? e then
+    trace[simp_mem.info] "{checkEmoji} Found read {er.span}."
     if let .some ew := WriteBytesExpr.ofExpr? er.mem then
-      trace[simp_mem.info] "{checkEmoji} Found read of write."
-      trace[simp_mem.info] "read: {er}"
-      trace[simp_mem.info] "write: {ew}"
+      trace[simp_mem.info] "{checkEmoji} Found read({er.span}) of write ({ew.span})."
       trace[simp_mem.info] "{processingEmoji} read({er.span})⟂/⊆write({ew.span})"
 
       let separate := MemSeparateProp.mk er.span ew.span
       let subset := MemSubsetProp.mk er.span ew.span
-      if let .some separateProof ← proveWithOmega? separate hyps then do
-        trace[simp_mem.info] "{checkEmoji} {separate}"
-        rewriteReadOfSeparatedWrite er ew separateProof
-        return true
-      else if let .some subsetProof ← proveWithOmega? subset hyps then do
-        trace[simp_mem.info] "{checkEmoji} {subset}"
-        rewriteReadOfSubsetWrite er ew subsetProof
-        return true
-      else
-        trace[simp_mem.info] "{crossEmoji} Could not prove {er.span} ⟂/⊆ {ew.span}"
-        return false
-    else
-      -- read
-      trace[simp_mem.info] "{checkEmoji} Found read {er}."
+      if useSeparate then
+        if let .some separateProof ← proveWithOmega? separate hyps then do
+          trace[simp_mem.info] "{checkEmoji} {separate}"
+          rewriteReadOfSeparatedWrite er ew separateProof
+          return true
+        else
+          trace[simp_mem.info] "{crossEmoji} {separate}"
+
+      if useSubset then
+        if let .some subsetProof ← proveWithOmega? subset hyps then do
+          trace[simp_mem.info] "{checkEmoji} {subset}"
+          rewriteReadOfSubsetWrite er ew subsetProof
+          return true
+        else
+          trace[simp_mem.info] "{crossEmoji} {separate}"
+
+    if useOverlappingRead then
       -- TODO: we don't need a separate `subset` branch for the writes: instead, for the write,
       -- we can add the theorem that `(write region).read = write val`.
       -- Then this generic theory will take care of it.
-      let changedInCurrentIter? ← withTraceNode m!"Searching for overlapping read {er.span}." do
-        let mut changedInCurrentIter? := false
-        for hyp in hyps do
-          if let Hypothesis.read_eq hReadEq := hyp then do
-            changedInCurrentIter? := changedInCurrentIter? ||
-              (← withTraceNode m!"{processingEmoji} ... ⊆ {hReadEq.read.span} ? " do
-                -- the read we are analyzing should be a subset of the hypothesis
-                let subset := (MemSubsetProp.mk er.span hReadEq.read.span)
-                if let some hSubsetProof ← proveWithOmega? subset hyps then
-                  trace[simp_mem.info] "{checkEmoji}  ... ⊆ {hReadEq.read.span}"
-                  rewriteReadOfSubsetRead er hReadEq hSubsetProof
-                  pure true
-                else
-                  trace[simp_mem.info] "{crossEmoji}  ... ⊊ {hReadEq.read.span}"
-                  pure false)
-        pure changedInCurrentIter?
-      return changedInCurrentIter?
+      trace[simp_mem.info] m!"Searching for overlapping read {er.span}."
+      for hyp in hyps do
+        if let Hypothesis.read_eq hReadEq := hyp then do
+          trace[simp_mem.info] "{processingEmoji} ... ⊆ {hReadEq.read.span} ? " do
+          -- the read we are analyzing should be a subset of the hypothesis
+          let subset := (MemSubsetProp.mk er.span hReadEq.read.span)
+          if let some hSubsetProof ← proveWithOmega? subset hyps then
+            trace[simp_mem.info] "{checkEmoji}  ... ⊆ {hReadEq.read.span}"
+            rewriteReadOfSubsetRead er hReadEq hSubsetProof
+            return true
+    return false
   else
     if e.isForall then
       Lean.Meta.forallTelescope e fun xs b => do
         let mut changedInCurrentIter? := false
         for x in xs do
-          changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr x hyps)
+          changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr x hyps useSeparate useSubset useOverlappingRead)
           -- we may have a hypothesis like
           -- ∀ (x : read_mem (read_mem_bytes ...) ... = out).
           -- we want to simplify the *type* of x.
-          changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr (← inferType x) hyps)
-        changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr b hyps)
+          changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr (← inferType x) hyps useSeparate useSubset useOverlappingRead)
+        changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr b hyps useSeparate useSubset useOverlappingRead)
         return changedInCurrentIter?
     else if e.isLambda then
       Lean.Meta.lambdaTelescope e fun xs b => do
         let mut changedInCurrentIter? := false
         for x in xs do
-          changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr x hyps)
-          changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr (← inferType x) hyps)
-        changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr b hyps)
+          changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr x hyps useSeparate useSubset useOverlappingRead)
+          changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr (← inferType x) hyps useSeparate useSubset useOverlappingRead)
+        changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr b hyps useSeparate useSubset useOverlappingRead)
         return changedInCurrentIter?
     else
       -- check if we have expressions.
       match e with
       | .app f x =>
         let mut changedInCurrentIter? := false
-        changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr f hyps)
-        changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr x hyps)
+        changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr f hyps useSeparate useSubset useOverlappingRead)
+        changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr x hyps useSeparate useSubset useOverlappingRead)
         return changedInCurrentIter?
       | _ => return false
 
@@ -983,24 +1045,6 @@ 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
-
-    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
   return ← g.isAssigned
 
 
@@ -1014,7 +1058,7 @@ partial def SimpMemM.simplifyGoal (g : MVarId) (hyps : Array Hypothesis) : SimpM
   SimpMemM.withContext g do
     let gt ← g.getType
     let changedInCurrentIter? ← withTraceNode m!"Simplifying goal." do
-        SimpMemM.simplifyExpr (← whnf gt) hyps
+        SimpMemM.simplifyExpr (← whnf gt) hyps (useSeparate := true) (useSubset := true) (useOverlappingRead := true)
     return changedInCurrentIter?
 end
 
@@ -1056,6 +1100,30 @@ partial def SimpMemM.simplifyLoop : SimpMemM Unit := do
     /- we haven't changed ever.. -/
     if !changedInAnyIter? && (← getConfig).failIfUnchanged then
         throwError "{crossEmoji} simp_mem failed to make any progress."
+
+def simpMemSpecialized (useSeparate : Bool) (useSubset : Bool) (useOverlappingRead : Bool) : SimpMemM Unit := do
+  let g ← getMainGoal
+  let gt ← getMainTarget
+  g.withContext do
+    let hyps := (← getLocalHyps)
+    let foundHyps : Array Hypothesis ← SimpMemM.withTraceNode m!"Searching for Hypotheses" do
+      let mut foundHyps : Array Hypothesis := #[]
+      for h in hyps do
+        foundHyps ← hypothesisOfExpr h foundHyps
+      pure foundHyps
+
+    SimpMemM.withTraceNode m!"Summary: Found {foundHyps.size} hypotheses" do
+    for (i, h) in foundHyps.toList.enum do
+      trace[simp_mem.info] m!"{i+1}) {h}"
+
+    let changed? ← SimpMemM.simplifyExpr (← whnf gt) foundHyps (useSeparate := useSeparate) (useSubset := useSubset) (useOverlappingRead := useOverlappingRead)
+    if !changed? then
+      throwError "{crossEmoji} simp_mem failed to make any progress."
+
+  def simpMemSeparate : SimpMemM Unit := simpMemSpecialized (useSeparate := true) (useSubset := false) (useOverlappingRead := false)
+  def simpMemSubset : SimpMemM Unit := simpMemSpecialized (useSeparate := false) (useSubset := true) (useOverlappingRead := false)
+  def simpMemOverlappingRead : SimpMemM Unit := simpMemSpecialized (useSeparate := false) (useSubset := false) (useOverlappingRead := true)
+
 end Simplify
 
 /--
@@ -1070,6 +1138,27 @@ def simpMem (cfg : SimpMemConfig := {}) : TacticM Unit := do
 /-- The `simp_mem` tactic, for simplifying away statements about memory. -/
 def simpMemTactic (cfg : SimpMemConfig) : TacticM Unit := simpMem cfg
 
+/-- The `mem_omega` finishing tactic, to close arithmetic related goals about memory addresses. -/
+def memOmegaTactic : TacticM Unit := do
+  SimpMemM.run (cfg := {}) do
+    let g ← getMainGoal
+    g.withContext do
+      let hyps := (← getLocalHyps)
+      let foundHyps ← SimpMemM.withTraceNode m!"Searching for Hypotheses" do
+        let mut foundHyps : Array Hypothesis := #[]
+        for h in hyps do
+          foundHyps ← hypothesisOfExpr h foundHyps
+        pure foundHyps
+
+      SimpMemM.withMainContext do
+      let _ ← Hypothesis.addOmegaFactsOfHyps foundHyps.toList #[]
+      trace[simp_mem.info] m!"Executing `omega` to close goal."
+      SimpMemM.withTraceNode m!"goal (Note: can be large)" do
+        trace[simp_mem.info] "{← getMainGoal}"
+      omega
+      trace[simp_mem.info] "{checkEmoji} `omega` succeeded."
+    return ()
+
 end SeparateAutomation
 
 /--
@@ -1077,14 +1166,43 @@ Allow elaboration of `SimpMemConfig` arguments to tactics.
 -/
 declare_config_elab elabSimpMemConfig SeparateAutomation.SimpMemConfig
 
+/--
+Direct `simp_mem` to assume certain memory relationships when trying to rewrite the context.
+· ⟂w direct `simp_mem` to assume that the write is separated from the read.
+· ⊆w directs `simp_mem` to assume that the read is a subset of a write.
+· ⊆r directs `simp_mem` to assume that the read is a subset of a read in the hypothesis.
+-/
+syntax simpMemTarget := "⟂" <|> "⊆w" <|> "⊆r"
+
 /--
 Implement the simp_mem tactic frontend.
 -/
-syntax (name := simp_mem) "simp_mem" (Lean.Parser.Tactic.config)? : tactic
+syntax (name := simp_mem) "simp_mem" (Lean.Parser.Tactic.config)? (simpMemTarget)? : tactic
+
+/--
+Use the `simp_mem` preprocessing to automatically close goals that involve
+reasoning about addresses in memory.
+-/
+syntax (name := mem_omega) "mem_omega" : tactic
 
 @[tactic simp_mem]
 def evalSimpMem : Tactic := fun
   | `(tactic| simp_mem $[$cfg]?) => do
     let cfg ← elabSimpMemConfig (mkOptionalNode cfg)
     SeparateAutomation.simpMemTactic cfg
+  | `(tactic| simp_mem $[$cfg]? ⟂) => do
+    let cfg ← elabSimpMemConfig (mkOptionalNode cfg)
+    SeparateAutomation.SimpMemM.run SeparateAutomation.simpMemSeparate cfg
+  | `(tactic| simp_mem $[$cfg]? ⊆w) => do
+    let cfg ← elabSimpMemConfig (mkOptionalNode cfg)
+    SeparateAutomation.SimpMemM.run SeparateAutomation.simpMemSubset cfg
+  | `(tactic| simp_mem $[$cfg]? ⊆r) => do
+    let cfg ← elabSimpMemConfig (mkOptionalNode cfg)
+    SeparateAutomation.SimpMemM.run SeparateAutomation.simpMemOverlappingRead cfg
   | _ => throwUnsupportedSyntax
+
+@[tactic mem_omega]
+def evalMemOmega : Tactic := fun
+| `(tactic| mem_omega) =>
+  SeparateAutomation.memOmegaTactic
+| _ => throwUnsupportedSyntax
diff --git a/Correctness/Correctness.lean b/Correctness/Correctness.lean
index 1ec8b9c9..cb384a2f 100644
--- a/Correctness/Correctness.lean
+++ b/Correctness/Correctness.lean
@@ -216,6 +216,43 @@ theorem partial_correctness_from_verification_conditions [Sys σ] [Spec' σ]
         ⟨n, Nat.le_refl _, hexit, hpost⟩
     find 0 (v1 s0 hp) (Nat.zero_le ..)
 
+
+/--
+Prove partial correctness using inductive assertions and functions
+`csteps` and `nextc`.
+
+We use `s0`, `si`, and `sf` to refer to initial, intermediate, and
+final (exit) states respectively.
+
+This is Theorem 1 from page 5 of the paper. This proof method is more
+convenient to use than `partial_correctness_by_stepwise_invariants`
+because we need only attach assertions at certain cutpoints. However,
+it may still be tedious to use from the point of view of automation
+because it is difficult to both symbolically simulate an instruction
+and unwind `csteps` in tandem. So far, we have found that it is
+easiest to determine what concrete value `csteps` yields (via symbolic
+simulation), and then perform symbolic simulation -- however, then we
+end up doing simulation twice, which is expensive.
+
+Also see `partial_correctness_from_assertions`.
+-/
+theorem partial_correctness_from_verification_conditions_concrete_num_steps [Sys σ] [Spec' σ]
+    (csteps' : σ → Nat) -- a computable function that tells us the number of steps.
+    (hnsteps : ∀ (s0 si : σ), (hs : assert s0 si) →
+      run si (csteps' si) = (nextc (run si 1))) -- csteps' si is the steps till the next cutpoint.
+    (v1 : ∀ s0 : σ, pre s0 → assert s0 s0)
+    (v2 : ∀ sf : σ, exit sf → cut sf)
+    (v3 : ∀ s0 sf : σ, assert s0 sf → exit sf → post s0 sf)
+    -- We use `run` since it plays well with `sym_n` proof automation.
+    (v4 : ∀ s0 si : σ, assert s0 si → ¬ exit si → assert s0 (run si (csteps' si)))
+    : PartialCorrectness σ := by
+  intro s0 n hp hexit
+  apply partial_correctness_from_verification_conditions <;> try assumption
+  intros s0' si' hassert' hexit'
+  specialize (v4 s0' si' hassert' hexit')
+  rw [← hnsteps s0' si' hassert']
+  exact v4
+
 ----------------------------------------------------------------------
 
 /-!
diff --git a/Proofs/AES-GCM/GCMGmultV8Sym.lean b/Proofs/AES-GCM/GCMGmultV8Sym.lean
index 6a5ecc7a..57ee57a5 100644
--- a/Proofs/AES-GCM/GCMGmultV8Sym.lean
+++ b/Proofs/AES-GCM/GCMGmultV8Sym.lean
@@ -91,7 +91,7 @@ theorem gcm_gmult_v8_program_run_27 (s0 sf : ArmState)
   · simp only [List.mem_cons, List.mem_singleton, not_or, and_imp]
     sym_aggregate
   · intro n addr h_separate
-    simp_mem (config := { useOmegaToClose := false })
+    simp_mem
     -- Aggregate the memory (non)effects.
     simp only [*]
   done
diff --git a/Proofs/Experiments/Memcpy/MemCpyVCG.lean b/Proofs/Experiments/Memcpy/MemCpyVCG.lean
index 76eeff7e..172f1616 100644
--- a/Proofs/Experiments/Memcpy/MemCpyVCG.lean
+++ b/Proofs/Experiments/Memcpy/MemCpyVCG.lean
@@ -440,10 +440,28 @@ end CutTheorems
 
 section PartialCorrectness
 
+/-
+tactic execution of Lean.Parser.Tactic.omega took 290ms
+tactic execution of Lean.Parser.Tactic.omega took 1.81s
+tactic execution of simp_mem took 751ms
+tactic execution of Lean.Parser.Tactic.omega took 1.11s
+tactic execution of Lean.Parser.Tactic.omega took 664ms
+tactic execution of Lean.Parser.Tactic.omega took 676ms
+instantiate metavars took 7.15s
+share common exprs took 3.9s
+type checking took 1.47s
+process pre-definitions took 440ms
+-/
 -- set_option skip_proof.skip true in
+set_option maxHeartbeats 0 in
 -- set_option trace.profiler true in
 -- set_option profiler true in
-set_option maxHeartbeats 0 in
+-- set_option trace.profiler true in
+-- set_option profiler true in
+set_option trace.simp_mem true
+set_option trace.simp_mem.info true
+set_option simp_mem.omegaNumIgnoredTimeouts 0 in
+set_option simp_mem.omegaTimeoutMs 1000 in
 theorem Memcpy.extracted_2 (s0 si : ArmState)
   (h_si_x0_nonzero : si.x0 ≠ 0)
   (h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64)))
@@ -471,7 +489,8 @@ theorem Memcpy.extracted_2 (s0 si : ArmState)
   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
-  have h_width_lt : (0x10#64).toNat * (s0.x0 - (si.x0 - 0x1#64)).toNat < 2 ^ 64 := by simp_mem (config := {useOmegaToClose := true})
+  have h_width_lt : (0x10#64).toNat * (s0.x0 - (si.x0 - 0x1#64)).toNat < 2 ^ 64 := by
+    sorry
   rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate']
   · rw [h_assert_6]
     skip_proof simp_mem
@@ -482,10 +501,41 @@ theorem Memcpy.extracted_2 (s0 si : ArmState)
       skip_proof refine ⟨?_, ?_, ?_, ?_⟩ <;> skip_proof bv_omega
     · apply mem_subset'_refl hsep.hb
 
+
+/-
+tactic execution of Lean.Parser.Tactic.omega took 1.54s
+tactic execution of simp_mem took 274ms
+tactic execution of Lean.Parser.Tactic.omega took 1.11s
+tactic execution of simp_mem took 403ms
+tactic execution of Lean.Parser.Tactic.omega took 302ms
+tactic execution of Lean.Parser.Tactic.omega took 284ms
+tactic execution of Lean.Parser.Tactic.omega took 4.25s
+tactic execution of simp_mem took 1.96s
+tactic execution of Lean.Parser.Tactic.omega took 8.95s
+tactic execution of simp_mem took 1.68s
+tactic execution of Lean.Parser.Tactic.omega took 102ms
+tactic execution of Lean.Parser.Tactic.omega took 1.9s
+tactic execution of simp_mem took 318ms
+tactic execution of Lean.Parser.Tactic.omega took 322ms
+tactic execution of Lean.Parser.Tactic.omega took 115ms
+tactic execution of Lean.Parser.Tactic.omega took 101ms
+instantiate metavars took 30s
+share common exprs took 16.7s
+fix level params took 118ms
+type checking took 4.37s
+process pre-definitions took 5.44s
+-/
+
+set_option maxHeartbeats 0
 -- set_option skip_proof.skip true in
 set_option maxHeartbeats 0 in
 -- set_option trace.profiler true in
 -- set_option profiler true in
+-- set_option trace.profiler true in
+-- set_option profiler true in
+set_option trace.simp_mem.info true
+set_option simp_mem.omegaNumIgnoredTimeouts 9999 in
+-- set_option simp_mem.omegaTimeoutMs 1000 in
 theorem Memcpy.extracted_0 (s0 si : ArmState)
   (h_si_x0_nonzero : si.x0 ≠ 0)
   (h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64)))
@@ -555,6 +605,23 @@ theorem Memcpy.extracted_0 (s0 si : ArmState)
   · intros n addr hsep
     apply Memcpy.extracted_2 <;> assumption
 
+/-
+tactic execution of Lean.Parser.Tactic.omega took 616ms
+tactic execution of Lean.Parser.Tactic.omega took 1.1s
+tactic execution of Lean.Parser.Tactic.assumption took 114ms
+instantiate metavars took 14.7s
+share common exprs took 1.94s
+type checking took 988ms
+-/
+
+set_option maxHeartbeats 0 in
+set_option trace.profiler true in
+set_option profiler true in
+set_option maxHeartbeats 0 in
+set_option trace.simp_mem.info true in
+set_option simp_mem.omegaNumIgnoredTimeouts 9999 in
+-- set_option trace.profiler true in
+-- set_option profiler true in
 -- set_option trace.profiler true in
 -- set_option profiler true in
 theorem partial_correctness :
@@ -673,7 +740,7 @@ theorem partial_correctness :
             simp only [memory_rules] at h_si_read_sep
             rw [h_si_read_sep]
             rw [h_si_x0_eq_zero]
-            skip_proof simp_mem -- nice!
+            skip_proof sorry -- nice!
           · simp only [step.h_err, step.h_program, step.h_sp_aligned, and_self]
       · have step_8f4_8e4 :=
           program.step_8f4_8e4_of_wellformed_of_z_eq_0 si s1 si_well_formed
diff --git a/Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted0Line583.lean b/Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted0Line583.lean
new file mode 100644
index 00000000..26482195
--- /dev/null
+++ b/Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted0Line583.lean
@@ -0,0 +1,111 @@
+import Arm.Memory.SeparateAutomation
+
+set_option linter.all false
+set_option maxHeartbeats 0
+set_option trace.profiler true
+set_option profiler true
+
+/-
+tactic execution of Lean.Parser.Tactic.omega took 3.71s
+instantiate metavars took 16.5s
+share common exprs took 3.59s
+type checking took 936ms
+process pre-definitions took 376ms
+elaboration took 2.32s
+-/
+theorem memcpy_extracted_0_line_585
+(h_si_x0_nonzero : six0 ≠ 0)
+(h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - six0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (six0 - 0x1#64)))
+(h_s0_x2 : s0.x2 + 0x10#64 * (s0.x0 - six0) + 0x10#64 = s0.x2 + 0x10#64 * (s0.x0 - (six0 - 0x1#64)))
+(h_assert_1 : six0 ≤ s0.x0)
+(h_assert_3 : six1 = s0.x1 + 0x10#64 * (s0.x0 - six0))
+(h_assert_4 : six2 = s0.x2 + 0x10#64 * (s0.x0 - six0))
+(h_pre_1 : mem_separate' s0.x1 (s0.x0.toNat * 16) s0.x2 (s0.x0.toNat * 16))
+(h_pre_2 : r StateField.PC s0 = 0x8e0#64)
+(h_pre_6 : 16 * s0.x0.toNat < 2 ^ 64)
+(h_subset_2 : mem_subset' s0.x2 (0x10#64 * (s0.x0 - six0)).toNat s0.x2 (s0.x0.toNat * 16))
+(h_subset_1 : mem_subset' (s0.x1 + 0x10#64 * (s0.x0 - six0)) 16 s0.x1 (s0.x0.toNat * 16))
+(s2_sum_inbounds : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hi : s0.x0 - six0 < s0.x0 - (six0 - 0x1#64))
+(i_sub_x0_mul_16 : 16 * (s0.x0 - six0).toNat < 16 * s0.x0.toNat)
+(hmemSeparate_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+  s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+    (s0.x1.toNat + s0.x0.toNat * 16 ≤ s0.x2.toNat ∨ s0.x1.toNat ≥ s0.x2.toNat + s0.x0.toNat * 16))
+(hmemLegal_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hmemLegal_omega : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hmemSubset_omega : s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - six0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤ 2 ^ 64 ∧
+  s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+    s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - six0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤
+      s0.x2.toNat + s0.x0.toNat * 16)
+(hmemLegal_omega : s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - six0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤ 2 ^ 64)
+(hmemLegal_omega : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hmemSubset_omega : (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - six0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤ 2 ^ 64 ∧
+  s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+    s0.x1.toNat ≤ (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - six0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 ∧
+      (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - six0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤
+        s0.x1.toNat + s0.x0.toNat * 16)
+(hmemLegal_omega : (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - six0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤ 2 ^ 64)
+(hmemLegal_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+: s0.x2.toNat + (0x10#64 * (s0.x0 - six0)).toNat ≤ 2 ^ 64 ∧
+  (s0.x1 + 0x10#64 * (s0.x0 - six0)).toNat + 16 ≤ 2 ^ 64 ∧
+    (s0.x2.toNat + (0x10#64 * (s0.x0 - six0)).toNat ≤ (s0.x1 + 0x10#64 * (s0.x0 - six0)).toNat ∨
+      s0.x2.toNat ≥ (s0.x1 + 0x10#64 * (s0.x0 - six0)).toNat + 16) := by
+  bv_omega
+
+
+#exit
+
+/-
+tactic execution of Lean.Parser.Tactic.omega took 3.67s
+instantiate metavars took 15.3s
+share common exprs took 3.28s
+type checking took 742ms
+process pre-definitions took 475ms
+linting took 262ms
+elaboration took 2.07s
+-/
+theorem memcpy_extracted_0_line_585
+(s0 si : ArmState)
+(h_si_x0_nonzero : si.x0 ≠ 0)
+(h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64)))
+(h_s0_x2 : s0.x2 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x2 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64)))
+(h_assert_1 : si.x0 ≤ s0.x0)
+(h_assert_3 : si.x1 = s0.x1 + 0x10#64 * (s0.x0 - si.x0))
+(h_assert_4 : si.x2 = s0.x2 + 0x10#64 * (s0.x0 - si.x0))
+(h_assert_6 : ∀ (n : Nat) (addr : BitVec 64),
+  mem_separate' s0.x2 (0x10#64 * (s0.x0 - si.x0)).toNat addr n →
+    Memory.read_bytes n addr si.mem = Memory.read_bytes n addr s0.mem)
+(h_assert_5 : ∀ (i : BitVec 64),
+  i < s0.x0 - si.x0 →
+    Memory.read_bytes 16 (s0.x2 + 0x10#64 * i) si.mem = Memory.read_bytes 16 (s0.x1 + 0x10#64 * i) s0.mem)
+(h_pre_1 : mem_separate' s0.x1 (s0.x0.toNat * 16) s0.x2 (s0.x0.toNat * 16))
+(h_pre_2 : r StateField.PC s0 = 0x8e0#64)
+(h_pre_6 : 16 * s0.x0.toNat < 2 ^ 64)
+(h_subset_2 : mem_subset' s0.x2 (0x10#64 * (s0.x0 - si.x0)).toNat s0.x2 (s0.x0.toNat * 16))
+(h_subset_1 : mem_subset' (s0.x1 + 0x10#64 * (s0.x0 - si.x0)) 16 s0.x1 (s0.x0.toNat * 16))
+(s2_sum_inbounds : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hi : s0.x0 - si.x0 < s0.x0 - (si.x0 - 0x1#64))
+(i_sub_x0_mul_16 : 16 * (s0.x0 - si.x0).toNat < 16 * s0.x0.toNat)
+(hmemSeparate_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+  s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+    (s0.x1.toNat + s0.x0.toNat * 16 ≤ s0.x2.toNat ∨ s0.x1.toNat ≥ s0.x2.toNat + s0.x0.toNat * 16))
+(hmemLegal_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hmemLegal_omega : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hmemSubset_omega : s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤ 2 ^ 64 ∧
+  s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+    s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤
+      s0.x2.toNat + s0.x0.toNat * 16)
+(hmemLegal_omega : s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤ 2 ^ 64)
+(hmemLegal_omega : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hmemSubset_omega : (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤ 2 ^ 64 ∧
+  s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+    s0.x1.toNat ≤ (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 ∧
+      (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤
+        s0.x1.toNat + s0.x0.toNat * 16)
+(hmemLegal_omega : (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤ 2 ^ 64)
+(hmemLegal_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+: s0.x2.toNat + (0x10#64 * (s0.x0 - si.x0)).toNat ≤ 2 ^ 64 ∧
+  (s0.x1 + 0x10#64 * (s0.x0 - si.x0)).toNat + 16 ≤ 2 ^ 64 ∧
+    (s0.x2.toNat + (0x10#64 * (s0.x0 - si.x0)).toNat ≤ (s0.x1 + 0x10#64 * (s0.x0 - si.x0)).toNat ∨
+      s0.x2.toNat ≥ (s0.x1 + 0x10#64 * (s0.x0 - si.x0)).toNat + 16) := by
+  bv_omega
diff --git a/Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted0Line586.lean b/Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted0Line586.lean
new file mode 100644
index 00000000..00663e2b
--- /dev/null
+++ b/Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted0Line586.lean
@@ -0,0 +1,63 @@
+import Arm
+import Arm.Memory.SeparateAutomation
+
+set_option maxHeartbeats 0
+set_option trace.profiler true 
+set_option profiler true
+
+
+/-
+tactic execution of Lean.Parser.Tactic.omega took 5.47s
+instantiate metavars took 7.69s
+share common exprs took 4.82s
+type checking took 860ms
+process pre-definitions took 1.59s
+linting took 353ms
+elaboration took 2.91s
+-/
+theorem memcpy 
+(s0 si : ArmState)
+(h_si_x0_nonzero : si.x0 ≠ 0)
+(h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64)))
+(h_s0_x2 : s0.x2 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x2 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64)))
+(h_assert_1 : si.x0 ≤ s0.x0)
+(h_assert_3 : si.x1 = s0.x1 + 0x10#64 * (s0.x0 - si.x0))
+(h_assert_4 : si.x2 = s0.x2 + 0x10#64 * (s0.x0 - si.x0))
+(h_assert_6 : ∀ (n : Nat) (addr : BitVec 64),
+  mem_separate' s0.x2 (0x10#64 * (s0.x0 - si.x0)).toNat addr n →
+    Memory.read_bytes n addr si.mem = Memory.read_bytes n addr s0.mem)
+(h_assert_5 : ∀ (i : BitVec 64),
+  i < s0.x0 - si.x0 →
+    Memory.read_bytes 16 (s0.x2 + 0x10#64 * i) si.mem = Memory.read_bytes 16 (s0.x1 + 0x10#64 * i) s0.mem)
+(h_pre_1 : mem_separate' s0.x1 (s0.x0.toNat * 16) s0.x2 (s0.x0.toNat * 16))
+(h_pre_2 : r StateField.PC s0 = 0x8e0#64)
+(h_pre_6 : 16 * s0.x0.toNat < 2 ^ 64)
+(h_subset_2 : mem_subset' s0.x2 (0x10#64 * (s0.x0 - si.x0)).toNat s0.x2 (s0.x0.toNat * 16))
+(h_subset_1 : mem_subset' (s0.x1 + 0x10#64 * (s0.x0 - si.x0)) 16 s0.x1 (s0.x0.toNat * 16))
+(s2_sum_inbounds : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hi : s0.x0 - si.x0 < s0.x0 - (si.x0 - 0x1#64))
+(i_sub_x0_mul_16 : 16 * (s0.x0 - si.x0).toNat < 16 * s0.x0.toNat)
+(hmemSeparate_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+   s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+     (s0.x1.toNat + s0.x0.toNat * 16 ≤ s0.x2.toNat ∨ s0.x1.toNat ≥ s0.x2.toNat + s0.x0.toNat * 16))
+(hmemLegal_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hmemLegal_omega : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hmemSubset_omega : s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤ 2 ^ 64 ∧
+   s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+     s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤
+       s0.x2.toNat + s0.x0.toNat * 16)
+(hmemLegal_omega : s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤ 2 ^ 64)
+(hmemLegal_omega: s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hmemSubset_omega : (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤ 2 ^ 64 ∧
+   s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+     s0.x1.toNat ≤ (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 ∧
+       (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤
+         s0.x1.toNat + s0.x0.toNat * 16)
+(hmemLegal_omega : (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤ 2 ^ 64)
+(hmemLegal_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64) :
+  (s0.x2 + 0x10#64 * (s0.x0 - si.x0)).toNat + 16 ≤ 2 ^ 64 ∧
+  (s0.x2 + 0x10#64 * (s0.x0 - si.x0)).toNat + 16 ≤ 2 ^ 64 ∧
+    (s0.x2 + 0x10#64 * (s0.x0 - si.x0)).toNat ≤ (s0.x2 + 0x10#64 * (s0.x0 - si.x0)).toNat ∧
+      (s0.x2 + 0x10#64 * (s0.x0 - si.x0)).toNat + 16 ≤ (s0.x2 + 0x10#64 * (s0.x0 - si.x0)).toNat + 16 := by
+  bv_omega
+
diff --git a/Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted2.lean b/Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted2.lean
new file mode 100644
index 00000000..60a299f1
--- /dev/null
+++ b/Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted2.lean
@@ -0,0 +1,60 @@
+import Arm
+import Arm.Memory.SeparateAutomation
+
+set_option maxHeartbeats 0 
+set_option trace.profiler true 
+set_option profiler true 
+
+
+/-
+tactic execution of Lean.Parser.Tactic.omega took 6.04s
+instantiate metavars took 31.6s
+share common exprs took 5.61s
+type checking took 1.36s
+process pre-definitions took 1.02s
+-/
+set_option maxHeartbeats 0 
+set_option trace.profiler true 
+set_option profiler true 
+theorem memcpy_extracted_2
+(s0 si : ArmState)
+(h_si_x0_nonzero : si.x0 ≠ 0)
+(h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64)))
+(h_s0_x2 : s0.x2 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x2 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64)))
+(h_assert_1 : si.x0 ≤ s0.x0)
+(h_assert_3 : si.x1 = s0.x1 + 0x10#64 * (s0.x0 - si.x0))
+(h_assert_4 : si.x2 = s0.x2 + 0x10#64 * (s0.x0 - si.x0))
+(h_assert_6 : ∀ (n : Nat) (addr : BitVec 64),
+  mem_separate' s0.x2 (0x10#64 * (s0.x0 - si.x0)).toNat addr n →
+    Memory.read_bytes n addr si.mem = Memory.read_bytes n addr s0.mem)
+(h_assert_5 : ∀ (i : BitVec 64),
+  i < s0.x0 - si.x0 →
+    Memory.read_bytes 16 (s0.x2 + 0x10#64 * i) si.mem = Memory.read_bytes 16 (s0.x1 + 0x10#64 * i) s0.mem)
+(h_pre_1 : mem_separate' s0.x1 (s0.x0.toNat * 16) s0.x2 (s0.x0.toNat * 16))
+(n : Nat)
+(addr : BitVec 64)
+(hsep : mem_separate' s0.x2 (0x10#64 * (s0.x0 - (si.x0 - 0x1#64))).toNat addr n)
+(h_le : (s0.x0 - (si.x0 - 0x1#64)).toNat ≤ s0.x0.toNat)
+(h_upper_bound : addr.toNat + n ≤ 2 ^ 64)
+(h_upper_bound₂ : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(h_upper_bound₃ : s0.x2.toNat + (0x10#64 * (s0.x0 - (si.x0 - 0x1#64))).toNat ≤ 2 ^ 64)
+(h_width_lt : (0x10#64).toNat * (s0.x0 - (si.x0 - 0x1#64)).toNat < 2 ^ 64)
+(hmemSeparate_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+  s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧
+    (s0.x1.toNat + s0.x0.toNat * 16 ≤ s0.x2.toNat ∨ s0.x1.toNat ≥ s0.x2.toNat + s0.x0.toNat * 16))
+(hmemLegal_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hmemLegal_omega : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64)
+(hmemSeparate_omega : s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - (2 ^ 64 - 1 % 2 ^ 64 + si.x0.toNat) % 2 ^ 64 + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤
+    2 ^ 64 ∧
+  addr.toNat + n ≤ 2 ^ 64 ∧
+    (s0.x2.toNat +
+          16 % 2 ^ 64 * ((2 ^ 64 - (2 ^ 64 - 1 % 2 ^ 64 + si.x0.toNat) % 2 ^ 64 + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤
+        addr.toNat ∨
+      s0.x2.toNat ≥ addr.toNat + n))
+(hmemLegal_omega : s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - (2 ^ 64 - 1 % 2 ^ 64 + si.x0.toNat) % 2 ^ 64 + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤
+  2 ^ 64)
+(hmemLegal_omega : addr.toNat + n ≤ 2 ^ 64) :
+ s0.x2.toNat + (0x10#64 * (s0.x0 - si.x0)).toNat ≤ 2 ^ 64 ∧
+  addr.toNat + n ≤ 2 ^ 64 ∧
+    (s0.x2.toNat + (0x10#64 * (s0.x0 - si.x0)).toNat ≤ addr.toNat ∨ s0.x2.toNat ≥ addr.toNat + n) := by
+    bv_omega
diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean
index a357172c..b601d1f0 100644
--- a/Proofs/Experiments/MemoryAliasing.lean
+++ b/Proofs/Experiments/MemoryAliasing.lean
@@ -47,7 +47,7 @@ theorem subset_3 (l : mem_subset' a 16 b 16) : mem_subset' (a+6) 10 b 16 := by
 
 /-- 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 (config := {useOmegaToClose := true})
+  mem_omega
 
 /-- Show that we can perform address arithmetic based on subset constraints.
 Only two configurations possible:
@@ -59,7 +59,7 @@ a0 a1 a2 ..
 b0 b1 b2 b3
 -/
 theorem subset_5 (l : mem_subset' a 3 b 4) : a ≤ b + 1 := by
-  simp_mem (config := {useOmegaToClose := true})
+  mem_omega
 
 end MemSubset
 
@@ -135,7 +135,7 @@ 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 (config := {useOmegaToClose := true})
+  mem_omega
 
 end MemSeparate
 
@@ -161,7 +161,7 @@ theorem mem_automation_test_2
   read_mem_bytes 16 src_addr (write_mem_bytes 16 dest_addr blah s0) =
   read_mem_bytes 16 src_addr s0 := by
   simp only [memory_rules]
-  simp_mem
+  simp_mem ⟂
   rfl
 
 
@@ -179,7 +179,7 @@ theorem mem_automation_test_3
   read_mem_bytes 10 (src_addr + 1) (write_mem_bytes ignore_n ignore_addr blah s0) =
    read_mem_bytes 10 (src_addr + 1) s0 := by
   simp only [memory_rules]
-  simp_mem
+  simp_mem ⟂
   rfl
 
 
@@ -198,7 +198,8 @@ theorem mem_automation_test_4
       (write_mem_bytes 48 src_addr val s0)) =
    val.extractLsBytes 1 10 := by
   simp only [memory_rules]
-  simp_mem
+  simp_mem ⟂
+  simp_mem ⊆w
   congr 1
   bv_omega -- TODO: address normalization.
 
@@ -226,7 +227,7 @@ theorem overlapping_read_test_2 {out : BitVec (16 * 8)}
     (h : read_mem_bytes 16 src_addr s = out) :
     read_mem_bytes 10 (src_addr + 6) s = out.extractLsBytes 6 10 := by
   simp only [memory_rules] at h ⊢
-  simp_mem
+  simp_mem ⊆r
   · congr
     -- ⊢ (src_addr + 6).toNat - src_addr.toNat = 6
     bv_omega
diff --git a/Proofs/Popcount32.lean b/Proofs/Popcount32.lean
index a00aa992..1fdbd872 100644
--- a/Proofs/Popcount32.lean
+++ b/Proofs/Popcount32.lean
@@ -70,6 +70,8 @@ def popcount32_program : Program :=
 
 #genStepEqTheorems popcount32_program
 
+-- raw `simp_mem`: time: 4786ms
+-- `simp_mem ⟂`: time: 4887ms
 theorem popcount32_sym_meets_spec (s0 sf : ArmState)
   (h_s0_pc         : read_pc s0 = 0x4005b4#64)
   (h_s0_program    : s0.program = popcount32_program)
@@ -103,7 +105,7 @@ theorem popcount32_sym_meets_spec (s0 sf : ArmState)
   · -- Memory Frame Condition
     intro n addr h_separate
     simp only [memory_rules] at *
-    repeat (simp_mem (config := { useOmegaToClose := false }); sym_aggregate)
+    repeat (simp_mem; sym_aggregate)
   done
 
 /--
diff --git a/Proofs/SHA512/SHA512Prelude.lean b/Proofs/SHA512/SHA512Prelude.lean
index 78a10f98..3a30429d 100644
--- a/Proofs/SHA512/SHA512Prelude.lean
+++ b/Proofs/SHA512/SHA512Prelude.lean
@@ -182,7 +182,7 @@ theorem sha512_block_armv8_prelude (s0 sf : ArmState)
   · constructor
     · -- (TODO @bollu) Think about whether `simp_mem` should be powerful enough to solve this goal.
       -- Also, `mem_omega` name suggestion from Alex for the already souped up `simp_mem`.
-      simp_mem (config := { useOmegaToClose := false } )
+      simp_mem
       simp only [h_s0_ctx_base, Nat.sub_self, minimal_theory, bitvec_rules]
     · constructor
       · -- (FIXME @bollu) simp_mem doesn't make progress here. :-(