diff --git a/src/muz_qe/dl_mk_karr_invariants.cpp b/src/muz_qe/dl_mk_karr_invariants.cpp
index 18b152589..d44b31979 100644
--- a/src/muz_qe/dl_mk_karr_invariants.cpp
+++ b/src/muz_qe/dl_mk_karr_invariants.cpp
@@ -11,7 +11,7 @@ Abstract:
 
     The linear invariants are extracted according to Karr's method.
     A short description is in 
-    Nikolaj Bjørner, Anca Browne and Zohar Manna. Automatic Generation 
+    Nikolaj Bjorner, Anca Browne and Zohar Manna. Automatic Generation 
     of Invariants and Intermediate Assertions, in CP 95.
 
     The algorithm is here adapted to Horn clauses.
diff --git a/src/muz_qe/hnf.cpp b/src/muz_qe/hnf.cpp
index 88e28699e..47370e0e6 100644
--- a/src/muz_qe/hnf.cpp
+++ b/src/muz_qe/hnf.cpp
@@ -353,7 +353,8 @@ private:
 
     void eliminate_disjunctions(expr_ref_vector& body, proof_ref_vector& proofs) {
         for (unsigned i = 0; i < body.size(); ++i) {
-            eliminate_disjunctions(body[i], proofs);
+            expr_ref_vector::element_ref r = body[i];
+            eliminate_disjunctions(r, proofs);
         }
     }
 
@@ -378,7 +379,8 @@ private:
 
     void eliminate_quantifier_body(expr_ref_vector& body, proof_ref_vector& proofs) {
         for (unsigned i = 0; i < body.size(); ++i) {
-            eliminate_quantifier_body(body[i], proofs);
+            expr_ref_vector::element_ref r = body[i];
+            eliminate_quantifier_body(r, proofs);
         }
     }
 
diff --git a/src/util/bit_vector.cpp b/src/util/bit_vector.cpp
index 3b470a3ce..a24774279 100644
--- a/src/util/bit_vector.cpp
+++ b/src/util/bit_vector.cpp
@@ -16,7 +16,7 @@ Author:
 Revision History:
 
 --*/
-
+#include<limits.h>
 #include"bit_vector.h"
 #include"util.h"
 #include"trace.h"