From 1d2de145b3c116573ca77fbc81394991a80d5156 Mon Sep 17 00:00:00 2001
From: Abdalrhman Mohamed <abdoo8080@outlook.com>
Date: Fri, 12 Jul 2024 00:48:48 -0500
Subject: [PATCH] Fix bug with Iff elimination. (#123)

---
 Smt/Preprocess.lean          |   8 ++
 Smt/Preprocess/Iff.lean      |  62 +++++++++++
 Smt/Tactic/Smt.lean          |  15 +--
 Smt/Util.lean                |  31 +-----
 Test/BitVec/XorComm.expected |   2 +-
 Test/Int/Binders.expected    |   4 +-
 Test/Int/linarith.expected   |   9 ++
 Test/Int/linarith.lean       | 199 +++++++++++++++++++++++++++++++++++
 Test/Nat/Cong.expected       |   2 +-
 Test/Nat/Max.expected        |   4 +-
 Test/Nat/Sum'.expected       |   6 +-
 Test/Nat/ZeroSub'.expected   |   2 +-
 Test/Prop/Iff.expected       |   0
 Test/Prop/Iff.lean           |   6 ++
 Test/String/Length.expected  |   2 +-
 15 files changed, 305 insertions(+), 47 deletions(-)
 create mode 100644 Smt/Preprocess.lean
 create mode 100644 Smt/Preprocess/Iff.lean
 create mode 100644 Test/Int/linarith.expected
 create mode 100644 Test/Int/linarith.lean
 create mode 100644 Test/Prop/Iff.expected
 create mode 100644 Test/Prop/Iff.lean

diff --git a/Smt/Preprocess.lean b/Smt/Preprocess.lean
new file mode 100644
index 00000000..fe56e253
--- /dev/null
+++ b/Smt/Preprocess.lean
@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2021-2024 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Abdalrhman Mohamed, Tomaz Gomes Mascarenhas
+-/
+
+import Smt.Preprocess.Iff
diff --git a/Smt/Preprocess/Iff.lean b/Smt/Preprocess/Iff.lean
new file mode 100644
index 00000000..19e1c79e
--- /dev/null
+++ b/Smt/Preprocess/Iff.lean
@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2021-2024 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Abdalrhman Mohamed, Tomaz Gomes Mascarenhas
+-/
+
+import Lean
+import Qq
+
+namespace Smt.Preprocess
+
+open Lean Qq
+
+theorem iff_eq_eq : (p ↔ q) = (p = q) := propext ⟨propext, (· ▸ ⟨(·), (·)⟩)⟩
+
+theorem eq_resolve {p q : Prop} (hp : p) (hpq : p = q) : q := hpq ▸ hp
+
+def replaceIff (e : Expr) : MetaM Expr :=
+  let f e :=
+    if let some ((l : Q(Prop)), (r : Q(Prop))) := e.app2? ``Iff then
+      q($l = $r)
+    else
+      none
+  Meta.mkAppM ``Eq #[e, e.replace f]
+
+def elimIff (mv : MVarId) (hs : List Expr) : MetaM (List Expr × MVarId) := mv.withContext do
+  let simpTheorems ← #[``eq_self, ``iff_eq_eq].foldlM (·.addConst ·) ({} : Meta.SimpTheorems)
+  let simpTheorems := #[simpTheorems]
+  let congrTheorems ← Meta.getSimpCongrTheorems
+  let ctx := { simpTheorems, congrTheorems }
+  let (hs, mv) ← elimIffLocalDecls mv hs ctx
+  let mv ← elimIffTarget mv ctx
+  return (hs, mv)
+where
+  elimIffLocalDecls mv hs ctx := mv.withContext do
+    let mut newHs := []
+    let mut toAssert := #[]
+    for h in hs do
+      let type ← Meta.inferType h
+      let eq ← replaceIff (← instantiateMVars type)
+      let (_, l, r) := eq.eq?.get!
+      if l == r then
+        newHs := h :: newHs
+      else
+        let userName ← if h.isFVar then h.fvarId!.getUserName else Lean.mkFreshId
+        let type := r
+        let (r, _) ←  Meta.simp eq ctx
+        let value ←  Meta.mkAppM ``eq_resolve #[h, ← Meta.mkOfEqTrue (← r.getProof)]
+        toAssert := toAssert.push { userName, type, value }
+    let (fvs, mv) ← mv.assertHypotheses toAssert
+    newHs := newHs.reverse ++ (fvs.map (.fvar ·)).toList
+    return (newHs, mv)
+  elimIffTarget mv ctx := mv.withContext do
+    let eq ← replaceIff (← instantiateMVars (← mv.getType))
+    let (r, _) ←  Meta.simp eq ctx
+    if r.expr.isTrue then
+      mv.replaceTargetEq eq.appArg! (← Meta.mkOfEqTrue (← r.getProof))
+    else
+      return mv
+
+end Smt.Preprocess
diff --git a/Smt/Tactic/Smt.lean b/Smt/Tactic/Smt.lean
index badaf347..b510a2cd 100644
--- a/Smt/Tactic/Smt.lean
+++ b/Smt/Tactic/Smt.lean
@@ -11,6 +11,7 @@ import Smt.Dsl.Sexp
 import Smt.Reconstruct
 import Smt.Reconstruct.Prop.Lemmas
 import Smt.Translate.Query
+import Smt.Preprocess
 import Smt.Util
 
 namespace Smt
@@ -39,10 +40,11 @@ where
         go mv hs (.fvar fv :: fvs) k
 
 def smt (mv : MVarId) (hs : List Expr) (timeout : Option Nat := none) : MetaM (List MVarId) := mv.withContext do
-  let mv ← Util.rewriteIffMeta mv
-  let goalType : Q(Prop) ← mv.getType
   -- 1. Process the hints passed to the tactic.
   withProcessedHints mv hs fun mv hs => mv.withContext do
+  let (hs, mv) ← Preprocess.elimIff mv hs
+  mv.withContext do
+  let goalType : Q(Prop) ← mv.getType
   -- 2. Generate the SMT query.
   let cmds ← prepareSmtQuery hs (← mv.getType)
   let cmds := .setLogic "ALL" :: cmds
@@ -122,11 +124,12 @@ def parseTimeout : TSyntax `smtTimeout → TacticM (Option Nat)
 
 @[tactic smtShow] def evalSmtShow : Tactic := fun stx => withMainContext do
   let g ← Meta.mkFreshExprMVar (← getMainTarget)
-  let mv ← Util.rewriteIffMeta g.mvarId!
-  let goalType ← mv.getType
-  let mut hs ← parseHints ⟨stx[1]⟩
-  hs := hs.eraseDups
+  let mv := g.mvarId!
+  let hs ← parseHints ⟨stx[1]⟩
   withProcessedHints mv hs fun mv hs => mv.withContext do
+  let (hs, mv) ← Preprocess.elimIff mv hs
+  mv.withContext do
+  let goalType ← mv.getType
   let cmds ← prepareSmtQuery hs (← mv.getType)
   let cmds := cmds ++ [.checkSat]
   logInfo m!"goal: {goalType}\n\nquery:\n{Command.cmdsAsQuery cmds}"
diff --git a/Smt/Util.lean b/Smt/Util.lean
index 1bee3a05..9c5ab4c2 100644
--- a/Smt/Util.lean
+++ b/Smt/Util.lean
@@ -108,33 +108,4 @@ where
     | some e => .visit e
     | none   => .continue
 
-theorem iff_eq_eq : (p ↔ q) = (p = q) := propext ⟨propext, (· ▸ ⟨(·), (·)⟩)⟩
-
-def rewriteIffGoal (mvar : MVarId) : MetaM MVarId :=
-  mvar.withContext do
-    let t ← mvar.getType
-    let r ← mvar.rewrite t (mkConst ``iff_eq_eq)
-    let mvar' ← mvar.replaceTargetEq r.eNew r.eqProof
-    pure mvar'
-
-def rewriteIffDecl (decl : LocalDecl) (mvar : MVarId) : MetaM MVarId :=
-  mvar.withContext do
-    let rwRes ← mvar.rewrite decl.type (mkConst ``iff_eq_eq)
-    let repRes ← mvar.replaceLocalDecl decl.fvarId rwRes.eNew rwRes.eqProof
-    pure repRes.mvarId
-
-partial def fixRewriteIff (mvar : MVarId) (f : MVarId → MetaM MVarId) : MetaM MVarId :=
-  mvar.withContext do
-    try
-      let mvar' ← f mvar
-      fixRewriteIff mvar' f
-    catch _ => return mvar
-
-def rewriteIffMeta (mvar : MVarId) : MetaM MVarId :=
-  mvar.withContext do
-    let mvar' ← fixRewriteIff mvar rewriteIffGoal
-    let lctx ← getLCtx
-    lctx.foldrM
-      (fun decl mvar'' => fixRewriteIff mvar'' (rewriteIffDecl decl)) mvar'
-
-namespace Smt.Util
+end Smt.Util
diff --git a/Test/BitVec/XorComm.expected b/Test/BitVec/XorComm.expected
index bb102ca6..6cd4a967 100644
--- a/Test/BitVec/XorComm.expected
+++ b/Test/BitVec/XorComm.expected
@@ -9,8 +9,8 @@ Test/BitVec/XorComm.lean:3:8: warning: declaration uses 'sorry'
 goal: x ^^^ y = y ^^^ x
 
 query:
-(declare-const x (_ BitVec 8))
 (declare-const y (_ BitVec 8))
+(declare-const x (_ BitVec 8))
 (assert (distinct (bvxor x y) (bvxor y x)))
 (check-sat)
 Test/BitVec/XorComm.lean:7:8: warning: declaration uses 'sorry'
diff --git a/Test/Int/Binders.expected b/Test/Int/Binders.expected
index 83c0b301..8473624c 100644
--- a/Test/Int/Binders.expected
+++ b/Test/Int/Binders.expected
@@ -11,8 +11,8 @@ goal: partCurryAdd a b = partCurryAdd b a
 
 query:
 (define-fun partCurryAdd ((a Int) (a._@.Test.Int.Binders._hyg.36 Int)) Int (+ a a._@.Test.Int.Binders._hyg.36))
-(declare-const b Int)
 (declare-const a Int)
+(declare-const b Int)
 (assert (distinct (partCurryAdd a b) (partCurryAdd b a)))
 (check-sat)
 Test/Int/Binders.lean:11:0: warning: declaration uses 'sorry'
@@ -29,8 +29,8 @@ goal: mismatchNamesAdd a b = mismatchNamesAdd b a
 
 query:
 (define-fun mismatchNamesAdd ((a Int) (b Int)) Int (+ a b))
-(declare-const b Int)
 (declare-const a Int)
+(declare-const b Int)
 (assert (distinct (mismatchNamesAdd a b) (mismatchNamesAdd b a)))
 (check-sat)
 Test/Int/Binders.lean:25:0: warning: declaration uses 'sorry'
diff --git a/Test/Int/linarith.expected b/Test/Int/linarith.expected
new file mode 100644
index 00000000..301667f2
--- /dev/null
+++ b/Test/Int/linarith.expected
@@ -0,0 +1,9 @@
+Test/Int/linarith.lean:51:9: warning: unused variable `e`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+Test/Int/linarith.lean:76:0: warning: declaration uses 'sorry'
+Test/Int/linarith.lean:93:62: warning: unused variable `h3`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+Test/Int/linarith.lean:98:36: warning: unused variable `z`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
+Test/Int/linarith.lean:99:5: warning: unused variable `h5`
+note: this linter can be disabled with `set_option linter.unusedVariables false`
diff --git a/Test/Int/linarith.lean b/Test/Int/linarith.lean
new file mode 100644
index 00000000..275f54a4
--- /dev/null
+++ b/Test/Int/linarith.lean
@@ -0,0 +1,199 @@
+import Smt
+
+-- example : ∃ (x : Int), x * x = 2 := by
+--   smt
+
+example : p ∧ q → p := by
+  smt
+
+example (a b : Int) : b < 0 → a > 0 → b * (- 2)  * a * b* b * (- 3) * a * a < 0 := by
+  smt
+  all_goals sorry
+
+example (a b : Int) (hb : b < 0) (ha : a < 0) : b * (- 2)  * a *  b * (- 3) * a * a < 0 := by
+  smt [hb, ha]
+  all_goals sorry
+
+-- example (m n : Int) (h : m > 0) : n % m < m := by
+--   smt [h]
+--   all_goals sorry
+
+example {x y : Int} {f : Int → Int} : ¬(x ≤ y ∧ y ≤ x ∧ ¬f x = f y) := by
+  smt
+  all_goals sorry
+
+example {p q r : Prop} (hp : ¬p) (hq : ¬q) (hr : r) : ¬(p ∨ q ∨ ¬r) := by
+  smt [hp, hq, hr]
+
+example {p q r : Prop} : ((p ∧ q) ∧ r) = (r ∧ True ∧ q ∧ p ∧ p) := by
+  smt
+
+example {p q r : Prop} : ((p ∧ q) ∧ r) = (r ∧ True ∧ q ∧ p ∧ p) := by
+  ac_rfl
+
+example {a b : Int} (h : a < b) (w : b < a) : False := by
+  smt [h, w]
+  all_goals sorry
+
+example
+    {a b c : Int}
+    (ha : a < 0)
+    (hb : ¬b = 0)
+    (hc' : c = 0)
+    (h₁ : (1 - a) * (b * b) ≤ 0)
+    (hc : (0 : Int) ≤ 0)
+    (w : -(a * -b * -b + b * -b + 0) = (1 - a) * (b * b))
+    (h₂ : (1 - a) * (b * b) ≤ 0) :
+    0 < 1 - a := by
+  smt [ha, hb, hc', h₁, hc, w, h₂]
+  all_goals sorry
+
+example (e b c a v0 v1 : Int) (h1 : v0 = 5*a) (h2 : v1 = 3*b)
+    (h3 : v0 + v1 + c = 10) : v0 + 5 + (v1 - 3) + (c - 2) = 10 := by
+  smt [h1, h2, h3]
+  all_goals sorry
+
+example (h : (1 : Int) < 0) (g : ¬ (37 : Int) < 42) (_k : True) (l : (-7 : Int) < 5): (3 : Int) < 7 := by
+  smt [h, g, _k, l]
+  all_goals sorry
+
+example (u v r s t : Int) (h : 0 < u*(t*v + t*r + s)) : 0 < (t*(r + v) + s)*3*u := by
+  smt [h]
+  all_goals sorry
+
+example (A B : Int) (h : 0 < 3 * A * B) : 0 < 8*A*B := by
+  smt [h]
+  all_goals sorry
+
+example (A B : Int) (h : 0 < 8 * A * B) : 0 < A*B := by
+  smt [h]
+  all_goals sorry
+
+example (A B : Int) (h : 0 < A * B) : 0 < A*8*B := by
+  smt [h]
+  all_goals sorry
+
+example (x : Int) : 0 ≤ x := by
+  have h : 0 ≤ x := sorry
+  smt [h]
+
+example (u v r s t : Int) (h : 0 < u*(t*v + t*r + s)) :
+    0 < (t*(r + v) + s)*3*u := by
+  smt [h]
+  all_goals sorry
+
+example (A B : Int) (h : 0 < A * B) : 0 < 8*A*B := by
+  smt [h]
+  all_goals sorry
+
+example (x y z : Int) (h1 : 2*x < 3*y) (h2 : -4*x + 2*z < 0) (h3 : 12*y - 4* z < 0) : False := by
+  smt [h1, h2, h3]
+  all_goals sorry
+
+example (x y z : Int) (h1 : 2*x < 3*y) (h2 : -4*x + 2*z < 0) (h3 : x*y < 5) (h3 : 12*y - 4* z < 0) :
+    False := by
+  smt [h1, h2, h3]
+  all_goals sorry
+
+example (prime : Int → Prop) (w x y z : Int) (h1 : 4*x + (-3)*y + 6*w ≤ 0) (h2 : (-1)*x < 0) (h3 : y < 0) (h4 : w ≥ 0)
+    (h5 : prime x) : False := by
+  smt [h1, h2, h3, h4]
+  all_goals sorry
+
+-- set_option maxRecDepth 2000000
+
+example (u v x y A B : Int)
+(a : 0 < A)
+(a_1 : 0 <= 1 - A)
+(a_2 : 0 <= B - 1)
+(a_3 : 0 <= B - x)
+(a_4 : 0 <= B - y)
+(a_5 : 0 <= u)
+(a_6 : 0 <= v)
+(a_7 : 0 < A - u)
+(a_8 : 0 < A - v) :
+ (0 < A * A)
+-> (0 <= A * (1 - A))
+-> (0 <= A * (B - 1))
+-> (0 <= A * (B - x))
+-> (0 <= A * (B - y))
+-> (0 <= A * u)
+-> (0 <= A * v)
+-> (0 < A * (A - u))
+-> (0 < A * (A - v))
+-> (0 <= (1 - A) * A)
+-> (0 <= (1 - A) * (1 - A))
+-> (0 <= (1 - A) * (B - 1))
+-> (0 <= (1 - A) * (B - x))
+-> (0 <= (1 - A) * (B - y))
+-> (0 <= (1 - A) * u)
+-> (0 <= (1 - A) * v)
+-> (0 <= (1 - A) * (A - u))
+-> (0 <= (1 - A) * (A - v))
+-> (0 <= (B - 1) * A)
+-> (0 <= (B - 1) * (1 - A))
+-> (0 <= (B - 1) * (B - 1))
+-> (0 <= (B - 1) * (B - x))
+-> (0 <= (B - 1) * (B - y))
+-> (0 <= (B - 1) * u)
+-> (0 <= (B - 1) * v)
+-> (0 <= (B - 1) * (A - u))
+-> (0 <= (B - 1) * (A - v))
+-> (0 <= (B - x) * A)
+-> (0 <= (B - x) * (1 - A))
+-> (0 <= (B - x) * (B - 1))
+-> (0 <= (B - x) * (B - x))
+-> (0 <= (B - x) * (B - y))
+-> (0 <= (B - x) * u)
+-> (0 <= (B - x) * v)
+-> (0 <= (B - x) * (A - u))
+-> (0 <= (B - x) * (A - v))
+-> (0 <= (B - y) * A)
+-> (0 <= (B - y) * (1 - A))
+-> (0 <= (B - y) * (B - 1))
+-> (0 <= (B - y) * (B - x))
+-> (0 <= (B - y) * (B - y))
+-> (0 <= (B - y) * u)
+-> (0 <= (B - y) * v)
+-> (0 <= (B - y) * (A - u))
+-> (0 <= (B - y) * (A - v))
+-> (0 <= u * A)
+-> (0 <= u * (1 - A))
+-> (0 <= u * (B - 1))
+-> (0 <= u * (B - x))
+-> (0 <= u * (B - y))
+-> (0 <= u * u)
+-> (0 <= u * v)
+-> (0 <= u * (A - u))
+-> (0 <= u * (A - v))
+-> (0 <= v * A)
+-> (0 <= v * (1 - A))
+-> (0 <= v * (B - 1))
+-> (0 <= v * (B - x))
+-> (0 <= v * (B - y))
+-> (0 <= v * u)
+-> (0 <= v * v)
+-> (0 <= v * (A - u))
+-> (0 <= v * (A - v))
+-> (0 < (A - u) * A)
+-> (0 <= (A - u) * (1 - A))
+-> (0 <= (A - u) * (B - 1))
+-> (0 <= (A - u) * (B - x))
+-> (0 <= (A - u) * (B - y))
+-> (0 <= (A - u) * u)
+-> (0 <= (A - u) * v)
+-> (0 < (A - u) * (A - u))
+-> (0 < (A - u) * (A - v))
+-> (0 < (A - v) * A)
+-> (0 <= (A - v) * (1 - A))
+-> (0 <= (A - v) * (B - 1))
+-> (0 <= (A - v) * (B - x))
+-> (0 <= (A - v) * (B - y))
+-> (0 <= (A - v) * u)
+-> (0 <= (A - v) * v)
+-> (0 < (A - v) * (A - u))
+-> (0 < (A - v) * (A - v))
+->
+ u * y + v * x + u * v < 3 * A * B := by
+  smt [a, a_1, a_2, a_3, a_4, a_5, a_6, a_7, a_8]
+  all_goals sorry
diff --git a/Test/Nat/Cong.expected b/Test/Nat/Cong.expected
index 768e190e..918d9ac5 100644
--- a/Test/Nat/Cong.expected
+++ b/Test/Nat/Cong.expected
@@ -3,7 +3,7 @@ goal: x = y → f x = f y
 query:
 (define-sort Nat () Int)
 (declare-fun f (Nat) Nat)
-(assert (forall ((_uniq.1520 Nat)) (=> (>= _uniq.1520 0) (>= (f _uniq.1520) 0))))
+(assert (forall ((_uniq.1556 Nat)) (=> (>= _uniq.1556 0) (>= (f _uniq.1556) 0))))
 (declare-const x Nat)
 (assert (>= x 0))
 (declare-const y Nat)
diff --git a/Test/Nat/Max.expected b/Test/Nat/Max.expected
index 266ef325..50d3ea9d 100644
--- a/Test/Nat/Max.expected
+++ b/Test/Nat/Max.expected
@@ -5,7 +5,7 @@ query:
 (declare-const x Nat)
 (assert (>= x 0))
 (declare-fun |Nat.max'| (Nat Nat) Nat)
-(assert (forall ((_uniq.2212 Nat)) (=> (>= _uniq.2212 0) (forall ((_uniq.2213 Nat)) (=> (>= _uniq.2213 0) (>= (|Nat.max'| _uniq.2212 _uniq.2213) 0))))))
+(assert (forall ((_uniq.2242 Nat)) (=> (>= _uniq.2242 0) (forall ((_uniq.2243 Nat)) (=> (>= _uniq.2243 0) (>= (|Nat.max'| _uniq.2242 _uniq.2243) 0))))))
 (declare-const y Nat)
 (assert (>= y 0))
 (assert (not (and (<= x (|Nat.max'| x y)) (<= y (|Nat.max'| x y)))))
@@ -15,7 +15,7 @@ goal: x ≤ x.max' y ∧ y ≤ x.max' y
 query:
 (define-sort Nat () Int)
 (define-fun |Nat.max'| ((x Nat) (y Nat)) Nat (ite (<= x y) y x))
-(assert (forall ((_uniq.4701 Nat)) (=> (>= _uniq.4701 0) (forall ((_uniq.4702 Nat)) (=> (>= _uniq.4702 0) (>= (|Nat.max'| _uniq.4701 _uniq.4702) 0))))))
+(assert (forall ((_uniq.4763 Nat)) (=> (>= _uniq.4763 0) (forall ((_uniq.4764 Nat)) (=> (>= _uniq.4764 0) (>= (|Nat.max'| _uniq.4763 _uniq.4764) 0))))))
 (declare-const x Nat)
 (assert (>= x 0))
 (declare-const y Nat)
diff --git a/Test/Nat/Sum'.expected b/Test/Nat/Sum'.expected
index c934fc3b..c88e6d39 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.4976» : Int), «_uniq.4976» ≥ 0 → sum «_uniq.4976» ≥ 0) ∧ Smt.Reconstruct.Builtin.distinct [sum 0, 0])
+      (∀ («_uniq.5035» : Int), «_uniq.5035» ≥ 0 → sum «_uniq.5035» ≥ 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.12014 Nat)) (=> (>= _uniq.12014 0) (>= (sum _uniq.12014) 0))))
+(assert (forall ((_uniq.12077 Nat)) (=> (>= _uniq.12077 0) (>= (sum _uniq.12077) 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/Nat/ZeroSub'.expected b/Test/Nat/ZeroSub'.expected
index 51848119..7b14eb1a 100644
--- a/Test/Nat/ZeroSub'.expected
+++ b/Test/Nat/ZeroSub'.expected
@@ -1,6 +1,6 @@
 Test/Nat/ZeroSub'.lean:6:12: error: tactic 'assumption' failed
 case zero
-_uniq✝⁴⁷⁸⁻⁰ : ¬Smt.Reconstruct.Builtin.distinct [0, 0]
+_uniq✝⁵¹⁷⁻⁰ : ¬Smt.Reconstruct.Builtin.distinct [0, 0]
 ⊢ ¬Smt.Reconstruct.andN' [] ¬0 - 0 = 0
 Test/Nat/ZeroSub'.lean:7:17: error: application type mismatch
   HAdd.hAdd x
diff --git a/Test/Prop/Iff.expected b/Test/Prop/Iff.expected
new file mode 100644
index 00000000..e69de29b
diff --git a/Test/Prop/Iff.lean b/Test/Prop/Iff.lean
new file mode 100644
index 00000000..86b84b61
--- /dev/null
+++ b/Test/Prop/Iff.lean
@@ -0,0 +1,6 @@
+import Smt
+
+variable {node : Type} [Nonempty node]
+
+example (a : node → Prop) (h : ∀ n, a n ↔ a n) : ∀ n, a n ↔ a n := by
+  smt [h]
diff --git a/Test/String/Length.expected b/Test/String/Length.expected
index 065a74fd..2a63582b 100644
--- a/Test/String/Length.expected
+++ b/Test/String/Length.expected
@@ -3,6 +3,6 @@ goal: "a".length = 1
 query:
 (define-sort Nat () Int)
 (declare-fun String.length (String) Nat)
-(assert (forall ((_uniq.769 String)) (>= (String.length _uniq.769) 0)))
+(assert (forall ((_uniq.805 String)) (>= (String.length _uniq.805) 0)))
 (assert (distinct (String.length "a") 1))
 (check-sat)