diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index 5f6edf6ea95..97c6f466f58 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -216,11 +216,10 @@ class lia2card_tactic : public tactic { } // IF_VERBOSE(0, verbose_stream() << mk_pp(g->form(i), m) << "\n--->\n" << new_curr << "\n";); g->update(i, new_curr, new_pr, g->dep(i)); - } - for (expr* a : axioms) { + for (expr* a : axioms) g->assert_expr(a); - } + if (m_mc) g->add(m_mc.get()); g->inc_depth(); result.push_back(g.get());