diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 330a608a4..d09069ce4 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1498,8 +1498,8 @@ void theory_seq::add_length(expr* l) { TRACE("seq", tout << mk_bounded_pp(e, m, 2) << "\n";); m_length.push_back(l); m_has_length.insert(e); - m_trail_stack.push(insert_obj_trail(m_has_length, e)); m_trail_stack.push(push_back_vector(m_length)); + m_trail_stack.push(insert_obj_trail(m_has_length, e)); } /**