From cf060eb6dfb25a6d8be2820fa6e7a627d1c0405f Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sat, 5 Jul 2025 16:40:51 +0100
Subject: [PATCH] SMV: KNOWNBUG test for integer range with negative numbers

---
 regression/smv/range-type/range_type10.desc |  8 ++++++++
 regression/smv/range-type/range_type10.smv  | 22 +++++++++++++++++++++
 2 files changed, 30 insertions(+)
 create mode 100644 regression/smv/range-type/range_type10.desc
 create mode 100644 regression/smv/range-type/range_type10.smv

diff --git a/regression/smv/range-type/range_type10.desc b/regression/smv/range-type/range_type10.desc
new file mode 100644
index 000000000..029beb192
--- /dev/null
+++ b/regression/smv/range-type/range_type10.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+range_type10.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This fails to parse.
diff --git a/regression/smv/range-type/range_type10.smv b/regression/smv/range-type/range_type10.smv
new file mode 100644
index 000000000..1a323f5e4
--- /dev/null
+++ b/regression/smv/range-type/range_type10.smv
@@ -0,0 +1,22 @@
+MODULE main
+
+VAR x : 1..6;
+VAR y : -6..-1;
+
+ASSIGN init(x) := 1;
+ASSIGN init(y) := -1;
+
+ASSIGN next(x) :=
+  case
+    x=6 : 1;
+    TRUE: x+1;
+  esac;
+
+ASSIGN next(y) :=
+  case
+    y=-6 : -1;
+    TRUE: y + -1;
+  esac;
+
+-- should pass
+LTLSPEC G x + y = 0