mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix a few compiler warnings
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
This commit is contained in:
parent
d3570484bb
commit
f7c3559c31
|
@ -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;
|
||||
|
|
|
@ -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);
|
||||
|
||||
|
|
|
@ -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;
|
||||
|
|
Loading…
Reference in a new issue