diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp index 2fa652828..396b5f092 100644 --- a/src/qe/qe_term_graph.cpp +++ b/src/qe/qe_term_graph.cpp @@ -701,7 +701,7 @@ namespace qe { } void solve() { - ptr_vector worklist; + ptr_vector worklist; for (term * t : m_tg.m_terms) { // skip pure terms if (m_term2app.contains(t->get_id())) continue; @@ -785,7 +785,8 @@ namespace qe { do { expr* member = mk_pure(*r); SASSERT(member); - if (!members.contains(member) && (!is_projected(*r) || !is_solved_eq(rep, member))) { + if (!members.contains(member) && + (!is_projected(*r) || !is_solved_eq(rep, member))) { res.push_back(m.mk_eq(rep, member)); members.insert(member); }