diff --git a/src/tactic/arith/bound_manager.cpp b/src/tactic/arith/bound_manager.cpp
index 1ed3265e2..66a6652c4 100644
--- a/src/tactic/arith/bound_manager.cpp
+++ b/src/tactic/arith/bound_manager.cpp
@@ -18,6 +18,7 @@ Notes:
 --*/
 #include "tactic/arith/bound_manager.h"
 #include "ast/ast_smt2_pp.h"
+#include "ast/ast_pp.h"
 #include "tactic/goal.h"
 
 bound_manager::bound_manager(ast_manager & m):
diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp
index 1e1b259fc..3a302993e 100644
--- a/src/tactic/arith/eq2bv_tactic.cpp
+++ b/src/tactic/arith/eq2bv_tactic.cpp
@@ -76,7 +76,7 @@ class eq2bv_tactic : public tactic {
     class bvmc : public model_converter {
         obj_map<func_decl, func_decl*> m_map;
         func_decl_ref_vector m_vars;
-        unsigned_vector m_values;
+        vector<rational> m_values;
     public:
         bvmc(ast_manager& m): m_vars(m) {}
         
@@ -84,7 +84,7 @@ class eq2bv_tactic : public tactic {
             m_map.insert(c_new, c_old);
         }
 
-        void insert(func_decl* var, unsigned val) { 
+        void insert(func_decl* var, rational const& val) { 
             m_vars.push_back(var);
             m_values.push_back(val);
         }
@@ -111,7 +111,7 @@ class eq2bv_tactic : public tactic {
             }
             for (unsigned i = 0; i < m_vars.size(); ++i) {
                 func_decl* f = m_vars.get(i);
-                new_m->register_decl(f, a.mk_numeral(rational(m_values[i]), f->get_range()));
+                new_m->register_decl(f, a.mk_numeral(m_values[i], f->get_range()));
             }
             mdl = new_m;
         }
@@ -203,16 +203,23 @@ public:
         for (unsigned i = 0; !g->inconsistent() && i < g->size(); i++) {            
             expr_ref   new_curr(m);
             proof_ref  new_pr(m);  
-            func_decl_ref var(m);
-            unsigned val;
-            if (is_bound(g->form(i), var, val) && !m_has_eq.is_marked(var)) {
+            expr_ref var(m);
+            if (is_bound(g->form(i), var) && !m_has_eq.is_marked(var)) {
                 if (m.proofs_enabled()) {
                     new_pr = m.mk_rewrite(g->form(i), m.mk_true());
                     new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
                 }
-                g->update(i, m.mk_true(), new_pr, nullptr);
-                mc1->insert(var, val);
-                continue;
+                bool strict = true;
+                rational v;
+                bool has_val = 
+                    (m_bounds.has_upper(var, v, strict) && !strict) && v.is_unsigned() ||
+                    (m_bounds.has_lower(var, v, strict) && !strict && v.is_unsigned());
+
+                if (has_val) {
+                    mc1->insert(to_app(var)->get_decl(), v);
+                    g->update(i, m.mk_true(), new_pr, nullptr);
+                    continue;
+                }
             }
             m_rw(g->form(i), new_curr, new_pr);
             if (g->form(i) == new_curr)
@@ -305,29 +312,31 @@ public:
         }
     }
 
-    bool is_upper(expr* f, func_decl_ref& var, unsigned& k) {
+    bool is_upper(expr* f, expr_ref& var) {
         expr* e1, *e2;
+        unsigned k;
         if ((a.is_le(f, e1, e2) || a.is_ge(f, e2, e1)) && is_var_const_pair(e1, e2, k)) {
             SASSERT(m_bounds.has_upper(e1));
-            var = to_app(e1)->get_decl();
+            var = e1;
             return true;
         } 
         return false;
     }
 
-    bool is_lower(expr* f, func_decl_ref& var, unsigned& k) {
+    bool is_lower(expr* f, expr_ref& var) {
         expr* e1, *e2;
+        unsigned k;
         if ((a.is_le(f, e1, e2) || a.is_ge(f, e2, e1)) && is_var_const_pair(e2, e1, k)) {
             SASSERT(m_bounds.has_lower(e2));
-            var = to_app(e2)->get_decl();
+            var = e2;
             return true;
         } 
         return false;
     }
 
 
-    bool is_bound(expr* f, func_decl_ref& var, unsigned& val) {
-        return is_lower(f, var, val) || is_upper(f, var, val);
+    bool is_bound(expr* f, expr_ref& var) {
+        return is_lower(f, var) || is_upper(f, var);
     }
 
     void mark_has_eq(expr* e) {
@@ -338,9 +347,8 @@ public:
 
     void collect_fd(expr* f) {
         m_trail.push_back(f);
-        func_decl_ref var(m);
-        unsigned val;
-        if (is_bound(f, var, val)) return;
+        expr_ref var(m);
+        if (is_bound(f, var)) return;
         m_todo.push_back(f);
         while (!m_todo.empty()) {
             f = m_todo.back();