From 59fa8964cad87215cc8f6e24661224cc8566e2c3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 2 Dec 2022 07:54:32 -0800
Subject: [PATCH] minor code cleanup

---
 src/tactic/arith/bound_propagator.cpp       | 5 ++---
 src/tactic/arith/propagate_ineqs_tactic.cpp | 4 +---
 src/tactic/smtlogics/qfauflia_tactic.cpp    | 1 -
 3 files changed, 3 insertions(+), 7 deletions(-)

diff --git a/src/tactic/arith/bound_propagator.cpp b/src/tactic/arith/bound_propagator.cpp
index 3c4844462..ba58b6160 100644
--- a/src/tactic/arith/bound_propagator.cpp
+++ b/src/tactic/arith/bound_propagator.cpp
@@ -840,9 +840,8 @@ void bound_propagator::explain(var x, bound * b, unsigned ts, assumption_vector
             break;
         }
     }
-    unsigned sz = todo.size();
-    for (unsigned i = 0; i < sz; i++)
-        todo[i].second->m_mark = false;
+    for (var_bound& vb : todo)
+        vb.second->m_mark = false;
     todo.reset();
 }
 
diff --git a/src/tactic/arith/propagate_ineqs_tactic.cpp b/src/tactic/arith/propagate_ineqs_tactic.cpp
index 0f62b45f4..871a9ac3b 100644
--- a/src/tactic/arith/propagate_ineqs_tactic.cpp
+++ b/src/tactic/arith/propagate_ineqs_tactic.cpp
@@ -135,9 +135,7 @@ struct propagate_ineqs_tactic::imp {
         mpq c_mpq_val;
         if (m_util.is_add(t)) {
             rational c_val;
-            unsigned num = to_app(t)->get_num_args();
-            for (unsigned i = 0; i < num; i++) {
-                expr * mon = to_app(t)->get_arg(i);
+            for (expr* mon : *to_app(t)) {
                 expr * c, * x;
                 if (m_util.is_mul(mon, c, x) && m_util.is_numeral(c, c_val)) {
                     nm.set(c_mpq_val, c_val.to_mpq());
diff --git a/src/tactic/smtlogics/qfauflia_tactic.cpp b/src/tactic/smtlogics/qfauflia_tactic.cpp
index 2f1879d58..5c2a92ef6 100644
--- a/src/tactic/smtlogics/qfauflia_tactic.cpp
+++ b/src/tactic/smtlogics/qfauflia_tactic.cpp
@@ -19,7 +19,6 @@ Notes:
 #include "tactic/tactical.h"
 #include "tactic/core/simplify_tactic.h"
 #include "tactic/core/propagate_values_tactic.h"
-#include "tactic/arith/propagate_ineqs_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
 #include "tactic/core/elim_uncnstr_tactic.h"
 #include "tactic/smtlogics/smt_tactic.h"