From 6f59ca1292303841aaf262a37e3237b5517c3231 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 7 Jul 2025 15:45:04 -0700
Subject: [PATCH] chore: tests for #9206

Add examples as tests for `grind`
---
 tests/lean/run/grind_cutsat_nat_eq.lean | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/tests/lean/run/grind_cutsat_nat_eq.lean b/tests/lean/run/grind_cutsat_nat_eq.lean
index 464bcd8f096f..daf48bcf4db5 100644
--- a/tests/lean/run/grind_cutsat_nat_eq.lean
+++ b/tests/lean/run/grind_cutsat_nat_eq.lean
@@ -121,3 +121,21 @@ set_option trace.grind.cutsat.model true in
 example (x y : Nat) : x = y + 3 → y > 0 → False := by
   fail_if_success grind
   sorry
+
+example (a b : Nat) : a  = a + b - b := by
+  grind
+
+example (a b : Int) : a = a + b - b := by
+  grind
+
+example (a b : Nat) : a = a + 2^b - 2^b := by
+  grind
+
+example (a b : Nat) : 2^a = 2^a + b - b := by
+  grind
+
+example (a b c : Nat) : c^a = c^a + b - b := by
+  grind
+
+example (n : Nat) : 0 ≤ 2 ^ n := by
+  grind