diff --git a/Proofs/Experiments/AddLoop/AddLoop.lean b/Proofs/Experiments/AddLoop/AddLoop.lean
index 31c2b09a..ac250a40 100644
--- a/Proofs/Experiments/AddLoop/AddLoop.lean
+++ b/Proofs/Experiments/AddLoop/AddLoop.lean
@@ -306,21 +306,8 @@ theorem effects_of_nextc_from_0x4005a4
   -- TODO: Tactic to "explode" conjunctions?
   obtain ⟨h_s0_pc, h_s0_program, h_s0_err, h_s0_sp_aligned⟩ := h_pre
   -- Symbolic simulation
-  -- (FIXME) sym_n doesn't play well with unconditional branches.
-  /-
-  application type mismatch
-  program.stepi_0x4005a8 s1 s2 h_s1_program h_s1_pc
-  argument
-  h_s1_pc
-  has type
-  r StateField.PC s1 = 0x4005b0#64 : Prop
-  but is expected to have type
-  r StateField.PC s1 = 0x4005a8#64 : Prop
-  -/
-  -- sym_n 2
-  sym_n 1 at s0
-  sym_n 1 at s1
-  simp (config := {ground := true}) only [*, state_simp_rules, bitvec_rules, minimal_theory]
+  sym_n 2
+  simp (config := {ground := true}) only []
   rw [AddWithCarry.all_ones_zero_flag_64]
   done
 
diff --git a/Tactics/Sym.lean b/Tactics/Sym.lean
index 8ca1df78..9c4aea1d 100644
--- a/Tactics/Sym.lean
+++ b/Tactics/Sym.lean
@@ -181,7 +181,11 @@ def withoutHyp (hyp : Name) (k : TacticM Unit) : TacticM (Option FVarId) :=
 
 /-- Given an equality `h_step : s{i+1} = w ... (... (w ... s{i})...)`,
 add hypotheses that axiomatically describe the effects in terms of
-reads from `s{i+1}` -/
+reads from `s{i+1}`.
+
+Return the context for the next step (see `SymContext.next`), where
+we attempt to determine the new PC by reflecting the obtained effects,
+falling back to incrementing the PC if reflection failed. -/
 def explodeStep (c : SymContext) (hStep : Expr) : TacticM SymContext :=
   withMainContext do
     let mut eff ← AxEffects.fromEq hStep
@@ -249,7 +253,21 @@ def explodeStep (c : SymContext) (hStep : Expr) : TacticM SymContext :=
         eff.validate
 
       eff.addHypothesesToLContext s!"h_{c.next_state}_"
-    return { c with axHyps := axHyps ++ c.axHyps}
+    let c := { c with axHyps := axHyps ++ c.axHyps}
+
+    -- Attempt to reflect the new PC
+    let nextPc ← eff.getField .PC
+    let nextPc? ← try
+      let nextPc ← reflectBitVecLiteral 64 nextPc.value
+      -- NOTE: `reflectBitVecLiteral` is fast when the value is a literal,
+      -- but might involve an expensive reduction when it is not
+      pure <| some nextPc
+    catch err =>
+      trace[Tactic.sym] "failed to reflect {nextPc.value}\n\n\
+        {err.toMessageData}"
+      pure none
+
+    return c.next nextPc?
 
 /-- A tactic wrapper around `explodeStep`.
 Note the use of `SymContext.fromLocalContext`,
@@ -313,7 +331,7 @@ def sym1 (c : SymContext) (whileTac : TSyntax `tactic) : TacticM SymContext :=
           skipping simplification step"
 
     -- Prepare `h_program`,`h_err`,`h_pc`, etc. for next state
-    let c ← withMainContext <| do
+    withMainContext <| do
       let hStep ← SymContext.findFromUserName h_step.getId
       -- ^^ we can't reuse `hStep` from before, since its fvarId might've been
       --    changed by `simp`
@@ -325,8 +343,6 @@ def sym1 (c : SymContext) (whileTac : TSyntax `tactic) : TacticM SymContext :=
 
       return c
 
-    return c.next
-
 /- used in `sym_n` tactic to specify an initial state -/
 syntax sym_at := "at" ident