diff --git a/src/duality/duality.h b/src/duality/duality.h
index fe86ed2ec..aa147d93e 100755
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@@ -29,7 +29,7 @@ using namespace stl_ext;
 
 namespace Duality {
 
-  class implicant_solver;
+  struct implicant_solver;
 
   /* Generic operations on Z3 formulas */
 
diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp
index a47e90f95..dc261a351 100755
--- a/src/duality/duality_solver.cpp
+++ b/src/duality/duality_solver.cpp
@@ -2201,7 +2201,7 @@ namespace Duality {
 #endif
 	    int expand_max = 1;
 	    if(0&&duality->BatchExpand){
-	      int thing = stack.size() * 0.1;
+                int thing = stack.size() /10; 
 	      expand_max = std::max(1,thing);
 	      if(expand_max > 1)
 		std::cout << "foo!\n";
diff --git a/src/interp/iz3hash.h b/src/interp/iz3hash.h
index 355c03817..02c533c85 100644
--- a/src/interp/iz3hash.h
+++ b/src/interp/iz3hash.h
@@ -52,7 +52,7 @@ namespace hash_space {
     class hash<std::string> {
   public:
     size_t operator()(const std::string &s) const {
-      return string_hash(s.c_str(), s.size(), 0);
+        return string_hash(s.c_str(), static_cast<unsigned>(s.size()), 0);
     }
   };
 
@@ -107,7 +107,7 @@ namespace hash_space {
       4294967291ul
     };
 
-  inline unsigned long next_prime(unsigned long n) {
+  inline size_t next_prime(size_t n) {
     const unsigned long* to = primes + (int)num_primes;
     for(const unsigned long* p = primes; p < to; p++)
       if(*p >= n) return *p;