diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp
index 677fd703c..875a65619 100644
--- a/src/sat/smt/arith_axioms.cpp
+++ b/src/sat/smt/arith_axioms.cpp
@@ -168,6 +168,13 @@ namespace arith {
             add_clause(eqz, mod_ge_0);
             add_clause(eqz, mod_lt_q);
 
+            // Add basic mod axiom for abs handling  
+            // (mod x y) = (mod x -y) when y != 0 - fundamental property for divisibility
+            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);
+
 #if 0
             /*literal div_ge_0   = */ mk_literal(a.mk_ge(div, zero));
             /*literal div_le_0   = */ mk_literal(a.mk_le(div, zero));
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index c657e4671..8b941a3d8 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -582,6 +582,12 @@ namespace smt {
             mk_axiom(eqz, lower, false);
             mk_axiom(eqz, upper, !m_util.is_numeral(abs_divisor));
 
+            // Add basic mod axioms for abs handling
+            // (mod x y) = (mod x -y) when y != 0 - fundamental property for divisibility
+            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));
+
             rational k;
 
             m_arith_eq_adapter.mk_axioms(ensure_enode(qr), ensure_enode(dividend));