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

fix re.range symbolic argument bug in z3str3 (#6189)

Browse source
This commit is contained in:
JohnLyu2 2022-07-26 22:24:20 -04:00 • committed by GitHub
parent 63ea7bd569
commit 3e8daa5965
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 4 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/smt/theory_str_regex.cpp
View file

@ -724,8 +724,7 @@ namespace smt {
unsigned cx = estimate_regex_complexity(sub1); unsigned cx = estimate_regex_complexity(sub1);
return _qadd(lo, cx); return _qadd(lo, cx);
} else if (u.re.is_range(re, sub1, sub2)) { } else if (u.re.is_range(re, sub1, sub2)) {
SASSERT(u.str.is_string(sub1)); if (!u.re.is_range(re, lo, hi)) throw default_exception("regular expressions must be built from string literals");
SASSERT(u.str.is_string(sub2));
zstring str1, str2; zstring str1, str2;
u.str.is_string(sub1, str1); u.str.is_string(sub1, str1);
u.str.is_string(sub2, str2); u.str.is_string(sub2, str2);
@ -767,8 +766,7 @@ namespace smt {
unsigned cx = estimate_regex_complexity_under_complement(sub1); unsigned cx = estimate_regex_complexity_under_complement(sub1);
return _qmul(2, cx); return _qmul(2, cx);
} else if (u.re.is_range(re, sub1, sub2)) { } else if (u.re.is_range(re, sub1, sub2)) {
SASSERT(u.str.is_string(sub1)); if (!u.re.is_range(re, lo, hi)) throw default_exception("regular expressions must be built from string literals");
SASSERT(u.str.is_string(sub2));
zstring str1, str2; zstring str1, str2;
u.str.is_string(sub1, str1); u.str.is_string(sub1, str1);
u.str.is_string(sub2, str2); u.str.is_string(sub2, str2);
@ -874,8 +872,7 @@ namespace smt {
// this is bad -- term generation requires this not to appear // this is bad -- term generation requires this not to appear
lens.reset(); lens.reset();
} else if (u.re.is_range(re, sub1, sub2)) { } else if (u.re.is_range(re, sub1, sub2)) {
SASSERT(u.str.is_string(sub1)); if (!u.re.is_range(re, lo, hi)) throw default_exception("regular expressions must be built from string literals");
SASSERT(u.str.is_string(sub2));
zstring str1, str2; zstring str1, str2;
u.str.is_string(sub1, str1); u.str.is_string(sub1, str1);
u.str.is_string(sub2, str2); u.str.is_string(sub2, str2);
@ -1006,8 +1003,7 @@ namespace smt {
SASSERT(retval); SASSERT(retval);
return retval; return retval;
} else if (u.re.is_range(re, sub1, sub2)) { } else if (u.re.is_range(re, sub1, sub2)) {
SASSERT(u.str.is_string(sub1)); if (!u.re.is_range(re, lo, hi)) throw default_exception("regular expressions must be built from string literals");
SASSERT(u.str.is_string(sub2));
zstring str1, str2; zstring str1, str2;
u.str.is_string(sub1, str1); u.str.is_string(sub1, str1);
u.str.is_string(sub2, str2); u.str.is_string(sub2, str2);