From 03276b12b1896b05c2fd29c0417247e4d76e2aeb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 22 Aug 2020 19:12:02 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/smt/arith_eq_adapter.cpp | 20 +++++++++----------- src/smt/smt_solver.cpp | 8 ++++---- 2 files changed, 13 insertions(+), 15 deletions(-) diff --git a/src/smt/arith_eq_adapter.cpp b/src/smt/arith_eq_adapter.cpp index e09a2af109c..20f4e2239b4 100644 --- a/src/smt/arith_eq_adapter.cpp +++ b/src/smt/arith_eq_adapter.cpp @@ -253,13 +253,13 @@ namespace smt { context & ctx = get_context(); TRACE("arith_eq_adapter", tout << "restart\n";); enode_pair_vector tmp(m_restart_pairs); - enode_pair_vector::iterator it = tmp.begin(); - enode_pair_vector::iterator end = tmp.end(); m_restart_pairs.reset(); - for (; it != end && !ctx.inconsistent(); ++it) { - TRACE("arith_eq_adapter", tout << "creating arith_eq_adapter axioms at the base level #" << it->first->get_owner_id() << " #" << - it->second->get_owner_id() << "\n";); - mk_axioms(it->first, it->second); + for (auto const& p : tmp) { + if (ctx.inconsistent()) + break; + TRACE("arith_eq_adapter", tout << "creating arith_eq_adapter axioms at the base level #" << p.first->get_owner_id() << " #" << + p.second->get_owner_id() << "\n";); + mk_axioms(p.first, p.second); } } @@ -268,11 +268,9 @@ namespace smt { } void arith_eq_adapter::display_already_processed(std::ostream & out) const { - obj_pair_map::iterator it = m_already_processed.begin(); - obj_pair_map::iterator end = m_already_processed.end(); - for (; it != end; ++it) { - enode * n1 = it->get_key1(); - enode * n2 = it->get_key2(); + for (auto const& d : m_already_processed) { + enode * n1 = d.get_key1(); + enode * n2 = d.get_key2(); out << "eq_adapter: #" << n1->get_owner_id() << " #" << n2->get_owner_id() << "\n"; } } diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 0b380f04d33..208b51f0a4d 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -209,10 +209,10 @@ namespace { } void user_propagate_init( - void* ctx, - std::function& push_eh, - std::function& pop_eh, - solver::fresh_eh_t& fresh_eh) override { + void* ctx, + solver::push_eh_t& push_eh, + solver::pop_eh_t& pop_eh, + solver::fresh_eh_t& fresh_eh) override { m_context.user_propagate_init(ctx, push_eh, pop_eh, fresh_eh); }