diff --git a/Smt/Reconstruct.lean b/Smt/Reconstruct.lean
index eec9e5db..21c79951 100644
--- a/Smt/Reconstruct.lean
+++ b/Smt/Reconstruct.lean
@@ -16,6 +16,7 @@ open Lean
 open Attribute
 
 structure Reconstruct.state where
+  userNames : HashMap String FVarId
   termCache : HashMap cvc5.Term Expr
   proofCache : HashMap cvc5.Proof Expr
   count : Nat
@@ -62,9 +63,10 @@ def traceReconstructTerm (t : cvc5.Term) (r : Except Exception Expr) : Reconstru
     | .error _ => m!"{bombEmoji}"
 
 def withNewTermCache (k : ReconstructM α) : ReconstructM α := do
-  let state ← get
+  let termCache := (← get).termCache
+  modify fun state => { state with termCache := {} }
   let r ← k
-  set { ← get with termCache := state.termCache }
+  modify fun state => { state with termCache := termCache }
   return r
 
 def reconstructTerm : cvc5.Term → ReconstructM Expr := withTermCache fun t => do
@@ -89,9 +91,10 @@ where
     throwError "Failed to reconstruct term {t} with kind {t.getKind}"
 
 def withNewProofCache (k : ReconstructM α) : ReconstructM α := do
-  let state ← get
+  let proofCache := (← get).proofCache
+  modify fun state => { state with proofCache := {} }
   let r ← k
-  set { ← get with proofCache := state.proofCache }
+  modify fun state => { state with proofCache := proofCache }
   return r
 
 def withProofCache (r : cvc5.Proof → ReconstructM Expr) (pf : cvc5.Proof) : ReconstructM Expr := do
@@ -172,10 +175,10 @@ def traceReconstructProof (r : Except Exception (Expr × Expr × List MVarId)) :
   | _     => m!"{bombEmoji}"
 
 open Qq in
-partial def reconstructProof (pf : cvc5.Proof) : MetaM (Expr × Expr × List MVarId) := do
+partial def reconstructProof (pf : cvc5.Proof) (fvNames : HashMap String FVarId) : MetaM (Expr × Expr × List MVarId) := do
   withTraceNode `smt.reconstruct.proof traceReconstructProof do
-  let Prod.mk (p : Q(Prop)) state ← (Reconstruct.reconstructTerm (pf.getResult)).run ⟨{}, {}, 0, #[], #[]⟩
-  let Prod.mk (h : Q(True → $p)) (.mk _ _ _ _ mvs) ← (Reconstruct.reconstructProof pf).run state
+  let Prod.mk (p : Q(Prop)) state ← (Reconstruct.reconstructTerm (pf.getResult)).run ⟨fvNames, {}, {}, 0, #[], #[]⟩
+  let Prod.mk (h : Q(True → $p)) (.mk _ _ _ _ _ mvs) ← (Reconstruct.reconstructProof pf).run state
   return (p, q($h trivial), mvs.toList)
 
 open cvc5 in
@@ -217,10 +220,15 @@ open Lean.Elab Tactic in
     match r with
       | .error e => logInfo (repr e)
       | .ok pf =>
-        let (p, hp, mvs) ← reconstructProof pf
+        let (p, hp, mvs) ← reconstructProof pf (← getFVarNames)
         let mv ← Tactic.getMainGoal
         let mv ← mv.assert (Name.num `s 0) p hp
         let (_, mv) ← mv.intro1
         replaceMainGoal (mv :: mvs)
+where
+  getFVarNames : MetaM (HashMap String FVarId) := do
+    let lCtx ← getLCtx
+    return lCtx.getFVarIds.foldl (init := {}) fun m fvarId =>
+      m.insert (lCtx.getRoundtrippingUserName? fvarId).get!.toString fvarId
 
 end Smt
diff --git a/Smt/Reconstruct/Builtin.lean b/Smt/Reconstruct/Builtin.lean
index a1a19ed1..c9f20ae8 100644
--- a/Smt/Reconstruct/Builtin.lean
+++ b/Smt/Reconstruct/Builtin.lean
@@ -29,16 +29,18 @@ def getFVarExpr! (n : Name) : MetaM Expr := do
   | some d => return d.toExpr
   | none   => throwError "unknown free variable '{n}'"
 
-def getFVarOrConstExpr! (n : Name) : MetaM Expr := do
-  match (← getLCtx).findFromUserName? n with
-  | some d => return d.toExpr
-  | none   =>
-    let c ← getConstInfo n
-    return .const c.name (c.numLevelParams.repeat (.zero :: ·) [])
+def getFVarOrConstExpr! (n : String) : ReconstructM Expr := do
+  match (← get).userNames.find? n with
+  | some fv => return .fvar fv
+  | none   => match (← getLCtx).findFromUserName? n.toName with
+    | some d => return d.toExpr
+    | none   =>
+      let c ← getConstInfo n.toName
+      return .const c.name (c.numLevelParams.repeat (.zero :: ·) [])
 
 @[smt_term_reconstruct] def reconstructBuiltin : TermReconstructor := fun t => do match t.getKind with
   | .VARIABLE => getFVarExpr! (getVariableName t)
-  | .CONSTANT => getFVarOrConstExpr! (Name.mkSimple t.getSymbol)
+  | .CONSTANT => getFVarOrConstExpr! t.getSymbol
   | .EQUAL =>
     let α : Q(Type) ← reconstructSort t[0]!.getSort
     let x : Q($α) ← reconstructTerm t[0]!
@@ -65,7 +67,12 @@ def getFVarOrConstExpr! (n : Name) : MetaM Expr := do
   | _ => return none
 where
   getVariableName (t : cvc5.Term) : Name :=
-    if t.hasSymbol then Name.mkSimple t.getSymbol else Name.num `x t.getId
+    if t.hasSymbol then
+      if t.getSymbol.toName == .anonymous then
+        Name.mkSimple t.getSymbol
+      else
+        t.getSymbol.toName
+    else Name.num `x t.getId
 
 def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
   match pf.getRewriteRule with
diff --git a/Smt/Reconstruct/Quant.lean b/Smt/Reconstruct/Quant.lean
index c8912531..c19fb138 100644
--- a/Smt/Reconstruct/Quant.lean
+++ b/Smt/Reconstruct/Quant.lean
@@ -28,7 +28,12 @@ namespace Smt.Reconstruct.Quant
 open Lean Qq
 
 def getVariableName (t : cvc5.Term) : Name :=
-  if t.hasSymbol then Name.mkSimple t.getSymbol else Name.num `x t.getId
+  if t.hasSymbol then
+    if t.getSymbol.toName == .anonymous then
+      Name.mkSimple t.getSymbol
+    else
+      t.getSymbol.toName
+  else Name.num `x t.getId
 
 @[smt_term_reconstruct] def reconstructQuant : TermReconstructor := fun t => do match t.getKind with
   | .FORALL =>
@@ -223,8 +228,8 @@ where
       xs.foldrM f (p, q, h)
     addThm q($p = $q) h
   reconstructSkolemize (pf : cvc5.Proof) : ReconstructM Expr := do
-    let res := pf.getChildren[0]!.getResult
-    let es ← reconstructQuant.reconstructForallSkolems res[0]! (res[0]![0]!.getNumChildren - 1)
+    let chRes := pf.getChildren[0]!.getResult
+    let es ← reconstructQuant.reconstructForallSkolems chRes[0]! (chRes[0]![0]!.getNumChildren - 1)
     let f := fun h e => do
       let α : Q(Type) ← pure (e.getArg! 0)
       let hα : Q(Nonempty $α) ← Meta.synthInstance q(Nonempty $α)
diff --git a/Smt/Reconstruct/UF.lean b/Smt/Reconstruct/UF.lean
index f5b5f9be..10f39253 100644
--- a/Smt/Reconstruct/UF.lean
+++ b/Smt/Reconstruct/UF.lean
@@ -13,16 +13,18 @@ namespace Smt.Reconstruct.UF
 
 open Lean Qq
 
-def getFVarOrConstExpr! (n : Name) : MetaM Expr := do
-  match (← getLCtx).findFromUserName? n with
-  | some d => return d.toExpr
-  | none   =>
-    let c ← getConstInfo n
-    return .const c.name (c.numLevelParams.repeat (.zero :: ·) [])
+def getFVarOrConstExpr! (n : String) : ReconstructM Expr := do
+  match (← get).userNames.find? n with
+  | some fv => return .fvar fv
+  | none   => match (← getLCtx).findFromUserName? n.toName with
+    | some d => return d.toExpr
+    | none   =>
+      let c ← getConstInfo n.toName
+      return .const c.name (c.numLevelParams.repeat (.zero :: ·) [])
 
 @[smt_sort_reconstruct] def reconstructUS : SortReconstructor := fun s => do match s.getKind with
   | .INTERNAL_SORT_KIND
-  | .UNINTERPRETED_SORT => getFVarOrConstExpr! (Name.mkSimple s.getSymbol)
+  | .UNINTERPRETED_SORT => getFVarOrConstExpr! s.getSymbol
   | _ => return none
 
 @[smt_term_reconstruct] def reconstructUF : TermReconstructor := fun t => do match t.getKind with
diff --git a/Smt/Tactic/Smt.lean b/Smt/Tactic/Smt.lean
index b510a2cd..de30697f 100644
--- a/Smt/Tactic/Smt.lean
+++ b/Smt/Tactic/Smt.lean
@@ -20,10 +20,19 @@ open Lean hiding Command
 open Elab Tactic Qq
 open Smt Translate Query Reconstruct Util
 
-def prepareSmtQuery (hs : List Expr) (goalType : Expr) : MetaM (List Command) := do
+def genUniqueFVarNames : MetaM (HashMap FVarId String × HashMap String FVarId) := do
+  let lCtx ← getLCtx
+  let st : NameSanitizerState := { options := {}}
+  let (lCtx, _) := (lCtx.sanitizeNames st).run
+  return lCtx.getFVarIds.foldl (init := ({}, {})) fun (m₁, m₂) fvarId =>
+    let m₁ := m₁.insert fvarId (lCtx.getRoundtrippingUserName? fvarId).get!.toString
+    let m₂ := m₂.insert (lCtx.getRoundtrippingUserName? fvarId).get!.toString fvarId
+    (m₁, m₂)
+
+def prepareSmtQuery (hs : List Expr) (goalType : Expr) (fvNames : HashMap FVarId String) : MetaM (List Command) := do
   let goalId ← Lean.mkFreshMVarId
   Lean.Meta.withLocalDeclD goalId.name (mkNot goalType) fun g =>
-  Query.generateQuery g hs
+  Query.generateQuery g hs fvNames
 
 def withProcessedHints (mv : MVarId) (hs : List Expr) (k : MVarId → List Expr → MetaM α): MetaM α :=
   go mv hs [] k
@@ -46,7 +55,8 @@ def smt (mv : MVarId) (hs : List Expr) (timeout : Option Nat := none) : MetaM (L
   mv.withContext do
   let goalType : Q(Prop) ← mv.getType
   -- 2. Generate the SMT query.
-  let cmds ← prepareSmtQuery hs (← mv.getType)
+  let (fvNames₁, fvNames₂) ← genUniqueFVarNames
+  let cmds ← prepareSmtQuery hs (← mv.getType) fvNames₁
   let cmds := .setLogic "ALL" :: cmds
   trace[smt] "goal: {goalType}"
   trace[smt] "\nquery:\n{Command.cmdsAsQuery (cmds ++ [.checkSat])}"
@@ -61,7 +71,7 @@ def smt (mv : MVarId) (hs : List Expr) (timeout : Option Nat := none) : MetaM (L
     throwError "unable to prove goal, either it is false or you need to define more symbols with `smt [foo, bar]`"
   | .ok pf =>
     -- 4b. Reconstruct proof.
-    let (p, hp, mvs) ← reconstructProof pf
+    let (p, hp, mvs) ← reconstructProof pf fvNames₂
     let mv ← mv.assert (← mkFreshId) p hp
     let ⟨_, mv⟩ ← mv.intro1
     let ts ← hs.mapM Meta.inferType
@@ -130,7 +140,7 @@ def parseTimeout : TSyntax `smtTimeout → TacticM (Option Nat)
   let (hs, mv) ← Preprocess.elimIff mv hs
   mv.withContext do
   let goalType ← mv.getType
-  let cmds ← prepareSmtQuery hs (← mv.getType)
+  let cmds ← prepareSmtQuery hs (← mv.getType) (← genUniqueFVarNames).fst
   let cmds := cmds ++ [.checkSat]
   logInfo m!"goal: {goalType}\n\nquery:\n{Command.cmdsAsQuery cmds}"
 
diff --git a/Smt/Translate.lean b/Smt/Translate.lean
index 78e0aa94..ce16d699 100644
--- a/Smt/Translate.lean
+++ b/Smt/Translate.lean
@@ -45,6 +45,8 @@ structure TranslationM.State where
   /-- A mapping from a scopped name to a suffix index that makes it unique. This field does not handle
   scopping, which should be handled by `withScopedName` -/
   scopedNames : HashMap Name Nat := .empty
+  /-- A mapping from fvars to unique names. -/
+  uniqueFVarNames : HashMap FVarId String := .empty
 
 abbrev TranslationM := StateT TranslationM.State MetaM
 
@@ -137,9 +139,13 @@ partial def applyTranslators? : Translator := withCache fun e => do
       -- Then try splitting subexpressions
       match e with
       | fvar fv =>
-        if !(← get).localFVars.contains fv then
+        if (← get).localFVars.contains fv then
+          return symbolT (← fv.getUserName).toString
+        else
           modify fun st => { st with depFVars := st.depFVars.insert fv }
-        return symbolT (← fv.getUserName).toString
+          match (← get).uniqueFVarNames.find? fv with
+          | some n => return symbolT n
+          | none   => return symbolT (← fv.getUserName).toString
       | const nm _ =>
         modify fun st => { st with depConstants := st.depConstants.insert nm }
         return symbolT nm.toString
diff --git a/Smt/Translate/Query.lean b/Smt/Translate/Query.lean
index de53dc33..b0314920 100644
--- a/Smt/Translate/Query.lean
+++ b/Smt/Translate/Query.lean
@@ -158,7 +158,10 @@ def addCommandFor (e tp : Expr) : QueryBuilderM (Array Expr) := do
 
   -- Otherwise it is a local/global declaration with name `nm`.
   let nm ← match e with
-    | fvar id .. => pure (← id.getDecl).userName.toString
+    | fvar id .. =>
+      match (← (get : TranslationM _)).uniqueFVarNames.find? id with
+      | some nm => pure nm
+      | none    => pure (← id.getUserName).toString
     | const n .. => pure n.toString
     | _          => throwError "internal error, expected fvar or const but got{indentD e}\nof kind {e.ctorName}"
 
@@ -253,14 +256,14 @@ def emitVertex (cmds : HashMap Expr Command) (e : Expr) : StateT (List Command)
   let some cmd := cmds.find? e | throwError "no command was computed for {e}"
   set (← addCommand cmd (← get))
 
-def generateQuery (goal : Expr) (hs : List Expr) : MetaM (List Command) :=
+def generateQuery (goal : Expr) (hs : List Expr) (fvNames : HashMap FVarId String) : MetaM (List Command) :=
   withTraceNode `smt.translate.query (fun _ => pure .nil) do
     trace[smt.translate.query] "Goal: {← inferType goal}"
     trace[smt.translate.query] "Provided Hints: {hs}"
     let ((_, st), _) ← QueryBuilderM.buildDependencyGraph goal
       |>.run { toDefine := hs : QueryBuilderM.Config }
       |>.run { : QueryBuilderM.State }
-      |>.run { : TranslationM.State }
+      |>.run { uniqueFVarNames := fvNames : TranslationM.State }
     trace[smt.translate.query] "Dependency Graph: {st.graph}"
     -- The type of the proof generated by a solver depends on the order of asserions. We assert the
     -- Lean goal at the end of the query to simplify unification during proof reconstruction.
diff --git a/Test/EUF/Issue126.expected b/Test/EUF/Issue126.expected
index 3dd05b3a..f2579f65 100644
--- a/Test/EUF/Issue126.expected
+++ b/Test/EUF/Issue126.expected
@@ -1,86 +1 @@
-goal: ¬b n →
-  te n o r v → (∃ q, nm q ∧ ∀ (s : a), nmm s q → tb s n o r v) ∨ ∃ q, ngt q ∧ ∀ (s : a), nmm s q → tc s n o r v
-
-query:
-(declare-sort n 0)
-(declare-fun ngt (n) Bool)
-(declare-fun ne (n) Bool)
-(assert (forall ((s n)) (=> (ngt s) (not (ne s)))))
-(declare-fun nm (n) Bool)
-(assert (forall ((s n)) (=> (nm s) (ngt s))))
-(declare-sort a 0)
-(declare-fun nmm (a n) Bool)
-(declare-fun b (a) Bool)
-(assert (forall ((s n)) (=> (ngt s) (exists ((a a)) (and (nmm a s) (not (b a)))))))
-(assert (forall ((s1 n)) (forall ((s2 n)) (exists ((a a)) (and (nmm a s1) (and (nmm a s2) (not (b a))))))))
-(declare-sort v 0)
-(declare-sort r 0)
-(declare-fun ta (a a r v) Bool)
-(declare-fun tf (a a r v) Bool)
-(declare-fun sd (a a r v) Bool)
-(declare-fun sb (a a a r v) Bool)
-(declare-fun sc (a a a r v) Bool)
-(declare-fun tc (a a a r v) Bool)
-(declare-fun se (a a r v) Bool)
-(declare-fun sg (a r) Bool)
-(declare-fun sa (a a r v) Bool)
-(declare-fun td (a a r v) Bool)
-(declare-fun tb (a a a r v) Bool)
-(declare-fun te (a a r v) Bool)
-(declare-fun tg (a r) Bool)
-(declare-fun sf (a a r v) Bool)
-(assert (and (forall ((s a)) (forall ((d a)) (forall ((r r)) (forall ((v v)) (or (and (not (b s)) (= (sa s d r v) (ta s d r v))) (and (b s) (=> (sa s d r v) (ta s d r v)))))))) (and (forall ((s a)) (forall ((d a)) (forall ((o a)) (forall ((r r)) (forall ((v v)) (or (and (not (b s)) (= (sb s d o r v) (tb s d o r v))) (and (b s) (=> (sb s d o r v) (tb s d o r v))))))))) (and (forall ((s a)) (forall ((d a)) (forall ((o a)) (forall ((r r)) (forall ((v v)) (or (and (not (b s)) (= (sc s d o r v) (tc s d o r v))) (and (b s) (=> (sc s d o r v) (tc s d o r v))))))))) (and (forall ((a_2 a)) (forall ((a_3 r)) (= (sg a_2 a_3) (tg a_2 a_3)))) (and (forall ((a_2 a)) (forall ((a_3 a)) (forall ((a_4 r)) (forall ((a_5 v)) (= (sd a_2 a_3 a_4 a_5) (td a_2 a_3 a_4 a_5)))))) (and (forall ((a_2 a)) (forall ((a_3 a)) (forall ((a_4 r)) (forall ((a_5 v)) (= (se a_2 a_3 a_4 a_5) (te a_2 a_3 a_4 a_5)))))) (forall ((a_2 a)) (forall ((a_3 a)) (forall ((a_4 r)) (forall ((a_5 v)) (= (sf a_2 a_3 a_4 a_5) (tf a_2 a_3 a_4 a_5)))))))))))))
-(assert (and (forall ((s a)) (forall ((|d₁| a)) (forall ((|d₂| a)) (forall ((r r)) (forall ((|v₁| v)) (forall ((|v₂| v)) (=> (and (not (b |d₁|)) (and (not (b |d₂|)) (and (sf |d₁| s r |v₁|) (sf |d₂| s r |v₂|)))) (= |v₁| |v₂|)))))))) (and (forall ((s a)) (forall ((d a)) (forall ((r r)) (forall ((v v)) (=> (and (not (b s)) (and (not (b d)) (sf d s r v))) (and (sg s r) (forall ((d a)) (sa s d r v)))))))) (and (forall ((s a)) (forall ((d a)) (forall ((r r)) (forall ((v v)) (=> (and (not (b s)) (and (not (b d)) (se d s r v))) (and (sg s r) (forall ((d a)) (sa s d r v)))))))) (and (forall ((s a)) (forall ((o a)) (forall ((|d₁| a)) (forall ((|d₂| a)) (forall ((r r)) (forall ((|v₁| v)) (forall ((|v₂| v)) (=> (not (b s)) (=> (and (sc s |d₁| o r |v₁|) (sc s |d₂| o r |v₂|)) (= |v₁| |v₂|)))))))))) (and (forall ((s a)) (forall ((o a)) (forall ((|d₁| a)) (forall ((|d₂| a)) (forall ((r r)) (forall ((|v₁| v)) (forall ((|v₂| v)) (=> (not (b s)) (=> (and (sb s |d₁| o r |v₁|) (sb s |d₂| o r |v₂|)) (= |v₁| |v₂|)))))))))) (and (forall ((s a)) (forall ((|d₁| a)) (forall ((|d₂| a)) (forall ((r r)) (forall ((|v₁| v)) (forall ((|v₂| v)) (=> (not (b s)) (=> (and (sa s |d₁| r |v₁|) (sa s |d₂| r |v₂|)) (= |v₁| |v₂|))))))))) (and (forall ((s a)) (forall ((d a)) (forall ((r r)) (forall ((v v)) (=> (not (b s)) (= (forall ((d a)) (sa s d r v)) (sa s d r v))))))) (and (forall ((n_1 a)) (forall ((o a)) (forall ((r r)) (forall ((v v)) (=> (not (b n_1)) (=> (sf n_1 o r v) (exists ((q n)) (and (nm q) (forall ((s a)) (=> (nmm s q) (sc s n_1 o r v))))))))))) (and (forall ((n_1 a)) (forall ((o a)) (forall ((r r)) (forall ((v v)) (=> (not (b n_1)) (=> (se n_1 o r v) (or (exists ((q n)) (and (nm q) (forall ((s a)) (=> (nmm s q) (sb s n_1 o r v))))) (exists ((q n)) (and (ngt q) (forall ((s a)) (=> (nmm s q) (sc s n_1 o r v)))))))))))) (and (forall ((n a)) (forall ((d a)) (forall ((o a)) (forall ((r r)) (forall ((v v)) (=> (not (b n)) (= (se n o r v) (sc n d o r v)))))))) (and (forall ((n a)) (forall ((o a)) (forall ((r r)) (forall ((v v)) (=> (not (b n)) (=> (sd n o r v) (sa o n r v))))))) (and (forall ((n a)) (forall ((d a)) (forall ((o a)) (forall ((r r)) (forall ((v v)) (=> (not (b n)) (= (sd n o r v) (sb n d o r v)))))))) (forall ((s a)) (forall ((r r)) (=> (not (b s)) (= (sg s r) (exists ((v v)) (forall ((d a)) (sa s d r v))))))))))))))))))))
-(declare-const v v)
-(declare-const o a)
-(declare-const n a)
-(declare-const r r)
-(assert (not (=> (not (b n)) (=> (te n o r v) (or (exists ((q n)) (and (nm q) (forall ((s a)) (=> (nmm s q) (tb s n o r v))))) (exists ((q n)) (and (ngt q) (forall ((s a)) (=> (nmm s q) (tc s n o r v))))))))))
-(check-sat)
-Test/EUF/Issue126.lean:77:55: error: unsolved goals
-n✝ a r✝ v✝ : Type
-b : a → Prop
-nmm : a → n✝ → Prop
-ne ngt nm : n✝ → Prop
-nsih : ∀ (s1 s2 : n✝), ∃ a, nmm a s1 ∧ nmm a s2 ∧ ¬b a
-noh : ∀ (s : n✝), ngt s → ∃ a, nmm a s ∧ ¬b a
-nsg : ∀ (s : n✝), nm s → ngt s
-nne : ∀ (s : n✝), ngt s → ¬ne s
-sa : a → a → r✝ → v✝ → Prop
-sb sc : a → a → a → r✝ → v✝ → Prop
-sg : a → r✝ → Prop
-sd se sf : a → a → r✝ → v✝ → Prop
-ha :
-  (∀ (s d₁ d₂ : a) (r : r✝) (v₁ v₂ : v✝), ¬b d₁ ∧ ¬b d₂ ∧ sf d₁ s r v₁ ∧ sf d₂ s r v₂ → v₁ = v₂) ∧
-    (∀ (s d : a) (r : r✝) (v : v✝), ¬b s ∧ ¬b d ∧ sf d s r v → sg s r ∧ ∀ (d : a), sa s d r v) ∧
-      (∀ (s d : a) (r : r✝) (v : v✝), ¬b s ∧ ¬b d ∧ se d s r v → sg s r ∧ ∀ (d : a), sa s d r v) ∧
-        (∀ (s o d₁ d₂ : a) (r : r✝) (v₁ v₂ : v✝), ¬b s → sc s d₁ o r v₁ ∧ sc s d₂ o r v₂ → v₁ = v₂) ∧
-          (∀ (s o d₁ d₂ : a) (r : r✝) (v₁ v₂ : v✝), ¬b s → sb s d₁ o r v₁ ∧ sb s d₂ o r v₂ → v₁ = v₂) ∧
-            (∀ (s d₁ d₂ : a) (r : r✝) (v₁ v₂ : v✝), ¬b s → sa s d₁ r v₁ ∧ sa s d₂ r v₂ → v₁ = v₂) ∧
-              (∀ (s d : a) (r : r✝) (v : v✝), ¬b s → ((∀ (d : a), sa s d r v) ↔ sa s d r v)) ∧
-                (∀ (n o : a) (r : r✝) (v : v✝), ¬b n → sf n o r v → ∃ q, nm q ∧ ∀ (s : a), nmm s q → sc s n o r v) ∧
-                  (∀ (n o : a) (r : r✝) (v : v✝),
-                      ¬b n →
-                        se n o r v →
-                          (∃ q, nm q ∧ ∀ (s : a), nmm s q → sb s n o r v) ∨
-                            ∃ q, ngt q ∧ ∀ (s : a), nmm s q → sc s n o r v) ∧
-                    (∀ (n d o : a) (r : r✝) (v : v✝), ¬b n → (se n o r v ↔ sc n d o r v)) ∧
-                      (∀ (n o : a) (r : r✝) (v : v✝), ¬b n → sd n o r v → sa o n r v) ∧
-                        (∀ (n d o : a) (r : r✝) (v : v✝), ¬b n → (sd n o r v ↔ sb n d o r v)) ∧
-                          ∀ (s : a) (r : r✝), ¬b s → (sg s r ↔ ∃ v, ∀ (d : a), sa s d r v)
-ta : a → a → r✝ → v✝ → Prop
-tb tc : a → a → a → r✝ → v✝ → Prop
-tg : a → r✝ → Prop
-td te tf : a → a → r✝ → v✝ → Prop
-hb :
-  (∀ (s d : a) (r : r✝) (v : v✝), ¬b s ∧ (sa s d r v ↔ ta s d r v) ∨ b s ∧ (sa s d r v → ta s d r v)) ∧
-    (∀ (s d o : a) (r : r✝) (v : v✝), ¬b s ∧ (sb s d o r v ↔ tb s d o r v) ∨ b s ∧ (sb s d o r v → tb s d o r v)) ∧
-      (∀ (s d o : a) (r : r✝) (v : v✝), ¬b s ∧ (sc s d o r v ↔ tc s d o r v) ∨ b s ∧ (sc s d o r v → tc s d o r v)) ∧
-        (∀ (a_2 : a) (a_3 : r✝), sg a_2 a_3 = tg a_2 a_3) ∧
-          (∀ (a_2 a_3 : a) (a_4 : r✝) (a_5 : v✝), sd a_2 a_3 a_4 a_5 = td a_2 a_3 a_4 a_5) ∧
-            (∀ (a_2 a_3 : a) (a_4 : r✝) (a_5 : v✝), se a_2 a_3 a_4 a_5 = te a_2 a_3 a_4 a_5) ∧
-              ∀ (a_2 a_3 : a) (a_4 : r✝) (a_5 : v✝), sf a_2 a_3 a_4 a_5 = tf a_2 a_3 a_4 a_5
-n o : a
-r : r✝
-v : v✝
-⊢ ¬b n → te n o r v → (∃ q, nm q ∧ ∀ (s : a), nmm s q → tb s n o r v) ∨ ∃ q, ngt q ∧ ∀ (s : a), nmm s q → tc s n o r v
+Test/EUF/Issue126.lean:3:8: warning: declaration uses 'sorry'
diff --git a/Test/EUF/Issue126.lean b/Test/EUF/Issue126.lean
index 91beb456..f8e68926 100644
--- a/Test/EUF/Issue126.lean
+++ b/Test/EUF/Issue126.lean
@@ -1,6 +1,8 @@
 import Smt
 
-theorem extracted_1 (n a r v : Type) (b : a → Prop)
+theorem extracted_1 (n a r v : Type)
+  [Nonempty n] [Nonempty a] [Nonempty r] [Nonempty v]
+  (b : a → Prop)
   (nmm : a → n → Prop) (ne ngt nm : n → Prop)
   (nsih : ∀ (s1 s2 : n), ∃ a, nmm a s1 ∧ nmm a s2 ∧ ¬b a)
   (noh : ∀ (s : n), ngt s → ∃ a, nmm a s ∧ ¬b a)
@@ -75,4 +77,5 @@ theorem extracted_1 (n a r v : Type) (b : a → Prop)
       (∃ q, nm q ∧ ∀ (s : a), nmm s q → tb s n o r v) ∨
         ∃ q,
           ngt q ∧ ∀ (s : a), nmm s q → tc s n o r v := by
-  smt_show [nsih, noh, nsg, nne, ha, hb]
+  smt [nsih, noh, nsg, nne, ha, hb]
+  all_goals sorry
diff --git a/Test/Nat/Sum'.expected b/Test/Nat/Sum'.expected
index 17344569..832d835e 100644
--- a/Test/Nat/Sum'.expected
+++ b/Test/Nat/Sum'.expected
@@ -1,8 +1,8 @@
 Test/Nat/Sum'.lean:7:12: error: tactic 'assumption' failed
 case zero.a
-_uniq✝⁹⁸⁸¹⁻⁰ :
+_uniq✝⁹⁸⁸²⁻⁰ :
   ¬((∀ (n : Int), sum n = if n = 0 then 0 else n + sum (if 1 ≤ n then n - 1 else 0)) ∧
-      (∀ («_uniq.4872» : Int), «_uniq.4872» ≥ 0 → sum «_uniq.4872» ≥ 0) ∧ Smt.Reconstruct.Builtin.distinct [sum 0, 0])
+      (∀ (_uniq.4872 : Int), _uniq.4872 ≥ 0 → sum _uniq.4872 ≥ 0) ∧ Smt.Reconstruct.Builtin.distinct [sum 0, 0])
 ⊢ ¬Smt.Reconstruct.andN' [Nat → Nat] ¬sum 0 = 0 * (0 + 1) / 2
 goal: sum (n + 1) = (n + 1) * (n + 1 + 1) / 2
 
@@ -11,7 +11,7 @@ query:
 (declare-const n Nat)
 (assert (>= n 0))
 (define-fun-rec sum ((n Nat)) Nat (ite (= n 0) 0 (+ n (sum (ite (<= 1 n) (- n 1) 0)))))
-(assert (forall ((_uniq.10851 Nat)) (=> (>= _uniq.10851 0) (>= (sum _uniq.10851) 0))))
+(assert (forall ((_uniq.10852 Nat)) (=> (>= _uniq.10852 0) (>= (sum _uniq.10852) 0))))
 (assert (= (sum n) (div (* n (+ n 1)) 2)))
 (assert (distinct (sum (+ n 1)) (div (* (+ n 1) (+ (+ n 1) 1)) 2)))
 (check-sat)
diff --git a/Test/linarith.expected b/Test/linarith.expected
index 9f0b3684..45481b77 100644
--- a/Test/linarith.expected
+++ b/Test/linarith.expected
@@ -1,19 +1,6 @@
-Test/linarith.lean:5:2: error: [arithPolyNorm]: could not prove y - x = -(-y + x - 0)
-Test/linarith.lean:8:2: error: [arithPolyNorm]: could not prove y - x = -(-y + x - 0)
 Test/linarith.lean:34:9: warning: unused variable `e`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
 Test/linarith.lean:53:0: warning: declaration uses 'sorry'
-Test/linarith.lean:65:2: error: [arithPolyNorm]: could not prove A * B * (1 / 8) = (-(A * B) - 0) * (-1 / 8)
-Test/linarith.lean:68:2: error: [arithPolyNorm]: could not prove B * A * (1 / 8) = (-(B * A) - 0) * (-1 / 8)
-Test/linarith.lean:71:2: error: [arithPolyNorm]: could not prove ε * (1 / 42) = (-ε - 0) * (-1 / 42)
-Test/linarith.lean:75:2: error: [arithPolyNorm]: could not prove z * (1 / 2) - x * 4 = (z - x * 8 - 0) * (1 / 2)
-Test/linarith.lean:78:2: error: [arithPolyNorm]: could not prove ε * (1 / 2) = (-ε - 0) * (-1 / 2)
-Test/linarith.lean:84:2: error: [arithPolyNorm]: could not prove x = -(-x - 0)
-Test/linarith.lean:87:2: error: [arithPolyNorm]: could not prove x = x - 0
-Test/linarith.lean:90:2: error: [arithPolyNorm]: could not prove x * (1 / 2) = (x - 0) * (1 / 2)
-Test/linarith.lean:93:2: error: [arithPolyNorm]: could not prove x * (5 / 4) = (x - 0) * (5 / 4)
-Test/linarith.lean:96:2: error: [arithPolyNorm]: could not prove x * (1 / 6) = (-x - 0) * (-1 / 6)
-Test/linarith.lean:99:2: error: [arithPolyNorm]: could not prove x * (3 / 2) = (-x - 0) * (-3 / 2)
 Test/linarith.lean:101:9: warning: unused variable `a`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
 Test/linarith.lean:101:13: warning: unused variable `c`
@@ -22,17 +9,12 @@ Test/linarith.lean:106:9: warning: unused variable `a`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
 Test/linarith.lean:106:13: warning: unused variable `c`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-Test/linarith.lean:113:2: error: [arithPolyNorm]: could not prove V - v = V - v - 0
 Test/linarith.lean:118:60: warning: unused variable `h3`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-Test/linarith.lean:123:2: error: [arithPolyNorm]: could not prove a = -(-a - 0)
-Test/linarith.lean:126:2: error: [arithPolyNorm]: could not prove b = -(-b - 0)
-Test/linarith.lean:129:2: error: [arithPolyNorm]: could not prove z * 2 - y = (z + y * (-1 / 2) - 0) * 2
-Test/linarith.lean:135:2: error: [arithPolyNorm]: could not prove z * 2 - y = (z + y * (-1 / 2) - 0) * 2
-Test/linarith.lean:143:2: error: [arithPolyNorm]: could not prove a * 2 = (a - 0) * 2
-Test/linarith.lean:146:2: error: [arithPolyNorm]: could not prove -x + y = -(x - y - 0)
-Test/linarith.lean:162:2: error: [arithPolyNorm]: could not prove z * 2 - x * 4 = (z - x * 2 - 0) * 2
-Test/linarith.lean:166:2: error: [arithPolyNorm]: could not prove -(x * 4) + z * 2 = (-(x * 2) + z - 0) * 2
+Test/linarith.lean:125:9: warning: unused variable `a`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+Test/linarith.lean:125:13: warning: unused variable `c`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
 Test/linarith.lean:168:34: warning: unused variable `z`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
 Test/linarith.lean:169:5: warning: unused variable `h5`
diff --git a/lake-manifest.json b/lake-manifest.json
index 93f23886..c72f9d8d 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "ea389d54a9050342df6980427c4da451475da0a2",
+   "rev": "c97ff4cfc218c11af8c1598b8225a6fcc094f5cd",
    "name": "cvc5",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lakefile.lean b/lakefile.lean
index ab470ebf..e4f5e63a 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -127,12 +127,12 @@ where
     return 0
 
 /--
-Run Lean profiler and generate profiler information.
+Run Lean profiler and generate profiling information.
 
 USAGE:
-  lake script run profile
+  lake script run profile <File>.lean <log>.json
 
-Update expected output of tests.
+Use Firefox Profiler UI to view profiling information.
 -/
 script profile args do
   let file : FilePath := args[0]!