3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

z3str3: fix control flow and return paths in regex model construction

This commit is contained in:
Murphy Berzish 2020-02-12 13:46:27 -05:00 committed by Nikolaj Bjorner
parent f5a307073a
commit 0146259ea4

View file

@ -488,6 +488,9 @@ namespace smt {
cex = m.mk_or(f, m.mk_not(ctx.mk_eq_atom(mk_strlen(str), mk_int(0))));
ctx.get_rewriter()(cex);
return false;
} else {
TRACE("str_fl", tout << "regex constraint satisfied without asserting constraints to subsolver" << std::endl;);
return true;
}
} else {
expr_ref_vector trail(m);
@ -560,6 +563,9 @@ namespace smt {
cex = m.mk_or(m.mk_not(f), m.mk_not(ctx.mk_eq_atom(mk_strlen(str), mk_int(str_chars.size()))));
ctx.get_rewriter()(cex);
return false;
} else {
TRACE("str_fl", tout << "regex constraint satisfied without asserting constraints to subsolver" << std::endl;);
return true;
}
} else {
// TODO fixed_length_lesson?
@ -571,8 +577,6 @@ namespace smt {
return true;
}
}
UNREACHABLE(); // added because compiler complains that not all control paths return a value.
return false;
}
/*