From f2e6d05c56f6280691125161df935006fe3a2da5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 17 Jun 2026 16:26:38 -0600
Subject: [PATCH] disable hoisting ite over union

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_derive.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp
index 6a95f2797..fdd27720c 100644
--- a/src/ast/rewriter/seq_derive.cpp
+++ b/src/ast/rewriter/seq_derive.cpp
@@ -677,7 +677,7 @@ namespace seq {
         auto xor_op   = [&](expr *x, expr *y) { return mk_xor(x, y); };
         switch (k) { 
         case OP_RE_UNION:
-            result = hoist_ite(a, b, union_op);
+            //result = hoist_ite(a, b, union_op);
             if (!result)
                result = mk_union_core(a, b); 
             break;