diff --git a/src/opt/bcd2.cpp b/src/opt/bcd2.cpp
index 5d5fa2f7c..779654e7e 100644
--- a/src/opt/bcd2.cpp
+++ b/src/opt/bcd2.cpp
@@ -398,7 +398,7 @@ namespace opt {
         }
     };
 
-    maxsmt_solver_base* opt::mk_bcd2(
+    maxsmt_solver_base* mk_bcd2(
         context& c, weights_t& ws, expr_ref_vector const& soft) {
         return alloc(bcd2, c, ws, soft);
     }
diff --git a/src/opt/hitting_sets.cpp b/src/opt/hitting_sets.cpp
index c3436f61d..37b800428 100644
--- a/src/opt/hitting_sets.cpp
+++ b/src/opt/hitting_sets.cpp
@@ -541,7 +541,7 @@ namespace opt {
             VERIFY(l_true == m_simplex.minimize(m_weights_var));
             mpq_inf const& val = m_simplex.get_value(m_weights_var);
             unsynch_mpq_inf_manager mg;
-            unsynch_mpq_manager& mq = mg.mpq_manager();
+            unsynch_mpq_manager& mq = mg.get_mpq_manager();
             scoped_mpq c(mq);
             mg.ceil(val, c);
             rational w(c);
diff --git a/src/util/mpq_inf.h b/src/util/mpq_inf.h
index d7202a79a..640c827ae 100644
--- a/src/util/mpq_inf.h
+++ b/src/util/mpq_inf.h
@@ -276,7 +276,7 @@ public:
         out << to_string(a);
     }
 
-    mpq_manager<SYNCH>& mpq_manager() { return m; }
+    mpq_manager<SYNCH>& get_mpq_manager() { return m; }
 };
 
 typedef mpq_inf_manager<true>  synch_mpq_inf_manager;