diff --git a/src/cmd_context/interpolant_cmds.cpp b/src/cmd_context/interpolant_cmds.cpp
index 2a7de3176..318569cd5 100644
--- a/src/cmd_context/interpolant_cmds.cpp
+++ b/src/cmd_context/interpolant_cmds.cpp
@@ -139,10 +139,11 @@ static void get_interpolant(cmd_context & ctx, expr * t, params_ref &m_params) {
   get_interpolant_and_maybe_check(ctx,t,m_params,false);
 }
 
+#if 0
 static void get_and_check_interpolant(cmd_context & ctx, params_ref &m_params, expr * t) {
   get_interpolant_and_maybe_check(ctx,t,m_params,true);
 }
-
+#endif
 
 static void compute_interpolant_and_maybe_check(cmd_context & ctx, expr * t, params_ref &m_params, bool check){
     
diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp
index ad89c1314..17b93d35b 100644
--- a/src/duality/duality_rpfp.cpp
+++ b/src/duality/duality_rpfp.cpp
@@ -3661,7 +3661,7 @@ namespace Duality {
 	for(unsigned j = 0; j < outs.size(); j++)
 	  for(unsigned k = 0; k < outs[j]->Children.size(); k++)
 	    chs.push_back(outs[j]->Children[k]);
-	Edge *fedge = CreateEdge(node,tr,chs);
+	CreateEdge(node,tr,chs);
 	for(unsigned j = 0; j < outs.size(); j++)
 	  edges_to_delete.insert(outs[j]);
       }
diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp
index 4b7d47e0f..0ce3297af 100755
--- a/src/interp/iz3translate_direct.cpp
+++ b/src/interp/iz3translate_direct.cpp
@@ -58,7 +58,9 @@ namespace stl_ext {
 
 
 static int lemma_count = 0;
+#if 0
 static int nll_lemma_count = 0;
+#endif
 #define SHOW_LEMMA_COUNT -1
 
 // One half of a resolution. We need this to distinguish