mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

#5331

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-07-19 16:09:13 -07:00
parent a8b433e6ac
commit 7af2309fae
1 changed files with 1 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/tactic/arith/recover_01_tactic.cpp
View file

@ -321,8 +321,6 @@ class recover_01_tactic : public tactic {
SASSERT(new_goal->depth() == g->depth());
SASSERT(new_goal->prec() == g->prec());
new_goal->inc_depth();
new_goal->add(g->mc());
new_goal->add(g->pc());
for (unsigned i = 0; i < g->size(); i++) {
expr * f = g->form(i);
@ -375,7 +373,7 @@ class recover_01_tactic : public tactic {
new_goal->update(idx, new_curr);
}
result.push_back(new_goal.get());
TRACE("recover_01", new_goal->display(tout););
TRACE("recover_01", new_goal->display(tout); if (new_goal->mc()) new_goal->mc()->display(tout););
SASSERT(new_goal->is_well_formed());
}