diff --git a/regression/smv/expressions/smv_union1.desc b/regression/smv/expressions/smv_union1.desc
new file mode 100644
index 000000000..393af51d4
--- /dev/null
+++ b/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
diff --git a/regression/smv/expressions/smv_union1.smv b/regression/smv/expressions/smv_union1.smv
new file mode 100644
index 000000000..bf38d4595
--- /dev/null
+++ b/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
diff --git a/regression/smv/expressions/smv_union2.desc b/regression/smv/expressions/smv_union2.desc
new file mode 100644
index 000000000..242c1f2e2
--- /dev/null
+++ b/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.
diff --git a/regression/smv/expressions/smv_union2.smv b/regression/smv/expressions/smv_union2.smv
new file mode 100644
index 000000000..9e05c41f9
--- /dev/null
+++ b/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