mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 13:53:39 +00:00
Code Activity

fix #4907

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-12-20 11:02:19 -08:00
parent dd05c683e0
commit 259a8ff786
2 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/hoist_rewriter.cpp
View file

@ -130,7 +130,9 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref &
} }
fmls.push_back(p); fmls.push_back(p);
} }
for (auto const& p : m_eqs) { for (auto& p : m_eqs) {
if (m().is_value(p.first))
std::swap(p.first, p.second);
m_subst.insert(p.first, p.second); m_subst.insert(p.first, p.second);
fmls.push_back(m().mk_eq(p.first, p.second)); fmls.push_back(m().mk_eq(p.first, p.second));
} }

4
src/tactic/core/solve_eqs_tactic.cpp
View file

@ -687,7 +687,7 @@ class solve_eqs_tactic : public tactic {
th_rewriter thrw(m()); th_rewriter thrw(m());
expr_ref tmp(m()), tmp2(m()); expr_ref tmp(m()), tmp2(m());
// TRACE("solve_eqs", g.display(tout);); TRACE("solve_eqs", g.display(tout););
for (unsigned idx = 0; !g.inconsistent() && idx < size; idx++) { for (unsigned idx = 0; !g.inconsistent() && idx < size; idx++) {
checkpoint(); checkpoint();
if (g.is_decided_unsat()) break; if (g.is_decided_unsat()) break;
@ -695,7 +695,7 @@ class solve_eqs_tactic : public tactic {
proof_ref pr1(m()), pr2(m()); proof_ref pr1(m()), pr2(m());
thrw(f, tmp, pr1); thrw(f, tmp, pr1);
rw(tmp, tmp2, pr2); rw(tmp, tmp2, pr2);
TRACE("solve_eqs", tout << mk_pp(f, m()) << " " << tmp << "\n" << tmp2 TRACE("solve_eqs", tout << mk_pp(f, m()) << "\n->\n" << tmp << "\n->\n" << tmp2
<< "\n" << pr1 << "\n" << pr2 << "\n" << mk_pp(g.pr(idx), m()) << "\n";); << "\n" << pr1 << "\n" << pr2 << "\n" << mk_pp(g.pr(idx), m()) << "\n";);
pr1 = m().mk_transitivity(pr1, pr2); pr1 = m().mk_transitivity(pr1, pr2);
if (!pr1) pr1 = g.pr(idx); else pr1 = m().mk_modus_ponens(g.pr(idx), pr1); if (!pr1) pr1 = g.pr(idx); else pr1 = m().mk_modus_ponens(g.pr(idx), pr1);