diff --git a/regression/smv/range-type/range_type10.desc b/regression/smv/range-type/range_type10.desc new file mode 100644 index 00000000..029beb19 --- /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 00000000..1a323f5e --- /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