diff --git a/Proofs/SHA512/SHA512Sym.lean b/Proofs/SHA512/SHA512Sym.lean
index 4587d571..5b20b08b 100644
--- a/Proofs/SHA512/SHA512Sym.lean
+++ b/Proofs/SHA512/SHA512Sym.lean
@@ -25,7 +25,7 @@ that the register `x2` is decremented early on in this program:
 
 In the near future, we'd like to prove that the hash computed for this
 one input block matches the expected value, i.e., one dictated by
-`SHA2.sha512`. 
+`SHA2.sha512`.
 
 Also see `Tests.SHA2.SHA512ProgramTest` for an example of a concrete
 run that checks the implementation against the specification.
@@ -47,6 +47,7 @@ abbrev ktbl_addr : BitVec 64 := 0x1b4300#64
 -- set_option profiler true in
 -- set_option profiler.threshold 1 in
 -- set_option pp.deepTerms false in
+set_option maxHeartbeats 9999999 in -- To be fixed by https://github.com/leanprover/LNSym/pull/113
 theorem sha512_block_armv8_1block (s0 sf : ArmState)
   -- (FIXME) Ignore the `stp` instruction for now.
   (h_s0_pc : read_pc s0 = 0x1264c4#64)
@@ -71,7 +72,7 @@ theorem sha512_block_armv8_1block (s0 sf : ArmState)
                   ktbl_addr      (SHA2.k_512.length * 8))
   -- (FIXME) Use program.length instead of 20 here (depends on the
   -- performance of the new symbolic simulation tactic).
-  (h_run : sf = run 20 s0) :  
+  (h_run : sf = run 20 s0) :
   r (StateField.GPR 2#5) sf = 0#64 ∧
   r StateField.ERR sf = StateError.None := by
   sym_n 20
@@ -79,7 +80,7 @@ theorem sha512_block_armv8_1block (s0 sf : ArmState)
   (FIXME @bollu) cse fails with the following message:
   no goals to be solved
   -/
-  -- cse (config := { processHyps := .allHyps })
+  cse (config := { processHyps := .allHyps })
   -- Final Steps
   unfold run at h_run
   subst sf
diff --git a/Tactics/CSE.lean b/Tactics/CSE.lean
index 10745fad..d94ac3f1 100644
--- a/Tactics/CSE.lean
+++ b/Tactics/CSE.lean
@@ -223,6 +223,7 @@ def CSEM.generalize (arg : GeneralizeArg) : CSEM Bool := do
   let e := arg.expr
 
   let mvarId ← getMainGoal
+  let checkpoint ← Tactic.saveState
   mvarId.withContext do
     -- implementation modeled after `Lean.Elab.Tactic.evalGeneralize`.
     trace[Tactic.cse.generalize] "{tryEmoji} Generalizing {hname} : {e} = {xname}"
@@ -246,6 +247,7 @@ def CSEM.generalize (arg : GeneralizeArg) : CSEM Bool := do
       trace[Tactic.cse.generalize] "{checkEmoji} succeeded in generalizing {hname}. ({← getMainGoal})"
       return true
     catch e =>
+      checkpoint.restore
       trace[Tactic.cse.generalize] "{bombEmoji} failed to generalize {hname}"
       return false