mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 11:58:31 +00:00
Code Activity

Merge branch 'master' into develop

Browse source
This commit is contained in:
Murphy Berzish 2017-12-11 17:36:12 -05:00
commit d2d79e3207
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_str.cpp
View file

@ -1450,7 +1450,7 @@ namespace smt {
// pos < strlen(base) // pos < strlen(base)
// --> pos + -1*strlen(base) < 0 // --> pos + -1*strlen(base) < 0
argumentsValid_terms.push_back(mk_not(m, m_autil.mk_ge( 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))); zero)));
// len >= 0 // len >= 0