mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
fix #4736
This commit is contained in:
parent
f354671465
commit
0e1def5bd6
|
@ -264,7 +264,7 @@ class factor_tactic : public tactic {
|
|||
expr_ref new_curr(m);
|
||||
proof_ref new_pr(m);
|
||||
unsigned size = g->size();
|
||||
for (unsigned idx = 0; idx < size; idx++) {
|
||||
for (unsigned idx = 0; !g->inconsistent() && idx < size; idx++) {
|
||||
expr * curr = g->form(idx);
|
||||
m_rw(curr, new_curr, new_pr);
|
||||
if (produce_proofs) {
|
||||
|
|
Loading…
Reference in a new issue