From 320105c71406f557a8c7fc470054ac1af5e213db Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 20 Sep 2017 13:30:31 -0700
Subject: [PATCH] removing iterators

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/mam.cpp      | 18 +++++-------------
 src/smt/qi_queue.cpp |  5 +----
 2 files changed, 6 insertions(+), 17 deletions(-)

diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index a88ef1e0d..497aab8db 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -2016,26 +2016,20 @@ namespace smt {
         void execute(code_tree * t) {
             TRACE("trigger_bug", tout << "execute for code tree:\n"; t->display(tout););
             init(t);
-            enode_vector::const_iterator it  = t->get_candidates().begin();
-            enode_vector::const_iterator end = t->get_candidates().end();
             if (t->filter_candidates()) {
-                for (; it != end; ++it) {
-                    enode * app = *it;
+                for (enode * app : t->get_candidates()) {
                     if (!app->is_marked() && app->is_cgr()) {
                         execute_core(t, app);
                         app->set_mark();
                     }
                 }
-                it  = t->get_candidates().begin();
-                for (; it != end; ++it) {
-                    enode * app = *it;
+                for (enode * app : t->get_candidates()) {
                     if (app->is_marked())
                         app->unset_mark();
                 }
             }
             else {
-                for (; it != end; ++it) {
-                    enode * app = *it;
+                for (enode * app : t->get_candidates()) {
                     TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m_ast_manager) << "\n";);
                     if (app->is_cgr()) {
                         TRACE("trigger_bug", tout << "is_cgr\n";);
@@ -2821,15 +2815,13 @@ namespace smt {
     } // end of execute_core
 
     void display_trees(std::ostream & out, const ptr_vector<code_tree> & trees) {
-        ptr_vector<code_tree>::const_iterator it  = trees.begin();
-        ptr_vector<code_tree>::const_iterator end = trees.end();
         unsigned lbl = 0;
-        for (; it != end; ++it, ++lbl) {
-            code_tree * tree = *it;
+        for (code_tree* tree : trees) {
             if (tree) {
                 out << "tree for f" << lbl << "\n";
                 out << *tree;
             }
+            ++lbl;
         }
     }
 
diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp
index f77fde29a..2a8d9d199 100644
--- a/src/smt/qi_queue.cpp
+++ b/src/smt/qi_queue.cpp
@@ -148,11 +148,8 @@ namespace smt {
     }
 
     void qi_queue::instantiate() {
-        svector<entry>::iterator it               = m_new_entries.begin();
-        svector<entry>::iterator end              = m_new_entries.end();
         unsigned                 since_last_check = 0;
-        for (; it != end; ++it) {
-            entry & curr       = *it;
+        for (entry & curr : m_new_entries) {
             fingerprint * f    = curr.m_qb;
             quantifier * qa    = static_cast<quantifier*>(f->get_data());