From f3fc6a50f317656314f0064b2a15c7de530550db Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 31 Jan 2022 11:57:42 -0800 Subject: [PATCH] formatting --- src/tactic/arith/lia2card_tactic.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) 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());