diff --git a/src/ast/rewriter/seq_eq_solver.cpp b/src/ast/rewriter/seq_eq_solver.cpp
index a268f3c41..b779d3f4b 100644
--- a/src/ast/rewriter/seq_eq_solver.cpp
+++ b/src/ast/rewriter/seq_eq_solver.cpp
@@ -422,7 +422,6 @@ namespace seq {
             unsigned num_ls_units = count_units_r2l(ls, ls.size() - 1);
             if (num_ls_units == 0 || num_ls_units == ls.size())
                 return false;
-            unsigned ls_units_offset = ls.size() - num_ls_units;
             unsigned num_rs_non_units = count_non_units_r2l(rs, rs.size() - 1);
             if (num_rs_non_units == rs.size())
                 return false;
diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp
index 1640d7663..70b09aba3 100644
--- a/src/math/lp/gomory.cpp
+++ b/src/math/lp/gomory.cpp
@@ -221,7 +221,7 @@ class create_cut {
         for (const auto & p : m_row) {
             dump_declaration(out, p.var());
         }
-        for (const auto& p : m_t) {
+        for (lar_term::ival p : m_t) {
             auto t = lia.lra.column2tv(p.column());
             if (t.is_term()) {
                 dump_declaration(out, t.id());
@@ -252,7 +252,7 @@ class create_cut {
     }
 
     std::ostream& dump_term_coefficients(std::ostream & out) const {
-        for (const auto& p : m_t) {
+        for (lar_term::ival p : m_t) {
             dump_coeff(out, p);
         }
         return out;
diff --git a/src/math/lp/int_cube.cpp b/src/math/lp/int_cube.cpp
index 6b6ab8980..269a85386 100644
--- a/src/math/lp/int_cube.cpp
+++ b/src/math/lp/int_cube.cpp
@@ -103,7 +103,7 @@ namespace lp {
         }
     usual_delta:
         mpq delta = zero_of_type<mpq>();
-        for (const auto & p : t)
+        for (lar_term::ival p : t)
             if (lia.column_is_int(p.column()))
                 delta += abs(p.coeff());
         
diff --git a/src/math/lp/lar_constraints.h b/src/math/lp/lar_constraints.h
index a425460f9..3bcd62d00 100644
--- a/src/math/lp/lar_constraints.h
+++ b/src/math/lp/lar_constraints.h
@@ -239,9 +239,8 @@ public:
         
     std::ostream& display(std::ostream& out) const {
         out << "number of constraints = " << m_constraints.size() << std::endl;
-        for (auto const& c : indices()) {
+        for (constraint_index c : indices()) 
             display(out << "(" << c << ") ", *m_constraints[c]);
-        }
         return out;
     }
 
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 534a63972..dba380010 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -337,7 +337,7 @@ namespace lp {
         auto& jset = m_mpq_lar_core_solver.m_r_solver.inf_set(); // hijack this set that should be empty right now
         lp_assert(jset.empty());
 
-        for (const auto& p : term) {
+        for (lar_term::ival p : term) {
             unsigned j = p.column();
             rslv.m_costs[j] = zero_of_type<mpq>();
             int i = rslv.m_basis_heading[j];
@@ -367,7 +367,7 @@ namespace lp {
         lp_assert(costs_are_zeros_for_r_solver());
         lp_assert(reduced_costs_are_zeroes_for_r_solver());
         rslv.m_costs.resize(A_r().column_count(), zero_of_type<mpq>());
-        for (const auto& p : term) {
+        for (lar_term::ival p : term) {
             unsigned j = p.column();
             rslv.m_costs[j] = p.coeff();
             if (rslv.m_basis_heading[j] < 0)
@@ -1069,7 +1069,7 @@ namespace lp {
         if (tv::is_term(var)) {
             lar_term const& t = get_term(var);
             value = 0;
-            for (auto const& cv : t) {
+            for (lar_term::ival cv : t) {
                 impq const& r = get_column_value(cv.column());
                 if (!numeric_traits<mpq>::is_zero(r.y)) return false;
                 value += r.x * cv.coeff();
@@ -1185,7 +1185,7 @@ namespace lp {
             return get_value(column_index(term_j));
 #endif
         mpq r(0);
-        for (const auto& p : get_term(t)) 
+        for (lar_term::ival p : get_term(t)) 
             r += p.coeff() * get_value(p.column());
         return r;
     }
@@ -1194,7 +1194,7 @@ namespace lp {
         if (t.is_var())
             return get_column_value(t.column());
         impq r;
-        for (const auto& p : get_term(t)) 
+        for (lar_term::ival p : get_term(t)) 
             r += p.coeff() * get_column_value(p.column());
         return r;
     }
@@ -1744,7 +1744,7 @@ namespace lp {
         m_mpq_lar_core_solver.m_r_solver.update_x(j, get_basic_var_value_from_row(A_r().row_count() - 1));
         if (use_lu())
             fill_last_row_of_A_d(A_d(), term);
-        for (const auto& c : *term) {
+        for (lar_term::ival c : *term) {
             unsigned j = c.column();
             while (m_usage_in_terms.size() <= j) {
                 m_usage_in_terms.push_back(0);
@@ -2326,7 +2326,7 @@ namespace lp {
                 continue;
             bool need_to_fix = false;
             const lar_term& t = *m_terms[i];
-            for (const auto& p : t) {
+            for (lar_term::ival p : t) {
                 if (m_incorrect_columns.contains(p.column())) {
                     need_to_fix = true;
                     break;
@@ -2343,7 +2343,7 @@ namespace lp {
     // return true if all y coords are zeroes
     bool lar_solver::sum_first_coords(const lar_term& t, mpq& val) const {
         val = zero_of_type<mpq>();
-        for (const auto& c : t) {
+        for (lar_term::ival c : t) {
             const auto& x = m_mpq_lar_core_solver.m_r_x[c.column()];
             if (!is_zero(x.y))
                 return false;
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index cff0f9028..36908a05d 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -466,7 +466,7 @@ public:
             return false;
         TRACE("nla_solver", tout << "j" << j << " not blocked\n";);
         impq delta = get_column_value(j) - ival;
-        for (const auto &c : A_r().column(j)) {
+        for (auto c : A_r().column(j)) {
             unsigned row_index = c.var();
             const mpq & a = c.coeff();        
             unsigned rj = m_mpq_lar_core_solver.m_r_basis[row_index];      
diff --git a/src/math/lp/lar_term.h b/src/math/lp/lar_term.h
index 39e2a7d3f..bea2d24d3 100644
--- a/src/math/lp/lar_term.h
+++ b/src/math/lp/lar_term.h
@@ -158,13 +158,13 @@ public:
     bool is_normalized() const {
         lpvar min_var = -1;
         mpq c;
-        for (const auto & p : *this) {
+        for (ival p : *this) {
             if (p.column() < min_var) {
                 min_var = p.column();
             }
         }
         lar_term r;
-        for (const auto & p : *this) {
+        for (ival p : *this) {
             if (p.column() == min_var) {
                 return p.coeff().is_one();
             }
diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp
index dbe66a4aa..0b6fa9f5c 100644
--- a/src/sat/smt/array_axioms.cpp
+++ b/src/sat/smt/array_axioms.cpp
@@ -223,9 +223,6 @@ namespace array {
             args1.push_back(k);
             args2.push_back(k);
         }
-        std::cout << "e1: " << mk_pp(e1, m) << "\n";
-        std::cout << "e2: " << mk_pp(e2, m) << "\n";
-        std::cout << "funcs: " << funcs << "\n";
         expr_ref sel1(a.mk_select(args1), m);
         expr_ref sel2(a.mk_select(args2), m);
         literal lit1 = eq_internalize(e1, e2);
diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp
index 2905d79d1..e1d52ca36 100644
--- a/src/sat/smt/bv_solver.cpp
+++ b/src/sat/smt/bv_solver.cpp
@@ -419,7 +419,7 @@ namespace bv {
             if (p.m_atom) {
                 for (auto vp : *p.m_atom)
                     propagate_bits(vp);
-                for (auto const& eq : p.m_atom->eqs()) 
+                for (eq_occurs const& eq : p.m_atom->eqs()) 
                     propagate_eq_occurs(eq);                
             }
             else 
@@ -691,7 +691,7 @@ namespace bv {
             result->m_bool_var2atom.setx(i, new_a, nullptr);
             for (auto vp : *a)
                 new_a->m_occs = new (result->get_region()) var_pos_occ(vp.first, vp.second, new_a->m_occs);
-            for (auto const& occ : a->eqs()) {
+            for (eq_occurs const& occ : a->eqs()) {
                 expr* e = occ.m_node->get_expr();
                 expr_ref e2(tr(e), tr.to());
                 euf::enode* n = ctx.get_enode(e2);
diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp
index 7e17c001c..892ba2f58 100644
--- a/src/sat/smt/dt_solver.cpp
+++ b/src/sat/smt/dt_solver.cpp
@@ -245,7 +245,6 @@ namespace dt {
         unsigned non_rec_idx = dt.get_constructor_idx(non_rec_c);        
         var_data* d = m_var_data[v];
         enode* recognizer = d->m_recognizers.get(non_rec_idx, nullptr);
-        func_decl* r = nullptr;
         SASSERT(!d->m_constructor);
         SASSERT(!recognizer || ctx.value(recognizer) == l_false || !is_final);
         
diff --git a/src/smt/seq_axioms.h b/src/smt/seq_axioms.h
index dc2548b85..e1dd99b64 100644
--- a/src/smt/seq_axioms.h
+++ b/src/smt/seq_axioms.h
@@ -37,7 +37,6 @@ namespace smt {
         seq::skolem    m_sk;
         seq::axioms    m_ax;
         bool           m_digits_initialized;
-        bool           m_use_new_axioms { true };
 
         literal mk_eq_empty(expr* e, bool phase = true) { return mk_eq_empty2(e, phase); }
         context& ctx() { return th.get_context(); }
diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp
index 2a9ed15d1..465b50604 100644
--- a/src/smt/seq_eq_solver.cpp
+++ b/src/smt/seq_eq_solver.cpp
@@ -777,6 +777,7 @@ bool theory_seq::branch_quat_variable(depeq const& e) {
         return propagate_lit(dep, lits.size(), lits.c_ptr(), false_literal);
     }
     UNREACHABLE();
+    return false;
 }
 
 
diff --git a/src/util/container_util.h b/src/util/container_util.h
index efee89952..4c76850b8 100644
--- a/src/util/container_util.h
+++ b/src/util/container_util.h
@@ -30,7 +30,7 @@ Revision History:
 template<class Set1, class Set2>
 void set_intersection(Set1 & tgt, const Set2 & src) {
     svector<typename Set1::data> to_remove;
-    for (auto const& itm : tgt) 
+    for (typename Set1::data const& itm : tgt) 
         if (!src.contains(itm)) 
             to_remove.push_back(itm);
     while (!to_remove.empty()) {