From 96c3669a68d4273d117bc2bb2890835b161422a3 Mon Sep 17 00:00:00 2001
From: robert <robujsph2001@gmail.com>
Date: Tue, 5 May 2026 06:46:18 +0000
Subject: [PATCH 1/2] Fix SMT translation of integer literals

---
 Strata/DL/SMT/Translate.lean          | 2 +-
 StrataTest/DL/SMT/TranslateTests.lean | 7 +++++++
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/Strata/DL/SMT/Translate.lean b/Strata/DL/SMT/Translate.lean
index d0d627e214..d8ddcfa924 100644
--- a/Strata/DL/SMT/Translate.lean
+++ b/Strata/DL/SMT/Translate.lean
@@ -325,7 +325,7 @@ def translateTerm (t : SMT.Term) : TranslateM (Expr × Expr) := do
     let (as, a) := ((a :: as).dropLast, (a :: as).getLast?.get rfl)
     return (mkProp, as.foldr mkArrow a)
   | .prim (.int x) =>
-    return (mkProp, toExpr x)
+    return (mkInt, toExpr x)
   | .app .neg [a] _ =>
     let (_, a) ← translateTerm a
     return (mkInt, .app mkIntNeg a)
diff --git a/StrataTest/DL/SMT/TranslateTests.lean b/StrataTest/DL/SMT/TranslateTests.lean
index 8dd928b9fd..e186bf44b0 100644
--- a/StrataTest/DL/SMT/TranslateTests.lean
+++ b/StrataTest/DL/SMT/TranslateTests.lean
@@ -41,3 +41,10 @@ info: ∀ (α : Type → Type → Type) [inst : ∀ (α_1 α_2 : Type), Nonempty
 #guard_msgs in
 #eval
   elabQuery {} [] (.app .eq [(.app .abs [(.prim (.int (-5)))] (.prim .int)), (.prim (.int 5))] (.prim .bool))
+
+/-- info: (if 0 = 0 then 0 else 1) = 0 -/
+#guard_msgs in
+#eval
+  let c := .app .eq [(.prim (.int 0)), (.prim (.int 0))] (.prim .bool)
+  let t := .app .ite [c, (.prim (.int 0)), (.prim (.int 1))] (.prim .int)
+  elabQuery {} [] (.app .eq [t, (.prim (.int 0))] (.prim .bool))

From d6f5091460b14b8bb22afaf4c90c00f19fa445c1 Mon Sep 17 00:00:00 2001
From: robert <robujsph2001@gmail.com>
Date: Tue, 5 May 2026 16:57:29 +0000
Subject: [PATCH 2/2] Strengthen SMT translation tests

---
 Strata/DL/SMT/Translate.lean          |  8 ++++++++
 StrataTest/DL/SMT/TranslateTests.lean | 26 ++++++++++++++++++++++++++
 2 files changed, 34 insertions(+)

diff --git a/Strata/DL/SMT/Translate.lean b/Strata/DL/SMT/Translate.lean
index d8ddcfa924..465a61dd01 100644
--- a/Strata/DL/SMT/Translate.lean
+++ b/Strata/DL/SMT/Translate.lean
@@ -274,6 +274,14 @@ def translateSort (ty : TermType) : TranslateM Expr := do
     let as ← as.mapM translateSort
     return mkAppN t as.toArray
 
+/--
+Translate an SMT term to a Lean expression, together with its Lean type.
+
+The first component is the actual type of the second component, not just a
+hint. Consumers use it as the type argument for generated Lean constructs such
+as `Eq` and `ite`, and helpers such as `leftAssocOp` propagate it as the result
+type of compound expressions.
+-/
 def translateTerm (t : SMT.Term) : TranslateM (Expr × Expr) := do
   match t with
   | .var v =>
diff --git a/StrataTest/DL/SMT/TranslateTests.lean b/StrataTest/DL/SMT/TranslateTests.lean
index e186bf44b0..79810f8b13 100644
--- a/StrataTest/DL/SMT/TranslateTests.lean
+++ b/StrataTest/DL/SMT/TranslateTests.lean
@@ -14,6 +14,7 @@ open Elab Command
 def elabQuery (ctx : Core.SMT.Context) (assums : List SMT.Term) (conc : SMT.Term) : CommandElabM Unit := do
   runTermElabM fun _ => do
     let e ← translateQueryMeta ctx assums conc
+    Meta.check e
     logInfo e
 
 /-- info: ∀ (a : Int), 42 > a -/
@@ -48,3 +49,28 @@ info: ∀ (α : Type → Type → Type) [inst : ∀ (α_1 α_2 : Type), Nonempty
   let c := .app .eq [(.prim (.int 0)), (.prim (.int 0))] (.prim .bool)
   let t := .app .ite [c, (.prim (.int 0)), (.prim (.int 1))] (.prim .int)
   elabQuery {} [] (.app .eq [t, (.prim (.int 0))] (.prim .bool))
+
+-- Int literal as the first operand of `.app .eq`: previously built
+-- `@Eq Prop 5 ...` because `.prim (.int 5)` returned `(mkProp, _)`.
+/-- info: 5 = -5 -/
+#guard_msgs in
+#eval
+  elabQuery {} [] (.app .eq [(.prim (.int 5)), (.app .neg [(.prim (.int 5))] (.prim .int))] (.prim .bool))
+
+-- Int literal as the first operand of arithmetic: `leftAssocOp` propagates the
+-- first operand's type as the whole expression's type, so before the fix the
+-- entire `add` was typed `Prop`.
+/-- info: 1 + 2 = 3 -/
+#guard_msgs in
+#eval
+  elabQuery {} [] (.app .eq [(.app .add [(.prim (.int 1)), (.prim (.int 2))] (.prim .int)), (.prim (.int 3))] (.prim .bool))
+
+-- Int literal as a branch of a nested ITE: exercises type propagation across
+-- nested conditionals.
+/-- info: (if 0 = 0 then if 0 = 0 then 1 else 2 else 3) = 1 -/
+#guard_msgs in
+#eval
+  let c := .app .eq [(.prim (.int 0)), (.prim (.int 0))] (.prim .bool)
+  let inner := .app .ite [c, (.prim (.int 1)), (.prim (.int 2))] (.prim .int)
+  let outer := .app .ite [c, inner, (.prim (.int 3))] (.prim .int)
+  elabQuery {} [] (.app .eq [outer, (.prim (.int 1))] (.prim .bool))