diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index f79a65705..aa415d187 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -324,7 +324,7 @@ namespace datalog {
         m_bind_variables.add_var(m.mk_const(var));
     }
 
-    expr_ref context::bind_variables(expr* fml, bool is_forall) {
+    expr_ref context::bind_vars(expr* fml, bool is_forall) {
         return m_bind_variables(fml, is_forall);
     }
 
@@ -1078,7 +1078,7 @@ namespace datalog {
    
     void context::get_raw_rule_formulas(expr_ref_vector& rules, svector<symbol>& names){
         for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
-	  expr_ref r = bind_variables(m_rule_fmls[i].get(), true);
+	  expr_ref r = bind_vars(m_rule_fmls[i].get(), true);
 	  rules.push_back(r.get());
 	  //            rules.push_back(m_rule_fmls[i].get());
 	  names.push_back(m_rule_names[i]);
diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index 85d4b7c0e..e96752721 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -287,7 +287,7 @@ namespace datalog {
           universal (if is_forall is true) or existential 
           quantifier.
          */
-        expr_ref bind_variables(expr* fml, bool is_forall);
+        expr_ref bind_vars(expr* fml, bool is_forall);
 
         /**
            Register datalog relation.
diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp
index 2015d4eea..c4a14845d 100644
--- a/src/muz/base/dl_rule.cpp
+++ b/src/muz/base/dl_rule.cpp
@@ -370,7 +370,7 @@ namespace datalog {
     }
 
     void rule_manager::bind_variables(expr* fml, bool is_forall, expr_ref& result) {
-        result = m_ctx.bind_variables(fml, is_forall);
+        result = m_ctx.bind_vars(fml, is_forall);
     }
 
     void rule_manager::flatten_body(app_ref_vector& body) {
diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp
index 9807cec4a..bb9a1bc10 100644
--- a/src/muz/fp/dl_cmds.cpp
+++ b/src/muz/fp/dl_cmds.cpp
@@ -103,7 +103,7 @@ struct dl_context {
     void add_rule(expr * rule, symbol const& name) {
         init();
         if (m_collected_cmds) {
-            expr_ref rl = m_context->bind_variables(rule, true);
+            expr_ref rl = m_context->bind_vars(rule, true);
             m_collected_cmds->m_rules.push_back(rl);
             m_collected_cmds->m_names.push_back(name);
             m_trail.push(push_back_vector<dl_context, expr_ref_vector>(m_collected_cmds->m_rules));
@@ -116,7 +116,7 @@ struct dl_context {
 
     bool collect_query(expr* q) {
         if (m_collected_cmds) {
-            expr_ref qr = m_context->bind_variables(q, false);
+            expr_ref qr = m_context->bind_vars(q, false);
             m_collected_cmds->m_queries.push_back(qr);
             m_trail.push(push_back_vector<dl_context, expr_ref_vector>(m_collected_cmds->m_queries));
             return true;
diff --git a/src/muz/rel/product_set.h b/src/muz/rel/product_set.h
index ebfe339fe..238a33d8a 100644
--- a/src/muz/rel/product_set.h
+++ b/src/muz/rel/product_set.h
@@ -248,7 +248,6 @@ namespace datalog {
 
 
     class product_set_factory {
-        friend class product_set_factory;
         unsigned char m_data[0];
     public:
         enum initial_t {
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 9dae2d0c4..d2e0c27a4 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -959,7 +959,7 @@ namespace smt {
             typename atoms::iterator hi_inf1 = begin2, hi_sup1 = begin2;
             bool flo_inf, fhi_inf, flo_sup, fhi_sup;
    //         std::cout << atoms.size() << "\n";
-            ptr_addr_hashtable<typename atom> visited;
+            ptr_addr_hashtable<atom> visited;
             for (unsigned i = 0; i < atoms.size(); ++i) {
                 atom* a1 = atoms[i];
                 lo_inf1 = next_inf(a1, A_LOWER, lo_inf, end, flo_inf);