From 6bb3b699a80543c96d245d4610ab3888588b5afe Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sun, 6 Jul 2025 15:55:22 -0400
Subject: [PATCH] SMV: union operator

The SMV union operator computes the union of two set expressions.
---
 regression/smv/expressions/smv_union2.desc |  3 +-
 src/smvlang/smv_typecheck.cpp              | 48 ++++++++++++++--------
 2 files changed, 32 insertions(+), 19 deletions(-)

diff --git a/regression/smv/expressions/smv_union2.desc b/regression/smv/expressions/smv_union2.desc
index 242c1f2e2..f52cce99f 100644
--- a/regression/smv/expressions/smv_union2.desc
+++ b/regression/smv/expressions/smv_union2.desc
@@ -1,4 +1,4 @@
-KNOWNBUG broken-smt-backend
+CORE broken-smt-backend
 smv_union2.smv
 
 ^\[spec1\] x != 3: PROVED \(CT=1\)$
@@ -8,4 +8,3 @@ smv_union2.smv
 --
 ^warning: ignoring
 --
-The type checker rejects this.
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
index f5bc8ea2e..e488edb32 100644
--- a/src/smvlang/smv_typecheck.cpp
+++ b/src/smvlang/smv_typecheck.cpp
@@ -999,6 +999,37 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
     // only get added by type checker
     PRECONDITION(false);
   }
+  else if(expr.id() == ID_smv_union)
+  {
+    auto &lhs = to_binary_expr(expr).lhs();
+    auto &rhs = to_binary_expr(expr).rhs();
+
+    typecheck_expr_rec(lhs, mode);
+    typecheck_expr_rec(rhs, mode);
+
+    // create smv_set expression
+    exprt::operandst elements;
+
+    if(lhs.id() == ID_smv_set)
+    {
+      elements.insert(
+        elements.end(), lhs.operands().begin(), lhs.operands().end());
+    }
+    else
+      elements.push_back(lhs);
+
+    if(rhs.id() == ID_smv_set)
+    {
+      elements.insert(
+        elements.end(), rhs.operands().begin(), rhs.operands().end());
+    }
+    else
+      elements.push_back(rhs);
+
+    expr.id(ID_smv_set);
+    expr.operands() = std::move(elements);
+    expr.type() = typet{ID_smv_set};
+  }
   else if(expr.id() == ID_smv_setin)
   {
     auto &lhs = to_binary_expr(expr).lhs();
@@ -1741,23 +1772,6 @@ void smv_typecheckt::convert(exprt &expr, expr_modet expr_mode)
         expr.id(ID_next_symbol);
     }
   }
-  else if(expr.id()=="smv_nondet_choice" ||
-          expr.id()=="smv_union")
-  {
-    if(expr.operands().size()==0)
-    {
-      throw errort().with_location(expr.find_source_location())
-        << "expected operand here";
-    }
-
-    std::string identifier=
-      module+"::var::"+std::to_string(nondet_count++);
-
-    expr.set(ID_identifier, identifier);
-    expr.set("#smv_nondet_choice", true);
-
-    expr.id(ID_constraint_select_one);
-  }
   else if(expr.id()=="smv_cases") // cases
   {
     if(expr.operands().size()<1)