Fix off-by-one error in nat syntax warnings

Fixes #9453

1 files changed, 7 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_9453.v b/test-suite/bugs/closed/bug_9453.v
new file mode 100644
index 0000000000..18745533b2
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9453.v
@@ -0,0 +1,7 @@
+(* check compatibility with 8.8 and earlier for lack of warnings on the nat 5000 *)
+Set Warnings Append "+large-nat,+abstract-large-number".
+Fail Check 5001.
+Check 5000.
+(* Error:
+To avoid stack overflow, large numbers in nat are interpreted as applications of
+Nat.of_uint. *)