From 1c11526d640773dd43780966a4bcd449d1af9365 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 3 Jul 2026 11:41:37 -0700
Subject: [PATCH] fix propagation of failure

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_split.cpp | 5 ++---
 src/smt/seq_regex.cpp          | 2 +-
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp
index d8963ce838..452bdc420e 100644
--- a/src/ast/rewriter/seq_split.cpp
+++ b/src/ast/rewriter/seq_split.cpp
@@ -90,7 +90,7 @@ struct split_set::iterator::imp {
                 next();
             }
             if (b_it.failed() || a_it.failed())
-                parent().m_failure = true;
+                parent().set_failure();           
         }
     };
 
@@ -206,8 +206,6 @@ struct split_set::iterator::imp {
         }
 
         void consume() override {
-            if (at_end())
-                return;
             while (!parent().has_split() && !at_end() && !a_it.failed() && !b_it.failed()) {
                 if (a_it == a_end) {
                     auto [p, q] = *b_it;
@@ -335,6 +333,7 @@ struct split_set::iterator::imp {
     }
 
     void unfold(expr* r) {
+        TRACE(seq, tout << "unfold " << mk_pp(r, m) << "\n");
         SASSERT(seq.is_re(r));
         if (re.is_empty(r))
             return;
diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp
index d9844b31a0..9f2dbd32c9 100644
--- a/src/smt/seq_regex.cpp
+++ b/src/smt/seq_regex.cpp
@@ -523,7 +523,7 @@ namespace smt {
             if (re().is_empty(q)) {
                 enode_pair_vector eqs;
                 literal_vector lits;
-                lits.push_back(~lit);
+                lits.push_back(lit);
                 th.set_conflict(eqs, lits);
                 return true;
             }