From 9b3826ed860da637b0c1decde3e01fc225c2b23a Mon Sep 17 00:00:00 2001 From: CEisenhofer Date: Thu, 2 Apr 2026 20:07:51 +0200 Subject: [PATCH] Missing case in concatenation --- src/smt/seq/seq_nielsen.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index d1f1a27f0..5d69f1faf 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -2898,6 +2898,7 @@ namespace seq { expr_ref p(m), q(m); if (seq.re.is_epsilon(left)) p = pair.m_p; else if (seq.re.is_epsilon(pair.m_p)) p = left; + else p = seq.re.mk_concat(left, pair.m_p); if (seq.re.is_epsilon(right)) q = pair.m_q; else if (seq.re.is_epsilon(pair.m_q)) q = right;