From 7aa4f8ba80c928db8b6f3e5e24e5aef3bc5cc8b2 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Mon, 17 Feb 2025 14:18:54 +0000
Subject: [PATCH] SMV: range types are enum types

The range types x..y are syntactic sugar for the explicit enumeration {x, ..., y}.
---
 regression/smv/range-type/range_is_enum1.desc |  9 +++++++++
 regression/smv/range-type/range_is_enum1.smv  | 10 ++++++++++
 2 files changed, 19 insertions(+)
 create mode 100644 regression/smv/range-type/range_is_enum1.desc
 create mode 100644 regression/smv/range-type/range_is_enum1.smv

diff --git a/regression/smv/range-type/range_is_enum1.desc b/regression/smv/range-type/range_is_enum1.desc
new file mode 100644
index 00000000..59d90abe
--- /dev/null
+++ b/regression/smv/range-type/range_is_enum1.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+range_is_enum1.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Conversion from range to enum not supported.
diff --git a/regression/smv/range-type/range_is_enum1.smv b/regression/smv/range-type/range_is_enum1.smv
new file mode 100644
index 00000000..a6aa3337
--- /dev/null
+++ b/regression/smv/range-type/range_is_enum1.smv
@@ -0,0 +1,10 @@
+MODULE main
+
+-- range types are syntactic sugar for enumeration types
+VAR x: 0..6;
+VAR y: {0, 1, 2, 3, 4, 5, 6};
+VAR z: 0..6;
+
+ASSIGN x := y;
+ASSIGN y := z;
+