mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-17 03:16:17 +00:00
Code Activity

fix npos semantics

Browse source
This commit is contained in:
Murphy Berzish 2017-02-27 20:51:30 -05:00
parent 3f1ceedcb1
commit c62b55f9b1
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_str.cpp
View file

@ -4877,7 +4877,7 @@ void theory_str::check_contain_by_eqc_val(expr * varNode, expr * constNode) {
cstItor != constList.end(); cstItor++) { cstItor != constList.end(); cstItor++) {
zstring pieceStr; zstring pieceStr;
u.str.is_string(*cstItor, pieceStr); u.str.is_string(*cstItor, pieceStr);
if (strConst.contains(pieceStr)) { if (!strConst.contains(pieceStr)) {
counterEgFound = true; counterEgFound = true;
if (aConcat != substrAst) { if (aConcat != substrAst) {
litems.push_back(ctx.mk_eq_atom(substrAst, aConcat)); litems.push_back(ctx.mk_eq_atom(substrAst, aConcat));
@ -5606,7 +5606,7 @@ bool theory_str::is_partial_in_grounded_concat(const std::vector<expr*> & strVec
for (int i = 0; i < strCnt; i++) { for (int i = 0; i < strCnt; i++) {
zstring strVal; zstring strVal;
if (u.str.is_string(strVec[i], strVal)) { if (u.str.is_string(strVec[i], strVal)) {
if (strVal.find(subStrVal) != std::string::npos) { if (strVal.contains(subStrVal)) {
return true; return true;
} }
} }
@ -5794,7 +5794,7 @@ bool theory_str::can_concat_eq_str(expr * concat, zstring& str) {
expr * oneArg = args[i]; expr * oneArg = args[i];
zstring arg_str; zstring arg_str;
if (u.str.is_string(oneArg, arg_str)) { if (u.str.is_string(oneArg, arg_str)) {
if (str.contains(arg_str)) { if (!str.contains(arg_str)) {
return false; return false;
} }
sumLen += arg_str.length(); sumLen += arg_str.length();