mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 00:48:45 +00:00
Code Activity

fix incorrect clause in argumentsValid subterm of substr reduction

Browse source
This commit is contained in:
Murphy Berzish 2017-12-08 20:31:22 -05:00
parent b581ab70ed
commit 9d2c86f214
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