mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

z3str3: check for and re-internalize str.in.re terms

Browse source
This commit is contained in:
Murphy Berzish 2019-10-11 11:56:52 -04:00 committed by Nikolaj Bjorner
parent 58bc2bff0b
commit 4fc64ab578
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_str.cpp
View file

@ -9926,6 +9926,12 @@ namespace smt {
expr * str = nullptr; expr * str = nullptr;
expr * re = nullptr; expr * re = nullptr;
u.str.is_in_re(str_in_re, str, re); u.str.is_in_re(str_in_re, str, re);
if (!ctx.b_internalized(str_in_re)) {
TRACE("str", tout << "regex term " << mk_pp(str_in_re, m) << " not internalized; fixing and continuing" << std::endl;);
ctx.internalize(str_in_re, false);
finalCheckProgressIndicator = true;
continue;
}
lbool current_assignment = ctx.get_assignment(str_in_re); lbool current_assignment = ctx.get_assignment(str_in_re);
TRACE("str", tout << "regex term: " << mk_pp(str, m) << " in " << mk_pp(re, m) << " : " << current_assignment << std::endl;); TRACE("str", tout << "regex term: " << mk_pp(str, m) << " in " << mk_pp(re, m) << " : " << current_assignment << std::endl;);
if (current_assignment == l_undef) { if (current_assignment == l_undef) {