mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

fix #4792

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-11-12 13:23:34 -08:00
parent d61f30fdc6
commit 7f869e513b
1 changed files with 6 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/smt/theory_seq.cpp
View file

@ -1980,15 +1980,16 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
seq_value_proc* sv = alloc(seq_value_proc, *this, n, srt); seq_value_proc* sv = alloc(seq_value_proc, *this, n, srt);
unsigned end = m_concat.size(); unsigned end = m_concat.size();
TRACE("seq", tout << mk_pp(e, m) << "\n";); TRACE("seq", tout << "sequence: " << start << " " << end << " " << mk_pp(e, m) << "\n";);
for (unsigned i = start; i < end; ++i) { for (unsigned i = start; i < end; ++i) {
expr* c = m_concat[i]; expr* c = m_concat[i];
expr *c1; expr *c1;
TRACE("seq", tout << mk_pp(c, m) << "\n";); TRACE("seq", tout << "elem: " << mk_pp(c, m) << "\n";);
if (m_util.str.is_unit(c, c1)) { if (m_util.str.is_unit(c, c1)) {
if (ctx.e_internalized(c1)) { if (ctx.e_internalized(c1))
sv->add_unit(ctx.get_enode(c1)); sv->add_unit(ctx.get_enode(c1));
} else if (m.is_value(c1))
sv->add_string(c);
else { else {
TRACE("seq", tout << "not internalized " << mk_pp(c, m) << "\n";); TRACE("seq", tout << "not internalized " << mk_pp(c, m) << "\n";);
} }
@ -2005,7 +2006,7 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
sv->add_string(mk_value(to_app(c))); sv->add_string(mk_value(to_app(c)));
} }
} }
m_concat.shrink(start); m_concat.shrink(start);
return sv; return sv;
} }
else { else {