From cc5ff2afb12a08cc5c7cf86a1c1ecf7c8c7b265b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 24 Aug 2025 20:04:32 -0700
Subject: [PATCH] test: `grind cutsat` (#10106)

---
 tests/lean/run/grind_cutsat_pow.lean | 32 ++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)
 create mode 100644 tests/lean/run/grind_cutsat_pow.lean

diff --git a/tests/lean/run/grind_cutsat_pow.lean b/tests/lean/run/grind_cutsat_pow.lean
new file mode 100644
index 0000000000..8f688eea47
--- /dev/null
+++ b/tests/lean/run/grind_cutsat_pow.lean
@@ -0,0 +1,32 @@
+example (n : Nat) : n = 3 → 2 ^ n > 8 → False := by
+  grind
+
+example (n : Nat) : n = 2 → n ^ 3 > 8 → False := by
+  grind
+
+example (n : Int) : n = 2 → n ^ 3 > 8 → False := by
+  grind
+
+example (n : Nat) : 2 ^ n > 8 → 3 ≤ n → n ≤ 3 → False := by
+  grind
+
+example (n : Nat) : n ^ 3 > 8 → 2 ≤ n → n ≤ 2 → False := by
+  grind
+
+example (n : Nat) : n = 2 → 2 ^ (n+1) > 8 → False := by
+  grind
+
+example (n : Nat) : n = 2 → 2 ^ (n+1) = 8 := by
+  grind
+
+example (n : Nat) : n = 2 → 2 ^ (2*n) = 16 := by
+  grind
+
+example (n m : Nat) : n ≤ 2 → m ≤ n → m = 2 → 2 ^ (2*n) = 16 := by
+  grind
+
+example (a n : Nat) : a ^ n ≠ 8 → 3 ≤ n → n ≤ 3 → a = 2 → False := by
+  grind
+
+example (a b : Int) (n : Nat) : a ^ n ≠ 8 → 3 ≤ n → n ≤ 3 → a = b + 1 → 1 ≤ b → b ≤ 1 → False := by
+  grind