diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index 3c2173a76..1735f2337 100644
--- a/azure-pipelines.yml
+++ b/azure-pipelines.yml
@@ -214,7 +214,7 @@ jobs:
 - job: "MacOSPython"
   displayName: "MacOS build"
   pool:
-    vmImage: "macOS-10.14"
+    vmImage: "macOS-latest"
   steps:
     - script: python scripts/mk_make.py -d --java --dotnet
     - script: |
@@ -244,7 +244,7 @@ jobs:
         set -e
         mkdir build
         cd build
-        CC=clang CXX=clang++ cmake -DJlCxx_DIR=$JlCxxDir $(cmakeJulia) $(cmakeJava) $(cmakePy) -DZ3_BUILD_DOTNET_BINDINGS=False -G "Ninja" ../
+        cmake -DJlCxx_DIR=$JlCxxDir $(cmakeJulia) $(cmakeJava) $(cmakePy) -DZ3_BUILD_DOTNET_BINDINGS=False -G "Ninja" ../
         ninja
         ninja test-z3
         cd ..
diff --git a/src/model/char_factory.h b/src/model/char_factory.h
index 0e99ecd79..55baad26d 100644
--- a/src/model/char_factory.h
+++ b/src/model/char_factory.h
@@ -20,9 +20,8 @@ Revision History:
 #include "model/model_core.h"
 #include "model/value_factory.h"
 
-class char_factory : public value_factory {
+class char_factory final : public value_factory {
     model_core&  m_model;
-    ast_manager& m;
     seq_util     u;
     uint_set     m_chars;
     unsigned     m_next { 'A' };
@@ -33,7 +32,6 @@ public:
     char_factory(ast_manager & m, family_id fid, model_core& md):
         value_factory(m, fid),
         m_model(md),
-        m(m),
         u(m),
         m_trail(m)
     {
@@ -76,4 +74,3 @@ public:
     }    
 
 };
-
diff --git a/src/model/seq_factory.h b/src/model/seq_factory.h
index ce395cef5..d40a7f7bd 100644
--- a/src/model/seq_factory.h
+++ b/src/model/seq_factory.h
@@ -19,7 +19,6 @@ Author:
 class seq_factory : public value_factory {
     typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> symbol_set;
     model_core& m_model;
-    ast_manager& m;
     seq_util     u;
     symbol_set   m_strings;
     unsigned     m_next;
@@ -31,7 +30,6 @@ public:
     seq_factory(ast_manager & m, family_id fid, model_core& md):
         value_factory(m, fid),
         m_model(md),
-        m(m),
         u(m),
         m_next(0),
         m_unique_delim("!"),
@@ -151,4 +149,3 @@ private:
                 goto try_again;
     }
 };
-
diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp
index 589540b6f..dea02d533 100644
--- a/src/muz/rel/dl_compiler.cpp
+++ b/src/muz/rel/dl_compiler.cpp
@@ -868,7 +868,6 @@ namespace datalog {
                                                     bool & dealloc, instruction_block & acc) {
         uint_set pos_vars;
         u_map<expr*> neg_vars;
-        ast_manager& m = m_context.get_manager();
         unsigned pt_len = r->get_positive_tail_size();
         unsigned ut_len = r->get_uninterpreted_tail_size();
 
@@ -903,7 +902,7 @@ namespace datalog {
             if (!pos_vars.contains(v)) {
                 single_res_expr.push_back(e);
                 make_add_unbound_column(r, v, pred, single_res, e->get_sort(), single_res, dealloc, acc);
-                TRACE("dl", tout << "Adding unbound column: " << mk_pp(e, m) << "\n";);
+                TRACE("dl", tout << "Adding unbound column: " << mk_pp(e, m_context.get_manager()) << "\n";);
             }
         }
     }
diff --git a/src/smt/theory_char.h b/src/smt/theory_char.h
index 146d522e4..cd37732b8 100644
--- a/src/smt/theory_char.h
+++ b/src/smt/theory_char.h
@@ -38,7 +38,6 @@ namespace smt {
         vector<expr_ref_vector> m_ebits;
         unsigned_vector         m_var2value;
         svector<theory_var>     m_value2var;
-        bool                    m_enabled { false };
         bit_blaster             m_bb;
         stats                   m_stats;
         symbol                  m_bits2char;
diff --git a/src/tactic/core/symmetry_reduce_tactic.cpp b/src/tactic/core/symmetry_reduce_tactic.cpp
index aa19428d6..6f215e922 100644
--- a/src/tactic/core/symmetry_reduce_tactic.cpp
+++ b/src/tactic/core/symmetry_reduce_tactic.cpp
@@ -248,14 +248,12 @@ private:
     }
 
     class sort_colors {
-        ast_manager& m_manager;
         app_map& m_app2sortid;
         obj_map<sort,unsigned>  m_sort2id;
         unsigned m_max_id;
 
     public:
-        sort_colors(ast_manager& m, app_map& app2sort): 
-          m_manager(m), m_app2sortid(app2sort), m_max_id(0) {}
+        sort_colors(app_map& app2sort) : m_app2sortid(app2sort), m_max_id(0) {}
 
         void operator()(app* n) {
             sort* s = n->get_sort();
@@ -273,7 +271,7 @@ private:
 
     void compute_sort_colors(expr* fml, app_map& app2sortId) {
         app2sortId.reset();
-        sort_colors sc(m(), app2sortId);
+        sort_colors sc(app2sortId);
         for_each_expr(sc, fml);
     }