mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 13:53:39 +00:00
Code Activity

formatting

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-31 11:57:42 -08:00
parent 6422b783b2
commit f3fc6a50f3
1 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/tactic/arith/lia2card_tactic.cpp
View file

@ -216,11 +216,10 @@ public:
} }
// IF_VERBOSE(0, verbose_stream() << mk_pp(g->form(i), m) << "\n--->\n" << new_curr << "\n";); // 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)); g->update(i, new_curr, new_pr, g->dep(i));
} }
for (expr* a : axioms) { for (expr* a : axioms)
g->assert_expr(a); g->assert_expr(a);
}
if (m_mc) g->add(m_mc.get()); if (m_mc) g->add(m_mc.get());
g->inc_depth(); g->inc_depth();
result.push_back(g.get()); result.push_back(g.get());