From b38497ac910de7b7750c93518ebc02c8ab1e994f Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 15 Aug 2025 00:10:06 +0000
Subject: [PATCH] Add mod axioms for abs divisor handling

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/sat/smt/arith_axioms.cpp | 13 +++++++++++++
 src/smt/theory_arith_core.h  | 11 +++++++++++
 2 files changed, 24 insertions(+)

diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp
index e594b8bc6..f7896e63c 100644
--- a/src/sat/smt/arith_axioms.cpp
+++ b/src/sat/smt/arith_axioms.cpp
@@ -200,6 +200,19 @@ namespace arith {
             else if (!a.is_numeral(q)) {
                 // (or (= y 0)  (<= (* y (div x y)) x))
                 add_clause(eqz, mk_literal(a.mk_le(a.mk_mul(q, div), p)));
+                
+                // Add axiom: (mod x y) = (mod x -y) when y != 0
+                // This is needed for divisibility problems to work correctly with abs(y)
+                expr_ref neg_q(a.mk_uminus(q), m);
+                expr_ref mod_neg(a.mk_mod(p, neg_q), m);
+                literal mod_eq_mod_neg = mk_literal(m.mk_eq(mod, mod_neg));
+                add_clause(eqz, mod_eq_mod_neg);
+                
+                // Also add the axiom for abs: (mod x y) = (mod x abs(y)) when y != 0
+                expr_ref abs_q(m.mk_ite(a.mk_ge(q, zero), q, a.mk_uminus(q)), m);
+                expr_ref mod_abs(a.mk_mod(p, abs_q), m);
+                literal mod_eq_mod_abs = mk_literal(m.mk_eq(mod, mod_abs));
+                add_clause(eqz, mod_eq_mod_abs);
             }
 
 
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 6f40cab0f..717fdf6a7 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -612,6 +612,17 @@ namespace smt {
                 s(div_ge);                
                 mk_axiom(eqz, div_ge, false);
                 TRACE(arith, tout << eqz << " " << div_ge << "\n");
+                
+                // Add axiom: (mod x y) = (mod x -y) when y != 0
+                // This is needed for divisibility problems to work correctly with abs(y)
+                expr_ref neg_divisor(m_util.mk_uminus(divisor), m);
+                expr_ref mod_neg(m_util.mk_mod(dividend, neg_divisor), m);
+                mk_axiom(eqz, m.mk_eq(mod, mod_neg));
+                
+                // Also add the axiom for abs: (mod x y) = (mod x abs(y)) when y != 0
+                expr_ref abs_divisor(m.mk_ite(m_util.mk_ge(divisor, zero), divisor, m_util.mk_uminus(divisor)), m);
+                expr_ref mod_abs(m_util.mk_mod(dividend, abs_divisor), m);
+                mk_axiom(eqz, m.mk_eq(mod, mod_abs));
             }
 
             if (m_params.m_arith_enum_const_mod && m_util.is_numeral(divisor, k) &&