mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

fix nightly regression from solve-eqs context solver addition

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-05-27 04:17:43 -07:00
parent 2d0ff7d68a
commit f99384c6a3
4 changed files with 7 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -599,11 +599,14 @@ class solve_eqs_tactic : public tactic {
hoist_rewriter_star rw(m());
th_rewriter thrw(m());
expr_ref tmp(m()), tmp2(m());
TRACE("solve_eqs", g.display(tout););
for (unsigned idx = 0; idx < size; idx++) {
checkpoint();
if (g.is_decided_unsat()) break;
expr* f = g.form(idx);
thrw(f, tmp);
rw(tmp, tmp2);
TRACE("solve_eqs", tout << mk_pp(f, m()) << " " << tmp2 << "\n";);
g.update(idx, tmp2, g.pr(idx), g.dep(idx));
}