From 34f8872ba83aa5e91d73a80034b4c58db25dbbf7 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 31 Jan 2019 14:08:30 -0500
Subject: Fix off-by-one error in nat syntax warnings

Fixes #9453
---
 test-suite/bugs/closed/bug_9453.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_9453.v

(limited to 'test-suite')

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. *)
-- 
cgit v1.2.3