Merge pull request #1179 from diffblue/smv_union1

SMV: two tests for `union`

Author: tautschnig

regression/smv/expressions/smv_union1.desc

@@ -0,0 +1,9 @@
+CORE broken-smt-backend
+smv_union1.smv
+
+^\[spec1\] x != 3: PROVED \(CT=1\)$
+^\[spec2\] x != 2: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/smv/expressions/smv_union1.smv

@@ -0,0 +1,11 @@
+MODULE main
+
+VAR x : 1..3;
+ASSIGN init(x) := 1 union 2;
+       next(x) := x;
+
+-- passes
+SPEC x != 3
+
+-- fails
+SPEC x != 2

regression/smv/expressions/smv_union2.desc

@@ -0,0 +1,11 @@
+KNOWNBUG broken-smt-backend
+smv_union2.smv
+
+^\[spec1\] x != 3: PROVED \(CT=1\)$
+^\[spec2\] x != 2: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The type checker rejects this.

regression/smv/expressions/smv_union2.smv

@@ -0,0 +1,11 @@
+MODULE main
+
+VAR x : 1..3;
+ASSIGN init(x) := 1 union { 2 };
+       next(x) := x;
+
+-- passes
+SPEC x != 3
+
+-- fails
+SPEC x != 2