diff --git a/src/muz/ddnf/ddnf.cpp b/src/muz/ddnf/ddnf.cpp
index eaf352475..6a04ae874 100644
--- a/src/muz/ddnf/ddnf.cpp
+++ b/src/muz/ddnf/ddnf.cpp
@@ -652,8 +652,8 @@ namespace datalog {
         void init_ctx(rule_set& rules) {
             m_inner_ctx.reset();
             func_decl_set const& predicates = m_ctx.get_predicates();
-            for (func_decl_set::iterator fit = predicates.begin(); fit != predicates.end(); ++fit) {
-                m_inner_ctx.register_predicate(*fit, false);
+            for (auto* fit : predicates) {
+                m_inner_ctx.register_predicate(fit, false);
             }
             m_inner_ctx.ensure_opened();
             m_inner_ctx.replace_rules(rules);
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index a97e2b125..a47009bce 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3185,15 +3185,13 @@ namespace smt {
             TRACE("theory_case_split", tout << "assigned literal " << l.index() << " is a theory case split literal" << std::endl;);
             // now find the sets of literals which contain l
             vector<literal_vector> const& case_split_sets = m_literal2casesplitsets[l.index()];
-            for (vector<literal_vector>::const_iterator it = case_split_sets.begin(); it != case_split_sets.end(); ++it) {
-                literal_vector case_split_set = *it;
+            for (const auto& case_split_set : case_split_sets) {
                 TRACE("theory_case_split", tout << "found case split set { ";
-                      for(literal_vector::iterator set_it = case_split_set.begin(); set_it != case_split_set.end(); ++set_it) {
-                          tout << set_it->index() << " ";
+                      for (const auto& set_elem : case_split_set) {
+                          tout << set_elem.index() << " ";
                       }
                       tout << "}" << std::endl;);
-                for(literal_vector::iterator set_it = case_split_set.begin(); set_it != case_split_set.end(); ++set_it) {
-                    literal l2 = *set_it;
+                for (const auto& l2 : case_split_set) {
                     if (l2 != l) {
                         b_justification js(l);
                         TRACE("theory_case_split", tout << "case split literal "; smt::display(tout, l2, m, m_bool_var2expr.data()); tout << std::endl;);
diff --git a/src/tactic/core/cofactor_term_ite_tactic.cpp b/src/tactic/core/cofactor_term_ite_tactic.cpp
index 1bd4cf11a..c46e5d9f2 100644
--- a/src/tactic/core/cofactor_term_ite_tactic.cpp
+++ b/src/tactic/core/cofactor_term_ite_tactic.cpp
@@ -30,7 +30,7 @@ class cofactor_term_ite_tactic : public tactic {
     void process(goal & g) {
         ast_manager & m = g.m();
         unsigned idx = 0;
-        for (auto [f, dep, pr] : g) {
+        for (const auto& [f, dep, pr] : g) {
             if (g.inconsistent())
                 break;
             expr_ref new_f(m);
diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp
index e2260dc3c..647bd18c5 100644
--- a/src/tactic/core/tseitin_cnf_tactic.cpp
+++ b/src/tactic/core/tseitin_cnf_tactic.cpp
@@ -853,7 +853,7 @@ class tseitin_cnf_tactic : public tactic {
                 m_mc = nullptr;
 
             unsigned idx = 0;
-            for (auto [f, dep, pr] : *g) {
+            for (const auto& [f, dep, pr] : *g) {
                 process(f, dep);
                 g->update(idx++, m.mk_true(), nullptr, nullptr);
             }
diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp
index 96cf4e888..7c0bb9b59 100644
--- a/src/tactic/goal.cpp
+++ b/src/tactic/goal.cpp
@@ -488,7 +488,7 @@ void goal::shrink(unsigned j) {
 */
 void goal::elim_true() {    
     unsigned i = 0, j = 0;
-    for (auto [f, dep, pr] : *this) {
+    for (const auto& [f, dep, pr] : *this) {
         if (m().is_true(f)) {
             ++i;
             continue;
diff --git a/src/test/algebraic.cpp b/src/test/algebraic.cpp
index 371997c02..8d1b60777 100644
--- a/src/test/algebraic.cpp
+++ b/src/test/algebraic.cpp
@@ -25,18 +25,18 @@ Notes:
 static void display_anums(std::ostream & out, scoped_anum_vector const & rs) {
     out << "numbers in decimal:\n";
     algebraic_numbers::manager & m = rs.m();
-    for (unsigned i = 0; i < rs.size(); i++) {
-        m.display_decimal(out, rs[i], 10);
+    for (const auto& r : rs) {
+        m.display_decimal(out, r, 10);
         out << "\n";
     }
     out << "numbers as root objects\n";
-    for (unsigned i = 0; i < rs.size(); i++) {
-        m.display_root(out, rs[i]);
+    for (const auto& r : rs) {
+        m.display_root(out, r);
         out << "\n";
     }
     out << "numbers as intervals\n";
-    for (unsigned i = 0; i < rs.size(); i++) {
-        m.display_interval(out, rs[i]);
+    for (const auto& r : rs) {
+        m.display_interval(out, r);
         out << "\n";
     }
 }
diff --git a/src/test/hashtable.cpp b/src/test/hashtable.cpp
index e26fbd5d8..f863c3dc4 100644
--- a/src/test/hashtable.cpp
+++ b/src/test/hashtable.cpp
@@ -83,18 +83,14 @@ static void tst2() {
         }
     }
     { 
-        safe_int_set::iterator it  = h2.begin();
-        safe_int_set::iterator end = h2.end();
-        for(; it != end; ++it) {
-            ENSURE(contains(h1, *it));
+        for (const auto& elem : h2) {
+            ENSURE(contains(h1, elem));
         }
     }
     {
-        int_set::iterator it = h1.begin();
-        int_set::iterator end = h1.end();
         int n = 0;
-        for (; it != end; ++it) {
-            ENSURE(contains(h1, *it));
+        for (const auto& elem : h1) {
+            ENSURE(contains(h1, elem));
             n++;
         }
         ENSURE(n == h1.size());
@@ -202,7 +198,7 @@ void test_hashtable_iterators() {
     ht.insert(3);
     
     int count = 0;
-    for(auto it = ht.begin(); it != ht.end(); ++it) {
+    for (const auto& elem : ht) {
         ++count;
     }
     VERIFY(count == 3);