diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 387e5d6f2..89840ea43 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -1475,9 +1475,7 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
         return BR_DONE;
     }
     if (m_util.re.is_full_char(a)) {
-        sort* seq_sort = nullptr;
-        VERIFY(m_util.is_re(a, seq_sort));
-        result = m_util.re.mk_full_seq(seq_sort);
+        result = m_util.re.mk_full_seq(m().get_sort(a));
         return BR_DONE;
     }
     if (m_util.re.is_empty(a)) {
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 91aeeac3b..c9dbc78f8 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -671,9 +671,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
 
     case _OP_REGEXP_FULL_CHAR:
-        if (!range) {
-            range = m_re;
-        }
+        if (!range) range = m_re;
         match(*m_sigs[k], arity, domain, range, rng);
         return m.mk_func_decl(symbol("re.allchar"), arity, domain, rng, func_decl_info(m_family_id, OP_RE_FULL_CHAR_SET));
 
@@ -690,9 +688,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, range, func_decl_info(m_family_id, k));        
 
     case _OP_REGEXP_EMPTY:
-        if (!range) {
-            range = m_re;
-        }
+        if (!range) range = m_re;
         match(*m_sigs[k], arity, domain, range, rng);
         return m.mk_func_decl(symbol("re.nostr"), arity, domain, rng, func_decl_info(m_family_id, OP_RE_EMPTY_SET));
 
diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index 971ec9193..29d01d1f3 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -1736,6 +1736,7 @@ namespace pdr {
     }
 
     void context::validate_model() {
+        IF_VERBOSE(1, verbose_stream() << "(pdr.validate_model)\n";);
         std::stringstream msg;
         expr_ref_vector refs(m);
         expr_ref tmp(m);
@@ -1745,11 +1746,10 @@ namespace pdr {
         get_level_property(m_inductive_lvl, refs, rs);
         inductive_property ex(m, mc, rs);
         ex.to_model(model);
-        decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
         var_subst vs(m, false);
         expr_free_vars fv;
-        for (; it != end; ++it) {
-            ptr_vector<datalog::rule> const& rules = it->m_value->rules();
+        for (auto const& kv : m_rels) {
+            ptr_vector<datalog::rule> const& rules = kv.m_value->rules();
             for (unsigned i = 0; i < rules.size(); ++i) {
                 datalog::rule& r = *rules[i];
                 model->eval(r.get_head(), tmp);
@@ -1916,7 +1916,7 @@ namespace pdr {
                     verbose_stream() << ex.to_string();
                 });
 
-            // upgrade invariants that are known to be inductive.
+            // upgrade invariants that are known to be inductive.            
             decl2rel::iterator it = m_rels.begin (), end = m_rels.end ();
             for (; m_inductive_lvl > 0 && it != end; ++it) {
                 if (it->m_value->head() != m_query_pred) {
diff --git a/src/util/lp/dense_matrix.h b/src/util/lp/dense_matrix.h
index 6b157ffd4..31b6617ac 100644
--- a/src/util/lp/dense_matrix.h
+++ b/src/util/lp/dense_matrix.h
@@ -79,8 +79,8 @@ public:
 
     void apply_from_left_to_X(vector<X> & w, lp_settings & );
 
-    virtual void set_number_of_rows(unsigned /*m*/) {}
-    virtual void set_number_of_columns(unsigned /*n*/) { }
+    void set_number_of_rows(unsigned /*m*/) override {}
+    void set_number_of_columns(unsigned /*n*/) override {}
 
     T get_elem(unsigned i, unsigned j) const { return m_values[i * m_n + j]; }
 
diff --git a/src/util/lp/lu.h b/src/util/lp/lu.h
index f9432c323..2f9a5ec38 100644
--- a/src/util/lp/lu.h
+++ b/src/util/lp/lu.h
@@ -74,8 +74,8 @@ public:
 #ifdef Z3DEBUG
     unsigned m_m;
     unsigned m_n;
-    virtual void set_number_of_rows(unsigned m) { m_m = m; m_n = m; }
-    virtual void set_number_of_columns(unsigned n) { m_m = n; m_n = n; }
+    void set_number_of_rows(unsigned m) override { m_m = m; m_n = m; }
+    void set_number_of_columns(unsigned n) override { m_m = n; m_n = n; }
     T m_one_over_val;
 
     T get_elem (unsigned i, unsigned j) const;
diff --git a/src/util/lp/sparse_matrix.h b/src/util/lp/sparse_matrix.h
index 400f2bfc0..7649e0983 100644
--- a/src/util/lp/sparse_matrix.h
+++ b/src/util/lp/sparse_matrix.h
@@ -305,8 +305,8 @@ public:
     T get_elem(unsigned i, unsigned j) const { return get(i, j); }
     unsigned get_number_of_rows() const { return dimension(); }
     unsigned get_number_of_columns() const { return dimension(); }
-    virtual void set_number_of_rows(unsigned /*m*/) { }
-    virtual void set_number_of_columns(unsigned /*n*/) { }
+    void set_number_of_rows(unsigned /*m*/) override { }
+    void set_number_of_columns(unsigned /*n*/) override { }
 #endif
     template <typename L>
     L dot_product_with_row (unsigned row, const vector<L> & y) const;