diff --git a/src/muz_qe/hilbert_basis.cpp b/src/muz_qe/hilbert_basis.cpp
index bc31572ea..dd0041fa9 100644
--- a/src/muz_qe/hilbert_basis.cpp
+++ b/src/muz_qe/hilbert_basis.cpp
@@ -63,7 +63,7 @@ public:
         for (; it != end; ++it) {
             offset_t offs(*it);
             ++m_stats.m_num_comparisons;
-            if (*it != idx.m_offset && hb.is_subsumed(idx, offs)) {
+            if (*it != static_cast<int>(idx.m_offset) && hb.is_subsumed(idx, offs)) {
                 found_idx = offs;
                 ++m_stats.m_num_hit;
                 return true;
@@ -743,7 +743,7 @@ hilbert_basis::sign_t hilbert_basis::get_sign(offset_t idx) const {
     return zero;
 }
 
-hilbert_basis::numeral hilbert_basis::get_weight(values& val, num_vector const& ineq) const {
+hilbert_basis::numeral hilbert_basis::get_weight(values const & val, num_vector const& ineq) const {
     numeral result(0);
     unsigned num_vars = get_num_vars();
     for (unsigned i = 0; i < num_vars; ++i) {
@@ -753,7 +753,6 @@ hilbert_basis::numeral hilbert_basis::get_weight(values& val, num_vector const&
 }
 
 void hilbert_basis::display(std::ostream& out) const {
-    unsigned nv = get_num_vars();
     out << "inequalities:\n";
     for (unsigned i = 0; i < m_ineqs.size(); ++i) {
         display_ineq(out, m_ineqs[i], m_iseq[i]);
diff --git a/src/muz_qe/hilbert_basis.h b/src/muz_qe/hilbert_basis.h
index 00b854271..8dd5e97cf 100644
--- a/src/muz_qe/hilbert_basis.h
+++ b/src/muz_qe/hilbert_basis.h
@@ -96,7 +96,7 @@ private:
 
     void add_unit_vector(unsigned i, numeral const& e);
     unsigned get_num_vars() const;
-    numeral get_weight(values& val, num_vector const& ineq) const;
+    numeral get_weight(values const & val, num_vector const& ineq) const;
     bool is_geq(values const& v, values const& w) const;
     bool is_abs_geq(numeral const& v, numeral const& w) const;
     bool is_subsumed(offset_t idx);