na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Aug 23, 2020 · 03276b1 · 03276b1
1 parent 96f10b8
commit 03276b1
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 15 deletions.
diff --git 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<enode, enode, data>::iterator it  = m_already_processed.begin();
-        obj_pair_map<enode, enode, data>::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
@@ -209,10 +209,10 @@ namespace {
         }
 
         void user_propagate_init(
-            void* ctx, 
-            std::function<void(void*)>&                  push_eh,
-            std::function<void(void*, unsigned)>&        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);
         }