From 9d2c86f214304d224b7c439bc3bfd43da002dbdc Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Fri, 8 Dec 2017 20:31:22 -0500 Subject: [PATCH] fix incorrect clause in argumentsValid subterm of substr reduction --- src/smt/theory_str.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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