From 33b644adadfbed35af772652d8c9462fb32dc7fc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 24 Mar 2020 10:25:42 -0700 Subject: [PATCH] fix #3500 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index af4bf1c87..aca35b04b 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2132,7 +2132,10 @@ void theory_seq::mk_decompose(expr* e, expr_ref& head, expr_ref& tail) { head = e; tail = m_util.str.mk_empty(m.get_sort(e)); } - else if (m_util.str.is_concat(e, e1, e2) && m_util.str.is_string(e1, s)) { + else if (m_util.str.is_concat(e, e1, e2) && m_util.str.is_empty(e1)) { + mk_decompose(e2, head, tail); + } + else if (m_util.str.is_concat(e, e1, e2) && m_util.str.is_string(e1, s) && s.length() > 0) { head = m_util.str.mk_unit(m_util.str.mk_char(s, 0)); tail = m_util.str.mk_concat(m_util.str.mk_string(s.extract(1, s.length()-1)), e2); }