diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean
index ba7b1eebc6..9841e17d05 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean
@@ -35,15 +35,15 @@ def mkContext (lratPath : System.FilePath) (cfg : BVDecideConfig) : TermElabM Ta
 /--
 Prepare an `Expr` that proves `bvExpr.unsat` using `ofReduceBool`.
 -/
-def lratChecker (ctx : TacticContext) (bvExpr : BVLogicalExpr) : MetaM Expr := do
+def lratChecker (ctx : TacticContext) (reflectionResult : ReflectionResult) : MetaM Expr := do
   let cert ← LratCert.ofFile ctx.lratPath ctx.config.trimProofs
-  cert.toReflectionProof ctx bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
+  cert.toReflectionProof ctx reflectionResult
 
 @[inherit_doc Lean.Parser.Tactic.bvCheck]
 def bvCheck (g : MVarId) (ctx : TacticContext) : MetaM Unit := do
   let unsatProver : UnsatProver := fun _ reflectionResult _ => do
     withTraceNode `Meta.Tactic.sat (fun _ => return "Preparing LRAT reflection term") do
-      let proof ← lratChecker ctx reflectionResult.bvExpr
+      let proof ← lratChecker ctx reflectionResult
       return .ok ⟨proof, ""⟩
   let _ ← closeWithBVReflection g unsatProver
   return ()
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean
index adda1025dc..393c2114eb 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean
@@ -79,9 +79,22 @@ def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Ar
   return finalMap
 
 structure ReflectionResult where
+  /--
+  The reflected expression.
+  -/
   bvExpr : BVLogicalExpr
+  /--
+  Function to prove `False` given a satisfiability proof of `bvExpr`
+  -/
   proveFalse : Expr → M Expr
+  /--
+  Set of unused hypotheses for diagnostic purposes.
+  -/
   unusedHypotheses : Std.HashSet FVarId
+  /--
+  A cache for `toExpr bvExpr`.
+  -/
+  expr : Expr
 
 /--
 A counter example generated from the bitblaster.
@@ -257,6 +270,54 @@ def explainCounterExampleQuality (counterExample : CounterExample) : MetaM Messa
   err := diagnosis.derivedEquations.foldl (init := err) folder
   return err
 
+/--
+Turn an `LratCert` into a proof that some `reflectedExpr` is UNSAT.
+-/
+def LratCert.toReflectionProof (cert : LratCert) (cfg : TacticContext)
+    (reflectionResult : ReflectionResult) : MetaM Expr := do
+  withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling expr term") do
+    mkAuxDecl cfg.exprDef reflectionResult.expr (mkConst ``BVLogicalExpr)
+
+  withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling proof certificate term") do
+    mkAuxDecl cfg.certDef (toExpr cert) (mkConst ``String)
+
+  let reflectedExpr := mkConst cfg.exprDef
+  let certExpr := mkConst cfg.certDef
+
+  withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling reflection proof term") do
+    let auxValue := mkApp2 (mkConst ``verifyBVExpr) reflectedExpr certExpr
+    mkAuxDecl cfg.reflectionDef auxValue (mkConst ``Bool)
+
+  let auxType ← mkEq (mkConst cfg.reflectionDef) (toExpr true)
+  let auxProof :=
+    mkApp3
+      (mkConst ``Lean.ofReduceBool)
+      (mkConst cfg.reflectionDef)
+      (toExpr true)
+      (← mkEqRefl (toExpr true))
+  try
+    let auxLemma ←
+      -- disable async TC so we can catch its exceptions
+      withOptions (Elab.async.set · false) do
+        withTraceNode `Meta.Tactic.sat (fun _ => return "Verifying LRAT certificate") do
+          mkAuxLemma [] auxType auxProof
+    return mkApp3 (mkConst ``unsat_of_verifyBVExpr_eq_true) reflectedExpr certExpr (mkConst auxLemma)
+  catch e =>
+    throwError m!"Failed to check the LRAT certificate in the kernel:\n{e.toMessageData}"
+where
+  /--
+  Add an auxiliary declaration. Only used to create constants that appear in our reflection proof.
+  -/
+  mkAuxDecl (name : Name) (value type : Expr) : CoreM Unit :=
+    addAndCompile <| .defnDecl {
+      name := name,
+      levelParams := [],
+      type := type,
+      value := value,
+      hints := .abbrev,
+      safety := .safe
+    }
+
 def lratBitblaster (goal : MVarId) (ctx : TacticContext) (reflectionResult : ReflectionResult)
     (atomsAssignment : Std.HashMap Nat (Nat × Expr × Bool)) :
     MetaM (Except CounterExample UnsatProver.Result) := do
@@ -287,14 +348,13 @@ def lratBitblaster (goal : MVarId) (ctx : TacticContext) (reflectionResult : Ref
   match res with
   | .ok cert =>
     trace[Meta.Tactic.sat] "SAT solver found a proof."
-    let proof ← cert.toReflectionProof ctx bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
+    let proof ← cert.toReflectionProof ctx reflectionResult
     return .ok ⟨proof, cert⟩
   | .error assignment =>
     trace[Meta.Tactic.sat] "SAT solver found a counter example."
     let equations := reconstructCounterExample map assignment aigSize atomsAssignment
     return .error { goal, unusedHypotheses := reflectionResult.unusedHypotheses, equations }
 
-
 def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do
   let hyps ← getPropHyps
   let mut sats := #[]
@@ -314,12 +374,12 @@ def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do
   else
     let sat := sats[1:].foldl (init := sats[0]) SatAtBVLogical.and
     return {
-      bvExpr := sat.bvExpr,
+      bvExpr := ShareCommon.shareCommon sat.bvExpr,
       proveFalse := sat.proveFalse,
-      unusedHypotheses := unusedHypotheses
+      unusedHypotheses := unusedHypotheses,
+      expr := sat.expr
     }
 
-
 def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) :
     MetaM (Except CounterExample LratCert) := M.run do
   g.withContext do
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
index 328f9f595b..f221c90f9c 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
@@ -142,6 +142,11 @@ structure State where
   contained in `atoms`.
   -/
   atomsAssignmentCache : Option Expr := none
+  /--
+  Cached calls to `evalsAtAtoms` of various reflection structures. Whenever `atoms` is modified
+  this cache is invalidated as `evalsAtAtoms` relies on `atoms`.
+  -/
+  evalsAtCache : Std.HashMap Expr (Option Expr) := {}
 
 /--
 The reflection monad, used to track `BitVec` variables that we see as we traverse the context.
@@ -158,14 +163,26 @@ structure ReifiedBVExpr where
   -/
   bvExpr : BVExpr width
   /--
-  A proof that `bvExpr.eval atomsAssignment = originalBVExpr`, none if it holds by `rfl`.
+  The expression that was reflected, used for caching of `evalsAtAtoms`.
   -/
-  evalsAtAtoms : M (Option Expr)
+  originalExpr : Expr
+  /--
+  A proof that `bvExpr.eval atomsAssignment = originalExpr`, none if it holds by `rfl`.
+  -/
+  evalsAtAtoms' : M (Option Expr)
   /--
   A cache for `toExpr bvExpr`.
   -/
   expr : Expr
 
+def ReifiedBVExpr.evalsAtAtoms (reified : ReifiedBVExpr) : M (Option Expr) := do
+  match (← get).evalsAtCache[reified.originalExpr]? with
+  | some hit => return hit
+  | none =>
+    let proof? ← reified.evalsAtAtoms'
+    modify fun s => { s with evalsAtCache :=  s.evalsAtCache.insert reified.originalExpr proof? }
+    return proof?
+
 /--
 A reified version of an `Expr` representing a `BVPred`.
 -/
@@ -175,14 +192,26 @@ structure ReifiedBVPred where
   -/
   bvPred : BVPred
   /--
-  A proof that `bvPred.eval atomsAssignment = originalBVPredExpr`, none if it holds by `rfl`.
+  The expression that was reflected, usef for caching of `evalsAtAtoms`.
   -/
-  evalsAtAtoms : M (Option Expr)
+  originalExpr : Expr
+  /--
+  A proof that `bvPred.eval atomsAssignment = originalExpr`, none if it holds by `rfl`.
+  -/
+  evalsAtAtoms' : M (Option Expr)
   /--
   A cache for `toExpr bvPred`
   -/
   expr : Expr
 
+def ReifiedBVPred.evalsAtAtoms (reified : ReifiedBVPred) : M (Option Expr) := do
+  match (← get).evalsAtCache[reified.originalExpr]? with
+  | some hit => return hit
+  | none =>
+    let proof? ← reified.evalsAtAtoms'
+    modify fun s => { s with evalsAtCache :=  s.evalsAtCache.insert reified.originalExpr proof? }
+    return proof?
+
 /--
 A reified version of an `Expr` representing a `BVLogicalExpr`.
 -/
@@ -192,14 +221,26 @@ structure ReifiedBVLogical where
   -/
   bvExpr : BVLogicalExpr
   /--
-  A proof that `bvExpr.eval atomsAssignment = originalBVLogicalExpr`, none if it holds by `rfl`.
+  The expression that was reflected, usef for caching of `evalsAtAtoms`.
   -/
-  evalsAtAtoms : M (Option Expr)
+  originalExpr : Expr
+  /--
+  A proof that `bvExpr.eval atomsAssignment = originalExpr`, none if it holds by `rfl`.
+  -/
+  evalsAtAtoms' : M (Option Expr)
   /--
   A cache for `toExpr bvExpr`
   -/
   expr : Expr
 
+def ReifiedBVLogical.evalsAtAtoms (reified : ReifiedBVLogical) : M (Option Expr) := do
+  match (← get).evalsAtCache[reified.originalExpr]? with
+  | some hit => return hit
+  | none =>
+    let proof? ← reified.evalsAtAtoms'
+    modify fun s => { s with evalsAtCache :=  s.evalsAtCache.insert reified.originalExpr proof? }
+    return proof?
+
 /--
 A reified version of an `Expr` representing a `BVLogicalExpr` that we know to be true.
 -/
@@ -266,7 +307,15 @@ def lookup (e : Expr) (width : Nat) (synthetic : Bool) : M Nat := do
     trace[Meta.Tactic.bv] "New atom of width {width}, synthetic? {synthetic}: {e}"
     let ident ← modifyGetThe State fun s =>
       let newAtom := { width, synthetic, atomNumber := s.atoms.size}
-      (s.atoms.size, { s with atoms := s.atoms.insert e newAtom, atomsAssignmentCache := none })
+      let newAtomNumber := s.atoms.size
+      let s := {
+        s with
+          atoms := s.atoms.insert e newAtom,
+          -- must clear the caches as they depend on `atoms`.
+          atomsAssignmentCache := none
+          evalsAtCache := {}
+      }
+      (newAtomNumber, s)
     return ident
 
 @[specialize]
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean
index ff3853ec33..68adfc54f6 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean
@@ -39,7 +39,7 @@ def mkAtom (e : Expr) (width : Nat) (synthetic : Bool) : M ReifiedBVExpr := do
   let expr := mkApp2 (mkConst ``BVExpr.var) (toExpr width) (toExpr ident)
   -- This is safe because this proof always holds definitionally.
   let proof := pure none
-  return ⟨width, .var ident, proof, expr⟩
+  return ⟨width, .var ident, expr, proof, expr⟩
 
 /--
 Parse `expr` as a `Nat` or `BitVec` constant depending on `ty`.
@@ -71,7 +71,7 @@ def mkBVConst (val : BitVec w) : M ReifiedBVExpr := do
   let expr := mkApp2 (mkConst ``BVExpr.const) (toExpr w) (toExpr val)
   -- This is safe because this proof always holds definitionally.
   let proof := pure none
-  return ⟨w, bvExpr, proof, expr⟩
+  return ⟨w, bvExpr, toExpr val, proof, expr⟩
 
 end ReifiedBVExpr
 
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean
index 2700b9718d..e9b422dc73 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean
@@ -33,8 +33,9 @@ Construct a `ReifiedBVLogical` from `ReifiedBVPred` by wrapping it as an atom.
 def ofPred (bvPred : ReifiedBVPred) : M ReifiedBVLogical := do
   let boolExpr := .literal bvPred.bvPred
   let expr := mkApp2 (mkConst ``BoolExpr.literal) (mkConst ``BVPred) bvPred.expr
+  -- important: This must be the same proof as the bvPred one in order for the cache to be correct
   let proof := bvPred.evalsAtAtoms
-  return ⟨boolExpr, proof, expr⟩
+  return ⟨boolExpr, bvPred.originalExpr, proof, expr⟩
 
 /--
 Construct an uninterrpeted `Bool` atom from `t`.
@@ -51,14 +52,14 @@ def mkBoolConst (val : Bool) : M ReifiedBVLogical := do
   let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr val)
   -- This is safe because this proof always holds definitionally.
   let proof := pure none
-  return ⟨boolExpr, proof, expr⟩
+  return ⟨boolExpr, toExpr val, proof, expr⟩
 
 /--
 Construct the reified version of applying the gate in `gate` to `lhs` and `rhs`.
 This function assumes that `lhsExpr` and `rhsExpr` are the corresponding expressions to `lhs`
 and `rhs`.
 -/
-def mkGate (lhs rhs : ReifiedBVLogical) (lhsExpr rhsExpr : Expr) (gate : Gate) :
+def mkGate (lhs rhs : ReifiedBVLogical) (lhsExpr rhsExpr : Expr) (gate : Gate) (origExpr : Expr) :
     M ReifiedBVLogical := do
   let congrThm := congrThmOfGate gate
   let boolExpr := .gate gate lhs.bvExpr rhs.bvExpr
@@ -84,7 +85,7 @@ def mkGate (lhs rhs : ReifiedBVLogical) (lhsExpr rhsExpr : Expr) (gate : Gate) :
       lhsExpr rhsExpr
       lhsEvalExpr rhsEvalExpr
       lhsProof rhsProof
-  return ⟨boolExpr, proof, expr⟩
+  return ⟨boolExpr, origExpr, proof, expr⟩
 where
   congrThmOfGate (gate : Gate) : Name :=
     match gate with
@@ -97,7 +98,7 @@ where
 Construct the reified version of `Bool.not subExpr`.
 This function assumes that `subExpr` is the expression corresponding to `sub`.
 -/
-def mkNot (sub : ReifiedBVLogical) (subExpr : Expr) : M ReifiedBVLogical := do
+def mkNot (sub : ReifiedBVLogical) (subExpr : Expr) (origExpr : Expr) : M ReifiedBVLogical := do
   let boolExpr := .not sub.bvExpr
   let expr := mkApp2 (mkConst ``BoolExpr.not) (mkConst ``BVPred) sub.expr
   let proof := do
@@ -105,14 +106,14 @@ def mkNot (sub : ReifiedBVLogical) (subExpr : Expr) : M ReifiedBVLogical := do
     let some subProof ← sub.evalsAtAtoms | return none
     let subEvalExpr ← ReifiedBVLogical.mkEvalExpr sub.expr
     return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.not_congr) subExpr subEvalExpr subProof
-  return ⟨boolExpr, proof, expr⟩
+  return ⟨boolExpr, origExpr, proof, expr⟩
 
 /--
 Construct the reified version of `if discrExpr then lhsExpr else rhsExpr`.
 This function assumes that `discrExpr`, lhsExpr` and `rhsExpr` are the corresponding expressions to
 `discr`, `lhs` and `rhs`.
 -/
-def mkIte (discr lhs rhs : ReifiedBVLogical) (discrExpr lhsExpr rhsExpr : Expr) :
+def mkIte (discr lhs rhs : ReifiedBVLogical) (discrExpr lhsExpr rhsExpr : Expr) (origExpr : Expr) :
     M ReifiedBVLogical := do
   let boolExpr := .ite discr.bvExpr lhs.bvExpr rhs.bvExpr
   let expr :=
@@ -140,7 +141,7 @@ def mkIte (discr lhs rhs : ReifiedBVLogical) (discrExpr lhsExpr rhsExpr : Expr)
       discrExpr lhsExpr rhsExpr
       discrEvalExpr lhsEvalExpr rhsEvalExpr
       discrProof lhsProof rhsProof
-  return ⟨boolExpr, proof, expr⟩
+  return ⟨boolExpr, origExpr, proof, expr⟩
 
 end ReifiedBVLogical
 
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean
index d700b43be1..c6c46f1f0d 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean
@@ -19,9 +19,9 @@ open Lean.Meta
 namespace ReifiedBVPred
 
 /--
-Construct an uninterpreted `Bool` atom from `t`.
+Construct an uninterpreted `Bool` atom from `origExpr`.
 -/
-def boolAtom (t : Expr) : M (Option ReifiedBVPred) := do
+def boolAtom (origExpr : Expr) : M (Option ReifiedBVPred) := do
   /-
   Idea: we have t : Bool here, let's construct:
     BitVec.ofBool t : BitVec 1
@@ -29,9 +29,9 @@ def boolAtom (t : Expr) : M (Option ReifiedBVPred) := do
     BitVec.getLsb (BitVec.ofBool t) 0 : Bool
   We can prove that this is equivalent to `t`. This allows us to have boolean variables in BVPred.
   -/
-  let ty ← inferType t
+  let ty ← inferType origExpr
   let_expr Bool := ty | return none
-  let atom ← ReifiedBVExpr.mkAtom (mkApp (mkConst ``BitVec.ofBool) t) 1 false
+  let atom ← ReifiedBVExpr.mkAtom (mkApp (mkConst ``BitVec.ofBool) origExpr) 1 false
   let bvExpr : BVPred := .getLsbD atom.bvExpr 0
   let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr 1) atom.expr (toExpr 0)
   let proof := do
@@ -41,18 +41,18 @@ def boolAtom (t : Expr) : M (Option ReifiedBVPred) := do
     let atomProof := (← atom.evalsAtAtoms).getD (ReifiedBVExpr.mkBVRefl atom.width atomEval)
     return mkApp3
       (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.ofBool_congr)
-      t
+      origExpr
       atomEval
       atomProof
-  return some ⟨bvExpr, proof, expr⟩
+  return some ⟨bvExpr, origExpr, proof, expr⟩
 
 /--
 Construct the reified version of applying the predicate in `pred` to `lhs` and `rhs`.
 This function assumes that `lhsExpr` and `rhsExpr` are the corresponding expressions to `lhs`
 and `rhs`.
 -/
-def mkBinPred (lhs rhs : ReifiedBVExpr) (lhsExpr rhsExpr : Expr) (pred : BVBinPred) :
-    M (Option ReifiedBVPred) := do
+def mkBinPred (lhs rhs : ReifiedBVExpr) (lhsExpr rhsExpr : Expr) (pred : BVBinPred)
+    (origExpr : Expr) : M (Option ReifiedBVPred) := do
   if h : lhs.width = rhs.width then
     let congrThm := congrThmofBinPred pred
     let bvExpr : BVPred := .bin (w := lhs.width) lhs.bvExpr pred (h ▸ rhs.bvExpr)
@@ -79,7 +79,7 @@ def mkBinPred (lhs rhs : ReifiedBVExpr) (lhsExpr rhsExpr : Expr) (pred : BVBinPr
         lhsExpr rhsExpr lhsEval rhsEval
         lhsProof
         rhsProof
-    return some ⟨bvExpr, proof, expr⟩
+    return some ⟨bvExpr, origExpr, proof, expr⟩
   else
     return none
 where
@@ -92,7 +92,8 @@ where
 Construct the reified version of `BitVec.getLsbD subExpr idx`.
 This function assumes that `subExpr` is the expression corresponding to `sub`.
 -/
-def mkGetLsbD (sub : ReifiedBVExpr) (subExpr : Expr) (idx : Nat) : M ReifiedBVPred := do
+def mkGetLsbD (sub : ReifiedBVExpr) (subExpr : Expr) (idx : Nat) (origExpr : Expr) :
+    M ReifiedBVPred := do
   let bvExpr : BVPred := .getLsbD sub.bvExpr idx
   let idxExpr := toExpr idx
   let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr sub.width) sub.expr idxExpr
@@ -107,7 +108,7 @@ def mkGetLsbD (sub : ReifiedBVExpr) (subExpr : Expr) (idx : Nat) : M ReifiedBVPr
       subExpr
       subEval
       subProof
-  return ⟨bvExpr, proof, expr⟩
+  return ⟨bvExpr, origExpr, proof, expr⟩
 
 end ReifiedBVPred
 
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean
index 554d3c2203..9739acae73 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean
@@ -37,15 +37,16 @@ where
     let resValExpr := lhs
     let lemmaName := ``Std.Tactic.BVDecide.Reflect.BitVec.cond_true
 
-
     let notDiscrExpr := mkApp (mkConst ``Bool.not) discrExpr
-    let notDiscr ← ReifiedBVLogical.mkNot discr discrExpr
+    let notDiscr ← ReifiedBVLogical.mkNot discr discrExpr notDiscrExpr
 
     let eqBVExpr ← mkAppM ``BEq.beq #[atomExpr, resExpr]
-    let some eqBVPred ← ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq | return none
+    let some eqBVPred ← ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq eqBVExpr
+      | return none
     let eqBV ← ReifiedBVLogical.ofPred eqBVPred
 
-    let imp ← ReifiedBVLogical.mkGate notDiscr eqBV notDiscrExpr eqBVExpr .or
+    let orExpr := mkApp2 (mkConst ``Bool.or) notDiscrExpr eqBVExpr
+    let imp ← ReifiedBVLogical.mkGate notDiscr eqBV notDiscrExpr eqBVExpr .or orExpr
 
     let proof := do
       let evalExpr ← ReifiedBVLogical.mkEvalExpr imp.expr
@@ -70,10 +71,12 @@ where
     let lemmaName := ``Std.Tactic.BVDecide.Reflect.BitVec.cond_false
 
     let eqBVExpr ← mkAppM ``BEq.beq #[atomExpr, resExpr]
-    let some eqBVPred ← ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq | return none
+    let some eqBVPred ← ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq eqBVExpr
+      | return none
     let eqBV ← ReifiedBVLogical.ofPred eqBVPred
 
-    let imp ← ReifiedBVLogical.mkGate discr eqBV discrExpr eqBVExpr .or
+    let orExpr := mkApp2 (mkConst ``Bool.or) discrExpr eqBVExpr
+    let imp ← ReifiedBVLogical.mkGate discr eqBV discrExpr eqBVExpr .or orExpr
 
     let proof := do
       let evalExpr ← ReifiedBVLogical.mkEvalExpr imp.expr
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean
index d5132acd05..4de8aa46ed 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean
@@ -24,29 +24,29 @@ Reify an `Expr` that's a constant-width `BitVec`.
 Unless this function is called on something that is not a constant-width `BitVec` it is always
 going to return `some`.
 -/
-partial def ReifiedBVExpr.of (x : Expr) : LemmaM (Option ReifiedBVExpr) := do
-  goOrAtom x
+partial def ReifiedBVExpr.of (origExpr : Expr) : LemmaM (Option ReifiedBVExpr) := do
+  goOrAtom origExpr
 where
   /--
   Reify `x`, returns `none` if the reification procedure failed.
   -/
-  go (x : Expr) : LemmaM (Option ReifiedBVExpr) := do
-    match_expr x with
-    | BitVec.ofNat _ _ => goBvLit x
+  go (origExpr : Expr) : LemmaM (Option ReifiedBVExpr) := do
+    match_expr origExpr with
+    | BitVec.ofNat _ _ => goBvLit origExpr
     | HAnd.hAnd _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.BitVec.and_congr
+      binaryReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.BitVec.and_congr origExpr
     | HXor.hXor _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.BitVec.xor_congr
+      binaryReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.BitVec.xor_congr origExpr
     | HAdd.hAdd _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .add ``Std.Tactic.BVDecide.Reflect.BitVec.add_congr
+      binaryReflection lhsExpr rhsExpr .add ``Std.Tactic.BVDecide.Reflect.BitVec.add_congr origExpr
     | HMul.hMul _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .mul ``Std.Tactic.BVDecide.Reflect.BitVec.mul_congr
+      binaryReflection lhsExpr rhsExpr .mul ``Std.Tactic.BVDecide.Reflect.BitVec.mul_congr origExpr
     | HDiv.hDiv _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .udiv ``Std.Tactic.BVDecide.Reflect.BitVec.udiv_congr
+      binaryReflection lhsExpr rhsExpr .udiv ``Std.Tactic.BVDecide.Reflect.BitVec.udiv_congr origExpr
     | HMod.hMod _ _ _ _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .umod ``Std.Tactic.BVDecide.Reflect.BitVec.umod_congr
+      binaryReflection lhsExpr rhsExpr .umod ``Std.Tactic.BVDecide.Reflect.BitVec.umod_congr origExpr
     | Complement.complement _ _ innerExpr =>
-      unaryReflection innerExpr .not ``Std.Tactic.BVDecide.Reflect.BitVec.not_congr
+      unaryReflection innerExpr .not ``Std.Tactic.BVDecide.Reflect.BitVec.not_congr origExpr
     | HShiftLeft.hShiftLeft _ β _ _ innerExpr distanceExpr =>
       let distance? ← ReifiedBVExpr.getNatOrBvValue? β distanceExpr
       if distance?.isSome then throwError "internal error: constant shift should have been eliminated."
@@ -57,6 +57,7 @@ where
         .shiftLeft
         ``BVExpr.shiftLeft
         ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeft_congr
+        origExpr
     | HShiftRight.hShiftRight _ β _ _ innerExpr distanceExpr =>
       let distance? ← ReifiedBVExpr.getNatOrBvValue? β distanceExpr
       if distance?.isSome then throwError "internal error: constant shift should have been eliminated."
@@ -67,6 +68,7 @@ where
         .shiftRight
         ``BVExpr.shiftRight
         ``Std.Tactic.BVDecide.Reflect.BitVec.shiftRight_congr
+        origExpr
     | BitVec.sshiftRight _ innerExpr distanceExpr =>
       let some distance ← getNatValue? distanceExpr | return none
       shiftConstLikeReflection
@@ -75,6 +77,7 @@ where
         .arithShiftRightConst
         ``BVUnOp.arithShiftRightConst
         ``Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRightNat_congr
+        origExpr
     | BitVec.sshiftRight' _ _ innerExpr distanceExpr =>
       shiftReflection
         distanceExpr
@@ -82,6 +85,7 @@ where
         .arithShiftRight
         ``BVExpr.arithShiftRight
         ``Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRight_congr
+        origExpr
     | HAppend.hAppend _ _ _ _ lhsExpr rhsExpr =>
       let some lhs ← goOrAtom lhsExpr | return none
       let some rhs ← goOrAtom rhsExpr | return none
@@ -109,7 +113,7 @@ where
           lhsExpr lhsEval
           rhsExpr rhsEval
           lhsProof rhsProof
-      return some ⟨lhs.width + rhs.width, bvExpr, proof, expr⟩
+      return some ⟨lhs.width + rhs.width, bvExpr, origExpr, proof, expr⟩
     | BitVec.replicate _ nExpr innerExpr =>
       let some inner ← goOrAtom innerExpr | return none
       let some n ← getNatValue? nExpr | return none
@@ -132,7 +136,7 @@ where
           innerExpr
           innerEval
           innerProof
-      return some ⟨inner.width * n, bvExpr, proof, expr⟩
+      return some ⟨inner.width * n, bvExpr, origExpr, proof, expr⟩
     | BitVec.extractLsb' _ startExpr lenExpr innerExpr =>
       let some start ← getNatValue? startExpr | return none
       let some len ← getNatValue? lenExpr | return none
@@ -154,7 +158,7 @@ where
           innerExpr
           innerEval
           innerProof
-      return some ⟨len, bvExpr, proof, expr⟩
+      return some ⟨len, bvExpr, origExpr, proof, expr⟩
     | BitVec.rotateLeft _ innerExpr distanceExpr =>
       rotateReflection
         distanceExpr
@@ -162,6 +166,7 @@ where
         .rotateLeft
         ``BVUnOp.rotateLeft
         ``Std.Tactic.BVDecide.Reflect.BitVec.rotateLeft_congr
+        origExpr
     | BitVec.rotateRight _ innerExpr distanceExpr =>
       rotateReflection
         distanceExpr
@@ -169,29 +174,30 @@ where
         .rotateRight
         ``BVUnOp.rotateRight
         ``Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr
+        origExpr
     | cond _ discrExpr lhsExpr rhsExpr =>
-      let some atom ← ReifiedBVExpr.bitVecAtom x true | return none
+      let some atom ← ReifiedBVExpr.bitVecAtom origExpr true | return none
       let some discr ← ReifiedBVLogical.of discrExpr | return none
       let some lhs ← goOrAtom lhsExpr | return none
       let some rhs ← goOrAtom rhsExpr | return none
-      addCondLemmas discr atom lhs rhs discrExpr x lhsExpr rhsExpr
+      addCondLemmas discr atom lhs rhs discrExpr origExpr lhsExpr rhsExpr
       return some atom
     | _ => return none
 
   /--
-  Reify `x` or abstract it as an atom.
+  Reify `origExpr` or abstract it as an atom.
   Unless this function is called on something that is not a fixed-width `BitVec` it is always going
   to return `some`.
   -/
-  goOrAtom (x : Expr) : LemmaM (Option ReifiedBVExpr) := do
-    LemmaM.withBVExprCache x fun x => do
-      let res ← go x
+  goOrAtom (origExpr : Expr) : LemmaM (Option ReifiedBVExpr) := do
+    LemmaM.withBVExprCache origExpr fun origExpr => do
+      let res ← go origExpr
       match res with
       | some exp => return some exp
-      | none => ReifiedBVExpr.bitVecAtom x false
+      | none => ReifiedBVExpr.bitVecAtom origExpr false
 
   shiftConstLikeReflection (distance : Nat) (innerExpr : Expr) (shiftOp : Nat → BVUnOp)
-      (shiftOpName : Name) (congrThm : Name) :
+      (shiftOpName : Name) (congrThm : Name) (origExpr : Expr) :
       LemmaM (Option ReifiedBVExpr) := do
     let some inner ← goOrAtom innerExpr | return none
     let bvExpr : BVExpr inner.width := .un (shiftOp distance) inner.bvExpr
@@ -206,17 +212,17 @@ where
         (mkConst congrThm)
         (toExpr distance)
     let proof := unaryCongrProof inner innerExpr congrProof
-    return some ⟨inner.width, bvExpr, proof, expr⟩
+    return some ⟨inner.width, bvExpr, origExpr, proof, expr⟩
 
   rotateReflection (distanceExpr : Expr) (innerExpr : Expr) (rotateOp : Nat → BVUnOp)
-      (rotateOpName : Name) (congrThm : Name) :
+      (rotateOpName : Name) (congrThm : Name) (origExpr : Expr) :
       LemmaM (Option ReifiedBVExpr) := do
     let some distance ← getNatValue? distanceExpr | return none
-    shiftConstLikeReflection distance innerExpr rotateOp rotateOpName congrThm
+    shiftConstLikeReflection distance innerExpr rotateOp rotateOpName congrThm origExpr
 
   shiftReflection (distanceExpr : Expr) (innerExpr : Expr)
       (shiftOp : {m n : Nat} → BVExpr m → BVExpr n → BVExpr m) (shiftOpName : Name)
-      (congrThm : Name) :
+      (congrThm : Name) (origExpr : Expr) :
       LemmaM (Option ReifiedBVExpr) := do
     let some inner ← goOrAtom innerExpr | return none
     let some distance ← goOrAtom distanceExpr | return none
@@ -234,9 +240,9 @@ where
         (toExpr inner.width)
         (toExpr distance.width)
     let proof := binaryCongrProof inner distance innerExpr distanceExpr congrProof
-    return some ⟨inner.width, bvExpr, proof, expr⟩
+    return some ⟨inner.width, bvExpr, origExpr, proof, expr⟩
 
-  binaryReflection (lhsExpr rhsExpr : Expr) (op : BVBinOp) (congrThm : Name) :
+  binaryReflection (lhsExpr rhsExpr : Expr) (op : BVBinOp) (congrThm : Name) (origExpr : Expr) :
       LemmaM (Option ReifiedBVExpr) := do
     let some lhs ← goOrAtom lhsExpr | return none
     let some rhs ← goOrAtom rhsExpr | return none
@@ -245,7 +251,7 @@ where
       let expr := mkApp4 (mkConst ``BVExpr.bin) (toExpr lhs.width) lhs.expr (toExpr op) rhs.expr
       let congrThm := mkApp (mkConst congrThm) (toExpr lhs.width)
       let proof := binaryCongrProof lhs rhs lhsExpr rhsExpr congrThm
-      return some ⟨lhs.width, bvExpr, proof, expr⟩
+      return some ⟨lhs.width, bvExpr, origExpr, proof, expr⟩
     else
       return none
 
@@ -262,13 +268,13 @@ where
         rhsEval rhsProof? | return none
     return mkApp6 congrThm lhsExpr rhsExpr lhsEval rhsEval lhsProof rhsProof
 
-  unaryReflection (innerExpr : Expr) (op : BVUnOp) (congrThm : Name) :
+  unaryReflection (innerExpr : Expr) (op : BVUnOp) (congrThm : Name) (origExpr : Expr) :
       LemmaM (Option ReifiedBVExpr) := do
     let some inner ← goOrAtom innerExpr | return none
     let bvExpr := .un op inner.bvExpr
     let expr := mkApp3 (mkConst ``BVExpr.un) (toExpr inner.width) (toExpr op) inner.expr
     let proof := unaryCongrProof inner innerExpr (mkConst congrThm)
-    return some ⟨inner.width, bvExpr, proof, expr⟩
+    return some ⟨inner.width, bvExpr, origExpr, proof, expr⟩
 
   unaryCongrProof (inner : ReifiedBVExpr) (innerExpr : Expr) (congrProof : Expr) : M (Option Expr) := do
     let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr
@@ -283,82 +289,83 @@ where
 Reify an `Expr` that is a predicate about `BitVec`.
 Unless this function is called on something that is not a `Bool` it is always going to return `some`.
 -/
-partial def ReifiedBVPred.of (t : Expr) : LemmaM (Option ReifiedBVPred) := do
-  LemmaM.withBVPredCache t fun t => do
-    match ← go t with
+partial def ReifiedBVPred.of (origExpr : Expr) : LemmaM (Option ReifiedBVPred) := do
+  LemmaM.withBVPredCache origExpr fun origExpr => do
+    match ← go origExpr with
     | some pred => return some pred
-    | none => ReifiedBVPred.boolAtom t
+    | none => ReifiedBVPred.boolAtom origExpr
 where
   /--
-  Reify `t`, returns `none` if the reification procedure failed.
+  Reify `origExpr`, returns `none` if the reification procedure failed.
   -/
-  go (t : Expr) : LemmaM (Option ReifiedBVPred) := do
-    match_expr t with
+  go (origExpr : Expr) : LemmaM (Option ReifiedBVPred) := do
+    match_expr origExpr with
     | BEq.beq α _ lhsExpr rhsExpr =>
       let_expr BitVec _ := α | return none
-      binaryReflection lhsExpr rhsExpr .eq
+      binaryReflection lhsExpr rhsExpr .eq origExpr
     | BitVec.ult _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .ult
+      binaryReflection lhsExpr rhsExpr .ult origExpr
     | BitVec.getLsbD _ subExpr idxExpr =>
       let some sub ← ReifiedBVExpr.of subExpr | return none
       let some idx ← getNatValue? idxExpr | return none
-      return some (← ReifiedBVPred.mkGetLsbD sub subExpr idx)
+      return some (← ReifiedBVPred.mkGetLsbD sub subExpr idx origExpr)
     | _ => return none
 
-  binaryReflection (lhsExpr rhsExpr : Expr) (pred : BVBinPred) : LemmaM (Option ReifiedBVPred) := do
+  binaryReflection (lhsExpr rhsExpr : Expr) (pred : BVBinPred) (origExpr : Expr) :
+      LemmaM (Option ReifiedBVPred) := do
     let some lhs ← ReifiedBVExpr.of lhsExpr | return none
     let some rhs ← ReifiedBVExpr.of rhsExpr | return none
-    ReifiedBVPred.mkBinPred lhs rhs lhsExpr rhsExpr pred
+    ReifiedBVPred.mkBinPred lhs rhs lhsExpr rhsExpr pred origExpr
 
 /--
 Reify an `Expr` that is a boolean expression containing predicates about `BitVec` as atoms.
 Unless this function is called on something that is not a `Bool` it is always going to return `some`.
 -/
-partial def ReifiedBVLogical.of (t : Expr) : LemmaM (Option ReifiedBVLogical) := do
-  goOrAtom t
+partial def ReifiedBVLogical.of (origExpr : Expr) : LemmaM (Option ReifiedBVLogical) := do
+  goOrAtom origExpr
 where
   /--
   Reify `t`, returns `none` if the reification procedure failed.
   -/
-  go (t : Expr) : LemmaM (Option ReifiedBVLogical) := do
-    match_expr t with
+  go (origExpr : Expr) : LemmaM (Option ReifiedBVLogical) := do
+    match_expr origExpr with
     | Bool.true => ReifiedBVLogical.mkBoolConst true
     | Bool.false => ReifiedBVLogical.mkBoolConst false
     | Bool.not subExpr =>
       let some sub ← goOrAtom subExpr | return none
-      return some (← ReifiedBVLogical.mkNot sub subExpr)
-    | Bool.and lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .and
-    | Bool.xor lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .xor
+      return some (← ReifiedBVLogical.mkNot sub subExpr origExpr)
+    | Bool.and lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .and origExpr
+    | Bool.xor lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .xor origExpr
     | BEq.beq α _ lhsExpr rhsExpr =>
       match_expr α with
-      | Bool => gateReflection lhsExpr rhsExpr .beq
-      | BitVec _ => goPred t
+      | Bool => gateReflection lhsExpr rhsExpr .beq origExpr
+      | BitVec _ => goPred origExpr
       | _ => return none
     | cond _ discrExpr lhsExpr rhsExpr =>
       let some discr ← goOrAtom discrExpr | return none
       let some lhs ← goOrAtom lhsExpr | return none
       let some rhs ← goOrAtom rhsExpr | return none
-      return some (← ReifiedBVLogical.mkIte discr lhs rhs discrExpr lhsExpr rhsExpr)
-    | _ => goPred t
+      return some (← ReifiedBVLogical.mkIte discr lhs rhs discrExpr lhsExpr rhsExpr origExpr)
+    | _ => goPred origExpr
 
   /--
   Reify `t` or abstract it as an atom.
   Unless this function is called on something that is not a `Bool` it is always going to return `some`.
   -/
-  goOrAtom (t : Expr) : LemmaM (Option ReifiedBVLogical) := do
-    LemmaM.withBVLogicalCache t fun t => do
-      match ← go t with
+  goOrAtom (origExpr : Expr) : LemmaM (Option ReifiedBVLogical) := do
+    LemmaM.withBVLogicalCache origExpr fun origExpr => do
+      match ← go origExpr with
       | some boolExpr => return some boolExpr
-      | none => ReifiedBVLogical.boolAtom t
+      | none => ReifiedBVLogical.boolAtom origExpr
 
-  gateReflection (lhsExpr rhsExpr : Expr) (gate : Gate) :
+  gateReflection (lhsExpr rhsExpr : Expr) (gate : Gate) (origExpr : Expr) :
       LemmaM (Option ReifiedBVLogical) := do
     let some lhs ← goOrAtom lhsExpr | return none
     let some rhs ← goOrAtom rhsExpr | return none
-    ReifiedBVLogical.mkGate lhs rhs lhsExpr rhsExpr gate
+    ReifiedBVLogical.mkGate lhs rhs lhsExpr rhsExpr gate origExpr
 
-  goPred (t : Expr) : LemmaM (Option ReifiedBVLogical) := do
-    let some pred ← ReifiedBVPred.of t | return none
+  goPred (origExpr : Expr) : LemmaM (Option ReifiedBVLogical) := do
+    let some pred ← ReifiedBVPred.of origExpr | return none
     ReifiedBVLogical.ofPred pred
 
 end
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean
index f1f28229b1..2b7267a577 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean
@@ -148,61 +148,5 @@ def runExternal (cnf : CNF Nat) (solver : System.FilePath) (lratPath : System.Fi
 
     return .ok lratProof
 
-/--
-Add an auxiliary declaration. Only used to create constants that appear in our reflection proof.
--/
-def mkAuxDecl (name : Name) (value type : Expr) : CoreM Unit :=
-  addAndCompile <| .defnDecl {
-    name := name,
-    levelParams := [],
-    type := type,
-    value := value,
-    hints := .abbrev,
-    safety := .safe
-  }
-
-/--
-Turn an `LratCert` into a proof that some `reflected` expression is UNSAT by providing a `verifier`
-function together with a correctness theorem for it.
-
-- `verifier` is expected to have type `α → LratCert → Bool`
-- `unsat_of_verifier_eq_true` is expected to have type
-  `∀ (b : α) (c : LratCert), verifier b c = true → unsat b`
--/
-def LratCert.toReflectionProof [ToExpr α] (cert : LratCert) (cfg : TacticContext) (reflected : α)
-    (verifier : Name) (unsat_of_verifier_eq_true : Name) : MetaM Expr := do
-  withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling expr term") do
-    mkAuxDecl cfg.exprDef (toExpr reflected) (toTypeExpr α)
-
-  let certType := toTypeExpr LratCert
-
-  withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling proof certificate term") do
-    mkAuxDecl cfg.certDef (toExpr cert) certType
-
-  let reflectedExpr := mkConst cfg.exprDef
-  let certExpr := mkConst cfg.certDef
-
-  withTraceNode `Meta.Tactic.sat (fun _ => return "Compiling reflection proof term") do
-    let auxValue := mkApp2 (mkConst verifier) reflectedExpr certExpr
-    mkAuxDecl cfg.reflectionDef auxValue (mkConst ``Bool)
-
-  let auxType ← mkEq (mkConst cfg.reflectionDef) (toExpr true)
-  let auxProof :=
-    mkApp3
-      (mkConst ``Lean.ofReduceBool)
-      (mkConst cfg.reflectionDef)
-      (toExpr true)
-      (← mkEqRefl (toExpr true))
-  try
-    let auxLemma ←
-      -- disable async TC so we can catch its exceptions
-      withOptions (Elab.async.set · false) do
-        withTraceNode `Meta.Tactic.sat (fun _ => return "Verifying LRAT certificate") do
-          mkAuxLemma [] auxType auxProof
-    return mkApp3 (mkConst unsat_of_verifier_eq_true) reflectedExpr certExpr (mkConst auxLemma)
-  catch e =>
-    throwError m!"Failed to check the LRAT certificate in the kernel:\n{e.toMessageData}"
-
-
 end Frontend
 end Lean.Elab.Tactic.BVDecide