From 89fb55a86422b24e922033f803c4cb78eacf6e65 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 12 Dec 2020 12:20:53 -0800
Subject: [PATCH] fix #4890

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/rel/dl_instruction.cpp    |  3 +++
 src/tactic/arith/eq2bv_tactic.cpp | 14 +++++++-------
 2 files changed, 10 insertions(+), 7 deletions(-)

diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp
index 98bb2be13..514ead983 100644
--- a/src/muz/rel/dl_instruction.cpp
+++ b/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"););
diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp
index 958cd93de..528812574 100644
--- a/src/tactic/arith/eq2bv_tactic.cpp
+++ b/src/tactic/arith/eq2bv_tactic.cpp
@@ -278,14 +278,11 @@ public:
     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 @@ public:
             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 @@ public:
         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;
         }