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

fix #4923

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-01-09 01:21:50 -08:00
parent ffd57bef24
commit 96ab9edbfd
2 changed files with 12 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/tactic/arith/eq2bv_tactic.cpp
View file

@ -278,13 +278,17 @@ public:
void cleanup_fd(ref<bvmc>& mc) { void cleanup_fd(ref<bvmc>& mc) {
SASSERT(m_fd.empty()); SASSERT(m_fd.empty());
ptr_vector<expr> rm; ptr_vector<expr> rm;
for (auto& kv : m_max)
if (m_nonfd.is_marked(kv.m_key))
rm.push_back(kv.m_key);
for (expr* r : rm)
m_max.erase(r);
for (auto& kv : m_max) { for (auto& kv : m_max) {
expr* key = kv.m_key; expr* key = kv.m_key;
rational& value = kv.m_value; rational& value = kv.m_value;
if (m_nonfd.is_marked(key)) {
rm.push_back(key);
continue;
}
// ensure there are enough elements. // ensure there are enough elements.
bool strict; bool strict;
rational bound; rational bound;
@ -298,17 +302,13 @@ public:
value = std::max(value, bound); value = std::max(value, bound);
++value; ++value;
}
for (expr* r : rm)
m_max.erase(r);
for (auto& kv : m_max) { unsigned p = value.get_num_bits();
unsigned p = kv.m_value.get_num_bits();
if (p <= 1) p = 2; if (p <= 1) p = 2;
app* z = m.mk_fresh_const("z", bv.mk_sort(p)); app* z = m.mk_fresh_const("z", bv.mk_sort(p));
m_trail.push_back(z); m_trail.push_back(z);
m_fd.insert(kv.m_key, z); m_fd.insert(key, z);
mc->insert(z->get_decl(), to_app(kv.m_key)->get_decl()); mc->insert(z->get_decl(), to_app(key)->get_decl());
} }
} }

2
src/tactic/core/solve_eqs_tactic.cpp
View file

@ -338,7 +338,7 @@ class solve_eqs_tactic : public tactic {
// solve lhs mod r1 = r2 // solve lhs mod r1 = r2
// as lhs = r1*mod!1 + r2 // as lhs = r1*mod!1 + r2
// //
if (m_a_util.is_numeral(rhs, r2) && r2 < r1) { if (m_a_util.is_numeral(rhs, r2) && !r2.is_neg() && r2 < r1) {
expr_ref def0(m()); expr_ref def0(m());
def0 = add(mk_int(r2), mul(fresh(), mk_int(r1))); def0 = add(mk_int(r2), mul(fresh(), mk_int(r1)));
return solve_eq(lhs, def0, eq, var, def, pr); return solve_eq(lhs, def0, eq, var, def, pr);