diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp
index 00503566e..a1d874b4f 100644
--- a/src/api/api_interp.cpp
+++ b/src/api/api_interp.cpp
@@ -305,8 +305,8 @@ static void get_file_params(const char *filename, hash_map<std::string,std::stri
       tokenize(first_line.substr(2,first_line.size()-2),tokens);
       for(unsigned i = 0; i < tokens.size(); i++){
 	std::string &tok = tokens[i];
-	int eqpos = tok.find('=');
-	if(eqpos >= 0 && eqpos < (int)tok.size()){
+	size_t eqpos = tok.find('=');
+	if(eqpos >= 0 && eqpos < tok.size()){
 	  std::string left = tok.substr(0,eqpos);
 	  std::string right = tok.substr(eqpos+1,tok.size()-eqpos-1);
 	  params[left] = right;
@@ -363,8 +363,8 @@ extern "C" {
 #else
 
 
-  static Z3_ast and_vec(Z3_context ctx,std::vector<Z3_ast> &c){
-    return (c.size() > 1) ? Z3_mk_and(ctx,c.size(),&c[0]) : c[0];
+  static Z3_ast and_vec(Z3_context ctx,svector<Z3_ast> &c){
+      return (c.size() > 1) ? Z3_mk_and(ctx,c.size(),&c[0]) : c[0];
   }
   
   static Z3_ast parents_vector_to_tree(Z3_context ctx, int num, Z3_ast *cnsts, int *parents){
@@ -381,15 +381,15 @@ extern "C" {
       }
     }
     else {
-      std::vector<std::vector<Z3_ast> > chs(num);
+      std::vector<svector<Z3_ast> > chs(num);
       for(int i = 0; i < num-1; i++){
-	std::vector<Z3_ast> &c = chs[i];
+          svector<Z3_ast> &c = chs[i];
 	c.push_back(cnsts[i]);
 	Z3_ast foo = Z3_mk_interp(ctx,and_vec(ctx,c));
 	chs[parents[i]].push_back(foo);
       }
       {
-	std::vector<Z3_ast> &c = chs[num-1];
+	svector<Z3_ast> &c = chs[num-1];
 	c.push_back(cnsts[num-1]);
 	res = and_vec(ctx,c);
       }
@@ -454,7 +454,7 @@ extern "C" {
   static std::string read_msg;
   static std::vector<Z3_ast> read_theory;
 
-  static bool iZ3_parse(Z3_context ctx, const char *filename, const char **error, std::vector<Z3_ast> &assertions){
+  static bool iZ3_parse(Z3_context ctx, const char *filename, const char **error, svector<Z3_ast> &assertions){
     read_error.clear();
     try {
       std::string foo(filename);
@@ -496,26 +496,26 @@ extern "C" {
 
     hash_map<std::string,std::string> file_params;
     get_file_params(filename,file_params);
-
-    int num_theory = 0;
+    
+    unsigned num_theory = 0;
     if(file_params.find("THEORY") != file_params.end())
       num_theory = atoi(file_params["THEORY"].c_str());
 
-    std::vector<Z3_ast> assertions;
+    svector<Z3_ast> assertions;
     if(!iZ3_parse(ctx,filename,error,assertions))
       return false;
     
-    if(num_theory > (int)assertions.size())
-      num_theory = assertions.size();
-    int num = assertions.size() - num_theory;
+    if(num_theory > assertions.size())
+        num_theory = assertions.size();
+    unsigned num = assertions.size() - num_theory;
 
     read_cnsts.resize(num);
     read_parents.resize(num);
     read_theory.resize(num_theory);
 
-    for(int j = 0; j < num_theory; j++)
+    for(unsigned j = 0; j < num_theory; j++)
       read_theory[j] = assertions[j];
-    for(int j = 0; j < num; j++)
+    for(unsigned j = 0; j < num; j++)
       read_cnsts[j] = assertions[j+num_theory];
     
     if(ret_num_theory)
@@ -529,12 +529,12 @@ extern "C" {
       return true;
     }
 
-    for(int j = 0; j < num; j++)
+    for(unsigned j = 0; j < num; j++)
       read_parents[j] = SHRT_MAX;
     
     hash_map<Z3_ast,int> pred_map;
 
-    for(int j = 0; j < num; j++){
+    for(unsigned j = 0; j < num; j++){
       Z3_ast lhs = 0, rhs = read_cnsts[j];
 
       if(Z3_get_decl_kind(ctx,Z3_get_app_decl(ctx,Z3_to_app(ctx,rhs))) == Z3_OP_IMPLIES){
@@ -588,7 +588,7 @@ extern "C" {
       }
     }
 
-    for(int j = 0; j < num-1; j++)
+    for(unsigned j = 0; j < num-1; j++)
       if(read_parents[j] == SHRT_MIN){
 	read_error << "formula " << j+1 << ": unreferenced";
 	goto fail;
diff --git a/src/ast/proof_checker/proof_checker.cpp b/src/ast/proof_checker/proof_checker.cpp
index 85e0cc791..41c43b26c 100644
--- a/src/ast/proof_checker/proof_checker.cpp
+++ b/src/ast/proof_checker/proof_checker.cpp
@@ -479,7 +479,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
             // otherwise t2 is also a quantifier.
             return true;
         }
-        UNREACHABLE();
+        IF_VERBOSE(0, verbose_stream() << "does not match last rule: " << mk_pp(p, m) << "\n";);
         return false;
     }
     case PR_DER: {
@@ -488,13 +488,12 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
             match_fact(p, fact) &&
             match_iff(fact.get(), t1, t2) &&
             match_quantifier(t1, is_forall, decls1, body1) &&
-            is_forall &&
-            match_or(body1.get(), terms1)) {
+            is_forall) {
             // TBD: check that terms are set of equalities.
             // t2 is an instance of a predicate in terms1
             return true;
-        }
-        UNREACHABLE();
+        }        
+        IF_VERBOSE(0, verbose_stream() << "does not match last rule: " << mk_pp(p, m) << "\n";);
         return false;
     }
     case PR_HYPOTHESIS: {
@@ -832,7 +831,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
             }
             else {
                 IF_VERBOSE(0, verbose_stream() << "Could not establish complementarity for:\n" << 
-                           mk_pp(lit1, m) << "\n" << mk_pp(lit2, m) << "\n";);
+                           mk_pp(lit1, m) << "\n" << mk_pp(lit2, m) << "\n" << mk_pp(p, m) << "\n";);
             }
             fmls[i] = premise1;
         }
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index 9f77934e5..7593e9a52 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -475,10 +475,11 @@ namespace smt {
     bool theory_arith<Ext>::all_coeff_int(row const & r) const {
         typename vector<row_entry>::const_iterator it  = r.begin_entries();
         typename vector<row_entry>::const_iterator end = r.end_entries();
-        for (; it != end; ++it) {                                                                                   
-            if (!it->is_dead() && !it->m_coeff.is_int())
+        for (; it != end; ++it) {                                                                 
+            if (!it->is_dead() && !it->m_coeff.is_int()) {
                 TRACE("gomory_cut", display_row(tout, r, true););
                 return false;
+            }
         }
         return true;
     }