From 8198a7e1ff81ada37ccf66c7c8383b915b9694d0 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 2 Jul 2025 15:50:26 +0100
Subject: [PATCH] SMV: two tests for union

This adds two tests for SMV union expressions.
---
 regression/smv/expressions/smv_union1.desc |  9 +++++++++
 regression/smv/expressions/smv_union1.smv  | 11 +++++++++++
 regression/smv/expressions/smv_union2.desc | 11 +++++++++++
 regression/smv/expressions/smv_union2.smv  | 11 +++++++++++
 4 files changed, 42 insertions(+)
 create mode 100644 regression/smv/expressions/smv_union1.desc
 create mode 100644 regression/smv/expressions/smv_union1.smv
 create mode 100644 regression/smv/expressions/smv_union2.desc
 create mode 100644 regression/smv/expressions/smv_union2.smv

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