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

nits

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-04-02 17:49:03 -07:00
parent 25feb0ebed
commit d0ef5948aa
1 changed files with 5 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/tactic/arith/nla2bv_tactic.cpp
View file

@ -103,17 +103,16 @@ class nla2bv_tactic : public tactic {
TRACE("nla2bv", g.display(tout << "substitute vars\n"));
reduce_bv2int(g);
reduce_bv2real(g);
TRACE("nla2bv", g.display(tout << "after reduce\n"););
TRACE("nla2bv", g.display(tout << "after reduce\n"));
mc = m_fmc.get();
for (unsigned i = 0; i < m_vars.size(); ++i) {
m_fmc->add(m_vars[i].get(), m_defs[i].get());
}
for (unsigned i = 0; i < m_vars.size(); ++i)
m_fmc->add(m_vars.get(i), m_defs.get(i));
for (unsigned i = 0; i < m_bv2real.num_aux_decls(); ++i) {
m_fmc->hide(m_bv2real.get_aux_decl(i));
}
IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(nla->bv :sat-preserving " << m_is_sat_preserving << ")\n";);
TRACE("nla2bv_verbose", g.display(tout););
TRACE("nla2bv", tout << "Muls: " << count_mul(g) << "\n";);
TRACE("nla2bv_verbose", g.display(tout));
TRACE("nla2bv", tout << "Muls: " << count_mul(g) << "\n");
g.inc_depth();
if (!is_sat_preserving())
g.updt_prec(goal::UNDER);