diff --git a/src/smt/seq_unicode.cpp b/src/smt/seq_unicode.cpp index 8077a968b..4f293db46 100644 --- a/src/smt/seq_unicode.cpp +++ b/src/smt/seq_unicode.cpp @@ -26,9 +26,7 @@ namespace smt { th(th), m(th.get_manager()), seq(m), - dl(), m_qhead(0), - m_nc_functor(), m_var_value_hash(*this), m_var_value_eq(*this), m_var_value_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, m_var_value_hash, m_var_value_eq) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 4f376c9c6..06215f7d4 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -304,11 +304,11 @@ theory_seq::theory_seq(context& ctx): m_ls(m), m_rs(m), m_lhs(m), m_rhs(m), m_new_eqs(m), - m_has_seq(m_util.has_seq()), - m_unhandled_expr(nullptr), m_res(m), m_max_unfolding_depth(1), m_max_unfolding_lit(null_literal), + m_unhandled_expr(nullptr), + m_has_seq(m_util.has_seq()), m_new_solution(false), m_new_propagation(false), m_mk_aut(m) { diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index a344d8831..22d94ddd4 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -410,8 +410,6 @@ namespace smt { ptr_vector m_todo, m_concat; expr_ref_vector m_ls, m_rs, m_lhs, m_rhs; expr_ref_pair_vector m_new_eqs; - bool m_has_seq; - expr* m_unhandled_expr; // maintain automata with regular expressions. scoped_ptr_vector m_automata; @@ -421,6 +419,8 @@ namespace smt { literal m_max_unfolding_lit; vector m_s_in_re; + expr* m_unhandled_expr; + bool m_has_seq; bool m_new_solution; // new solution added bool m_new_propagation; // new propagation to core re2automaton m_mk_aut;