diff --git a/src/ast/rewriter/bv2int_translator.cpp b/src/ast/rewriter/bv2int_translator.cpp
index 3200cc6c7..4e49e85e4 100644
--- a/src/ast/rewriter/bv2int_translator.cpp
+++ b/src/ast/rewriter/bv2int_translator.cpp
@@ -183,6 +183,20 @@ void bv2int_translator::translate_app(app* e) {
     set_translated(e, m.mk_app(f, m_args));
 }
 
+expr_ref bv2int_translator::mk_le(expr* x, expr* y) {
+    if (a.is_numeral(y))
+        return expr_ref(a.mk_le(x, y), m);
+    if (a.is_numeral(x))
+        return expr_ref(a.mk_ge(y, x), m);
+    return expr_ref(a.mk_le(a.mk_sub(x, y), a.mk_numeral(rational(0), x->get_sort())), m);
+}
+
+expr_ref bv2int_translator::mk_lt(expr* x, expr* y) {
+    return expr_ref(m.mk_not(mk_le(y, x)), m);
+}
+
+
+
 void bv2int_translator::translate_bv(app* e) {
 
     auto bnot = [&](expr* e) {
@@ -229,35 +243,35 @@ void bv2int_translator::translate_bv(app* e) {
         break;
     case OP_ULEQ:
         bv_expr = e->get_arg(0);
-        r = a.mk_le(umod(bv_expr, 0), umod(bv_expr, 1));
+        r = mk_le(umod(bv_expr, 0), umod(bv_expr, 1));
         break;
     case OP_UGEQ:
         bv_expr = e->get_arg(0);
-        r = a.mk_ge(umod(bv_expr, 0), umod(bv_expr, 1));
+        r = mk_ge(umod(bv_expr, 0), umod(bv_expr, 1));
         break;
     case OP_ULT:
         bv_expr = e->get_arg(0);
-        r = a.mk_lt(umod(bv_expr, 0), umod(bv_expr, 1));
+        r = mk_lt(umod(bv_expr, 0), umod(bv_expr, 1));
         break;
     case OP_UGT:
         bv_expr = e->get_arg(0);
-        r = a.mk_gt(umod(bv_expr, 0), umod(bv_expr, 1));
+        r = mk_gt(umod(bv_expr, 0), umod(bv_expr, 1));
         break;
     case OP_SLEQ:
         bv_expr = e->get_arg(0);
-        r = a.mk_le(smod(bv_expr, 0), smod(bv_expr, 1));
+        r = mk_le(smod(bv_expr, 0), smod(bv_expr, 1));
         break;
     case OP_SGEQ:
         bv_expr = e->get_arg(0);
-        r = a.mk_ge(smod(bv_expr, 0), smod(bv_expr, 1));
+        r = mk_ge(smod(bv_expr, 0), smod(bv_expr, 1));
         break;
     case OP_SLT:
         bv_expr = e->get_arg(0);
-        r = a.mk_lt(smod(bv_expr, 0), smod(bv_expr, 1));
+        r = mk_lt(smod(bv_expr, 0), smod(bv_expr, 1));
         break;
     case OP_SGT:
         bv_expr = e->get_arg(0);
-        r = a.mk_gt(smod(bv_expr, 0), smod(bv_expr, 1));
+        r = mk_gt(smod(bv_expr, 0), smod(bv_expr, 1));
         break;
     case OP_BNEG:
         r = a.mk_uminus(arg(0));
@@ -308,7 +322,7 @@ void bv2int_translator::translate_bv(app* e) {
     }
     case OP_BUMUL_NO_OVFL: {
         bv_expr = e->get_arg(0);
-        r = a.mk_lt(mul(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(bv_size(bv_expr)));
+        r = mk_lt(mul(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(bv_size(bv_expr)));
         break;
     }
     case OP_BSHL: {
diff --git a/src/ast/rewriter/bv2int_translator.h b/src/ast/rewriter/bv2int_translator.h
index c84b86f56..67c39c01a 100644
--- a/src/ast/rewriter/bv2int_translator.h
+++ b/src/ast/rewriter/bv2int_translator.h
@@ -47,6 +47,11 @@ class bv2int_translator {
     expr_ref if_eq(expr* n, unsigned k, expr* th, expr* el);
     expr* amod(expr* bv_expr, expr* x, rational const& N);
     rational bv_size(expr* bv_expr);
+    expr_ref mk_le(expr* a, expr* b);
+    expr_ref mk_lt(expr* a, expr* b);
+    expr_ref mk_ge(expr* a, expr* b) { return mk_le(b, a); }
+    expr_ref mk_gt(expr* a, expr* b) { return mk_lt(b, a); }
+    
     
     void translate_bv(app* e);
     void translate_basic(app* e);
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 10c4d0718..6b51e2f69 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2573,6 +2573,14 @@ public:
         return true;
     }
 
+    expr_ref mk_le(expr* x, expr* y) {
+        if (a.is_numeral(y))
+            return expr_ref(a.mk_le(x, y), m);
+        if (a.is_numeral(x))
+            return expr_ref(a.mk_ge(y, x), m);
+        return expr_ref(a.mk_le(a.mk_sub(x, y), a.mk_numeral(rational(0), x->get_sort())), m);
+    }
+
     void mk_bv_axiom(app* n) {
         unsigned sz = 0;
         expr* _x = nullptr, * _y = nullptr;
@@ -2592,8 +2600,8 @@ public:
             // x&y <= y
             // TODO? x = y => x&y = x
 
-            ctx().mk_th_axiom(get_id(), mk_literal(a.mk_le(n, x)));
-            ctx().mk_th_axiom(get_id(), mk_literal(a.mk_le(n, y)));
+            ctx().mk_th_axiom(get_id(), mk_literal(mk_le(n, x)));
+            ctx().mk_th_axiom(get_id(), mk_literal(mk_le(n, y)));
         }
         else if (a.is_shl(n)) {
             // y >= sz => n = 0