diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 7936b581c..022a2ad73 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -1450,7 +1450,7 @@ namespace smt { // pos < strlen(base) // --> pos + -1*strlen(base) < 0 argumentsValid_terms.push_back(mk_not(m, m_autil.mk_ge( - m_autil.mk_add(substrPos, m_autil.mk_mul(minusOne, substrLen)), + m_autil.mk_add(substrPos, m_autil.mk_mul(minusOne, mk_strlen(substrBase))), zero))); // len >= 0