mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

#5778

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-04-09 12:06:39 +02:00
parent 011c1b2dd2
commit f55b233228
2 changed files with 11 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/sat/smt/arith_solver.cpp
View file

@ -549,13 +549,14 @@ namespace arith {
found_compatible = false; found_compatible = false;
for (; it != end; ++it) { for (; it != end; ++it) {
api_bound* a2 = *it; api_bound* a2 = *it;
if (a1 == a2) continue; if (a1 == a2)
if (a2->get_bound_kind() != kind) continue; continue;
if (a2->get_bound_kind() != kind)
continue;
rational const& k2(a2->get_value()); rational const& k2(a2->get_value());
found_compatible = true; found_compatible = true;
if (k1 < k2) { if (k1 < k2)
return it; return it;
}
} }
return end; return end;
} }

6
src/sat/smt/q_model_fixer.cpp
View file

@ -184,6 +184,8 @@ namespace q {
for (euf::enode* n : ctx.get_egraph().enodes_of(f)) { for (euf::enode* n : ctx.get_egraph().enodes_of(f)) {
expr* t = n->get_arg(idx)->get_expr(); expr* t = n->get_arg(idx)->get_expr();
values.push_back(mdl(t)); values.push_back(mdl(t));
if (!m.is_value(values.back()))
return expr_ref(m.mk_var(idx, srt), m);
md->v2t.insert(values.back(), t); md->v2t.insert(values.back(), t);
md->t2v.insert(t, values.back()); md->t2v.insert(t, values.back());
} }
@ -299,6 +301,10 @@ namespace q {
auto term = [&](unsigned j) { auto term = [&](unsigned j) {
return md->v2t[md->values[j]]; return md->v2t[md->values[j]];
}; };
for (unsigned j = 0; j < sz; ++j)
std::cout << mk_pp(md->values[j], m) << "\n";
expr* arg = t->get_arg(i); expr* arg = t->get_arg(i);