diff --git a/src/interp/iz3foci.cpp b/src/interp/iz3foci.cpp
index 31d8b56c7..0317a9834 100755
--- a/src/interp/iz3foci.cpp
+++ b/src/interp/iz3foci.cpp
@@ -73,9 +73,9 @@ public:
   // create a symbol corresponding to a DeBruijn index of a particular type
   // the type has to be encoded into the name because the same index can
   // occur with different types
-  foci2::symb make_deBruijn_symbol(int index, int type){
+  foci2::symb make_deBruijn_symbol(int index, type ty){
     std::ostringstream s;
-    s << "#" << index << "#" << type;
+    // s << "#" << index << "#" << type;
     return foci->mk_func(s.str());
   }
 
@@ -181,7 +181,7 @@ public:
       case Variable: {  // a deBruijn index
         int index = get_variable_index_value(t);
 	type ty = get_type(t);
-        foci2::symb symbol = make_deBruijn_symbol(index,(int)(ty));
+        foci2::symb symbol = make_deBruijn_symbol(index,ty);
         res = foci->mk_app(symbol,std::vector<foci2::ast>());
       }
       default:
diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp
index b1f07f5ce..83ec1578a 100644
--- a/src/interp/iz3mgr.cpp
+++ b/src/interp/iz3mgr.cpp
@@ -264,8 +264,8 @@ void iz3mgr::pretty_print(std::ostream &f, const std::string &s){
 	col = indent;
 	continue;
       }
-      unsigned paren = s.find('(',pos);
-      if(paren != std::string::npos){
+      int paren = s.find('(',pos);
+      if(paren != (int)std::string::npos){
 	int chars = paren - pos + 1;
 	f << s.substr(pos,chars);
 	indent += pretty_indent_chars;