fix #4890

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/muz/rel/dl_instruction.cpp

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

src/tactic/arith/eq2bv_tactic.cpp

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