diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp
index f7896e63c..677fd703c 100644
--- a/src/sat/smt/arith_axioms.cpp
+++ b/src/sat/smt/arith_axioms.cpp
@@ -208,11 +208,27 @@ namespace arith {
                 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
+                // 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);
+                
+                // Add conditional axioms for the ite form that abs gets rewritten to
+                // (mod x (ite (>= y 0) y (-y))) should equal (mod x y) when y >= 0
+                // (mod x (ite (>= y 0) y (-y))) should equal (mod x (-y)) when y < 0
+                expr_ref q_ge_0(a.mk_ge(q, zero), m);
+                expr_ref ite_divisor(m.mk_ite(q_ge_0, q, neg_q), m);
+                expr_ref mod_ite(a.mk_mod(p, ite_divisor), m);
+                
+                // When y >= 0: mod(x, ite(...)) = mod(x, y)
+                literal q_ge_0_lit = mk_literal(q_ge_0);
+                literal mod_ite_eq_mod = mk_literal(m.mk_eq(mod_ite, mod));
+                add_clause(eqz, ~q_ge_0_lit, mod_ite_eq_mod);
+                
+                // When y < 0: mod(x, ite(...)) = mod(x, -y)  
+                literal mod_ite_eq_mod_neg = mk_literal(m.mk_eq(mod_ite, mod_neg));
+                add_clause(eqz, q_ge_0_lit, mod_ite_eq_mod_neg);
             }
 
 
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 717fdf6a7..c657e4671 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -623,6 +623,19 @@ namespace smt {
                 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));
+                
+                // Add conditional axioms for the ite form that abs gets rewritten to
+                expr_ref divisor_ge_0(m_util.mk_ge(divisor, zero), m);
+                expr_ref ite_divisor(m.mk_ite(divisor_ge_0, divisor, neg_divisor), m);
+                expr_ref mod_ite(m_util.mk_mod(dividend, ite_divisor), m);
+                
+                // When y >= 0: mod(x, ite(...)) = mod(x, y)
+                expr_ref ante1(m.mk_and(m.mk_not(eqz), divisor_ge_0), m);
+                mk_axiom(ante1, m.mk_eq(mod_ite, mod));
+                
+                // When y < 0: mod(x, ite(...)) = mod(x, -y)  
+                expr_ref ante2(m.mk_and(m.mk_not(eqz), m.mk_not(divisor_ge_0)), m);
+                mk_axiom(ante2, m.mk_eq(mod_ite, mod_neg));
             }
 
             if (m_params.m_arith_enum_const_mod && m_util.is_numeral(divisor, k) &&