diff --git a/tests/lean/run/wfLean3Issue.lean b/tests/lean/run/wfLean3Issue.lean
new file mode 100644
index 0000000000..f65609d9b7
--- /dev/null
+++ b/tests/lean/run/wfLean3Issue.lean
@@ -0,0 +1,6 @@
+def foo : Nat → Nat → Nat
+  | 0,   0   => 1
+  | s+1, 0   => foo s 0 + 1
+  | 0,   b+1 => foo 0 b + 1
+  | s+1, b+1 => foo (s+1) b + foo s (b+1)
+termination_by foo b s => (b, s)