diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp
index e594b8bc6..49736e4c3 100644
--- a/src/sat/smt/arith_axioms.cpp
+++ b/src/sat/smt/arith_axioms.cpp
@@ -168,6 +168,9 @@ namespace arith {
             add_clause(eqz, mod_ge_0);
             add_clause(eqz, mod_lt_q);
 
+            if (!a.is_uminus(q))
+                add_clause(mk_literal(m.mk_eq(mod, a.mk_mod(p, a.mk_uminus(q)))));
+
 #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_lra.cpp b/src/smt/theory_lra.cpp
index 5eba2eba1..8c6dbead1 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1301,8 +1301,8 @@ public:
             mk_axiom(eqz, eq);
             mk_axiom(eqz, mod_ge_0);
             mk_axiom(eqz, mod_lt_q);
-//            if (!a.is_uminus(q)) 
-//                mk_axiom(mk_literal(m.mk_eq(mod, a.mk_mod(p, a.mk_uminus(q)))));
+            if (!a.is_uminus(q)) 
+                mk_axiom(mk_literal(m.mk_eq(mod, a.mk_mod(p, a.mk_uminus(q)))));
             
             m_arith_eq_adapter.mk_axioms(th.ensure_enode(mod_r), th.ensure_enode(p));