diff --git a/Smt/Reconstruct.lean b/Smt/Reconstruct.lean
index aa3c309c..196127a3 100644
--- a/Smt/Reconstruct.lean
+++ b/Smt/Reconstruct.lean
@@ -219,7 +219,7 @@ def solve (query : String) (timeout : Option Nat) : MetaM (Except Error cvc5.Pro
       if h : 0 < ps.size then
         trace[smt.solve] "proof:\n{← Solver.proofToString ps[0]}"
         return ps[0]
-    throw (self := instMonadExceptOfMonadExceptOf _ _) (Error.user_error "something went wrong")
+    throw (self := instMonadExceptOfMonadExceptOf _ _) (Error.error s!"Expected unsat, got {r}")
 
 syntax (name := reconstruct) "reconstruct" str : tactic
 
diff --git a/Smt/Reconstruct/Arith/Rewrites.lean b/Smt/Reconstruct/Arith/Rewrites.lean
index 659760cb..c4b4eb6b 100644
--- a/Smt/Reconstruct/Arith/Rewrites.lean
+++ b/Smt/Reconstruct/Arith/Rewrites.lean
@@ -24,7 +24,7 @@ theorem arith_div_by_const_elim_real_pos {t c₁ c₂ : Real} : t / (c₁ / c₂
 theorem arith_div_by_const_elim_real_neg {t c₁ c₂ : Real} : t / (-c₁ / c₂) = t * (-c₂ / c₁) :=
   div_eq_mul_one_div t (-c₁ / c₂) ▸ one_div_div (-c₁) c₂ ▸ div_neg c₂ ▸ neg_div c₁ c₂ ▸ rfl
 
--- https://github.com/cvc5/cvc5/blob/proof-new/src/theory/arith/rewrites
+-- https://github.com/cvc5/cvc5/blob/main/src/theory/arith/rewrites
 
 variable {α : Type} [h : LinearOrderedRing α]
 
diff --git a/Smt/Reconstruct/BitVec.lean b/Smt/Reconstruct/BitVec.lean
index 71e6343d..4c4f791c 100644
--- a/Smt/Reconstruct/BitVec.lean
+++ b/Smt/Reconstruct/BitVec.lean
@@ -22,12 +22,12 @@ open Lean Qq
 
 @[smt_sort_reconstruct] def reconstructBitVecSort : SortReconstructor := fun s => do match s.getKind with
   | .BITVECTOR_SORT =>
-    let w : Nat := s.getBitVectorSize.val
+    let w : Nat := s.getBitVectorSize!.val
     return q(BitVec $w)
   | _             => return none
 
 partial def synthDecidableInst (t : cvc5.Term) : ReconstructM Expr := do match t.getKind with
-    | .CONST_BOOLEAN => return if t.getBooleanValue then q(instDecidableTrue) else q(instDecidableFalse)
+    | .CONST_BOOLEAN => return if t.getBooleanValue! then q(instDecidableTrue) else q(instDecidableFalse)
     | .NOT =>
       let p : Q(Prop) ← reconstructTerm t[0]!
       let hp : Q(Decidable $p) ← synthDecidableInst t[0]!
@@ -43,14 +43,14 @@ partial def synthDecidableInst (t : cvc5.Term) : ReconstructM Expr := do match t
         let hq : Q(Decidable $q) ← synthDecidableInst t[1]!
         return q(@instDecidableEqOfIff $p $q (@instDecidableIff $p $q $hp $hq))
       if t[0]!.getSort.getKind == .BITVECTOR_SORT then
-        let w : Nat := t[0]!.getSort.getBitVectorSize.val
+        let w : Nat := t[0]!.getSort.getBitVectorSize!.val
         return q(@instDecidableEqBitVec $w)
       let p : Q(Prop) ← reconstructTerm t
       Meta.synthInstance q(Decidable $p)
     | .BITVECTOR_BIT =>
-      let w : Nat := t[0]!.getSort.getBitVectorSize.val
+      let w : Nat := t[0]!.getSort.getBitVectorSize!.val
       let x : Q(BitVec $w) ← reconstructTerm t[0]!
-      let i : Nat := t.getOp[0]!.getIntegerValue.toNat
+      let i : Nat := t.getOp![0]!.getIntegerValue!.toNat
       return q(instDecidableEqBool («$x».getLsbD $i) true)
     | _ =>
       let p : Q(Prop) ← reconstructTerm t
@@ -67,152 +67,152 @@ where
 
 @[smt_term_reconstruct] def reconstructBitVec : TermReconstructor := fun t => do match t.getKind with
   | .CONST_BITVECTOR =>
-    let w : Nat := t.getSort.getBitVectorSize.val
-    let v : Nat := (t.getBitVectorValue 10).toNat!
+    let w : Nat := t.getSort.getBitVectorSize!.val
+    let v : Nat := (t.getBitVectorValue! 10).toNat!
     return q(BitVec.ofNat $w $v)
   | .BITVECTOR_CONCAT =>
     let n : Nat := t.getNumChildren
-    let w₁ : Nat := t[0]!.getSort.getBitVectorSize.val
+    let w₁ : Nat := t[0]!.getSort.getBitVectorSize!.val
     let a : Q(BitVec $w₁) ← reconstructTerm t[0]!
     let f := fun ⟨w₁, a⟩ i => do
-      let w₂ : Nat := t[i]!.getSort.getBitVectorSize.val
+      let w₂ : Nat := t[i]!.getSort.getBitVectorSize!.val
       let x : Q(BitVec $w₂) ← reconstructTerm t[i]!
       return ⟨q($w₁ + $w₂), q($a ++ $x)⟩
     let ⟨_, a⟩ ← [1:n].foldlM f (⟨q($w₁), a⟩ : Σ w : Q(Nat), Q(BitVec $w))
     return a
   | .BITVECTOR_AND =>
-    let w : Nat := t.getSort.getBitVectorSize.val
+    let w : Nat := t.getSort.getBitVectorSize!.val
     leftAssocOp q(@AndOp.and (BitVec $w) _) t
   | .BITVECTOR_OR =>
-    let w : Nat := t.getSort.getBitVectorSize.val
+    let w : Nat := t.getSort.getBitVectorSize!.val
     leftAssocOp q(@OrOp.or (BitVec $w) _) t
   | .BITVECTOR_XOR =>
-    let w : Nat := t.getSort.getBitVectorSize.val
+    let w : Nat := t.getSort.getBitVectorSize!.val
     leftAssocOp q(@Xor.xor (BitVec $w) _) t
   | .BITVECTOR_NOT =>
-    let w : Nat := t.getSort.getBitVectorSize.val
+    let w : Nat := t.getSort.getBitVectorSize!.val
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
     return q(~~~$x)
   | .BITVECTOR_MULT =>
-    let w : Nat := t.getSort.getBitVectorSize.val
+    let w : Nat := t.getSort.getBitVectorSize!.val
     leftAssocOp q(@HMul.hMul (BitVec $w) (BitVec $w) (BitVec $w) _) t
   | .BITVECTOR_ADD =>
-    let w : Nat := t.getSort.getBitVectorSize.val
+    let w : Nat := t.getSort.getBitVectorSize!.val
     leftAssocOp q(@HAdd.hAdd (BitVec $w) (BitVec $w) (BitVec $w) _) t
   | .BITVECTOR_SUB =>
-    let w : Nat := t.getSort.getBitVectorSize.val
+    let w : Nat := t.getSort.getBitVectorSize!.val
     leftAssocOp q(@HSub.hSub (BitVec $w) (BitVec $w) (BitVec $w) _) t
   | .BITVECTOR_NEG =>
-    let w : Nat := t.getSort.getBitVectorSize.val
+    let w : Nat := t.getSort.getBitVectorSize!.val
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
     return q(-$x)
   | .BITVECTOR_UDIV =>
-    let w : Nat := t.getSort.getBitVectorSize.val
+    let w : Nat := t.getSort.getBitVectorSize!.val
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
     let y : Q(BitVec $w) ← reconstructTerm t[1]!
     return q(BitVec.smtUDiv $x $y)
   | .BITVECTOR_UREM =>
-    let w : Nat := t.getSort.getBitVectorSize.val
+    let w : Nat := t.getSort.getBitVectorSize!.val
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
     let y : Q(BitVec $w) ← reconstructTerm t[1]!
     return q($x % $y)
   | .BITVECTOR_SDIV =>
-    let w : Nat := t.getSort.getBitVectorSize.val
+    let w : Nat := t.getSort.getBitVectorSize!.val
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
     let y : Q(BitVec $w) ← reconstructTerm t[1]!
     return q(BitVec.smtSDiv $x $y)
   | .BITVECTOR_SREM =>
-    let w : Nat := t.getSort.getBitVectorSize.val
+    let w : Nat := t.getSort.getBitVectorSize!.val
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
     let y : Q(BitVec $w) ← reconstructTerm t[1]!
     return q(BitVec.srem $x $y)
   | .BITVECTOR_SMOD =>
-    let w : Nat := t.getSort.getBitVectorSize.val
+    let w : Nat := t.getSort.getBitVectorSize!.val
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
     let y : Q(BitVec $w) ← reconstructTerm t[1]!
     return q(BitVec.smod $x $y)
   | .BITVECTOR_SHL =>
-    let w : Nat := t.getSort.getBitVectorSize.val
+    let w : Nat := t.getSort.getBitVectorSize!.val
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
-    let i : Nat := t.getOp[0]!.getIntegerValue.toNat
+    let i : Nat := t.getOp![0]!.getIntegerValue!.toNat
     return q($x <<< $i)
   | .BITVECTOR_LSHR =>
-    let w : Nat := t.getSort.getBitVectorSize.val
+    let w : Nat := t.getSort.getBitVectorSize!.val
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
-    let i : Nat := t.getOp[0]!.getIntegerValue.toNat
+    let i : Nat := t.getOp![0]!.getIntegerValue!.toNat
     return q($x >>> $i)
   | .BITVECTOR_ASHR =>
-    let w : Nat := t.getSort.getBitVectorSize.val
+    let w : Nat := t.getSort.getBitVectorSize!.val
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
-    let i : Nat := t.getOp[0]!.getIntegerValue.toNat
+    let i : Nat := t.getOp![0]!.getIntegerValue!.toNat
     return q(BitVec.sshiftRight $x $i)
   | .BITVECTOR_ULT =>
-    let w : Nat := t.getSort.getBitVectorSize.val
+    let w : Nat := t.getSort.getBitVectorSize!.val
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
     let y : Q(BitVec $w) ← reconstructTerm t[1]!
     return q($x < $y)
   | .BITVECTOR_ULE =>
-    let w : Nat := t.getSort.getBitVectorSize.val
+    let w : Nat := t.getSort.getBitVectorSize!.val
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
     let y : Q(BitVec $w) ← reconstructTerm t[1]!
     return q($x ≤ $y)
   | .BITVECTOR_UGT =>
-    let w : Nat := t.getSort.getBitVectorSize.val
+    let w : Nat := t.getSort.getBitVectorSize!.val
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
     let y : Q(BitVec $w) ← reconstructTerm t[1]!
     return q($x > $y)
   | .BITVECTOR_UGE =>
-    let w : Nat := t.getSort.getBitVectorSize.val
+    let w : Nat := t.getSort.getBitVectorSize!.val
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
     let y : Q(BitVec $w) ← reconstructTerm t[1]!
     return q($x ≥ $y)
   | .BITVECTOR_SLT =>
-    let w : Nat := t.getSort.getBitVectorSize.val
+    let w : Nat := t.getSort.getBitVectorSize!.val
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
     let y : Q(BitVec $w) ← reconstructTerm t[1]!
     return q(BitVec.slt $x $y)
   | .BITVECTOR_SLE =>
-    let w : Nat := t.getSort.getBitVectorSize.val
+    let w : Nat := t.getSort.getBitVectorSize!.val
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
     let y : Q(BitVec $w) ← reconstructTerm t[1]!
     return q(BitVec.sle $x $y)
   | .BITVECTOR_EXTRACT =>
-    let w : Nat := t.getSort.getBitVectorSize.val
-    let i : Nat := t.getOp[0]!.getIntegerValue.toNat
-    let j : Nat := t.getOp[1]!.getIntegerValue.toNat
+    let w : Nat := t.getSort.getBitVectorSize!.val
+    let i : Nat := t.getOp![0]!.getIntegerValue!.toNat
+    let j : Nat := t.getOp![1]!.getIntegerValue!.toNat
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
     return q(«$x».extractLsb $i $j)
   | .BITVECTOR_REPEAT =>
-    let w : Nat := t.getSort.getBitVectorSize.val
-    let n : Nat := t.getOp[0]!.getIntegerValue.toNat
+    let w : Nat := t.getSort.getBitVectorSize!.val
+    let n : Nat := t.getOp![0]!.getIntegerValue!.toNat
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
     return q(«$x».replicate $n)
   | .BITVECTOR_ZERO_EXTEND =>
-    let w : Nat := t.getSort.getBitVectorSize.val
-    let n : Nat := t.getOp[0]!.getIntegerValue.toNat
+    let w : Nat := t.getSort.getBitVectorSize!.val
+    let n : Nat := t.getOp![0]!.getIntegerValue!.toNat
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
     return q(«$x».zeroExtend $n)
   | .BITVECTOR_SIGN_EXTEND =>
-    let w : Nat := t.getSort.getBitVectorSize.val
-    let n : Nat := t.getOp[0]!.getIntegerValue.toNat
+    let w : Nat := t.getSort.getBitVectorSize!.val
+    let n : Nat := t.getOp![0]!.getIntegerValue!.toNat
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
     return q(«$x».signExtend $n)
   | .BITVECTOR_ROTATE_LEFT =>
-    let w : Nat := t.getSort.getBitVectorSize.val
-    let n : Nat := t.getOp[0]!.getIntegerValue.toNat
+    let w : Nat := t.getSort.getBitVectorSize!.val
+    let n : Nat := t.getOp![0]!.getIntegerValue!.toNat
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
     return q(«$x».rotateLeft $n)
   | .BITVECTOR_ROTATE_RIGHT =>
-    let w : Nat := t.getSort.getBitVectorSize.val
-    let n : Nat := t.getOp[0]!.getIntegerValue.toNat
+    let w : Nat := t.getSort.getBitVectorSize!.val
+    let n : Nat := t.getOp![0]!.getIntegerValue!.toNat
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
     return q(«$x».rotateRight $n)
   | .INT_TO_BITVECTOR =>
-    let w : Nat := t.getSort.getBitVectorSize.val
+    let w : Nat := t.getSort.getBitVectorSize!.val
     let x : Q(Int) ← reconstructTerm t[0]!
     return q(BitVec.ofNat $w «$x».toNat)
   | .BITVECTOR_TO_NAT =>
-    let w : Nat := t[0]!.getSort.getBitVectorSize.val
+    let w : Nat := t[0]!.getSort.getBitVectorSize!.val
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
     return q(«$x».toNat)
   | .BITVECTOR_FROM_BOOLS =>
@@ -226,9 +226,9 @@ where
     let bs : Q(BitVec $w) ← (List.range w).foldlM f bs
     return q($bs)
   | .BITVECTOR_BIT =>
-    let w : Nat := t[0]!.getSort.getBitVectorSize.val
+    let w : Nat := t[0]!.getSort.getBitVectorSize!.val
     let x : Q(BitVec $w) ← reconstructTerm t[0]!
-    let i : Nat := t.getOp[0]!.getIntegerValue.toNat
+    let i : Nat := t.getOp![0]!.getIntegerValue!.toNat
     return q(«$x».getLsbD $i = true)
   | _ => return none
 where
@@ -248,12 +248,12 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
     let t := pf.getArguments[0]![0]!
     match t.getKind with
     | .CONST_BITVECTOR =>
-      let w : Nat := t.getSort.getBitVectorSize.toNat
+      let w : Nat := t.getSort.getBitVectorSize!.toNat
       let t : Q(BitVec $w) ← reconstructTerm pf.getResult[0]!
       let t' : Q(BitVec $w) ← reconstructTerm pf.getResult[1]!
       addThm q($t = $t') q(Eq.refl $t)
     | .CONSTANT =>
-      let w : Nat := t.getSort.getBitVectorSize.toNat
+      let w : Nat := t.getSort.getBitVectorSize!.toNat
       let x : Q(BitVec $w) ← reconstructTerm pf.getResult[0]!
       let x' : Q(BitVec $w) ← reconstructTerm pf.getResult[1]!
       let h : Q(«$x».bb = $x') ← Meta.mkFreshExprMVar q(«$x».bb = $x')
@@ -266,7 +266,7 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
       mv.refl
       addThm q($x = $x') q(Eq.trans (BitVec.self_eq_bb $x) $h)
     | .EQUAL =>
-      let w : Nat := t[0]!.getSort.getBitVectorSize.toNat
+      let w : Nat := t[0]!.getSort.getBitVectorSize!.toNat
       let x : Q(BitVec $w) ← reconstructTerm pf.getResult[0]![0]!
       let y : Q(BitVec $w) ← reconstructTerm pf.getResult[0]![1]!
       let p : Q(Prop) ← reconstructTerm pf.getResult[1]!
@@ -283,7 +283,7 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
       mv.refl
       addThm q(($x = $y) = $p) q(Eq.trans (BitVec.eq_eq_beq $x $y) (Bool.eq_of_decide_eq $h))
     | .BITVECTOR_ADD =>
-      let w : Nat := t[0]!.getSort.getBitVectorSize.toNat
+      let w : Nat := t[0]!.getSort.getBitVectorSize!.toNat
       let x : Q(BitVec $w) ← reconstructTerm pf.getResult[0]![0]!
       let y : Q(BitVec $w) ← reconstructTerm pf.getResult[0]![1]!
       let z : Q(BitVec $w) ← reconstructTerm pf.getResult[1]!
diff --git a/Smt/Reconstruct/Builtin.lean b/Smt/Reconstruct/Builtin.lean
index ac6b0731..ed42b906 100644
--- a/Smt/Reconstruct/Builtin.lean
+++ b/Smt/Reconstruct/Builtin.lean
@@ -16,11 +16,11 @@ open Lean Qq
 
 @[smt_sort_reconstruct] def reconstructBuiltinSort : SortReconstructor := fun s => do match s.getKind with
   | .FUNCTION_SORT =>
-    let mut ct : Q(Type) ← reconstructSort s.getFunctionCodomainSort
+    let mut ct : Q(Type) ← reconstructSort s.getFunctionCodomainSort!
     let f s (a : Q(Type)) := do
       let t : Q(Type) ← reconstructSort s
       return q($t → $a)
-    let t ← s.getFunctionDomainSorts.foldrM f ct
+    let t ← s.getFunctionDomainSorts!.foldrM f ct
     return t
   | _              => return none
 
@@ -40,7 +40,7 @@ def getFVarOrConstExpr! (n : String) : ReconstructM Expr := do
 
 @[smt_term_reconstruct] def reconstructBuiltin : TermReconstructor := fun t => do match t.getKind with
   | .VARIABLE => getFVarExpr! (getVariableName t)
-  | .CONSTANT => getFVarOrConstExpr! t.getSymbol
+  | .CONSTANT => getFVarOrConstExpr! t.getSymbol!
   | .EQUAL =>
     let α : Q(Type) ← reconstructSort t[0]!.getSort
     let x : Q($α) ← reconstructTerm t[0]!
@@ -61,17 +61,17 @@ def getFVarOrConstExpr! (n : String) : ReconstructM Expr := do
     let x : Q($α) ← reconstructTerm t[1]!
     let y : Q($α) ← reconstructTerm t[2]!
     return q(@ite $α $c $h $x $y)
-  | .SKOLEM => match t.getSkolemId with
-    | .PURIFY => reconstructTerm t.getSkolemIndices[0]!
+  | .SKOLEM => match t.getSkolemId! with
+    | .PURIFY => reconstructTerm t.getSkolemIndices![0]!
     | _ => return none
   | _ => return none
 where
   getVariableName (t : cvc5.Term) : Name :=
     if t.hasSymbol then
-      if t.getSymbol.toName == .anonymous then
-        Name.mkSimple t.getSymbol
+      if t.getSymbol!.toName == .anonymous then
+        Name.mkSimple t.getSymbol!
       else
-        t.getSymbol.toName
+        t.getSymbol!.toName
     else Name.num `x t.getId
 
 def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
diff --git a/Smt/Reconstruct/Builtin/Rewrites.lean b/Smt/Reconstruct/Builtin/Rewrites.lean
index ca57b867..c676fd45 100644
--- a/Smt/Reconstruct/Builtin/Rewrites.lean
+++ b/Smt/Reconstruct/Builtin/Rewrites.lean
@@ -7,7 +7,7 @@ Authors: Abdalrhman Mohamed
 
 namespace Smt.Reconstruct.Builtin
 
--- https://github.com/cvc5/cvc5/blob/proof-new/src/theory/builtin/rewrites
+-- https://github.com/cvc5/cvc5/blob/main/src/theory/builtin/rewrites
 
 -- ITE
 
diff --git a/Smt/Reconstruct/Int.lean b/Smt/Reconstruct/Int.lean
index 7409ae62..9b00f4f8 100644
--- a/Smt/Reconstruct/Int.lean
+++ b/Smt/Reconstruct/Int.lean
@@ -22,12 +22,12 @@ open Qq
   | _             => return none
 
 @[smt_term_reconstruct] def reconstructInt : TermReconstructor := fun t => do match t.getKind with
-  | .SKOLEM => match t.getSkolemId with
+  | .SKOLEM => match t.getSkolemId! with
     | .INT_DIV_BY_ZERO => return q(fun (x : Int) => x / 0)
     | .MOD_BY_ZERO => return q(fun (x : Int) => x % 0)
     | _ => return none
   | .CONST_INTEGER =>
-    let x : Int := t.getIntegerValue
+    let x : Int := t.getIntegerValue!
     let x' : Q(Nat) := mkRawNatLit x.natAbs
     if x ≥ 0 then
       return q(OfNat.ofNat $x' : Int)
@@ -92,6 +92,12 @@ where
 
 def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
   match pf.getRewriteRule with
+  | .ARITH_POW_ELIM =>
+    if !pf.getResult[0]![0]!.getSort.isInteger then return none
+    let x : Q(Int) ← reconstructTerm pf.getResult[0]![0]!
+    let c : Q(Nat) ← reconstructTerm pf.getResult[0]![1]!
+    let y : Q(Int) ← reconstructTerm pf.getResult[1]!
+    addThm q($x ^ $c = $y) q(Eq.refl ($x ^ $c))
   | .ARITH_PLUS_ZERO =>
     if !pf.getArguments[1]![0]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
@@ -126,19 +132,6 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
   | .ARITH_INT_MOD_TOTAL_ZERO =>
     let t : Q(Int) ← reconstructTerm pf.getArguments[1]!
     addThm q($t % 0 = $t) q(@Rewrite.int_mod_total_zero $t)
-  | .ARITH_NEG_NEG_ONE =>
-    if !pf.getArguments[1]!.getSort.isInteger then return none
-    let t : Q(Int) ← reconstructTerm pf.getArguments[1]!
-    addThm q(-1 * (-1 * $t) = $t) q(@Rewrite.neg_neg_one $t)
-  | .ARITH_ELIM_UMINUS =>
-    if !pf.getArguments[1]!.getSort.isInteger then return none
-    let t : Q(Int) ← reconstructTerm pf.getArguments[1]!
-    addThm q(-$t = -1 * $t) q(@Rewrite.elim_uminus $t)
-  | .ARITH_ELIM_MINUS =>
-    if !pf.getArguments[1]!.getSort.isInteger then return none
-    let t : Q(Int) ← reconstructTerm pf.getArguments[1]!
-    let s : Q(Int) ← reconstructTerm pf.getArguments[2]!
-    addThm q($t - $s = $t + -1 * $s) q(@Rewrite.elim_minus $t $s)
   | .ARITH_ELIM_GT =>
     if !pf.getArguments[1]!.getSort.isInteger then return none
     let t : Q(Int) ← reconstructTerm pf.getArguments[1]!
@@ -208,14 +201,6 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
     if !pf.getArguments[2]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
     addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Int Int Int _) q(1 : Int) q(@Rewrite.mult_dist) args)
-  | .ARITH_PLUS_CANCEL1 =>
-    if !pf.getArguments[2]!.getSort.isInteger then return none
-    let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Int Int Int _) q(0 : Int) q(@Rewrite.plus_cancel1) args)
-  | .ARITH_PLUS_CANCEL2 =>
-    if !pf.getArguments[2]!.getSort.isInteger then return none
-    let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Int Int Int _) q(0 : Int) q(@Rewrite.plus_cancel2) args)
   | .ARITH_ABS_ELIM =>
     if !pf.getArguments[1]!.getSort.isInteger then return none
     let t : Q(Int) ← reconstructTerm pf.getArguments[1]!
@@ -403,10 +388,10 @@ where
     addTac q($a = $b) Int.nativePolyNorm
   | .ARITH_POLY_NORM_REL =>
     if !pf.getResult[0]![0]!.getSort.isInteger then return none
-    let cx : Int := pf.getChildren[0]!.getResult[0]![0]!.getIntegerValue
+    let cx : Int := pf.getChildren[0]!.getResult[0]![0]!.getIntegerValue!
     let x₁ : Q(Int) ← reconstructTerm pf.getResult[0]![0]!
     let x₂ : Q(Int) ← reconstructTerm pf.getResult[0]![1]!
-    let cy : Int := pf.getChildren[0]!.getResult[1]![0]!.getIntegerValue
+    let cy : Int := pf.getChildren[0]!.getResult[1]![0]!.getIntegerValue!
     let y₁ : Q(Int) ← reconstructTerm pf.getResult[1]![0]!
     let y₂ : Q(Int) ← reconstructTerm pf.getResult[1]![1]!
     let h : Q($cx * ($x₁ - $x₂) = $cy * ($y₁ - $y₂)) ← reconstructProof pf.getChildren[0]!
diff --git a/Smt/Reconstruct/Int/Rewrites.lean b/Smt/Reconstruct/Int/Rewrites.lean
index 6a4745ba..116c2180 100644
--- a/Smt/Reconstruct/Int/Rewrites.lean
+++ b/Smt/Reconstruct/Int/Rewrites.lean
@@ -9,7 +9,7 @@ namespace Smt.Reconstruct.Int.Rewrite
 
 open Function
 
--- https://github.com/cvc5/cvc5/blob/proof-new/src/theory/arith/rewrites
+-- https://github.com/cvc5/cvc5/blob/main/src/theory/arith/rewrites
 
 variable {t ts x xs : Int}
 
@@ -35,15 +35,8 @@ theorem int_mod_total_one {t : Int} : t % 1 = 0 :=
 theorem int_mod_total_zero {t : Int} : t % 0 = t :=
   Int.emod_zero t
 
-theorem neg_neg_one : -1 * (-1 * t) = t :=
-  Int.neg_mul _ t ▸ (Int.one_mul t).symm ▸ Int.neg_mul_neg _ t ▸ (Int.one_mul t).symm ▸ rfl
-
 -- Eliminations
 
-theorem elim_uminus : -t = -1 * t :=
-  Int.neg_eq_neg_one_mul t ▸ rfl
-theorem elim_minus : t - s = t + -1 * s :=
-  Int.neg_eq_neg_one_mul s ▸ Int.sub_eq_add_neg ▸ rfl
 theorem elim_gt : (t > s) = ¬(t ≤ s) :=
   propext Int.not_le.symm
 theorem elim_lt : (t < s) = ¬(t ≥ s) :=
@@ -89,13 +82,6 @@ theorem mult_flatten : xs * (w * ys) * zs = xs * w * ys * zs :=
 theorem mult_dist : x * (y + z + ws) = x * y + x * (z + ws) :=
   Int.add_assoc y z ws ▸ Int.mul_add x y (z + ws) ▸ rfl
 
-theorem plus_cancel1 : ts + x + ss + (-1 * x) + rs = ts + ss + rs :=
-  Int.neg_eq_neg_one_mul x ▸ Int.add_assoc ts x ss ▸ Int.add_assoc ts (x + ss) (-x) ▸
-  Int.add_comm x ss ▸ (Int.add_neg_cancel_right ss x).symm ▸ rfl
-theorem plus_cancel2 : ts + (-1 * x) + ss + x + rs = ts + ss + rs :=
-  Int.neg_eq_neg_one_mul x ▸ Int.add_assoc ts (-x) ss ▸ Int.add_assoc ts (-x + ss) x ▸
-  Int.add_comm (-x) ss ▸ (Int.neg_add_cancel_right ss x).symm ▸ rfl
-
 theorem abs_elim : (if x < 0 then -x else x) = if x < 0 then -x else x :=
   rfl
 
diff --git a/Smt/Reconstruct/Prop.lean b/Smt/Reconstruct/Prop.lean
index e364fd58..1c7a8b79 100644
--- a/Smt/Reconstruct/Prop.lean
+++ b/Smt/Reconstruct/Prop.lean
@@ -21,7 +21,7 @@ open Lean Qq
   | _             => return none
 
 @[smt_term_reconstruct] def reconstructProp : TermReconstructor := fun t => do match t.getKind with
-  | .CONST_BOOLEAN => return if t.getBooleanValue then q(True) else q(False)
+  | .CONST_BOOLEAN => return if t.getBooleanValue! then q(True) else q(False)
   | .NOT =>
     let b : Q(Prop) ← reconstructTerm t[0]!
     return q(¬$b)
@@ -107,9 +107,15 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
   | .BOOL_AND_CONF =>
     let args ← reconstructArgs pf.getArguments[1:]
     addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(And) q(True) q(@Prop.bool_and_conf) args)
+  | .BOOL_AND_CONF2 =>
+    let args ← reconstructArgs pf.getArguments[1:]
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(And) q(True) q(@Prop.bool_and_conf2) args)
   | .BOOL_OR_TAUT =>
     let args ← reconstructArgs pf.getArguments[1:]
     addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Or) q(False) q(@Prop.bool_or_taut) args)
+  | .BOOL_OR_TAUT2 =>
+    let args ← reconstructArgs pf.getArguments[1:]
+    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Or) q(False) q(@Prop.bool_or_taut2) args)
   | .BOOL_OR_DE_MORGAN =>
     let args ← reconstructArgs pf.getArguments[1:]
     addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(Or) q(False) q(@Prop.bool_or_de_morgan) args)
@@ -185,6 +191,16 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
     let p : Q(Prop) ← reconstructTerm pf.getArguments[2]!
     let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
     addThm q(ite $c $p $c = ite $c $p False) q(@Prop.ite_else_lookahead_self $c $p $h)
+  | .ITE_THEN_LOOKAHEAD_NOT_SELF =>
+    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[2]!
+    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    addThm q(ite $c (¬$c) $p = ite $c False $p) q(@Prop.ite_then_lookahead_not_self $c $p $h)
+  | .ITE_ELSE_LOOKAHEAD_NOT_SELF =>
+    let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
+    let p : Q(Prop) ← reconstructTerm pf.getArguments[2]!
+    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    addThm q(ite $c $p (¬$c) = ite $c $p True) q(@Prop.ite_else_lookahead_not_self $c $p $h)
   | .BOOL_NOT_ITE_ELIM =>
     let c : Q(Prop) ← reconstructTerm pf.getArguments[1]!
     let p : Q(Prop) ← reconstructTerm pf.getArguments[2]!
@@ -220,8 +236,8 @@ def clausify (c l : cvc5.Term) : Array cvc5.Term :=
   reclausify (nary .OR c) l
 
 def getResolutionResult (c₁ c₂ : Array cvc5.Term) (pol l : cvc5.Term) : Array cvc5.Term := Id.run do
-  let l₁ := if pol.getBooleanValue then l else l.not
-  let l₂ := if pol.getBooleanValue then l.not else l
+  let l₁ := if pol.getBooleanValue! then l else l.not!
+  let l₂ := if pol.getBooleanValue! then l.not! else l
   let mut ls := #[]
   for li in c₁ do
     if li != l₁ then
@@ -239,12 +255,12 @@ def reconstructResolution (c₁ c₂ : Array cvc5.Term) (pol l : cvc5.Term) (hps
   let qs : Q(List Prop) ← c₂.foldrM f q([])
   let hps : Q(orN $ps) ← pure hps
   let hqs : Q(orN $qs) ← pure hqs
-  let (i?, j?) := if pol.getBooleanValue then (c₁.getIdx? l, c₂.getIdx? l.not) else (c₁.getIdx? l.not, c₂.getIdx? l)
+  let (i?, j?) := if pol.getBooleanValue! then (c₁.getIdx? l, c₂.getIdx? l.not!) else (c₁.getIdx? l.not!, c₂.getIdx? l)
   if let (some i, some j) := (i?, j?) then
     let hi : Q($i < «$ps».length) := .app q(@of_decide_eq_true ($i < «$ps».length) _) q(Eq.refl true)
     let hj : Q($j < «$qs».length) := .app q(@of_decide_eq_true ($j < «$qs».length) _) q(Eq.refl true)
     let hij : Q($ps[$i] = ¬$qs[$j]) :=
-      if pol.getBooleanValue then .app q(Prop.eq_not_not) q($ps[$i])
+      if pol.getBooleanValue! then .app q(Prop.eq_not_not) q($ps[$i])
       else .app q(@Eq.refl Prop) q($ps[$i])
     return q(Prop.orN_resolution $hps $hqs $hi $hj $hij)
   else
@@ -334,7 +350,7 @@ def reconstructChainResolution (cs as : Array cvc5.Term) (ps : Array Expr) : Rec
       let p : Q(Prop) ← reconstructTerm t
       return q($p :: $ps)
     let ps : Q(List Prop) ← (nary .AND pf.getChildren[0]!.getResult).foldrM f q([])
-    let i : Nat := pf.getArguments[0]!.getIntegerValue.toNat
+    let i : Nat := pf.getArguments[0]!.getIntegerValue!.toNat
     let hi : Q($i < «$ps».length) := .app q(@of_decide_eq_true ($i < «$ps».length) _) q(Eq.refl true)
     let hps : Q(andN $ps) ← reconstructProof pf.getChildren[0]!
     addThm (← reconstructTerm pf.getResult) q(@Prop.and_elim _ $hps $i $hi)
@@ -353,7 +369,7 @@ def reconstructChainResolution (cs as : Array cvc5.Term) (ps : Array Expr) : Rec
       let p : Q(Prop) ← reconstructTerm t
       return q($p :: $ps)
     let ps : Q(List Prop) ← (nary .OR pf.getChildren[0]!.getResult[0]!).foldrM f q([])
-    let i : Nat := pf.getArguments[0]!.getIntegerValue.toNat
+    let i : Nat := pf.getArguments[0]!.getIntegerValue!.toNat
     let hi : Q($i < «$ps».length) := .app q(@of_decide_eq_true ($i < «$ps».length) _) q(Eq.refl true)
     let hnps : Q(¬orN $ps) ← reconstructProof pf.getChildren[0]!
     addThm (← reconstructTerm pf.getResult) q(@Prop.not_or_elim _ $hnps $i $hi)
@@ -423,7 +439,7 @@ def reconstructChainResolution (cs as : Array cvc5.Term) (ps : Array Expr) : Rec
     addThm (← reconstructTerm pf.getResult) (.app q(Prop.notAnd $ps) hnps)
   | .CNF_AND_POS =>
     let cnf := pf.getArguments[0]!
-    let i : Nat := pf.getArguments[1]!.getIntegerValue.toNat
+    let i : Nat := pf.getArguments[1]!.getIntegerValue!.toNat
     let mut ps : Q(List Prop) := q([])
     let n := cnf.getNumChildren
     for i in [:n] do
@@ -448,7 +464,7 @@ def reconstructChainResolution (cs as : Array cvc5.Term) (ps : Array Expr) : Rec
     addThm (← reconstructTerm pf.getResult) q(@Prop.cnfOrPos $ps)
   | .CNF_OR_NEG =>
     let cnf := pf.getArguments[0]!
-    let i : Nat := pf.getArguments[1]!.getIntegerValue.toNat
+    let i : Nat := pf.getArguments[1]!.getIntegerValue!.toNat
     let mut ps : Q(List Prop) := q([])
     let n := cnf.getNumChildren
     for i in [:n] do
diff --git a/Smt/Reconstruct/Prop/Rewrites.lean b/Smt/Reconstruct/Prop/Rewrites.lean
index d2ab82f5..85210af8 100644
--- a/Smt/Reconstruct/Prop/Rewrites.lean
+++ b/Smt/Reconstruct/Prop/Rewrites.lean
@@ -9,7 +9,7 @@ import Smt.Reconstruct.Prop.Core
 
 namespace Smt.Reconstruct.Prop
 
--- https://github.com/cvc5/cvc5/blob/proof-new/src/theory/booleans/rewrites
+-- https://github.com/cvc5/cvc5/blob/main/src/theory/booleans/rewrites
 
 open Function
 
@@ -58,9 +58,14 @@ theorem bool_and_dup : (xs ∧ b ∧ ys ∧ b ∧ zs) = (xs ∧ b ∧ ys ∧ zs)
 
 theorem bool_and_conf : (xs ∧ w ∧ ys ∧ ¬w ∧ zs) = False :=
   propext ⟨fun ⟨_, hw, _, hnw, _⟩ => absurd hw hnw, False.elim⟩
+theorem bool_and_conf2 : (xs ∧ ¬w ∧ ys ∧ w ∧ zs) = False :=
+  propext ⟨fun ⟨_, hnw, _, hw, _⟩ => absurd hw hnw, False.elim⟩
 theorem bool_or_taut : (xs ∨ w ∨ ys ∨ ¬w ∨ zs) = True := propext $ .intro
   (const _ trivial)
   (eq_true (Classical.em w) ▸ (·.elim (Or.inr ∘ Or.inl) (Or.inr ∘ Or.inr ∘ Or.inr ∘ Or.inl)))
+theorem bool_or_taut2 : (xs ∨ ¬w ∨ ys ∨ w ∨ zs) = True := propext $ .intro
+  (const _ trivial)
+  (eq_true (Classical.em w).symm ▸ (·.elim (Or.inr ∘ Or.inl) (Or.inr ∘ Or.inr ∘ Or.inr ∘ Or.inl)))
 
 theorem bool_or_de_morgan : (¬(x ∨ y ∨ zs)) = (¬x ∧ ¬(y ∨ zs)) :=
   propext not_or
@@ -126,6 +131,13 @@ theorem ite_else_lookahead_self [h : Decidable c] : ite c x c = ite c x False :=
   (fun hc => if_pos hc ▸ if_pos hc ▸ rfl)
   (fun hnc => if_neg hnc ▸ if_neg hnc ▸ eq_false hnc)
 
+theorem ite_then_lookahead_not_self [h : Decidable c] : ite c (¬c) x = ite c False x := h.byCases
+  (fun hc => if_pos hc ▸ if_pos hc ▸ eq_false (not_not_intro hc))
+  (fun hnc => if_neg hnc ▸ if_neg hnc ▸ rfl)
+theorem ite_else_lookahead_not_self [h : Decidable c] : ite c x (¬c) = ite c x True := h.byCases
+  (fun hc => if_pos hc ▸ if_pos hc ▸ rfl)
+  (fun hnc => if_neg hnc ▸ if_neg hnc ▸ eq_true hnc)
+
 theorem bool_not_ite_elim [h : Decidable c] : (¬ite c x y) = ite c (¬x) (¬y) := h.byCases
   (fun hc => if_pos hc ▸ if_pos hc ▸ rfl)
   (fun hnc => if_neg hnc ▸ if_neg hnc ▸ rfl)
diff --git a/Smt/Reconstruct/Quant.lean b/Smt/Reconstruct/Quant.lean
index c19fb138..c955d79c 100644
--- a/Smt/Reconstruct/Quant.lean
+++ b/Smt/Reconstruct/Quant.lean
@@ -29,10 +29,10 @@ open Lean Qq
 
 def getVariableName (t : cvc5.Term) : Name :=
   if t.hasSymbol then
-    if t.getSymbol.toName == .anonymous then
-      Name.mkSimple t.getSymbol
+    if t.getSymbol!.toName == .anonymous then
+      Name.mkSimple t.getSymbol!
     else
-      t.getSymbol.toName
+      t.getSymbol!.toName
   else Name.num `x t.getId
 
 @[smt_term_reconstruct] def reconstructQuant : TermReconstructor := fun t => do match t.getKind with
@@ -59,10 +59,10 @@ def getVariableName (t : cvc5.Term) : Name :=
       Meta.mkLambdaFVars xs b
   | .HO_APPLY =>
     return (← reconstructTerm t[0]!).app (← reconstructTerm t[1]!)
-  | .SKOLEM => match t.getSkolemId with
+  | .SKOLEM => match t.getSkolemId! with
     | .QUANTIFIERS_SKOLEMIZE =>
-      let q := t.getSkolemIndices[0]!
-      let n := t.getSkolemIndices[1]!.getIntegerValue.toNat
+      let q := t.getSkolemIndices![0]!
+      let n := t.getSkolemIndices![1]!.getIntegerValue!.toNat
       let es ← reconstructForallSkolems q n
       return es[n]!
     | _ => return none
diff --git a/Smt/Reconstruct/Rat.lean b/Smt/Reconstruct/Rat.lean
index eace39a7..d1faa701 100644
--- a/Smt/Reconstruct/Rat.lean
+++ b/Smt/Reconstruct/Rat.lean
@@ -23,11 +23,11 @@ open Qq
   | _          => return none
 
 @[smt_term_reconstruct] def reconstructRat : TermReconstructor := fun t => do match t.getKind with
-  | .SKOLEM => match t.getSkolemId with
+  | .SKOLEM => match t.getSkolemId! with
     | .DIV_BY_ZERO => return q(fun (x : Rat) => x / 0)
     | _ => return none
   | .CONST_RATIONAL =>
-    let c : Lean.Rat := t.getRationalValue
+    let c : Lean.Rat := t.getRationalValue!
     let num : Q(Rat) := mkRatLit c.num.natAbs
     if c.den == 1 then
       if c.num ≥ 0 then
@@ -107,6 +107,12 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
     let t : Q(Rat) ← reconstructTerm pf.getResult[0]![0]!
     let c : Q(Rat) ← reconstructTerm pf.getResult[0]![1]!
     addThm q($t / $c = $t * (1 / $c)) q(@Rewrite.div_by_const_elim $t $c)
+  | .ARITH_POW_ELIM =>
+    if pf.getResult[0]![0]!.getSort.isInteger then return none
+    let x : Q(Rat) ← reconstructTerm pf.getResult[0]![0]!
+    let c : Q(Nat) ← reconstructTerm pf.getResult[0]![1]!
+    let y : Q(Rat) ← reconstructTerm pf.getResult[1]!
+    addThm q($x ^ $c = $y) q(Eq.refl ($x ^ $c))
   | .ARITH_PLUS_ZERO =>
     if pf.getArguments[1]![0]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
@@ -124,19 +130,9 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
     let s : Q(Rat) ← reconstructTerm pf.getArguments[2]!
     let h : Q($s ≠ 0) ← reconstructProof pf.getChildren[0]!
     addThm q($t / $s = $t / $s) q(@Rewrite.div_total $t $s $h)
-  | .ARITH_NEG_NEG_ONE =>
-    if pf.getArguments[1]!.getSort.isInteger then return none
-    let t : Q(Rat) ← reconstructTerm pf.getArguments[1]!
-    addThm q(-1 * (-1 * $t) = $t) q(@Rewrite.neg_neg_one $t)
-  | .ARITH_ELIM_UMINUS =>
-    if pf.getArguments[1]!.getSort.isInteger then return none
-    let t : Q(Rat) ← reconstructTerm pf.getArguments[1]!
-    addThm q(-$t = -1 * $t) q(@Rewrite.elim_uminus $t)
-  | .ARITH_ELIM_MINUS =>
-    if pf.getArguments[1]!.getSort.isInteger then return none
-    let t : Q(Rat) ← reconstructTerm pf.getArguments[1]!
-    let s : Q(Rat) ← reconstructTerm pf.getArguments[2]!
-    addThm q($t - $s = $t + -1 * $s) q(@Rewrite.elim_minus $t $s)
+  | .ARITH_DIV_TOTAL_ZERO =>
+    let x : Q(Rat) ← reconstructTerm pf.getArguments[1]!
+    addThm q($x / 0 = 0) q(@Rewrite.div_total_zero $x)
   | .ARITH_ELIM_GT =>
     if pf.getArguments[1]!.getSort.isInteger then return none
     let t : Q(Rat) ← reconstructTerm pf.getArguments[1]!
@@ -190,14 +186,6 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
     if pf.getArguments[2]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
     addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Rat Rat Rat _) q(1 : Rat) q(@Rewrite.mult_dist) args)
-  | .ARITH_PLUS_CANCEL1 =>
-    if pf.getArguments[2]!.getSort.isInteger then return none
-    let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Rat Rat Rat _) q(0 : Rat) q(@Rewrite.plus_cancel1) args)
-  | .ARITH_PLUS_CANCEL2 =>
-    if pf.getArguments[2]!.getSort.isInteger then return none
-    let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Rat Rat Rat _) q(0 : Rat) q(@Rewrite.plus_cancel2) args)
   | .ARITH_ABS_ELIM =>
     if pf.getArguments[1]!.getSort.isInteger then return none
     let t : Q(Rat) ← reconstructTerm pf.getArguments[1]!
@@ -385,7 +373,7 @@ where
     addTac q($a = $b) Rat.nativePolyNorm
   | .ARITH_POLY_NORM_REL =>
     if pf.getResult[0]![0]!.getSort.isInteger then return none
-    let lcx : Lean.Rat := pf.getChildren[0]!.getResult[0]![0]!.getRationalValue
+    let lcx : Lean.Rat := pf.getChildren[0]!.getResult[0]![0]!.getRationalValue!
     let cx : Q(Rat) ← reconstructTerm pf.getChildren[0]!.getResult[0]![0]!
     let x₁ : Q(Rat) ← reconstructTerm pf.getResult[0]![0]!
     let x₂ : Q(Rat) ← reconstructTerm pf.getResult[0]![1]!
@@ -466,7 +454,7 @@ where
     let y : Q(Rat) ← reconstructTerm pf.getArguments[1]!
     let a : Q(Rat) ← reconstructTerm pf.getArguments[2]!
     let b : Q(Rat) ← reconstructTerm pf.getArguments[3]!
-    if pf.getArguments[4]!.getIntegerValue == -1 then
+    if pf.getArguments[4]!.getBooleanValue! == false then
       addThm q(($x * $y ≤ $b * $x + $a * $y - $a * $b) = ($x ≤ $a ∧ $y ≥ $b ∨ $x ≥ $a ∧ $y ≤ $b)) q(@Rat.mul_tangent_lower_eq $a $b $x $y)
     else
       addThm q(($x * $y ≥ $b * $x + $a * $y - $a * $b) = ($x ≤ $a ∧ $y ≤ $b ∨ $x ≥ $a ∧ $y ≥ $b)) q(@Rat.mul_tangent_upper_eq $a $b $x $y)
diff --git a/Smt/Reconstruct/Rat/Core.lean b/Smt/Reconstruct/Rat/Core.lean
index bf13d7ae..f664ccd9 100644
--- a/Smt/Reconstruct/Rat/Core.lean
+++ b/Smt/Reconstruct/Rat/Core.lean
@@ -9,7 +9,14 @@ import Batteries.Data.Rat
 
 namespace Rat
 
-def abs (x : Rat) := if x < 0 then -x else x
+protected def abs (x : Rat) := if x < 0 then -x else x
+
+protected def pow (m : Rat) : Nat → Rat
+  | 0 => 1
+  | n + 1 => Rat.pow m n * m
+
+instance : NatPow Rat where
+  pow := Rat.pow
 
 protected theorem add_zero : ∀ a : Rat, a + 0 = a := by
   sorry
diff --git a/Smt/Reconstruct/Rat/Rewrites.lean b/Smt/Reconstruct/Rat/Rewrites.lean
index 20eda57d..613f6f83 100644
--- a/Smt/Reconstruct/Rat/Rewrites.lean
+++ b/Smt/Reconstruct/Rat/Rewrites.lean
@@ -14,7 +14,7 @@ open Function
 theorem div_by_const_elim {t c : Rat} : t / c = t * (1 / c) :=
   sorry
 
--- https://github.com/cvc5/cvc5/blob/proof-new/src/theory/arith/rewrites
+-- https://github.com/cvc5/cvc5/blob/main/src/theory/arith/rewrites
 
 variable {t ts x xs : Rat}
 
@@ -28,16 +28,11 @@ theorem mul_zero : ts * 0 * ss = 0 :=
 
 theorem div_total : s ≠ 0 → t / s = t / s :=
   const _ rfl
-
-theorem neg_neg_one : -1 * (-1 * t) = t :=
-  sorry
+theorem div_total_zero : x / 0 = 0 :=
+  Rat.div_def x 0 ▸ Rat.inv_zero.symm ▸ Rat.mul_zero x
 
 -- Eliminations
 
-theorem elim_uminus : -t = -1 * t :=
-  sorry
-theorem elim_minus : t - s = t + -1 * s :=
-  sorry
 theorem elim_gt : (t > s) = ¬(t ≤ s) :=
   sorry
 theorem elim_lt : (t < s) = ¬(t ≥ s) :=
@@ -72,11 +67,6 @@ theorem mult_flatten : xs * (w * ys) * zs = xs * w * ys * zs :=
 theorem mult_dist : x * (y + z + ws) = x * y + x * (z + ws) :=
   sorry
 
-theorem plus_cancel1 : ts + x + ss + (-1 * x) + rs = ts + ss + rs :=
-  sorry
-theorem plus_cancel2 : ts + (-1 * x) + ss + x + rs = ts + ss + rs :=
-  sorry
-
 theorem abs_elim : (if x < 0 then -x else x) = if x < 0 then -x else x :=
   rfl
 
diff --git a/Smt/Reconstruct/Real.lean b/Smt/Reconstruct/Real.lean
index 949d4fa0..0483d765 100644
--- a/Smt/Reconstruct/Real.lean
+++ b/Smt/Reconstruct/Real.lean
@@ -21,11 +21,11 @@ open Lean Qq
   | _          => return none
 
 @[smt_term_reconstruct] def reconstructReal : TermReconstructor := fun t => do match t.getKind with
-  | .SKOLEM => match t.getSkolemId with
+  | .SKOLEM => match t.getSkolemId! with
     | .DIV_BY_ZERO => return q(fun (x : Real) => x / 0)
     | _ => return none
   | .CONST_RATIONAL =>
-    let c : Lean.Rat := t.getRationalValue
+    let c : Lean.Rat := t.getRationalValue!
     let num : Q(Real) := mkRealLit c.num.natAbs
     if c.den == 1 then
       if c.num ≥ 0 then
@@ -107,7 +107,7 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
   match pf.getRewriteRule with
   | .ARITH_DIV_BY_CONST_ELIM =>
     let t : Q(Real) ← reconstructTerm pf.getResult[0]![0]!
-    let r := pf.getResult[0]![1]!.getRationalValue
+    let r := pf.getResult[0]![1]!.getRationalValue!
     if r.den == 1 then
       let c : Q(Real) := reconstructReal.mkRealLit r.num.natAbs
       if r.num ≥ 0 then
@@ -127,6 +127,17 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
         addThm q($t / ($c₁ / $c₂) = $t * ($c₂ / $c₁)) q(@Rewrite.div_by_const_elim_real_pos $t $c₁ $c₂)
       else
         addThm q($t / (-$c₁ / $c₂) = $t * (-$c₂ / $c₁)) q(@Rewrite.div_by_const_elim_real_neg $t $c₁ $c₂)
+  | .ARITH_POW_ELIM =>
+    if pf.getResult[0]![0]!.getSort.isInteger then return none
+    let x : Q(Real) ← reconstructTerm pf.getResult[0]![0]!
+    let c : Nat := pf.getResult[0]![1]!.getIntegerValue!.toNat
+    let y : Q(Real) ← reconstructTerm pf.getResult[1]!
+    let mut h : Q($x ^ $c = $y) := .app q(@Eq.refl Real) y
+    if c > 0 then
+      let qPow : Q(Real) := c.repeat (fun acc => q($acc * $x)) (.bvar 0)
+      let p : Q(Real → Prop) := .lam `x q(Real) q($qPow = $y) .default
+      h := .app q(Eq.subst (motive := $p) (one_mul $x).symm) h
+    addThm q($x ^ $c = $y) h
   | .ARITH_PLUS_ZERO =>
     if pf.getArguments[1]![0]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
@@ -144,19 +155,9 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
     let s : Q(Real) ← reconstructTerm pf.getArguments[2]!
     let h : Q($s ≠ 0) ← reconstructProof pf.getChildren[0]!
     addThm q($t / $s = $t / $s) q(@Rewrite.div_total $t $s $h)
-  | .ARITH_NEG_NEG_ONE =>
-    if pf.getArguments[1]!.getSort.isInteger then return none
-    let t : Q(Real) ← reconstructTerm pf.getArguments[1]!
-    addThm q(-1 * (-1 * $t) = $t) q(@Rewrite.neg_neg_one $t)
-  | .ARITH_ELIM_UMINUS =>
-    if pf.getArguments[1]!.getSort.isInteger then return none
-    let t : Q(Real) ← reconstructTerm pf.getArguments[1]!
-    addThm q(-$t = -1 * $t) q(@Rewrite.elim_uminus $t)
-  | .ARITH_ELIM_MINUS =>
-    if pf.getArguments[1]!.getSort.isInteger then return none
-    let t : Q(Real) ← reconstructTerm pf.getArguments[1]!
-    let s : Q(Real) ← reconstructTerm pf.getArguments[2]!
-    addThm q($t - $s = $t + -1 * $s) q(@Rewrite.elim_minus $t $s)
+  | .ARITH_DIV_TOTAL_ZERO =>
+    let x : Q(Real) ← reconstructTerm pf.getArguments[1]!
+    addThm q($x / 0 = 0) q(@Rewrite.div_total_zero $x)
   | .ARITH_ELIM_GT =>
     if pf.getArguments[1]!.getSort.isInteger then return none
     let t : Q(Real) ← reconstructTerm pf.getArguments[1]!
@@ -210,14 +211,6 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
     if pf.getArguments[2]!.getSort.isInteger then return none
     let args ← reconstructArgs pf.getArguments[1:]
     addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HMul.hMul Real Real Real _) q(1 : Real) q(@Rewrite.mult_dist) args)
-  | .ARITH_PLUS_CANCEL1 =>
-    if pf.getArguments[2]!.getSort.isInteger then return none
-    let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Real Real Real _) q(0 : Real) q(@Rewrite.plus_cancel1) args)
-  | .ARITH_PLUS_CANCEL2 =>
-    if pf.getArguments[2]!.getSort.isInteger then return none
-    let args ← reconstructArgs pf.getArguments[1:]
-    addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@HAdd.hAdd Real Real Real _) q(0 : Real) q(@Rewrite.plus_cancel2) args)
   | .ARITH_ABS_ELIM =>
     if pf.getArguments[1]!.getSort.isInteger then return none
     let t : Q(Real) ← reconstructTerm pf.getArguments[1]!
@@ -411,7 +404,7 @@ where
     addTac q($a = $b) Real.polyNorm
   | .ARITH_POLY_NORM_REL =>
     if pf.getResult[0]![0]!.getSort.isInteger then return none
-    let lcx : Lean.Rat := pf.getChildren[0]!.getResult[0]![0]!.getRationalValue
+    let lcx : Lean.Rat := pf.getChildren[0]!.getResult[0]![0]!.getRationalValue!
     let cx : Q(Real) ← reconstructTerm pf.getChildren[0]!.getResult[0]![0]!
     let x₁ : Q(Real) ← reconstructTerm pf.getResult[0]![0]!
     let x₂ : Q(Real) ← reconstructTerm pf.getResult[0]![1]!
@@ -498,7 +491,7 @@ where
     let y : Q(Real) ← reconstructTerm pf.getArguments[1]!
     let a : Q(Real) ← reconstructTerm pf.getArguments[2]!
     let b : Q(Real) ← reconstructTerm pf.getArguments[3]!
-    if pf.getArguments[4]!.getIntegerValue == -1 then
+    if pf.getArguments[4]!.getBooleanValue! == false then
       addThm q(($x * $y ≤ $b * $x + $a * $y - $a * $b) = ($x ≤ $a ∧ $y ≥ $b ∨ $x ≥ $a ∧ $y ≤ $b)) q(@Real.mul_tangent_lower_eq $a $b $x $y)
     else
       addThm q(($x * $y ≥ $b * $x + $a * $y - $a * $b) = ($x ≤ $a ∧ $y ≤ $b ∨ $x ≥ $a ∧ $y ≥ $b)) q(@Real.mul_tangent_upper_eq $a $b $x $y)
diff --git a/Smt/Reconstruct/Real/Rewrites.lean b/Smt/Reconstruct/Real/Rewrites.lean
index 102b8674..149b6ebd 100644
--- a/Smt/Reconstruct/Real/Rewrites.lean
+++ b/Smt/Reconstruct/Real/Rewrites.lean
@@ -24,7 +24,7 @@ theorem div_by_const_elim_real_pos {t c₁ c₂ : Real} : t / (c₁ / c₂) = t
 theorem div_by_const_elim_real_neg {t c₁ c₂ : Real} : t / (-c₁ / c₂) = t * (-c₂ / c₁) :=
   div_eq_mul_one_div t (-c₁ / c₂) ▸ one_div_div (-c₁) c₂ ▸ div_neg c₂ ▸ neg_div c₁ c₂ ▸ rfl
 
--- https://github.com/cvc5/cvc5/blob/proof-new/src/theory/arith/rewrites
+-- https://github.com/cvc5/cvc5/blob/main/src/theory/arith/rewrites
 
 variable {t ts x xs : Real}
 
@@ -38,16 +38,11 @@ theorem mul_zero : ts * 0 * ss = 0 :=
 
 theorem div_total : s ≠ 0 → t / s = t / s :=
   const _ rfl
-
-theorem neg_neg_one : -1 * (-1 * t) = t :=
-  neg_mul _ t ▸ (one_mul t).symm ▸ neg_mul_neg _ t ▸ (one_mul t).symm ▸ rfl
+theorem div_total_zero : x / 0 = 0 :=
+  div_zero x
 
 -- Eliminations
 
-theorem elim_uminus : -t = -1 * t :=
-  neg_eq_neg_one_mul t ▸ rfl
-theorem elim_minus : t - s = t + -1 * s :=
-  neg_eq_neg_one_mul s ▸ sub_eq_add_neg _ s ▸ rfl
 theorem elim_gt : (t > s) = ¬(t ≤ s) :=
   propext not_le.symm
 theorem elim_lt : (t < s) = ¬(t ≥ s) :=
@@ -82,13 +77,6 @@ theorem mult_flatten : xs * (w * ys) * zs = xs * w * ys * zs :=
 theorem mult_dist : x * (y + z + ws) = x * y + x * (z + ws) :=
   add_assoc y z ws ▸ mul_add x y (z + ws) ▸ rfl
 
-theorem plus_cancel1 : ts + x + ss + (-1 * x) + rs = ts + ss + rs :=
-  neg_eq_neg_one_mul x ▸ add_assoc ts x ss ▸ add_assoc ts (x + ss) (-x) ▸
-  add_comm x ss ▸ (add_neg_cancel_right ss x).symm ▸ rfl
-theorem plus_cancel2 : ts + (-1 * x) + ss + x + rs = ts + ss + rs :=
-  neg_eq_neg_one_mul x ▸ add_assoc ts (-x) ss ▸ add_assoc ts (-x + ss) x ▸
-  add_comm (-x) ss ▸ (neg_add_cancel_right ss x).symm ▸ rfl
-
 theorem abs_elim : (if x < 0 then -x else x) = if x < 0 then -x else x :=
   rfl
 
diff --git a/Smt/Reconstruct/UF.lean b/Smt/Reconstruct/UF.lean
index bb33145a..a7f20a1d 100644
--- a/Smt/Reconstruct/UF.lean
+++ b/Smt/Reconstruct/UF.lean
@@ -23,8 +23,7 @@ def getFVarOrConstExpr! (n : String) : ReconstructM Expr := do
       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! s.getSymbol
+  | .UNINTERPRETED_SORT => getFVarOrConstExpr! s.getSymbol!
   | _ => return none
 
 @[smt_term_reconstruct] def reconstructUF : TermReconstructor := fun t => do match t.getKind with
@@ -46,6 +45,13 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
     let t : Q($α) ← reconstructTerm pf.getArguments[1]!
     let s : Q($α) ← reconstructTerm pf.getArguments[2]!
     addThm q(($t = $s) = ($s = $t)) q(@UF.eq_symm $α $t $s)
+  | .EQ_COND_DEQ =>
+    let α : Q(Type) ← reconstructSort pf.getArguments[1]!.getSort
+    let t : Q($α) ← reconstructTerm pf.getArguments[1]!
+    let s : Q($α) ← reconstructTerm pf.getArguments[2]!
+    let r : Q($α) ← reconstructTerm pf.getArguments[3]!
+    let h : Q(($s = $r) = False) ← reconstructProof pf.getChildren[0]!
+    addThm q((($t = $s) = ($t = $r)) = (¬$t = $s ∧ ¬$t = $r)) q(@UF.eq_cond_deq $α $t $s $r $h)
   | .DISTINCT_BINARY_ELIM =>
     let α : Q(Type) ← reconstructSort pf.getArguments[1]!.getSort
     let t : Q($α) ← reconstructTerm pf.getArguments[1]!
diff --git a/Smt/Reconstruct/UF/Rewrites.lean b/Smt/Reconstruct/UF/Rewrites.lean
index 330aa158..d7258ad7 100644
--- a/Smt/Reconstruct/UF/Rewrites.lean
+++ b/Smt/Reconstruct/UF/Rewrites.lean
@@ -7,13 +7,21 @@ Authors: Abdalrhman Mohamed
 
 namespace Smt.Reconstruct.UF
 
--- https://github.com/cvc5/cvc5/blob/proof-new/src/theory/uf/rewrites
+-- https://github.com/cvc5/cvc5/blob/main/src/theory/uf/rewrites
+
+variable {t s r : α}
 
 -- Equality
 
 theorem eq_refl : (t = t) = True := eq_self t
 theorem eq_symm : (t = s) = (s = t) := propext ⟨(· ▸ rfl), (· ▸ rfl)⟩
 
+theorem eq_cond_deq (h : (s = r) = False) : ((t = s) = (t = r)) = (¬t = s ∧ ¬t = r) :=
+  propext <| Iff.intro
+    (fun hsr => And.intro (fun hts => absurd (hts ▸ hsr ▸ hts) (of_eq_false h))
+                          (fun htr => absurd (htr ▸ Eq.symm (hsr ▸ htr)) (of_eq_false h)))
+    (fun hnsr => propext ⟨(absurd · hnsr.left), (absurd · hnsr.right)⟩)
+
 theorem distinct_binary_elim : (t ≠ s) = ¬(t = s) := rfl
 
 end Smt.Reconstruct.UF
diff --git a/Test/Int/Arith.expected b/Test/Int/Arith.expected
index 1a5d2bd2..28adadd2 100644
--- a/Test/Int/Arith.expected
+++ b/Test/Int/Arith.expected
@@ -16,14 +16,12 @@ h : 0 < m
           m + -1 * n + m * (n / m) ≥ 1 →
             m + -1 * n + m * (n / m) ≥ 1 → n % m = if m = 0 then (fun x => x % 0) n else n % m
 
-n m : Int
-h : 0 < m
-⊢ 0 < m → ¬n % m < m → n % m = n - m * (n / m)
-
 n m : Int
 h : 0 < m
 ⊢ 0 < m →
-    ¬n % m < m → (m > 0 → m * (n / m) ≤ n ∧ n < m * (n / m + 1)) ∧ (m < 0 → m * (n / m) ≤ n ∧ n < m * (n / m + -1))
+    ¬n % m < m →
+      n % m = n - m * (n / m) ∧
+        (m > 0 → m * (n / m) ≤ n ∧ n < m * (n / m + 1)) ∧ (m < 0 → m * (n / m) ≤ n ∧ n < m * (n / m + -1))
 
 n m : Int
 h : 0 < m
diff --git a/Test/Prop/Exists'.lean b/Test/Prop/Exists'.lean
index 97cf8d4e..679daf07 100644
--- a/Test/Prop/Exists'.lean
+++ b/Test/Prop/Exists'.lean
@@ -4,6 +4,6 @@ theorem exists' : ∃ p : Prop, p := by
   smt
   · intro; apply propext; apply Iff.intro
     · intro hp ht
-      exact hp True ht
+      cases hp True <;> contradiction
     · intro hnt
       contradiction
diff --git a/Test/linarith.expected b/Test/linarith.expected
index cf024286..84d3033b 100644
--- a/Test/linarith.expected
+++ b/Test/linarith.expected
@@ -19,14 +19,22 @@ but function has type
 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: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`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
-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:102:2: error: application type mismatch
+  1 ≥ 0
+argument
+  0
+has type
+  ℤ : Type
+but is expected to have type
+  ℝ : Type
+Test/linarith.lean:107:2: error: application type mismatch
+  1 ≥ 0
+argument
+  0
+has type
+  ℤ : Type
+but is expected to have type
+  ℝ : Type
 Test/linarith.lean:118:60: warning: unused variable `h3`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
 Test/linarith.lean:125:9: warning: unused variable `a`
diff --git a/lake-manifest.json b/lake-manifest.json
index 64ecf4f2..2500e917 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c97ff4cfc218c11af8c1598b8225a6fcc094f5cd",
+   "rev": "aff591ae23965f28f15d8a1437a06d9febb704b0",
    "name": "cvc5",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "c97ff4cfc218c11af8c1598b8225a6fcc094f5cd",
+   "inputRev": "aff591ae23965f28f15d8a1437a06d9febb704b0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/batteries",
diff --git a/lakefile.lean b/lakefile.lean
index fc11d19e..1c24cbfa 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -3,7 +3,7 @@ import Lake
 open Lake DSL
 
 require cvc5 from
-  git "https://github.com/abdoo8080/lean-cvc5.git" @ "c97ff4cfc218c11af8c1598b8225a6fcc094f5cd"
+  git "https://github.com/abdoo8080/lean-cvc5.git" @ "aff591ae23965f28f15d8a1437a06d9febb704b0"
 
 require mathlib from
   git "https://github.com/leanprover-community/mathlib4.git" @ "v4.13.0"