From f7c3559c31b5d5c7335706a61a7f9c6e47a55545 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <a-nlopes@microsoft.com>
Date: Tue, 16 Sep 2014 15:26:01 +0100
Subject: [PATCH] fix a few compiler warnings

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
---
 src/api/api_interp.cpp             | 2 +-
 src/muz/pdr/pdr_farkas_learner.cpp | 1 -
 src/smt/smt_model_checker.cpp      | 3 +--
 3 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp
index 03d5ff843..e06ad5192 100644
--- a/src/api/api_interp.cpp
+++ b/src/api/api_interp.cpp
@@ -411,7 +411,7 @@ static void get_file_params(const char *filename, hash_map<std::string,std::stri
       for(unsigned i = 0; i < tokens.size(); i++){
 	std::string &tok = tokens[i];
 	size_t eqpos = tok.find('=');
-	if(eqpos >= 0 && eqpos < tok.size()){
+	if(eqpos != std::string::npos){
 	  std::string left = tok.substr(0,eqpos);
 	  std::string right = tok.substr(eqpos+1,tok.size()-eqpos-1);
 	  params[left] = right;
diff --git a/src/muz/pdr/pdr_farkas_learner.cpp b/src/muz/pdr/pdr_farkas_learner.cpp
index 7c38bf86f..b440ef519 100644
--- a/src/muz/pdr/pdr_farkas_learner.cpp
+++ b/src/muz/pdr/pdr_farkas_learner.cpp
@@ -905,7 +905,6 @@ namespace pdr {
     void farkas_learner::get_asserted(proof* p, expr_set const& bs, ast_mark& b_closed, obj_hashtable<expr>& lemma_set, expr_ref_vector& lemmas) {
         ast_manager& m = lemmas.get_manager();
         ast_mark visited;
-        proof* p0 = p;
         ptr_vector<proof> todo;        
         todo.push_back(p);
                       
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index 526447f9f..7053d63ec 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -136,9 +136,8 @@ namespace smt {
         if (cex == 0)
             return false; // no model available.
         unsigned num_decls = q->get_num_decls();
-        unsigned   num_sks = sks.size();
         // Remark: sks were created for the flat version of q.
-        SASSERT(num_sks >= num_decls); 
+        SASSERT(sks.size() >= num_decls);
         expr_ref_buffer bindings(m_manager);
         bindings.resize(num_decls);
         unsigned max_generation = 0;