diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 8fd0e08bc..e9b0e069a 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -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