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

z3str3: ignore non-relevant formulas in bitvector model construction

Browse source
This commit is contained in:
Murphy Berzish 2020-01-20 19:43:40 -05:00 • committed by Nikolaj Bjorner
parent cf3f271f5b
commit 812049ca4a
1 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_str_mc.cpp
View file

@ -659,6 +659,10 @@ namespace smt {
sort * bool_sort = m.mk_bool_sort(); sort * bool_sort = m.mk_bool_sort();
for (expr * f : formulas) { for (expr * f : formulas) {
if (!get_context().is_relevant(f)) {
TRACE("str_fl", tout << "skip reducing formula " << mk_pp(f, m) << ", not relevant" << std::endl;);
continue;
}
// reduce string formulas only. ignore others // reduce string formulas only. ignore others
sort * fSort = m.get_sort(f); sort * fSort = m.get_sort(f);
if (fSort == bool_sort && !is_quantifier(f)) { if (fSort == bool_sort && !is_quantifier(f)) {