Merge pull request #993 from diffblue/range_is_enum1

SMV: range types are enum types
diffblue · Feb 18, 2025 · f6b1acd · f6b1acd
2 parents b5a624c + 7aa4f8b
commit f6b1acd
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 0 deletions.
diff --git a/regression/smv/range-type/range_is_enum1.desc 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
@@ -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;
+