feat: correctly identify UInt counter examples as non spurious

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean

@@ -148,15 +148,27 @@ Diagnose spurious counter examples, currently this checks:
 -/
 def diagnose : DiagnosisM Unit := do
   for (expr, _) in ← equations do
-    match_expr expr with
-    | BitVec.ofBool x =>
-      match x with
-      | .fvar fvarId => checkRelevantHypsUsed fvarId
-      | _ => addUninterpretedSymbol expr
-    | _ =>
-      match expr with
-      | .fvar fvarId => checkRelevantHypsUsed fvarId
-      | _ => addUninterpretedSymbol expr
+    match findRelevantFVar expr with
+    | some fvarId => checkRelevantHypsUsed fvarId
+    | none => addUninterpretedSymbol expr
+where
+  findRelevantFVar (expr : Expr) : Option FVarId :=
+    match fvarId? expr with
+    | some fvarId => some fvarId
+    | none =>
+      match_expr expr with
+      | BitVec.ofBool x => fvarId? x
+      | UInt8.toBitVec x => fvarId? x
+      | UInt16.toBitVec x => fvarId? x
+      | UInt32.toBitVec x => fvarId? x
+      | UInt64.toBitVec x => fvarId? x
+      | USize.toBitVec x => fvarId? x
+      | _ => none
+  fvarId? (expr : Expr) : Option FVarId :=
+    match expr with
+    | .fvar fvarId => some fvarId
+    | _ => none
+
 
 end DiagnosisM
 

tests/lean/run/bv_uint.lean

@@ -1,7 +1,59 @@
 import Std.Tactic.BVDecide
 
+/-! UInt8 -/
 example (a b : UInt8) : a + b = b + a := by
   bv_decide
 
+/--
+error: The prover found a counterexample, consider the following assignment:
+a.toBitVec = 0xff#8
+b.toBitVec = 0xff#8
+-/
+#guard_msgs in
 example (a b : UInt8) : a + b = a := by
   bv_decide
+
+
+
+/-! UInt16 -/
+example (a b : UInt16) : a + b = b + a := by
+  bv_decide
+
+/--
+error: The prover found a counterexample, consider the following assignment:
+a.toBitVec = 0xffff#16
+b.toBitVec = 0xffff#16
+-/
+#guard_msgs in
+example (a b : UInt16) : a + b = a := by
+  bv_decide
+
+
+
+/-! UInt32 -/
+example (a b : UInt32) : a + b = b + a := by
+  bv_decide
+
+/--
+error: The prover found a counterexample, consider the following assignment:
+a.toBitVec = 0xffffffff#32
+b.toBitVec = 0xffffffff#32
+-/
+#guard_msgs in
+example (a b : UInt32) : a + b = a := by
+  bv_decide
+
+
+
+/-! UInt64 -/
+example (a b : UInt64) : a + b = b + a := by
+  bv_decide
+
+/--
+error: The prover found a counterexample, consider the following assignment:
+a.toBitVec = 0xffffffffffffffff#64
+b.toBitVec = 0xffffffffffffffff#64
+-/
+#guard_msgs in
+example (a b : UInt64) : a + b = a := by
+  bv_decide