mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix #4890

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-12-12 12:20:53 -08:00
parent 89a6c7a349
commit 89fb55a864
2 changed files with 10 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/muz/rel/dl_instruction.cpp
View file

@ -581,6 +581,7 @@ namespace datalog {
bool perform(execution_context & ctx) override { bool perform(execution_context & ctx) override {
log_verbose(ctx); log_verbose(ctx);
if (!ctx.reg(m_src)) { if (!ctx.reg(m_src)) {
std::cout << "not " << m_src << "\n";
ctx.make_empty(m_res); ctx.make_empty(m_res);
return true; return true;
} }
@ -590,6 +591,7 @@ namespace datalog {
relation_base & reg = *ctx.reg(m_src); relation_base & reg = *ctx.reg(m_src);
TRACE("dl_verbose", reg.display(tout <<"pre-filter-interpreted-and-project:\n");); TRACE("dl_verbose", reg.display(tout <<"pre-filter-interpreted-and-project:\n"););
if (!find_fn(reg, fn)) { if (!find_fn(reg, fn)) {
std::cout << m_cond << "\n";
fn = reg.get_manager().mk_filter_interpreted_and_project_fn(reg, m_cond, m_cols.size(), m_cols.c_ptr()); fn = reg.get_manager().mk_filter_interpreted_and_project_fn(reg, m_cond, m_cols.size(), m_cols.c_ptr());
if (!fn) { if (!fn) {
throw default_exception(default_exception::fmt(), throw default_exception(default_exception::fmt(),
@ -602,6 +604,7 @@ namespace datalog {
ctx.set_reg(m_res, (*fn)(reg)); ctx.set_reg(m_res, (*fn)(reg));
if (ctx.reg(m_res)->fast_empty()) { if (ctx.reg(m_res)->fast_empty()) {
std::cout << "fast empty\n";
ctx.make_empty(m_res); ctx.make_empty(m_res);
} }
// TRACE("dl_verbose", reg.display(tout << "post-filter-interpreted-and-project:\n");); // TRACE("dl_verbose", reg.display(tout << "post-filter-interpreted-and-project:\n"););

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

@ -278,14 +278,11 @@ 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) { for (auto& kv : m_max)
if (m_nonfd.is_marked(kv.m_key)) { if (m_nonfd.is_marked(kv.m_key))
rm.push_back(kv.m_key); rm.push_back(kv.m_key);
} for (expr* r : rm)
} m_max.erase(r);
for (unsigned i = 0; i < rm.size(); ++i) {
m_max.erase(rm[i]);
}
for (auto& kv : m_max) { for (auto& kv : m_max) {
// ensure there are enough elements. // ensure there are enough elements.
bool strict; bool strict;
@ -305,6 +302,7 @@ public:
if (p <= 1) p = 2; if (p <= 1) p = 2;
if (kv.m_value == p) p *= 2; if (kv.m_value == p) p *= 2;
unsigned n = log2(p); unsigned n = log2(p);
SASSERT(p >= kv.m_value);
app* z = m.mk_fresh_const("z", bv.mk_sort(n)); app* z = m.mk_fresh_const("z", bv.mk_sort(n));
m_trail.push_back(z); m_trail.push_back(z);
m_fd.insert(kv.m_key, z); m_fd.insert(kv.m_key, z);
@ -391,6 +389,8 @@ public:
rational r; rational r;
if (is_uninterp_const(v) && a.is_numeral(c, r) && !m_nonfd.is_marked(v) && a.is_int(v) && r.is_unsigned()) { if (is_uninterp_const(v) && a.is_numeral(c, r) && !m_nonfd.is_marked(v) && a.is_int(v) && r.is_unsigned()) {
val = r.get_unsigned(); val = r.get_unsigned();
if (val > UINT_MAX/4)
return false;
add_fd(v, val); add_fd(v, val);
return true; return true;
} }