diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index d303b477d..fbe112e4c 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -7453,7 +7453,7 @@ def WithParams(t, p):
     >>> x, y = Ints('x y')
     >>> p = ParamsRef()
     >>> p.set("som", True)
-    >>> t = With(Tactic('simplify'), p)
+    >>> t = WithParams(Tactic('simplify'), p)
     >>> t((x + 1)*(y + 2) == 0)
     [[2*x + y + x*y == -2]]
     """
diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp
index 4088d607c..b1f222f6e 100644
--- a/src/muz/transforms/dl_mk_rule_inliner.cpp
+++ b/src/muz/transforms/dl_mk_rule_inliner.cpp
@@ -210,8 +210,7 @@ namespace datalog {
         }
 
         rule_set::iterator rend = orig.end();
-        for (rule_set::iterator rit = orig.begin(); rit!=rend; ++rit) {
-            rule * r = *rit;
+        for (rule * r : orig) {
             func_decl * head_pred = r->get_decl();
             m_head_pred_ctr.inc(head_pred);
 
@@ -283,9 +282,7 @@ namespace datalog {
         
         const rule_stratifier::comp_vector& comps = r.get_stratifier().get_strats();
 
-        rule_stratifier::comp_vector::const_iterator cend = comps.end();
-        for (rule_stratifier::comp_vector::const_iterator it = comps.begin(); it!=cend; ++it) {
-            rule_stratifier::item_set * stratum = *it;
+        for (rule_stratifier::item_set * stratum : comps) {
             if (stratum->size()==1) {
                 continue;
             }
@@ -307,9 +304,7 @@ namespace datalog {
         const rule_stratifier::comp_vector& comps = 
             proposed_inlined_rules.get_stratifier().get_strats();
 
-        rule_stratifier::comp_vector::const_iterator cend = comps.end();
-        for (rule_stratifier::comp_vector::const_iterator it = comps.begin(); it!=cend; ++it) {
-            rule_stratifier::item_set * stratum = *it;
+        for (rule_stratifier::item_set * stratum : comps) {
 
             SASSERT(stratum->size()==1);
             func_decl * head_pred = *stratum->begin();
@@ -318,10 +313,7 @@ namespace datalog {
             bool is_multi_occurrence_pred = m_tail_pred_ctr.get(head_pred)>1;
 
             const rule_vector& pred_rules = proposed_inlined_rules.get_predicate_rules(head_pred);
-            rule_vector::const_iterator iend = pred_rules.end();
-            for (rule_vector::const_iterator iit = pred_rules.begin(); iit!=iend; ++iit) {
-                rule * r = *iit;
-
+            for (rule * r : pred_rules) {
                 unsigned pt_len = r->get_positive_tail_size();
                 for (unsigned ti = 0; ti<pt_len; ++ti) {
                     func_decl * tail_pred = r->get_decl(ti);
@@ -409,7 +401,6 @@ namespace datalog {
 
         const rule_stratifier::comp_vector& comps = candidate_inlined_set->get_stratifier().get_strats();
 
-        rule_stratifier::comp_vector::const_iterator cend = comps.end();
         for (rule_stratifier::item_set * stratum : comps) {
             SASSERT(stratum->size()==1);
             func_decl * pred = *stratum->begin();
diff --git a/src/util/lp/permutation_matrix.h b/src/util/lp/permutation_matrix.h
index f080d45b9..3c89b3646 100644
--- a/src/util/lp/permutation_matrix.h
+++ b/src/util/lp/permutation_matrix.h
@@ -109,13 +109,13 @@ class permutation_matrix : public tail_matrix<T, X> {
 
         void transpose_from_right(unsigned i, unsigned j);
 #ifdef Z3DEBUG
-        T get_elem(unsigned i, unsigned j) const{
+        T get_elem(unsigned i, unsigned j) const override {
             return m_permutation[i] == j? numeric_traits<T>::one() : numeric_traits<T>::zero();
         }
-        unsigned row_count() const{ return size(); }
-        unsigned column_count() const { return size(); }
-        virtual void set_number_of_rows(unsigned /*m*/) { }
-        virtual void set_number_of_columns(unsigned /*n*/) { }
+        unsigned row_count() const override { return size(); }
+        unsigned column_count() const override { return size(); }
+        void set_number_of_rows(unsigned /*m*/) override { }
+        void set_number_of_columns(unsigned /*n*/) override { }
 #endif
         void multiply_by_permutation_from_left(permutation_matrix<T, X> & p);