diff --git a/src/duality/duality.h b/src/duality/duality.h
index fc70ffa70..4005adc1a 100644
--- 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 ff3bc190b..c10d83603 100644
--- 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 = static_cast<int>(stack.size() * 0.1);
 	      expand_max = std::max(1,thing);
 	      if(expand_max > 1)
 		std::cout << "foo!\n";
diff --git a/src/opt/pb_sls.cpp b/src/opt/pb_sls.cpp
index f04301c06..29d814a43 100644
--- a/src/opt/pb_sls.cpp
+++ b/src/opt/pb_sls.cpp
@@ -623,6 +623,9 @@ namespace smt {
                 m_orig_clauses.push_back(f);
                 return result;
             }            
+            if (pb.is_ge(f)) {
+                
+            }
             IF_VERBOSE(0, verbose_stream() << "not handled: " << mk_pp(f, m) << "\n";);
             return mk_aux_literal(f);
         }