mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

fix #3500

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-24 10:25:42 -07:00
parent 601b3998f3
commit 33b644adad
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_seq.cpp
View file

@ -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);
}