mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 19:53:34 +00:00
Code Activity

use size_t for return values from strlen

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-03-01 11:09:57 -08:00
parent f2ecd70e65
commit e27b7e3038
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/smt/smt_quantifier.cpp
View file

@ -439,12 +439,12 @@ namespace smt {
virtual bool model_based() const { return m_fparams->m_mbqi; }
virtual bool mbqi_enabled(quantifier *q) const {
if(!m_fparams->m_mbqi_id) return true;
const symbol &s = q->get_qid();
unsigned len = strlen(m_fparams->m_mbqi_id);
if(s == symbol::null || s.is_numerical())
return len == 0;
return strncmp(s.bare_str(),m_fparams->m_mbqi_id,len) == 0;
if(!m_fparams->m_mbqi_id) return true;
const symbol &s = q->get_qid();
size_t len = strlen(m_fparams->m_mbqi_id);
if(s == symbol::null || s.is_numerical())
return len == 0;
return strncmp(s.bare_str(),m_fparams->m_mbqi_id,len) == 0;
}
/* Quantifier id's must begin with the prefix specified by