Issue 438 (#10085)

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>

src/ast/bv_decl_plugin.cpp

@@ -997,3 +997,30 @@ app* bv_util::mk_bv_rotate_right(expr* arg, unsigned n) {
     parameter p(n);
     return m_manager.mk_app(get_fid(), OP_ROTATE_RIGHT, 1, &p, 1, &arg);
 }
+
+void bv_util::mk_bv_divrem_bound(expr* t, expr_ref_vector& clause) {
+    clause.reset();
+    if (!is_app(t) || !is_bv_divrem(t))
+        return;
+    expr* a = to_app(t)->get_arg(0);
+    expr* b = to_app(t)->get_arg(1);
+    if (is_numeral(b))
+        return;
+    expr* bound = nullptr;
+    // Use ¬(b ≤u t) instead of (t <u b) and ¬(abs(b) ≤u abs(t)) instead of (abs(t) <u abs(b))
+    // so that all bound atoms are OP_ULEQ (handled by theory_bv::internalize_atom).
+    // OP_ULT is not handled by theory_bv::internalize_atom and would trigger UNREACHABLE.
+    if (is_bv_urem(t) || is_bv_uremi(t))
+        bound = m_manager.mk_not(mk_ule(b, t));
+    else if (is_bv_srem(t) || is_bv_sremi(t) || is_bv_smod(t) || is_bv_smodi(t))
+        bound = m_manager.mk_not(mk_ule(mk_abs(b), mk_abs(t)));
+    else if (is_bv_udiv(t) || is_bv_udivi(t))
+        bound = mk_ule(t, a);
+    else if (is_bv_sdiv(t) || is_bv_sdivi(t))
+        bound = mk_ule(mk_abs(t), mk_abs(a));
+    if (!bound)
+        return;
+    // clause encodes  b != 0 => bound  as the disjunction  (b = 0) \/ bound
+    clause.push_back(m_manager.mk_eq(b, mk_zero(b->get_sort())));
+    clause.push_back(bound);
+}

src/ast/bv_decl_plugin.h

@@ -473,6 +473,7 @@ public:
 
 
     app * mk_ule(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_ULEQ, arg1, arg2); }
+    app * mk_ult(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_ULT, arg1, arg2); }
     app * mk_sle(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_SLEQ, arg1, arg2); }
     app * mk_slt(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_SLT, arg1, arg2); }
     app * mk_extract(unsigned high, unsigned low, expr * n) {
@@ -499,6 +500,25 @@ public:
 
     app * mk_bv_not(expr * arg) { return m_manager.mk_app(get_fid(), OP_BNOT, arg); }
     app * mk_bv_neg(expr * arg) { return m_manager.mk_app(get_fid(), OP_BNEG, arg); }
+    // absolute value: ite(arg <s 0, -arg, arg). Note mk_abs(INT_MIN) = INT_MIN.
+    // Uses ¬(0 ≤s arg) instead of (arg <s 0) so that the ITE condition is OP_NOT(OP_SLEQ)
+    // (handled by theory_bv::internalize_atom) rather than OP_SLT (not handled).
+    app * mk_abs(expr * arg) { return m_manager.mk_ite(mk_sle(mk_zero(arg->get_sort()), arg), arg, mk_bv_neg(arg)); }
+    // Magnitude-bound clause for a division/remainder term t with a symbolic (non-numeral)
+    // divisor. Fills clause with the disjuncts { divisor = 0, bound }, encoding
+    // divisor != 0 => bound, where bound is expressed using only OP_ULEQ and OP_NOT(OP_ULEQ)
+    // (so it can be internalized by theory_bv::internalize_atom):
+    //   urem:      ¬(b ≤u t)          srem/smod: ¬(|b| ≤u |t|)
+    //   udiv:      t ≤u a             sdiv:      |t| ≤u |a|
+    // Leaves clause empty if t is not a division/remainder operator or the divisor is a
+    // numeral. The bound is a bit-vector theory axiom (implied for a non-zero divisor); the
+    // unsigned comparison on absolute values keeps it sound at INT_MIN.
+    bool is_bv_divrem(expr* t) const {
+        return is_bv_urem(t) || is_bv_uremi(t) || is_bv_srem(t) || is_bv_sremi(t) ||
+               is_bv_smod(t) || is_bv_smodi(t) || is_bv_udiv(t) || is_bv_udivi(t) ||
+               is_bv_sdiv(t) || is_bv_sdivi(t);
+    }
+    void mk_bv_divrem_bound(expr* t, expr_ref_vector& clause);
     app * mk_bv_urem(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BUREM, arg1, arg2); }
     app * mk_bv_srem(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSREM, arg1, arg2); }
     app * mk_bv_smod(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSMOD, arg1, arg2); }

src/ast/simplifiers/CMakeLists.txt

@@ -6,6 +6,7 @@ z3_add_component(simplifiers
     bound_propagator.cpp
     bound_simplifier.cpp
     bv_bounds_simplifier.cpp
+    bv_divrem_bounds.cpp
     bv_slice.cpp
     card2bv.cpp
     demodulator_simplifier.cpp

src/ast/simplifiers/bv_divrem_bounds.cpp

@@ -0,0 +1,43 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+Module Name:
+
+    bv_divrem_bounds.cpp
+
+Abstract:
+
+    Simplifier that adds range/bound lemmas for bit-vector division and
+    remainder terms with a non-constant divisor. See bv_divrem_bounds.h.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner)
+
+--*/
+#include "ast/simplifiers/bv_divrem_bounds.h"
+#include "ast/for_each_expr.h"
+
+namespace bv {
+
+    void divrem_bounds::reduce() {
+        expr_ref_vector targets(m), fmls(m), clause(m);
+        for (unsigned i : indices())
+            fmls.push_back(m_fmls[i].fml());
+        for (expr* e : subterms::ground(fmls))
+            if (m_util.is_bv_divrem(e))
+                targets.push_back(e);
+        for (expr* t : targets) {
+            m_util.mk_bv_divrem_bound(t, clause);
+            if (clause.empty())
+                continue;
+            expr_ref lemma(m.mk_or(clause), m);
+            // the lemma is a bit-vector theory axiom (valid with no premises)
+            proof_ref pr(m);
+            if (m.proofs_enabled())
+                pr = m.mk_th_lemma(m_util.get_fid(), lemma, 0, nullptr);
+            m_fmls.add(dependent_expr(m, lemma, pr, nullptr));
+            ++m_num_lemmas;
+        }
+    }
+}

src/ast/simplifiers/bv_divrem_bounds.h

@@ -0,0 +1,64 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+Module Name:
+
+    bv_divrem_bounds.h
+
+Abstract:
+
+    Simplifier that adds range/bound lemmas for bit-vector division and
+    remainder terms with a non-constant divisor.
+
+    Bit-blasting a division circuit with a symbolic divisor hides the algebraic
+    fact that the remainder magnitude is bounded by the divisor magnitude. For a
+    divisor b that is not a numeral the following facts hold and are added as
+    (implied) lemmas so that a downstream bit-blasting + SAT solver can reason
+    about the magnitudes without unfolding the division circuit:
+
+        b != 0 => bvult (bvurem a b) b                 (unsigned remainder)
+        b != 0 => bvult |bvsrem a b| |b|               (signed remainder)
+        b != 0 => bvult |bvsmod a b| |b|               (signed modulo)
+        b != 0 => bvule (bvudiv a b) a                 (unsigned quotient)
+        b != 0 => bvule |bvsdiv a b| |a|               (signed quotient)
+
+    where |x| = ite(x <s 0, -x, x). These lemmas are logically implied by the
+    semantics of the operators for a non-zero divisor, so the transformation
+    preserves satisfiability and all models. The unsigned comparison on the
+    absolute values keeps the bounds sound at INT_MIN: -INT_MIN overflows to
+    INT_MIN whose unsigned value is the maximum magnitude, so the bound only
+    ever loosens, never becomes unsound.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner)
+
+--*/
+#pragma once
+
+#include "ast/bv_decl_plugin.h"
+#include "ast/simplifiers/dependent_expr_state.h"
+
+namespace bv {
+
+    class divrem_bounds : public dependent_expr_simplifier {
+        bv_util  m_util;
+        unsigned m_num_lemmas = 0;
+
+    public:
+        divrem_bounds(ast_manager& m, dependent_expr_state& fmls) :
+            dependent_expr_simplifier(m, fmls), m_util(m) {}
+
+        char const* name() const override { return "bv-divrem-bounds"; }
+
+        void reduce() override;
+
+        bool supports_proofs() const override { return true; }
+
+        void collect_statistics(statistics& st) const override {
+            st.update("bv-divrem-bounds", m_num_lemmas);
+        }
+
+        void reset_statistics() override { m_num_lemmas = 0; }
+    };
+}

src/sat/smt/bv_internalize.cpp

@@ -176,11 +176,11 @@ namespace bv {
         case OP_BNEG:             internalize_un(mk_neg); break;
         case OP_BREDAND:          internalize_un(mk_redand); break;
         case OP_BREDOR:           internalize_un(mk_redor); break;
-        case OP_BSDIV_I:          internalize_bin(mk_sdiv); break;
-        case OP_BUDIV_I:          internalize_bin(mk_udiv); break;
-        case OP_BUREM_I:          internalize_bin(mk_urem); break;
-        case OP_BSREM_I:          internalize_bin(mk_srem); break;
-        case OP_BSMOD_I:          internalize_bin(mk_smod); break;
+        case OP_BSDIV_I:          internalize_bin(mk_sdiv); assert_bv_divrem_bound_axiom(a); break;
+        case OP_BUDIV_I:          internalize_bin(mk_udiv); assert_bv_divrem_bound_axiom(a); break;
+        case OP_BUREM_I:          internalize_bin(mk_urem); assert_bv_divrem_bound_axiom(a); break;
+        case OP_BSREM_I:          internalize_bin(mk_srem); assert_bv_divrem_bound_axiom(a); break;
+        case OP_BSMOD_I:          internalize_bin(mk_smod); assert_bv_divrem_bound_axiom(a); break;
         case OP_BSHL:             internalize_bin(mk_shl); break;
         case OP_BLSHR:            internalize_bin(mk_lshr); break;
         case OP_BASHR:            internalize_bin(mk_ashr); break;
@@ -544,6 +544,20 @@ namespace bv {
         internalize_binary(a, bin);
     }
 
+    // Add, on the fly, the magnitude bound axioms for division/remainder operators.
+    // Uses the shared bv_util::mk_bv_divrem_bound clause builder so the axiom matches the one
+    // produced by the bv-divrem-bounds simplifier. Only fires for a symbolic divisor.
+    void solver::assert_bv_divrem_bound_axiom(app* a) {
+        expr_ref_vector clause(m);
+        bv.mk_bv_divrem_bound(a, clause);
+        if (clause.empty())
+            return;
+        sat::literal_vector lits;
+        for (expr* e : clause)
+            lits.push_back(mk_literal(e));
+        add_clause(lits);
+    }
+
     void solver::internalize_interp(app* n, std::function<expr* (expr*, expr*)>& ibin, std::function<expr* (expr*)>& iun) {
         bv_rewriter_params p(s().params());
         expr* arg1 = n->get_arg(0);

src/sat/smt/bv_solver.h

@@ -288,6 +288,7 @@ namespace bv {
         void internalize_bit2bool(app* n);
         void internalize_overflow(app* n);
         void internalize_udiv_i(app* n);
+        void assert_bv_divrem_bound_axiom(app* n);
         template<bool Signed, bool Reverse, bool Negated>
         void internalize_le(app* n);
         void assert_bv2int_axiom(app * n);

src/smt/theory_bv.cpp

@@ -908,15 +908,15 @@ namespace smt {
         case OP_BADD:           internalize_add(term); return true;
         case OP_BSUB:           internalize_sub(term); return true;
         case OP_BMUL:           internalize_mul(term); return true;
-        case OP_BSDIV_I:        internalize_sdiv(term); return true;
+        case OP_BSDIV_I:        internalize_sdiv(term); if (!ctx.relevancy()) assert_bv_divrem_bound_axiom(term); return true;
 #if ENABLE_QUOT_REM_ENCODING
-        case OP_BUDIV_I:        internalize_udiv_quot_rem(term); return true;
+        case OP_BUDIV_I:        internalize_udiv_quot_rem(term); if (!ctx.relevancy()) assert_bv_divrem_bound_axiom(term); return true;
 #else
-        case OP_BUDIV_I:        internalize_udiv(term); return true;
+        case OP_BUDIV_I:        internalize_udiv(term); if (!ctx.relevancy()) assert_bv_divrem_bound_axiom(term); return true;
 #endif
-        case OP_BSREM_I:        internalize_srem(term); return true;
-        case OP_BUREM_I:        internalize_urem(term); return true;
-        case OP_BSMOD_I:        internalize_smod(term); return true;
+        case OP_BSREM_I:        internalize_srem(term); if (!ctx.relevancy()) assert_bv_divrem_bound_axiom(term); return true;
+        case OP_BUREM_I:        internalize_urem(term); if (!ctx.relevancy()) assert_bv_divrem_bound_axiom(term); return true;
+        case OP_BSMOD_I:        internalize_smod(term); if (!ctx.relevancy()) assert_bv_divrem_bound_axiom(term); return true;
         case OP_BAND:           internalize_and(term); return true;
         case OP_BOR:            internalize_or(term); return true;
         case OP_BNOT:           internalize_not(term); return true;
@@ -1395,6 +1395,11 @@ namespace smt {
     void theory_bv::relevant_eh(expr * n) {
         TRACE(arith, tout << "relevant: #" << n->get_id() << " " << ctx.e_internalized(n) << ": " << mk_bounded_pp(n, m) << "\n";);
         TRACE(bv, tout << "relevant: #" << n->get_id() << " " << ctx.e_internalized(n) << ": " << mk_pp(n, m) << "\n";);
+        if (ctx.relevancy() && m_util.is_bv_divrem(n)) {
+            ctx.mark_as_relevant(to_app(n)->get_arg(0));
+            ctx.mark_as_relevant(to_app(n)->get_arg(1));
+            assert_bv_divrem_bound_axiom(to_app(n));
+        }
         if (m.is_bool(n)) {
             if (!ctx.b_internalized(n))
                 return;
@@ -2070,5 +2075,19 @@ namespace smt {
     }
 #endif
 
+    // Add, on the fly, the magnitude bound axioms for division/remainder operators.
+    // Uses the shared bv_util::mk_bv_divrem_bound clause builder so the axiom matches the
+    // one produced by the bv-divrem-bounds simplifier. Only fires for a symbolic divisor.
+    void theory_bv::assert_bv_divrem_bound_axiom(app * n) {
+        expr_ref_vector clause(m);
+        m_util.mk_bv_divrem_bound(n, clause);
+        if (clause.empty())
+            return;
+        literal_vector lits;
+        for (expr* e : clause)
+            lits.push_back(mk_literal(e));
+        ctx.mk_th_axiom(get_id(), lits.size(), lits.data());
+    }
+
 
 }

src/smt/theory_bv.h

@@ -229,6 +229,7 @@ namespace smt {
         void assert_int2bv_axiom(app* n);
         void assert_bv2int_axiom(app* n);
         void assert_udiv_quot_rem_axiom(app * n);
+        void assert_bv_divrem_bound_axiom(app * n);
 
 
     protected:

src/tactic/bv/CMakeLists.txt

@@ -18,6 +18,7 @@ z3_add_component(bv_tactics
     bv1_blaster_tactic.h
     bv_bound_chk_tactic.h
     bv_bounds_tactic.h
+    bv_divrem_bounds_tactic.h
     bv_size_reduction_tactic.h
     bv_slice_tactic.h
     bvarray2uf_tactic.h

src/tactic/bv/bv_divrem_bounds_tactic.h

@@ -0,0 +1,63 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+Module Name:
+
+    bv_divrem_bounds_tactic.h
+
+Abstract:
+
+    Tactic wrapper around the bv::divrem_bounds simplifier. It adds range
+    lemmas for bit-vector division and remainder terms with a non-constant
+    divisor. See ast/simplifiers/bv_divrem_bounds.h for details.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner)
+
+Tactic Documentation
+
+## Tactic bv-divrem-bounds
+
+### Short Description
+
+Add range lemmas for bit-vector division/remainder terms with a symbolic divisor.
+
+### Long Description
+
+For a divisor `b` that is not a numeral, the remainder magnitude is bounded by
+the divisor magnitude and the unsigned quotient is bounded by the dividend.
+These facts are hidden once a division circuit is bit-blasted, so the tactic
+emits them as implied lemmas up front, letting a downstream SAT solver reason
+about magnitudes without unfolding the circuit.
+
+### Example
+
+```z3
+(declare-const a (_ BitVec 8))
+(declare-const b (_ BitVec 8))
+(declare-const c (_ BitVec 8))
+(assert (= (bvsrem a (bvadd b c)) #x05))
+(apply bv-divrem-bounds)
+```
+
+--*/
+#pragma once
+
+#include "util/params.h"
+#include "tactic/tactic.h"
+#include "tactic/dependent_expr_state_tactic.h"
+#include "ast/simplifiers/bv_divrem_bounds.h"
+
+class ast_manager;
+class tactic;
+
+inline tactic* mk_bv_divrem_bounds_tactic(ast_manager& m, params_ref const& p = params_ref()) {
+    return alloc(dependent_expr_state_tactic, m, p,
+                 [](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* { return alloc(bv::divrem_bounds, m, s); });
+}
+
+/*
+  ADD_TACTIC("bv-divrem-bounds", "add range lemmas for bit-vector division/remainder terms with a symbolic divisor.", "mk_bv_divrem_bounds_tactic(m, p)")
+  ADD_SIMPLIFIER("bv-divrem-bounds", "add range lemmas for bit-vector division/remainder terms with a symbolic divisor.", "alloc(bv::divrem_bounds, m, s)")
+*/

src/tactic/smtlogics/qfaufbv_tactic.cpp

@@ -23,6 +23,7 @@ Notes:
 #include "tactic/core/elim_uncnstr_tactic.h"
 #include "tactic/bv/max_bv_sharing_tactic.h"
 #include "tactic/bv/bv_size_reduction_tactic.h"
+#include "tactic/bv/bv_divrem_bounds_tactic.h"
 #include "tactic/core/ctx_simplify_tactic.h"
 #include "tactic/smtlogics/qfbv_tactic.h"
 #include "tactic/smtlogics/smt_tactic.h"
@@ -42,6 +43,7 @@ static tactic * mk_qfaufbv_preamble(ast_manager & m, params_ref const & p) {
                     mk_propagate_values_tactic(m),
                     mk_solve_eqs_tactic(m),
                     mk_elim_uncnstr_tactic(m),
+                    mk_bv_divrem_bounds_tactic(m),
                     // sound to use? if_no_proofs(if_no_unsat_cores(mk_reduce_args_tactic(m))),
                     if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
                     using_params(mk_simplify_tactic(m), simp2_p),

src/tactic/smtlogics/qfbv_tactic.cpp

@@ -25,6 +25,7 @@ Notes:
 #include "tactic/bv/bv1_blaster_tactic.h"
 #include "tactic/bv/max_bv_sharing_tactic.h"
 #include "tactic/bv/bv_size_reduction_tactic.h"
+#include "tactic/bv/bv_divrem_bounds_tactic.h"
 #include "tactic/aig/aig_tactic.h"
 #include "sat/tactic/sat_tactic.h"
 #include "sat/sat_solver/inc_sat_solver.h"
@@ -63,6 +64,7 @@ static tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {
             using_params(mk_propagate_values_tactic(m), flat_and_or_p),
             using_params(mk_solve_eqs_tactic(m), solve_eq_p),
             mk_elim_uncnstr_tactic(m),
+            mk_bv_divrem_bounds_tactic(m),
             if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
             using_params(mk_simplify_tactic(m), simp2_p),