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; +