diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 745aa5da5..2bdaf66c5 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -260,7 +260,7 @@ namespace smt {
         struct var_value_hash {
             imp & m_th;
             var_value_hash(imp & th):m_th(th) {}
-            unsigned operator()(theory_var v) const { return std::hash<lean::impq>()(m_th.get_ivalue(v)); }
+            unsigned operator()(theory_var v) const { return (unsigned)std::hash<lean::impq>()(m_th.get_ivalue(v)); }
         };
         int_hashtable<var_value_hash, var_value_eq>   m_model_eqs;
 
@@ -1307,7 +1307,7 @@ namespace smt {
                 set_conflict();
             }
             else {
-                for (size_t i = 0; !m.canceled() && !ctx().inconsistent() && i < bp.m_ibounds.size(); ++i) {
+                for (unsigned i = 0; !m.canceled() && !ctx().inconsistent() && i < bp.m_ibounds.size(); ++i) {
                     propagate_lp_solver_bound(bp.m_ibounds[i]);
                 }
             }
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 1fe5c6ca1..3c10e7626 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -43,7 +43,7 @@ struct conversion_helper {
 
 template<>
 struct conversion_helper <double> {
-    static double conversion_helper <double>::get_upper_bound(const column_info<mpq> & ci) {
+    static double get_upper_bound(const column_info<mpq> & ci) {
         if (!ci.upper_bound_is_strict())
             return ci.get_upper_bound().get_double();
         double eps = 0.00001;