mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

fix #2795

Browse source
This commit is contained in:
Nikolaj Bjorner 2019-12-10 03:06:45 -08:00
parent 4b22ff2d3b
commit 184f7cedf6
2 changed files with 6 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/tactic/arith/bv2real_rewriter.cpp
View file

@ -152,7 +152,7 @@ void bv2real_util::mk_sbv2real(expr* e, expr_ref& result) {
expr* bv2real_util::mk_bv_mul(rational const& n, expr* t) {
if (n.is_one()) return t;
expr* s = mk_sbv(n);
expr_ref s(mk_sbv(n), m());
return mk_bv_mul(s, t);
}

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

@ -81,9 +81,7 @@ class nla2bv_tactic : public tactic {
~imp() {}
void updt_params(params_ref const& p) {
}
void updt_params(params_ref const& p) {}
void operator()(goal & g, model_converter_ref & mc) {
TRACE("nla2bv", g.display(tout);
@ -132,14 +130,13 @@ class nla2bv_tactic : public tactic {
m_bv2int_ctx.collect_power2(g);
obj_map<expr, expr*> const& p2 = m_bv2int_ctx.power2();
if (p2.empty()) return;
obj_map<expr, expr*>::iterator it = p2.begin(), end = p2.end();
for (; it != end; ++it) {
expr* v = it->m_value;
for (auto const& kv : p2) {
expr* v = kv.m_value;
unsigned num_bits = m_bv.get_bv_size(v);
expr* w = m_bv.mk_bv2int(m_bv.mk_bv_shl(m_bv.mk_numeral(1, num_bits), v));
m_trail.push_back(w);
m_subst.insert(it->m_key, w);
TRACE("nla2bv", tout << mk_ismt2_pp(it->m_key, m_manager) << " " << mk_ismt2_pp(w, m_manager) << "\n";);
m_subst.insert(kv.m_key, w);
TRACE("nla2bv", tout << mk_ismt2_pp(kv.m_key, m_manager) << " " << mk_ismt2_pp(w, m_manager) << "\n";);
}
// eliminate the variables that are power of two.
substitute_vars(g);