diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean
index 01ce8224aa..d5098d0428 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean
@@ -35,9 +35,13 @@ Reconstruct bit by bit which value expression must have had which `BitVec` value
 expression - pair values.
 -/
 def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Array (Bool × Nat))
-    (aigSize : Nat) (atomsAssignment : Std.HashMap Nat (Nat × Expr)) :
+    (aigSize : Nat) (atomsAssignment : Std.HashMap Nat (Nat × Expr × Bool)) :
     Array (Expr × BVExpr.PackedBitVec) := Id.run do
   let mut sparseMap : Std.HashMap Nat (RBMap Nat Bool Ord.compare) := {}
+  let filter bvBit _ :=
+    let (_, _, synthetic) := atomsAssignment.get! bvBit.var
+    !synthetic
+  let var2Cnf := var2Cnf.filter filter
   for (bitVar, cnfVar) in var2Cnf.toArray do
     /-
     The setup of the variables in CNF is as follows:
@@ -70,7 +74,7 @@ def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Ar
       if bitValue then
         value := value ||| (1 <<< currentBit)
       currentBit := currentBit + 1
-    let atomExpr := atomsAssignment.get! bitVecVar |>.snd
+    let (_, atomExpr, _) := atomsAssignment.get! bitVecVar
     finalMap := finalMap.push (atomExpr, ⟨BitVec.ofNat currentBit value⟩)
   return finalMap
 
@@ -101,7 +105,7 @@ structure UnsatProver.Result where
   proof : Expr
   lratCert : LratCert
 
-abbrev UnsatProver := MVarId → ReflectionResult → Std.HashMap Nat (Nat × Expr) →
+abbrev UnsatProver := MVarId → ReflectionResult → Std.HashMap Nat (Nat × Expr × Bool) →
     MetaM (Except CounterExample UnsatProver.Result)
 
 /--
@@ -183,7 +187,7 @@ def explainCounterExampleQuality (counterExample : CounterExample) : MetaM Messa
     return err
 
 def lratBitblaster (goal : MVarId) (cfg : TacticContext) (reflectionResult : ReflectionResult)
-    (atomsAssignment : Std.HashMap Nat (Nat × Expr)) :
+    (atomsAssignment : Std.HashMap Nat (Nat × Expr × Bool)) :
     MetaM (Except CounterExample UnsatProver.Result) := do
   let bvExpr := reflectionResult.bvExpr
   let entry ←
@@ -253,7 +257,8 @@ def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) :
         reflectBV g
     trace[Meta.Tactic.bv] "Reflected bv logical expression: {reflectionResult.bvExpr}"
 
-    let atomsPairs := (← getThe State).atoms.toList.map (fun (expr, ⟨width, ident⟩) => (ident, (width, expr)))
+    let flipper := (fun (expr, {width, atomNumber, synthetic}) => (atomNumber, (width, expr, synthetic)))
+    let atomsPairs := (← getThe State).atoms.toList.map flipper
     let atomsAssignment := Std.HashMap.ofList atomsPairs
     match ← unsatProver g reflectionResult atomsAssignment with
     | .ok ⟨bvExprUnsat, cert⟩ =>
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
index bf4e4680bc..25187d8e57 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
@@ -107,6 +107,25 @@ where
 
 open Lean.Meta
 
+/--
+A `BitVec` atom.
+-/
+structure Atom where
+  /--
+  The width of the `BitVec` that is being abstracted.
+  -/
+  width : Nat
+  /--
+  A unique numeric identifier for the atom.
+  -/
+  atomNumber : Nat
+  /--
+  Whether the atom is synthetic. The effect of this is that values for this atom are not considered
+  for the counter example deriviation. This is for example useful when we introduce an atom over
+  an expression, together with additional lemmas that fully describe the behavior of the atom.
+  -/
+  synthetic : Bool
+
 /--
 The state of the reflection monad
 -/
@@ -115,7 +134,7 @@ structure State where
   The atoms encountered so far. Saved as a map from `BitVec` expressions to a (width, atomNumber)
   pair.
   -/
-  atoms : Std.HashMap Expr (Nat × Nat) := {}
+  atoms : Std.HashMap Expr Atom := {}
   /--
   A cache for `atomsAssignment`.
   -/
@@ -208,8 +227,8 @@ def run (m : M α) : MetaM α :=
 Retrieve the atoms as pairs of their width and expression.
 -/
 def atoms : M (List (Nat × Expr)) := do
-  let sortedAtoms := (← getThe State).atoms.toArray.qsort (·.2.2 < ·.2.2)
-  return sortedAtoms.map (fun (expr, width, _) => (width, expr)) |>.toList
+  let sortedAtoms := (← getThe State).atoms.toArray.qsort (·.2.atomNumber < ·.2.atomNumber)
+  return sortedAtoms.map (fun (expr, {width, ..}) => (width, expr)) |>.toList
 
 /--
 Retrieve a `BitVec.Assignment` representing the atoms we found so far.
@@ -220,16 +239,17 @@ def atomsAssignment : M Expr := do
 /--
 Look up an expression in the atoms, recording it if it has not previously appeared.
 -/
-def lookup (e : Expr) (width : Nat) : M Nat := do
+def lookup (e : Expr) (width : Nat) (synthetic : Bool) : M Nat := do
   match (← getThe State).atoms[e]? with
-  | some (width', ident) =>
-    if width != width' then
+  | some atom =>
+    if width != atom.width then
       panic! "The same atom occurs with different widths, this is a bug"
-    return ident
+    return atom.atomNumber
   | none =>
-    trace[Meta.Tactic.bv] "New atom of width {width}: {e}"
+    trace[Meta.Tactic.bv] "New atom of width {width}, synthetic? {synthetic}: {e}"
     let ident ← modifyGetThe State fun s =>
-      (s.atoms.size, { s with atoms := s.atoms.insert e (width, s.atoms.size) })
+      let newAtom := { width, synthetic, atomNumber := s.atoms.size}
+      (s.atoms.size, { s with atoms := s.atoms.insert e newAtom })
     updateAtomsAssignment
     return ident
 where
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean
index aeb0526e97..a7e5d1fb55 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean
@@ -32,10 +32,10 @@ def mkBVRefl (w : Nat) (expr : Expr) : Expr :=
    expr
 
 /--
-Register `e` as an atom of width `width`.
+Register `e` as an atom of `width` that might potentially be `synthetic`.
 -/
-def mkAtom (e : Expr) (width : Nat) : M ReifiedBVExpr := do
-  let ident ← M.lookup e width
+def mkAtom (e : Expr) (width : Nat) (synthetic : Bool) : M ReifiedBVExpr := do
+  let ident ← M.lookup e width synthetic
   let expr := mkApp2 (mkConst ``BVExpr.var) (toExpr width) (toExpr ident)
   let proof := do
     let evalExpr ← mkEvalExpr width expr
@@ -55,13 +55,13 @@ def getNatOrBvValue? (ty : Expr) (expr : Expr) : M (Option Nat) := do
   | _ => return none
 
 /--
-Construct an uninterpreted `BitVec` atom from `x`.
+Construct an uninterpreted `BitVec` atom from `x`, potentially `synthetic`.
 -/
-def bitVecAtom (x : Expr) : M (Option ReifiedBVExpr) := do
+def bitVecAtom (x : Expr) (synthetic : Bool) : M (Option ReifiedBVExpr) := do
   let t ← instantiateMVars (← whnfR (← inferType x))
   let_expr BitVec widthExpr := t | return none
   let some width ← getNatValue? widthExpr | return none
-  let atom ← mkAtom x width
+  let atom ← mkAtom x width synthetic
   return some atom
 
 /--
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean
index 76dae112c4..31cabd742f 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean
@@ -31,7 +31,7 @@ def boolAtom (t : Expr) : M (Option ReifiedBVPred) := do
   -/
   let ty ← inferType t
   let_expr Bool := ty | return none
-  let atom ← ReifiedBVExpr.mkAtom (mkApp (mkConst ``BitVec.ofBool) t) 1
+  let atom ← ReifiedBVExpr.mkAtom (mkApp (mkConst ``BitVec.ofBool) t) 1 false
   let bvExpr : BVPred := .getLsbD atom.bvExpr 0
   let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr 1) atom.expr (toExpr 0)
   let proof := do
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean
index 002ed92408..6aaeaf917d 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean
@@ -209,7 +209,7 @@ where
       let_expr Eq α discrExpr val := discrExpr | return none
       let_expr Bool := α | return none
       let_expr Bool.true := val | return none
-      let some atom ← ReifiedBVExpr.bitVecAtom x | return none
+      let some atom ← ReifiedBVExpr.bitVecAtom x 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
@@ -226,7 +226,7 @@ where
     let res ← go x
     match res with
     | some exp => return some exp
-    | none => ReifiedBVExpr.bitVecAtom x
+    | none => ReifiedBVExpr.bitVecAtom x false
 
   shiftConstLikeReflection (distance : Nat) (innerExpr : Expr) (shiftOp : Nat → BVUnOp)
       (shiftOpName : Name) (congrThm : Name) :
@@ -316,7 +316,7 @@ where
     return mkApp4 congrProof (toExpr inner.width) innerExpr innerEval innerProof
 
   goBvLit (x : Expr) : M (Option ReifiedBVExpr) := do
-    let some ⟨_, bvVal⟩ ← getBitVecValue? x | return ← ReifiedBVExpr.bitVecAtom x
+    let some ⟨_, bvVal⟩ ← getBitVecValue? x | return ← ReifiedBVExpr.bitVecAtom x false
     ReifiedBVExpr.mkBVConst bvVal
 
 /--
diff --git a/tests/lean/run/bv_counterexample.lean b/tests/lean/run/bv_counterexample.lean
index b4a66b8a97..e622ef3350 100644
--- a/tests/lean/run/bv_counterexample.lean
+++ b/tests/lean/run/bv_counterexample.lean
@@ -108,3 +108,11 @@ y = 0xffffffff#32
 #guard_msgs in
 example (x y : BitVec 32) (h1 : x.toNat = y.toNat) (h2 : x = zeros 32) : y = 0 := by
   bv_decide
+
+/--
+error: The prover found a counterexample, consider the following assignment:
+x = 0x3#2
+-/
+#guard_msgs in
+example (x : BitVec 2) : (bif x.ult 0#2 then 1#2 else 2#2) == 3#2 := by
+  bv_decide