diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp
index aad1d6c5e..0bd9ffc13 100644
--- a/src/tactic/arith/eq2bv_tactic.cpp
+++ b/src/tactic/arith/eq2bv_tactic.cpp
@@ -278,13 +278,17 @@ 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))
+                rm.push_back(kv.m_key);
+        
+        for (expr* r : rm)
+            m_max.erase(r);
+
         for (auto& kv : m_max) {
             expr* key = kv.m_key;
             rational& value = kv.m_value;
-            if (m_nonfd.is_marked(key)) {
-                rm.push_back(key);
-                continue;
-            }
+
             // ensure there are enough elements.
             bool strict;
             rational bound;            
@@ -298,17 +302,13 @@ public:
                 value = std::max(value, bound);
             
             ++value;
-        }
-        for (expr* r : rm)
-            m_max.erase(r);
 
-        for (auto& kv : m_max) {
-            unsigned p = kv.m_value.get_num_bits();      
+            unsigned p = value.get_num_bits();      
             if (p <= 1) p = 2;
             app* z = m.mk_fresh_const("z", bv.mk_sort(p));
             m_trail.push_back(z);
-            m_fd.insert(kv.m_key, z);
-            mc->insert(z->get_decl(), to_app(kv.m_key)->get_decl());
+            m_fd.insert(key, z);
+            mc->insert(z->get_decl(), to_app(key)->get_decl());
         }
     }
 
diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index e4f1b4dbd..6dced5b7b 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -338,7 +338,7 @@ class solve_eqs_tactic : public tactic {
             // solve lhs mod r1 = 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());
                 def0 = add(mk_int(r2), mul(fresh(), mk_int(r1)));
                 return solve_eq(lhs, def0, eq, var, def, pr);