diff --git a/src/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp
index 4a79f1dc6..61368c58a 100644
--- a/src/ackermannization/ackermannize_bv_tactic.cpp
+++ b/src/ackermannization/ackermannize_bv_tactic.cpp
@@ -38,8 +38,7 @@ public:
         TRACE(goal, g->display(tout << "in\n"););
 
         ptr_vector<expr> flas;
-        const unsigned sz = g->size();
-        for (unsigned i = 0; i < sz; ++i) flas.push_back(g->form(i));
+        for (auto [f, dep, pr] : *g) flas.push_back(f);
         lackr lackr(m, m_p, m_st, flas, nullptr);
 
         // mk result
diff --git a/src/ackermannization/ackr_bound_probe.cpp b/src/ackermannization/ackr_bound_probe.cpp
index 0c7433761..a1c8d43aa 100644
--- a/src/ackermannization/ackr_bound_probe.cpp
+++ b/src/ackermannization/ackr_bound_probe.cpp
@@ -62,10 +62,9 @@ class ackr_bound_probe : public probe {
 public:
     result operator()(goal const & g) override {
         proc p(g.m());
-        unsigned sz = g.size();
         expr_fast_mark1 visited;
-        for (unsigned i = 0; i < sz; ++i) {
-            for_each_expr_core<proc, expr_fast_mark1, true, true>(p, visited, g.form(i));
+        for (auto [curr, dep, pr] : g) {
+            for_each_expr_core<proc, expr_fast_mark1, true, true>(p, visited, curr);
         }
         p.prune_non_select();
         double total = ackr_helper::calculate_lemma_bound(p.m_fun2terms, p.m_sel2terms);
diff --git a/src/ackermannization/ackr_model_converter.cpp b/src/ackermannization/ackr_model_converter.cpp
index 47308e7c2..57d414464 100644
--- a/src/ackermannization/ackr_model_converter.cpp
+++ b/src/ackermannization/ackr_model_converter.cpp
@@ -103,7 +103,7 @@ void ackr_model_converter::convert_constants(model * source, model * destination
     evaluator.set_model_completion(true);
     array_util autil(m);
 
-    for (unsigned i = 0; i < source->get_num_constants(); ++i) {
+    for (unsigned i = 0, n = source->get_num_constants(); i < n; ++i) {
         func_decl * const c = source->get_constant(i);
         app * const term = info->find_term(c);
         expr * value = source->get_const_interp(c);