diff --git a/tests/lean/grind/algebra/linarith_cc.lean b/tests/lean/grind/algebra/linarith_cc.lean
new file mode 100644
index 0000000000..4a3e88bb0e
--- /dev/null
+++ b/tests/lean/grind/algebra/linarith_cc.lean
@@ -0,0 +1,4 @@
+-- This fails unless we manually substitute `hb`.
+-- `grind` doesn't recognise this as a linear arithmetic problem.
+example (a : Nat) (ha : a < 8) (b : Nat) (hb : b = 2) : a * b < 8 * b := by
+  grind -- fails