diff --git a/src/smt/smt_justification.cpp b/src/smt/smt_justification.cpp index 94dd2e263..d7b9bdff0 100644 --- a/src/smt/smt_justification.cpp +++ b/src/smt/smt_justification.cpp @@ -321,12 +321,11 @@ namespace smt { region& r = ctx.get_region(); m_eqs = new (r) enode_pair[num_eqs]; std::uninitialized_copy(eqs, eqs + num_eqs, m_eqs); - DEBUG_CODE(( + DEBUG_CODE( for (unsigned i = 0; i < num_eqs; ++i) { - enode_pair const & [n1, n2] = eqs[i]; - SASSERT(n1->get_root() == n2->get_root()); + SASSERT(eqs[i].first->get_root() == eqs[i].second->get_root()); } - )); + ); } void ext_simple_justification::get_antecedents(conflict_resolution & cr) {