From 847ee63b2d6034160cb0539ca98ad4e2a847fecf Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Wed, 22 Jul 2026 10:34:23 -0700
Subject: [PATCH] Fix invalid model from int_to_bv missing modular reduction in
 bv2int_translator (#10185)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

With `smt.bv.solver=2`, `int_to_bv(x)` was translated to the raw integer
`x` without normalizing it to `[0, 2^N)`. Bitwise operations like
`bvxor(A, B)` are translated as `A + B - 2·band(A, B)`, which is only
valid when both operands are in `[0, 2^N)`. When `x` was negative or ≥
2^N, the LP solver could assign a band value inconsistent with bit
semantics, producing a model that fails validation.

## Changes

- **`OP_INT2BV` translation** (`translate_bv`): Apply `umod(e, 0)`
instead of passing the raw integer argument through. This normalizes the
value to `[0, 2^N)` before it participates in any bitwise arithmetic.

  ```cpp
  // Before
  case OP_INT2BV:
      r = arg(0);  // raw integer, may be negative or ≥ 2^N

  // After
  case OP_INT2BV:
      r = umod(e, 0);  // normalized to [0, 2^N)
  ```

- **`amod` shortcut**: Add a fast-path for `mod(t, N)` when the divisor
already equals `N` — the result is already in `[0, N)`, so wrapping it
again with another `mod(_, N)` is unnecessary and avoids expression
bloat.

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
---
 src/ast/rewriter/bv2int_translator.cpp | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

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))