diff --git a/src/Init/Sym/Lemmas.lean b/src/Init/Sym/Lemmas.lean
index 17cb732cf5..46e9297a8c 100644
--- a/src/Init/Sym/Lemmas.lean
+++ b/src/Init/Sym/Lemmas.lean
@@ -33,15 +33,27 @@ theorem ite_cond_congr {α : Sort u} (c : Prop) {inst : Decidable c} (a b : α)
 theorem ite_true {α : Sort u} (c : Prop) {inst : Decidable c} (a b : α) {ht : c} : @ite α c inst a b = a := by
   simp [*]
 
+theorem ite_true_congr {α : Sort u} (c : Prop) {inst : Decidable c} (a b : α) (c' : Prop) (h : c = c') {ht : c'} : @ite α c inst a b = a := by
+  simp [*]
+
 theorem ite_false {α : Sort u} (c : Prop) {inst : Decidable c} (a b : α) {ht : ¬ c} : @ite α c inst a b = b := by
   simp [*]
 
+theorem ite_false_congr {α : Sort u} (c : Prop) {inst : Decidable c} (a b : α) (c' : Prop) (h : c = c') {ht : ¬ c'} : @ite α c inst a b = b := by
+  simp [*]
+
 theorem dite_true {α : Sort u} (c : Prop) {inst : Decidable c} (a : c → α) (b : ¬ c → α) {ht : c} : @dite α c inst a b = a ht := by
   simp [*]
 
+theorem dite_true_congr {α : Sort u} (c : Prop) {inst : Decidable c} (a : c → α) (b : ¬ c → α) (c' : Prop) (h : c = c') {ht : c'} : @dite α c inst a b = a (h.mpr_prop ht) := by
+  subst h; simp [*]
+
 theorem dite_false {α : Sort u} (c : Prop) {inst : Decidable c} (a : c → α) (b : ¬ c → α) {ht : ¬ c} : @dite α c inst a b = b ht := by
   simp [*]
 
+theorem dite_false_congr {α : Sort u} (c : Prop) {inst : Decidable c} (a : c → α) (b : ¬ c → α) (c' : Prop) (h : c = c') {ht : ¬ c'} : @dite α c inst a b = b (h.mpr_not ht) := by
+  subst h; simp [*]
+
 theorem dite_cond_congr {α : Sort u} (c : Prop) {inst : Decidable c} (a : c → α) (b : ¬ c → α)
     (c' : Prop) {inst' : Decidable c'} (h : c = c')
     : @dite α c inst a b = @dite α c' inst' (fun h' => a (h.mpr_prop h')) (fun h' => b (h.mpr_not h')) := by
diff --git a/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean b/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean
index 1658fdfb3d..4e73a25a19 100644
--- a/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean
+++ b/src/Lean/Meta/Tactic/Cbv/ControlFlow.lean
@@ -19,6 +19,8 @@ import Lean.Meta.AppBuilder
 import Init.Sym.Lemmas
 import Lean.Meta.Tactic.Cbv.TheoremsLookup
 import Lean.Meta.Tactic.Cbv.Opaque
+import Lean.Meta.Tactic.Cbv.CbvEvalExt
+import Lean.Compiler.NoncomputableAttr
 
 /-!
 # Control Flow Handling for Cbv
@@ -35,20 +37,47 @@ corresponding branch.
 namespace Lean.Meta.Sym.Simp
 open Internal
 
+def isCbvNoncomputable (p : Name) : CoreM Bool := do
+  let evalLemmas ← Tactic.Cbv.getCbvEvalLemmas p
+  return evalLemmas.isNone && Lean.isNoncomputable (← getEnv) p
+
+/--
+Attemps to synthesize `Decidable p` instance and guards against picking up a `noncomputable` instance
+-/
+def trySynthComputableInstance (p : Expr) : SymM <| Option Expr := do
+  let .some inst' ← trySynthInstance (mkApp (mkConst ``Decidable) p) | return .none
+  if (← inst'.getUsedConstants.anyM (isCbvNoncomputable ·)) then return .none
+  shareCommon inst'
+
 /-- Reduce `ite` by matching the `Decidable` instance for `isTrue`/`isFalse`. -/
-def simpIteDecidable (f α c inst a b : Expr) (fallback : SimpM Result) : SimpM Result := do
-  match_expr inst with
+def matchIteDecidable (f α c inst a b instToMatch : Expr) (fallback : SimpM Result) : SimpM Result := do
+  match_expr instToMatch with
   | Decidable.isTrue _ hp =>
     return .step a <| mkApp6 (mkConst ``Sym.ite_true f.constLevels!) α c inst a b hp
   | Decidable.isFalse _ hnp =>
     return .step b <| mkApp6 (mkConst ``Sym.ite_false f.constLevels!) α c inst a b hnp
   | _ => fallback
 
+/-- Like `matchIteDecidable`, but for the congruence case where `c` was simplified to `c'` with proof `h`. -/
+def matchIteDecidableCongr (f α c inst a b c' h inst' : Expr) (fallback : SimpM Result) : SimpM Result := do
+  match_expr inst' with
+  | Decidable.isTrue _ hp =>
+    return .step a <| mkApp8 (mkConst ``Sym.ite_true_congr f.constLevels!) α c inst a b c' h hp
+  | Decidable.isFalse _ hnp =>
+    return .step b <| mkApp8 (mkConst ``Sym.ite_false_congr f.constLevels!) α c inst a b c' h hnp
+  | _ => fallback
+
 /-- Simplify the `Decidable` instance, then try `simpIteDecidable`. -/
-def simpIteDecidableWithFallback (f α c inst a b : Expr) (fallback : SimpM Result) : SimpM Result := do
+def simpAndMatchIteDecidable (f α c inst a b : Expr) (fallback : SimpM Result) : SimpM Result := do
   match (← simp inst) with
-  | .rfl _ => simpIteDecidable f α c inst a b fallback
-  | .step inst' _ _ => simpIteDecidable f α c inst' a b fallback
+  | .rfl _ => matchIteDecidable f α c inst a b inst fallback
+  | .step inst' _ _ => matchIteDecidable f α c inst a b inst' fallback
+
+/-- Like `simpAndMatchIteDecidable`, but for the congruence case where `c` was simplified to `c'`. -/
+def simpAndMatchIteDecidableCongr (f α c inst a b c' h inst' : Expr) (fallback : SimpM Result) : SimpM Result := do
+  match (← simp inst') with
+  | .rfl _ => matchIteDecidableCongr f α c inst a b c' h inst' fallback
+  | .step inst'' _ _ => matchIteDecidableCongr f α c inst a b c' h inst'' fallback
 
 /-- Like `simpIte` but also evaluates `Decidable.decide` when the condition does not
 reduce to `True`/`False` directly. -/
@@ -64,23 +93,27 @@ public def simpIteCbv : Simproc := fun e => do
       else if (← isFalseExpr c) then
         return .step b <| mkApp3 (mkConst ``ite_false f.constLevels!) α a b
       else
-        simpIteDecidableWithFallback f α c inst a b <| return .rfl (done := true)
+        simpAndMatchIteDecidable f α c inst a b do return .rfl (done := true)
     | .step c' h _ =>
       if (← isTrueExpr c') then
         return .step a <| mkApp (e.replaceFn ``ite_cond_eq_true) h
       else if (← isFalseExpr c') then
         return .step b <| mkApp (e.replaceFn ``ite_cond_eq_false) h
       else
-        simpIteDecidableWithFallback f α c inst a b <| do
+        -- If we got stuck with simplifying `p` then let's try evaluating the original isntance
+        simpAndMatchIteDecidable f α c inst a b do
+          -- If we get stuck here, maybe the problem is that we need to look at `Decidable c'`
           let inst' := mkApp4 (mkConst ``decidable_of_decidable_of_eq) c c' inst h
-          let e' := e.getBoundedAppFn 4
-          let e' ← mkAppS₄ e' c' inst' a b
-          let h' := mkApp3 (e.replaceFn ``Sym.ite_cond_congr) c' inst' h
-          return .step e' h' (done := true)
+          simpAndMatchIteDecidableCongr f α c inst a b c' h inst' do
+            -- If we fail, then we just rewrite `c` to `c'`
+            let e' := e.getBoundedAppFn 4
+            let e' ← mkAppS₄ e' c' inst' a b
+            let h' := mkApp3 (e.replaceFn ``Sym.ite_cond_congr) c' inst' h
+            return .step e' h' (done := true)
 
 /-- Reduce `dite` by matching the `Decidable` instance for `isTrue`/`isFalse`. -/
-def simpDIteDecidable (f α c inst a b : Expr) (fallback : SimpM Result) : SimpM Result := do
-  match_expr inst with
+def matchDIteDecidable (f α c inst a b instToMatch : Expr) (fallback : SimpM Result) : SimpM Result := do
+  match_expr instToMatch with
   | Decidable.isTrue _ hp =>
     let a' ← share <| a.betaRev #[hp]
     return .step a' <| mkApp6 (mkConst ``Sym.dite_true f.constLevels!) α c inst a b hp
@@ -89,11 +122,30 @@ def simpDIteDecidable (f α c inst a b : Expr) (fallback : SimpM Result) : SimpM
     return .step b' <| mkApp6 (mkConst ``Sym.dite_false f.constLevels!) α c inst a b hnp
   | _ => fallback
 
+/-- Like `matchDIteDecidable`, but for the congruence case where `c` was simplified to `c'` with proof `h`. -/
+def matchDIteDecidableCongr (f α c inst a b c' h inst' : Expr) (fallback : SimpM Result) : SimpM Result := do
+  match_expr inst' with
+  | Decidable.isTrue _ hp =>
+    let hp' := mkApp4 (mkConst ``Eq.mpr_prop) c c' h hp
+    let a' ← share <| a.betaRev #[hp']
+    return .step a' <| mkApp8 (mkConst ``Sym.dite_true_congr f.constLevels!) α c inst a b c' h hp
+  | Decidable.isFalse _ hnp =>
+    let hnp' := mkApp4 (mkConst ``Eq.mpr_not) c c' h hnp
+    let b' ← share <| b.betaRev #[hnp']
+    return .step b' <| mkApp8 (mkConst ``Sym.dite_false_congr f.constLevels!) α c inst a b c' h hnp
+  | _ => fallback
+
 /-- Simplify the `Decidable` instance, then try `simpDIteDecidable`. -/
-def simpDIteDecidableWithFallback (f α c inst a b : Expr) (fallback : SimpM Result) : SimpM Result := do
+def simpAndMatchDIteDecidable (f α c inst a b : Expr) (fallback : SimpM Result) : SimpM Result := do
   match (← simp inst) with
-  | .rfl _ => simpDIteDecidable f α c inst a b fallback
-  | .step inst' _ _ => simpDIteDecidable f α c inst' a b fallback
+  | .rfl _ => matchDIteDecidable f α c inst a b inst fallback
+  | .step inst' _ _ => matchDIteDecidable f α c inst a b inst' fallback
+
+/-- Like `simpAndMatchDIteDecidable`, but for the congruence case where `c` was simplified to `c'`. -/
+def simpAndMatchDIteDecidableCongr (f α c inst a b c' h inst' : Expr) (fallback : SimpM Result) : SimpM Result := do
+  match (← simp inst') with
+  | .rfl _ => matchDIteDecidableCongr f α c inst a b c' h inst' fallback
+  | .step inst'' _ _ => matchDIteDecidableCongr f α c inst a b c' h inst'' fallback
 
 /-- Like `simpDIte` but also evaluates `Decidable.decide` when the condition does not
 reduce to `True`/`False` directly. -/
@@ -111,7 +163,7 @@ public def simpDIteCbv : Simproc := fun e => do
         let b' ← share <| b.betaRev #[mkConst ``not_false]
         return .step b' <| mkApp3 (mkConst ``dite_false f.constLevels!) α a b
       else
-        simpDIteDecidableWithFallback f α c inst a b <| return .rfl (done := true)
+        simpAndMatchDIteDecidable f α c inst a b do return .rfl (done := true)
     | .step c' h _ =>
       if (← isTrueExpr c') then
         let h' ← shareCommon <| mkOfEqTrueCore c h
@@ -122,15 +174,18 @@ public def simpDIteCbv : Simproc := fun e => do
         let b ← share <| b.betaRev #[h']
         return .step b <| mkApp (e.replaceFn ``dite_cond_eq_false) h
       else
-        simpDIteDecidableWithFallback f α c inst a b <| do
+        -- If we get stuck after simplifying `p` to `p'`, then we try to evaluate the original instance 
+        simpAndMatchDIteDecidable f α c inst a b do
+          -- Otherwise, we make `Decidable c'` instance and try to evaluate it instead
           let inst' := mkApp4 (mkConst ``decidable_of_decidable_of_eq) c c' inst h
-          let e' := e.getBoundedAppFn 4
-          let h ← shareCommon h
-          let a ← share <| mkLambda `h .default c' (a.betaRev #[mkApp4 (mkConst ``Eq.mpr_prop) c c' h (mkBVar 0)])
-          let b ← share <| mkLambda `h .default (mkNot c') (b.betaRev #[mkApp4 (mkConst ``Eq.mpr_not) c c' h (mkBVar 0)])
-          let e' ← mkAppS₄ e' c' inst' a b
-          let h' := mkApp3 (e.replaceFn ``Sym.dite_cond_congr) c' inst' h
-          return .step e' h' (done := true)
+          simpAndMatchDIteDecidableCongr f α c inst a b c' h inst' do
+            let e' := e.getBoundedAppFn 4
+            let h ← shareCommon h
+            let a ← share <| mkLambda `h .default c' (a.betaRev #[mkApp4 (mkConst ``Eq.mpr_prop) c c' h (mkBVar 0)])
+            let b ← share <| mkLambda `h .default (mkNot c') (b.betaRev #[mkApp4 (mkConst ``Eq.mpr_not) c c' h (mkBVar 0)])
+            let e' ← mkAppS₄ e' c' inst' a b
+            let h' := mkApp3 (e.replaceFn ``Sym.dite_cond_congr) c' inst' h
+            return .step e' h' (done := true)
 
 /-- Short-circuit evaluation of `Or`. Simplifies only the left argument;
 if it reduces to `True`, returns `True` immediately without evaluating the right side. -/
@@ -173,16 +228,16 @@ public def simpAnd : Simproc := fun e => do
       return .rfl
 
 /-- Reduce `decide` by matching the `Decidable` instance for `isTrue`/`isFalse`. -/
-def simpDecideByInst (p inst : Expr) : SimpM Result := do
-  match_expr inst with
+def matchDecideDecidable (p inst instToMatch : Expr) (fallback : SimpM Result) : SimpM Result := do
+  match_expr instToMatch with
   | Decidable.isTrue _ hp =>
     return .step (← getBoolTrueExpr) <| mkApp3 (mkConst ``Sym.decide_isTrue) p inst hp
   | Decidable.isFalse _ hnp =>
     return .step (← getBoolFalseExpr) <| mkApp3 (mkConst ``Sym.decide_isFalse) p inst hnp
-  | _ => return .rfl (done := true)
+  | _ => fallback
 
 /-- Like `simpDecideByInst`, but for the case where `p` was simplified to `p'` with proof `h`. -/
-def simpDecideByInstCongr (p p' h inst inst' : Expr) (fallback : SimpM Result) : SimpM Result := do
+def matchDecideDecidableCongr (p p' h inst inst' : Expr) (fallback : SimpM Result) : SimpM Result := do
   match_expr inst' with
   | Decidable.isTrue _ hp =>
     return .step (← getBoolTrueExpr) <| mkApp5 (mkConst ``Sym.decide_isTrue_congr) p p' h inst hp
@@ -191,16 +246,16 @@ def simpDecideByInstCongr (p p' h inst inst' : Expr) (fallback : SimpM Result) :
   | _ => fallback
 
 /-- Simplify the `Decidable` instance, then try `simpDecideByInst`. -/
-def simpDecideByInstWithFallback (p inst : Expr) : SimpM Result := do
+def simpAndMatchDecideDecidable (p inst : Expr) (fallback : SimpM Result) : SimpM Result := do
   match (← simp inst) with
-  | .rfl _ => simpDecideByInst p inst
-  | .step inst' _ _ => simpDecideByInst p inst'
+  | .rfl _ => matchDecideDecidable p inst inst fallback
+  | .step inst' _ _ => matchDecideDecidable p inst inst' fallback
 
 /-- Like `simpDecideByInstWithFallback`, but for the case where `p` was simplified to `p'`. -/
-def simpDecideByInstWithFallbackCongr (p p' h inst inst' : Expr) (fallback : SimpM Result) : SimpM Result := do
+def simpAndMatchDecideDecidableCongr (p p' h inst inst' : Expr) (fallback : SimpM Result) : SimpM Result := do
   match (← simp inst') with
-  | .rfl _ => simpDecideByInstCongr p p' h inst inst' fallback
-  | .step inst'' _ _ => simpDecideByInstCongr p p' h inst inst'' fallback
+  | .rfl _ => matchDecideDecidableCongr p p' h inst inst' fallback
+  | .step inst'' _ _ => matchDecideDecidableCongr p p' h inst inst'' fallback
 
 /-- Simplify `Decidable.decide` by simplifying the proposition and reducing the instance.
 
@@ -221,20 +276,20 @@ public def simpDecideCbv : Simproc := fun e => do
       else if (← isFalseExpr p) then
         return .step (← getBoolFalseExpr) (mkApp (mkConst ``decide_false) inst)
       else
-        simpDecideByInstWithFallback p inst
+        simpAndMatchDecideDecidable p inst do return .rfl (done := true)
     | .step p' hp _ =>
       if (← isTrueExpr p') then
         return .step (← getBoolTrueExpr) <| mkApp3 (mkConst ``Sym.decide_prop_eq_true) p inst hp
       else if (← isFalseExpr p') then
         return .step (← getBoolFalseExpr) <| mkApp3 (mkConst ``Sym.decide_prop_eq_false) p inst hp
       else
-        let .some inst' ← trySynthInstance (mkApp (mkConst ``Decidable) p') | return .rfl
-        let inst' ← shareCommon inst'
-        simpDecideByInstWithFallbackCongr p p' hp inst inst' (do
+        let inst' ← trySynthComputableInstance p'
+        let inst' := inst'.getD <| mkApp4 (mkConst ``decidable_of_decidable_of_eq) p p' inst hp
+        simpAndMatchDecideDecidableCongr p p' hp inst inst' do
           let res := (mkConst ``Decidable.decide)
           let res ← shareCommon res
           let res ← mkAppS₂ res p' inst'
-          return .step res (mkApp5 (mkConst ``Decidable.decide.congr_simp) p p' hp inst inst') (done := true))
+          return .step res (mkApp5 (mkConst ``Decidable.decide.congr_simp) p p' hp inst inst') (done := true)
 
 end Lean.Meta.Sym.Simp
 
diff --git a/tests/elab/cbv_classical.lean b/tests/elab/cbv_classical.lean
new file mode 100644
index 0000000000..c36b185716
--- /dev/null
+++ b/tests/elab/cbv_classical.lean
@@ -0,0 +1,38 @@
+set_option cbv.warning false
+
+/-!
+# A regression test against `cbv` picking up `Classical.propDecidable`,
+when re-synthesizing instances.
+
+When `cbv` encounters `decide P`, it simplifies the proposition `P`. If `P`
+unfolds (e.g. `IsEven 2` → `∃ k, 2 * k = 2`), `simpDecideCbv` tries to
+synthetize `Decidable` instance for the *unfolded* form. With `open Classical`,
+this was picking up `Classical.propDecidable` (which uses `choice`), replacing
+the original computable instance with one that cannot be evaluated.
+
+The code now contains a guard ensuring that the instance is not made of constants
+marked as `noncomputable`.
+-/
+
+-- A predicate wrapping an existential — has a computable `DecidablePred` instance,
+-- but the unfolded existential has none (except the classical one).
+def IsEven (n : Nat) : Prop := ∃ k, n = 2 * k
+
+instance : DecidablePred IsEven := fun n =>
+  if h : n % 2 = 0 then
+    .isTrue ⟨n / 2, by omega⟩
+  else
+    .isFalse (by intro ⟨k, hk⟩; omega)
+
+
+-- Works, using the provided `DecidablePred` instance.
+example : decide (IsEven 2) = true := by cbv
+
+example : decide (IsEven 3) = false := by cbv
+
+-- Should not fail, when `Classical.propDecidable` becomes available.
+open Classical in
+example : decide (IsEven 2) = true := by cbv
+
+open Classical in
+example : decide (IsEven 3) = false := by cbv
diff --git a/tests/elab/cbv_decidable_congr.lean b/tests/elab/cbv_decidable_congr.lean
new file mode 100644
index 0000000000..94faa0e784
--- /dev/null
+++ b/tests/elab/cbv_decidable_congr.lean
@@ -0,0 +1,35 @@
+set_option cbv.warning false
+set_option trace.Meta.Tactic true
+axiom P : Prop
+axiom instDecidableP : Decidable P
+axiom Q : Prop
+
+axiom P_eval : P = Q
+attribute [cbv_eval] P_eval
+example : P = Q := by cbv
+
+axiom hQ : Q
+
+axiom instDecidableQ : Decidable Q
+noncomputable instance : Decidable P := instDecidableP
+noncomputable instance : Decidable Q := instDecidableQ
+axiom dQ_eval : instDecidableQ = Decidable.isTrue hQ
+attribute [cbv_eval] dQ_eval
+
+example : (if P then true else false) = true := by cbv
+
+example : (if P then true else false) = true := by conv => lhs; cbv
+
+example : (if _ : P then true else false) = true := by cbv
+
+example : P := by decide_cbv
+
+example : decide P = true := by conv => lhs; cbv
+
+example : Q := by decide_cbv
+
+example : decide Q = true := by conv => lhs; cbv
+
+example : (if Q then true else false) = true := by cbv
+
+example : (if _ : Q then true else false) = true := by cbv