diff --git a/src/ast/rewriter/bv2int_translator.cpp b/src/ast/rewriter/bv2int_translator.cpp
index b8696923c0..3da2c0e8d5 100644
--- a/src/ast/rewriter/bv2int_translator.cpp
+++ b/src/ast/rewriter/bv2int_translator.cpp
@@ -428,7 +428,10 @@ void bv2int_translator::translate_bv(app* e) {
     case OP_INT2BV:
         m_int2bv.push_back(e);
         ctx.push(push_back_vector(m_int2bv));
-        r = arg(0);
+        // Normalize the integer argument to [0, 2^N) so that bitwise operations
+        // on int_to_bv produce correct results when the argument is negative or
+        // otherwise outside the valid range.
+        r = umod(e, 0);
         break;
     case OP_UBV2INT:
         m_bv2int.push_back(e);
@@ -697,6 +700,9 @@ expr* bv2int_translator::amod(expr* bv_expr, expr* x, rational const& N) {
         r = x;
     else if (a.is_mod(x, t, e) && a.is_numeral(t, v) && 0 <= v && v < N)
         r = x;
+    else if (a.is_mod(x, t, e) && a.is_numeral(e, v) && v == N)
+        // mod(t, N) is already in [0, N); no need to wrap it again.
+        r = x;
     else if (a.is_numeral(x, v))
         r = a.mk_int(mod(v, N));
     else if (is_bounded(x, N))