diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp
index 9e02a764f..5bb47c5c3 100644
--- a/src/muz/rel/dl_relation_manager.cpp
+++ b/src/muz/rel/dl_relation_manager.cpp
@@ -36,13 +36,10 @@ namespace datalog {
 
 
     void relation_manager::reset_relations() {
-        relation_map::iterator it=m_relations.begin();
-        relation_map::iterator end=m_relations.end();
-        for(;it!=end;++it) {
-            func_decl * pred = it->m_key;
+        for (auto const& kv : m_relations) {
+            func_decl * pred = kv.m_key;
             get_context().get_manager().dec_ref(pred); //inc_ref in get_relation
-            relation_base * r=(*it).m_value;
-            r->deallocate();
+            kv.m_value->deallocate();
         }
         m_relations.reset();
     }
@@ -119,35 +116,25 @@ namespace datalog {
     }
 
     void relation_manager::collect_non_empty_predicates(decl_set & res) const {
-        relation_map::iterator it = m_relations.begin();
-        relation_map::iterator end = m_relations.end();
-        for(; it!=end; ++it) {
-            if(!it->m_value->fast_empty()) {
-                res.insert(it->m_key);
+        for (auto const& kv : m_relations) {
+            if (!kv.m_value->fast_empty()) {
+                res.insert(kv.m_key);
             }
         }
     }
 
     void relation_manager::restrict_predicates(const decl_set & preds) {
-        typedef ptr_vector<func_decl> fd_vector;
-        fd_vector to_remove;
+        ptr_vector<func_decl> to_remove;
 
-        relation_map::iterator rit = m_relations.begin();
-        relation_map::iterator rend = m_relations.end();
-        for(; rit!=rend; ++rit) {
-            func_decl * pred = rit->m_key;
+        for (auto const& kv : m_relations) {
+            func_decl* pred = kv.m_key;
             if (!preds.contains(pred)) {
                 to_remove.insert(pred);
             }
         }
 
-        fd_vector::iterator pit = to_remove.begin();
-        fd_vector::iterator pend = to_remove.end();
-        for(; pit!=pend; ++pit) {
-            func_decl * pred = *pit;
-            relation_base * rel;
-            VERIFY( m_relations.find(pred, rel) );
-            rel->deallocate();
+        for (func_decl* pred : to_remove) {
+            m_relations.find(pred)->deallocate();
             m_relations.remove(pred);
             get_context().get_manager().dec_ref(pred);
         }
@@ -283,11 +270,9 @@ namespace datalog {
     }
 
     table_plugin * relation_manager::get_table_plugin(symbol const& k) {
-        table_plugin_vector::iterator tpit = m_table_plugins.begin();
-        table_plugin_vector::iterator tpend = m_table_plugins.end();
-        for(; tpit!=tpend; ++tpit) {
-            if((*tpit)->get_name()==k) {
-                return *tpit;
+        for (table_plugin * tp : m_table_plugins) {
+            if (tp->get_name()==k) {
+                return tp;
             }
         }
         return 0;
@@ -341,10 +326,9 @@ namespace datalog {
             return res;
         }
 
-        for (unsigned i = 0; i < m_relation_plugins.size(); ++i) {
-            p = m_relation_plugins[i];
-            if (p->can_handle_signature(s)) {
-                return p->mk_empty(s);
+        for (relation_plugin* p1 : m_relation_plugins) {
+            if (p1->can_handle_signature(s)) {
+                return p1->mk_empty(s);
             }
         }
 
diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
index 3c1d1b924..1ed847e89 100644
--- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
+++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
@@ -250,7 +250,7 @@ namespace datalog {
         bool detect_equivalences(expr_ref_vector& v, bool inside_disjunction)
         {
             bool have_pair = false;
-            unsigned prev_pair_idx;
+            unsigned prev_pair_idx = 0;
             arg_pair ap;
 
             unsigned read_idx = 0;
@@ -296,21 +296,20 @@ namespace datalog {
         br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, 
             proof_ref & result_pr)
         {
-
             if (m.is_not(f) && (m.is_and(args[0]) || m.is_or(args[0]))) {
-                SASSERT(num==1);
+                SASSERT(num == 1);
                 expr_ref tmp(m);
                 app* a = to_app(args[0]);
                 m_app_args.reset();
-                for (unsigned i = 0; i < a->get_num_args(); ++i) {
-                    m_brwr.mk_not(a->get_arg(i), tmp);
+                for (expr* arg : *a) {
+                    m_brwr.mk_not(arg, tmp);
                     m_app_args.push_back(tmp);
                 }
                 if (m.is_and(args[0])) {
-                    result = m.mk_or(m_app_args.size(), m_app_args.c_ptr());
+                    result = mk_or(m_app_args); 
                 }
                 else {
-                    result = m.mk_and(m_app_args.size(), m_app_args.c_ptr());
+                    result = mk_and(m_app_args); 
                 }
                 return BR_REWRITE2;
             }
diff --git a/src/test/old_interval.cpp b/src/test/old_interval.cpp
index 92064c03e..12a45555d 100644
--- a/src/test/old_interval.cpp
+++ b/src/test/old_interval.cpp
@@ -120,9 +120,9 @@ class interval_tester {
     
     interval singleton(int i) { return interval(m, rational(i)); }
     interval all() { return interval(m); }
-    interval l(int i, bool o = false, int idx = 0) { return interval(m, rational(i), o, true, idx == 0 ? 0 : m.mk_leaf(reinterpret_cast<void*>(idx))); }
-    interval r(int i, bool o = false, int idx = 0) { return interval(m, rational(i), o, false, idx == 0 ? 0 : m.mk_leaf(reinterpret_cast<void*>(idx))); }
-    interval b(int l, int u, bool lo = false, bool uo = false, int idx_l = 0, int idx_u = 0) {
+    interval l(int i, bool o = false, size_t idx = 0) { return interval(m, rational(i), o, true, idx == 0 ? 0 : m.mk_leaf(reinterpret_cast<void*>(idx))); }
+    interval r(int i, bool o = false, size_t idx = 0) { return interval(m, rational(i), o, false, idx == 0 ? 0 : m.mk_leaf(reinterpret_cast<void*>(idx))); }
+    interval b(int l, int u, bool lo = false, bool uo = false, size_t idx_l = 0, size_t idx_u = 0) {
         return interval(m, rational(l), lo, idx_l == 0 ? 0 : m.mk_leaf(reinterpret_cast<void*>(idx_l)), rational(u), uo, idx_u == 0 ? 0 : m.mk_leaf(reinterpret_cast<void*>(idx_u)));
     }
 
diff --git a/src/test/small_object_allocator.cpp b/src/test/small_object_allocator.cpp
index 1ecf865dd..5ae2836d0 100644
--- a/src/test/small_object_allocator.cpp
+++ b/src/test/small_object_allocator.cpp
@@ -36,5 +36,14 @@ void tst_small_object_allocator() {
     r3 = new (soa) char[1];
     TRACE("small_object_allocator", 
           tout << "r1: " << (void*)r1 << " r2: " << (void*)r2 << " r3: " << (void*)r3 << " r4: " << (void*)r4 << "\n";);
+    (void)r1;
+    (void)r2;
+    (void)r3;
+    (void)r4;
 
+    (void)q1;
+
+    (void)p1;
+    (void)p2;
+    (void)p3;
 }
diff --git a/src/test/sorting_network.cpp b/src/test/sorting_network.cpp
index 81340651a..87cc05375 100644
--- a/src/test/sorting_network.cpp
+++ b/src/test/sorting_network.cpp
@@ -364,15 +364,13 @@ void test_at_most_1(unsigned n, bool full) {
     for (unsigned i = 0; i < ext.m_clauses.size(); ++i) {
         solver.assert_expr(ext.m_clauses[i].get());
     }
-    lbool res;
     if (full) {
         solver.push();
         solver.assert_expr(m.mk_not(m.mk_eq(result1, result2)));
 
         std::cout << result1 << "\n";
 
-        res = solver.check();
-        SASSERT(res == l_false);
+        VERIFY(l_false == solver.check());
 
         solver.pop(1);
     }
@@ -390,8 +388,7 @@ void test_at_most_1(unsigned n, bool full) {
             std::cout << atom << "\n";
             if (is_true) ++k;
         }
-        res = solver.check();
-        SASSERT(res == l_true);
+        VERIFY(l_false == solver.check());
         if (k > 1) {
             solver.assert_expr(result1);
         }
@@ -402,8 +399,7 @@ void test_at_most_1(unsigned n, bool full) {
         else {
             solver.assert_expr(m.mk_not(result1));
         }
-        res = solver.check();
-        SASSERT(res == l_false);
+        VERIFY(l_false == solver.check());
         solver.pop(1);
     }
 }
diff --git a/src/test/substitution.cpp b/src/test/substitution.cpp
index cdc7f2080..5609225c6 100644
--- a/src/test/substitution.cpp
+++ b/src/test/substitution.cpp
@@ -35,6 +35,8 @@ void tst_substitution()
 
     bool ok1 = unif(v1.get(), v2.get(), subst, false);
     bool ok2 = unif(v2.get(), v1.get(), subst, false);
+    (void)ok1;
+    (void)ok2;
 
     expr_ref res(m);
 
diff --git a/src/util/total_order.h b/src/util/total_order.h
index 7238a5ef9..6fda88110 100644
--- a/src/util/total_order.h
+++ b/src/util/total_order.h
@@ -79,12 +79,7 @@ class total_order {
     }
     
     cell * to_cell(T const & a) const {
-        void * r;
-#ifdef Z3DEBUG
-        bool ok =
-#endif
-        m_map.find(a, r);
-        SASSERT(ok);
+        void * r = m_map.find(a);
         return reinterpret_cast<cell*>(r);
     }
 
diff --git a/src/util/uint_map.h b/src/util/uint_map.h
index 13e0a9db3..0344de322 100644
--- a/src/util/uint_map.h
+++ b/src/util/uint_map.h
@@ -38,6 +38,11 @@ public:
             return v != 0;
         }
     }
+    
+    T * find(unsigned k) const { 
+        SASSERT(k < m_map.size() && m_map[k] != 0); 
+        return m_map[k]; 
+    }
 
     void insert(unsigned k, T * v) {
         m_map.reserve(k+1);