memory: overlapping_read_test_4 hangs at bv_omega.

[bollu]

This test case needs to be reduced.

[shigoel]

@bollu plans to upstream this benchmark in omega's perf regression.

[bollu]

This was a really interesting bugfix, and was my bug. The simp_mem tactic tries to handle hypotheses of the form mem.read addr1 n1 = mem.read addr2 n2 by registering both sides as useful information that it should exploit.

However, the part that flips the equality forgot to flip the equality :)

Debugging this was enormously painful, because for whatever reason, the kernel spends an enormously long time checking the proof, and then gives up with "deterministic timeout". Regardless, here's the patch that fixes it:

@@ -314,7 +305,7 @@ we can have some kind of funny situation where both LHS and RHS are ReadBytes.
 For example, `mem1.read base1 n = mem2.read base2 n`.
 In such a scenario, we should record both reads.
 -/
-def ReadBytesEqProof.ofExpr? (eval : Expr) (etype : Expr) :  Array ReadBytesEqProof := Id.run do
+def ReadBytesEqProof.ofExpr? (eval : Expr) (etype : Expr) :  MetaM (Array ReadBytesEqProof) := do
   let mut out := #[]
   if let .some ⟨_ty, lhs, rhs⟩ := etype.eq? then do
     let lhs := lhs
@@ -323,7 +314,7 @@ def ReadBytesEqProof.ofExpr? (eval : Expr) (etype : Expr) :  Array ReadBytesEqPr
       out := out.push { val := rhs, read := read, h := eval }
 
     if let .some read := ReadBytesExpr.ofExpr? rhs then
-      out:= out.push { val := lhs, read := read, h := eval }
+      out:= out.push { val := lhs, read := read, h := ← mkEqSymm eval }
   return out
 
 inductive Hypothesis
@@ -358,8 +349,8 @@ def State.init (cfg : SimpMemConfig) : State :=