diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 5f92b4d94..c23de3bfa 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -2155,15 +2155,15 @@ void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * arg
     SASSERT(f->get_num_parameters() == 1);
     SASSERT(f->get_parameter(0).is_int());
     
-    unsigned ebits = m_util.get_ebits(f->get_range());
-    unsigned sbits = m_util.get_sbits(f->get_range());
-    int width = f->get_parameter(0).get_int();
+    //unsigned ebits = m_util.get_ebits(f->get_range());
+    //unsigned sbits = m_util.get_sbits(f->get_range());
+    //int width = f->get_parameter(0).get_int();
 
-    expr * rm = args[0];
-    expr * x = args[1];
+    //expr * rm = args[0];
+    //expr * x = args[1];
     
-    expr * sgn, *s, *e;
-    split(x, sgn, s, e);
+    //expr * sgn, *s, *e;
+    //split(x, sgn, s, e);
 
     NOT_IMPLEMENTED_YET();
 }
@@ -2173,15 +2173,15 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
     SASSERT(f->get_num_parameters() == 1);
     SASSERT(f->get_parameter(0).is_int());
 
-    unsigned ebits = m_util.get_ebits(f->get_range());
-    unsigned sbits = m_util.get_sbits(f->get_range());
-    int width = f->get_parameter(0).get_int();
+    //unsigned ebits = m_util.get_ebits(f->get_range());
+    //unsigned sbits = m_util.get_sbits(f->get_range());
+    //int width = f->get_parameter(0).get_int();
 
-    expr * rm = args[0];
-    expr * x = args[1];
+    //expr * rm = args[0];
+    //expr * x = args[1];
 
-    expr * sgn, *s, *e;
-    split(x, sgn, s, e);
+    //expr * sgn, *s, *e;
+    //split(x, sgn, s, e);
 
     NOT_IMPLEMENTED_YET();
 }
@@ -2189,15 +2189,15 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
 void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 1);
 
-    unsigned ebits = m_util.get_ebits(f->get_range());
-    unsigned sbits = m_util.get_sbits(f->get_range());
-    int width = f->get_parameter(0).get_int();
+    //unsigned ebits = m_util.get_ebits(f->get_range());
+    //unsigned sbits = m_util.get_sbits(f->get_range());
+    //int width = f->get_parameter(0).get_int();
 
-    expr * rm = args[0];
-    expr * x = args[1];
+    //expr * rm = args[0];
+    //expr * x = args[1];
 
-    expr * sgn, *s, *e;
-    split(x, sgn, s, e);
+    //expr * sgn, *s, *e;
+    //split(x, sgn, s, e);
 
     NOT_IMPLEMENTED_YET();
 }
diff --git a/src/interp/iz3base.h b/src/interp/iz3base.h
index bca9b8518..956191290 100755
--- a/src/interp/iz3base.h
+++ b/src/interp/iz3base.h
@@ -161,7 +161,7 @@ class iz3base : public iz3mgr, public scopes {
   stl_ext::hash_map<ast,ast> simplify_memo;
   stl_ext::hash_map<ast,int> frame_map;                      // map assertions to frames
 
-  int frames;                               // number of frames
+  // int frames;                               // number of frames
 
  protected:
   void add_frame_range(int frame, ast t);
diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp
index 52ddcd64f..b487b2892 100755
--- a/src/interp/iz3proof_itp.cpp
+++ b/src/interp/iz3proof_itp.cpp
@@ -2747,7 +2747,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
     ast orig_e = e;
     pf = make_refl(e);  // proof that e = e
 
-    prover::range erng = pv->ast_scope(e);
+    // prover::range erng = 
+    pv->ast_scope(e);
 #if 0
     if(!(erng.lo > erng.hi) && pv->ranges_intersect(pv->ast_scope(e),rng)){
       return e; // this term occurs in range, so it's O.K.