From 7198d093c8d34fbdeb69204e2c44f7e25eed04ea Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 2 Jun 2026 21:30:36 +0000
Subject: [PATCH] Constant-fold unsigned division/remainder in bv_utils

bv_utilst::unsigned_divider always allocated fresh variables for the
quotient and remainder, with a quotient*divisor + rem == dividend
multiplier constraint, even when both operands are constant.  The result
was therefore never a constant literal, so a constant division feeding a
later multiply produced a (hard) variable*variable multiplier instead of
folding away.

Add a fast path: when both operands are constant (and the divisor is
non-zero), compute the quotient and remainder directly as constants.
Division by zero falls through to the existing nondeterministic encoding,
so semantics are unchanged.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 src/solvers/flattening/bv_utils.cpp  | 20 +++++++++++
 unit/solvers/flattening/bv_utils.cpp | 52 ++++++++++++++++++++++++++++
 2 files changed, 72 insertions(+)

diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp
index b487207bb6f..3eac829ca0b 100644
--- a/src/solvers/flattening/bv_utils.cpp
+++ b/src/solvers/flattening/bv_utils.cpp
@@ -1163,6 +1163,26 @@ void bv_utilst::unsigned_divider(
 {
   std::size_t width=op0.size();
 
+  // If both operands are constant, compute the result directly so it folds to
+  // constant literals downstream instead of introducing fresh variables and a
+  // multiplier constraint.  Division by zero falls through to the general
+  // (non-deterministic) encoding below.
+  if(is_constant(op0) && is_constant(op1))
+  {
+    mp_integer n0 = 0, n1 = 0;
+    for(std::size_t i = width; i-- > 0;)
+    {
+      n0 = (n0 << 1) + (op0[i].is_true() ? 1 : 0);
+      n1 = (n1 << 1) + (op1[i].is_true() ? 1 : 0);
+    }
+    if(n1 != 0)
+    {
+      res = build_constant(n0 / n1, width);
+      rem = build_constant(n0 % n1, width);
+      return;
+    }
+  }
+
   // check if we divide by a power of two
   #if 0
   {
diff --git a/unit/solvers/flattening/bv_utils.cpp b/unit/solvers/flattening/bv_utils.cpp
index cf19ae5c85c..1f467755dd2 100644
--- a/unit/solvers/flattening/bv_utils.cpp
+++ b/unit/solvers/flattening/bv_utils.cpp
@@ -17,6 +17,7 @@ Author: Daniel Kroening
 #include <util/symbol_table.h>
 
 #include <solvers/flattening/boolbv.h>
+#include <solvers/flattening/bv_utils.h>
 #include <solvers/sat/satcheck.h>
 #include <testing-utils/use_catch.h>
 
@@ -82,3 +83,54 @@ SCENARIO("1-bit signed less-than", "[core][solvers][flattening][bv_utils]")
     }
   }
 }
+
+SCENARIO(
+  "unsigned_divider folds constant operands",
+  "[core][solvers][flattening][bv_utils]")
+{
+  console_message_handlert message_handler;
+  message_handler.set_verbosity(0);
+
+  GIVEN("a bv_utilst over a SAT back-end")
+  {
+    satcheckt satcheck(message_handler);
+    bv_utilst bv_utils(satcheck);
+    const std::size_t width = 32;
+
+    WHEN("dividing two constants 100 / 7")
+    {
+      bvt res, rem;
+      bv_utils.divider(
+        bv_utilst::build_constant(100, width),
+        bv_utilst::build_constant(7, width),
+        res,
+        rem,
+        bv_utilst::representationt::UNSIGNED);
+
+      THEN("the result is constant (no fresh variables) and correct")
+      {
+        REQUIRE(bv_utilst::is_constant(res));
+        REQUIRE(bv_utilst::is_constant(rem));
+        REQUIRE(res == bv_utilst::build_constant(14, width));
+        REQUIRE(rem == bv_utilst::build_constant(2, width));
+      }
+    }
+
+    WHEN("dividing a constant by a constant zero")
+    {
+      bvt res, rem;
+      bv_utils.divider(
+        bv_utilst::build_constant(100, width),
+        bv_utilst::build_constant(0, width),
+        res,
+        rem,
+        bv_utilst::representationt::UNSIGNED);
+
+      THEN("the fall-through (nondeterministic) encoding is used")
+      {
+        // division by zero must not be folded; it keeps fresh variables
+        REQUIRE_FALSE(bv_utilst::is_constant(res));
+      }
+    }
+  }
+}