diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index 77ded074b..4ec0b3883 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -975,6 +975,10 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
         result = arg1; 
         return BR_DONE; 
     } 
+    if (m_util.is_numeral(arg2, v2, is_int) && v2.is_minus_one()) {
+        result = m_util.mk_mul(m_util.mk_int(-1), arg1); 
+        return BR_REWRITE1; 
+    }
     if (m_util.is_numeral(arg2, v2, is_int) && v2.is_zero()) { 
         return BR_FAILED; 
     } 
@@ -1119,7 +1123,7 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
         return BR_DONE;
     }
 
-    if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_one()) {
+    if (m_util.is_numeral(arg2, v2, is_int) && is_int && (v2.is_one() || v2.is_minus_one())) {
         result = m_util.mk_numeral(numeral(0), true);
         return BR_DONE;
     }
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index f58b3dfc1..fcc1550bb 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1325,12 +1325,14 @@ public:
             mk_axiom(q_le_0, m_le_0);
             return;
         }
+#if 0
+        expr_ref eqr(m.mk_eq(a.mk_add(a.mk_mul(q, div), mod), p), m);
+        ctx().get_rewriter()(eqr);
+        literal eq = mk_literal(eqr);
+#else
         literal eq         = th.mk_eq(a.mk_add(a.mk_mul(q, div), mod), p, false);
+#endif
         literal mod_ge_0   = mk_literal(a.mk_ge(mod, zero));
-        literal div_ge_0   = mk_literal(a.mk_ge(div, zero));
-        literal div_le_0   = mk_literal(a.mk_le(div, zero));
-        literal p_ge_0     = mk_literal(a.mk_ge(p, zero));
-        literal p_le_0     = mk_literal(a.mk_le(p, zero));
 
         rational k(0);
         expr_ref upper(m);
@@ -1361,9 +1363,18 @@ public:
                 if_trace_stream _ts(m, log);
             }
 
+#if 0
+            // creates more literals than useful.
+            literal div_ge_0   = mk_literal(a.mk_ge(div, zero));
+            literal div_le_0   = mk_literal(a.mk_le(div, zero));
+            literal p_ge_0     = mk_literal(a.mk_ge(p, zero));
+            literal p_le_0     = mk_literal(a.mk_le(p, zero));
+
             if (k.is_pos()) {
                 mk_axiom(~p_ge_0, div_ge_0);                
                 mk_axiom(~p_le_0, div_le_0);
+                mk_axiom(p_ge_0, ~div_ge_0);                
+                mk_axiom(p_le_0, ~div_le_0);
                 std::function<void(void)> log = [&,this]() {
                     th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var())));
                     th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var())));
@@ -1373,14 +1384,22 @@ public:
             else {
                 mk_axiom(~p_ge_0, div_le_0);
                 mk_axiom(~p_le_0, div_ge_0);
+                mk_axiom(p_ge_0, ~div_le_0);
+                mk_axiom(p_le_0, ~div_ge_0);
                 std::function<void(void)> log = [&,this]() {
                     th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var())));
                     th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var())));
                 };
                 if_trace_stream _ts(m, log);
             }
+#endif
         }
         else {
+            literal div_ge_0   = mk_literal(a.mk_ge(div, zero));
+            literal div_le_0   = mk_literal(a.mk_le(div, zero));
+            literal p_ge_0     = mk_literal(a.mk_ge(p, zero));
+            literal p_le_0     = mk_literal(a.mk_le(p, zero));
+
             // q >= 0 or p = (p mod q) + q * (p div q)
             // q <= 0 or p = (p mod q) + q * (p div q)
             // q >= 0 or (p mod q) >= 0
@@ -1396,20 +1415,30 @@ public:
             mk_axiom(q_le_0, mod_ge_0);
             mk_axiom(q_le_0, ~mk_literal(a.mk_ge(a.mk_sub(mod, q), zero)));            
             mk_axiom(q_ge_0, ~mk_literal(a.mk_ge(a.mk_add(mod, q), zero)));        
+#if 0
+            // seem expensive
             mk_axiom(q_le_0, ~p_ge_0, div_ge_0); 
             mk_axiom(q_le_0, ~p_le_0, div_le_0); 
             mk_axiom(q_ge_0, ~p_ge_0, div_le_0);             
             mk_axiom(q_ge_0, ~p_le_0, div_ge_0);
+
+            mk_axiom(q_le_0, p_ge_0, ~div_ge_0); 
+            mk_axiom(q_le_0, p_le_0, ~div_le_0); 
+            mk_axiom(q_ge_0, p_ge_0, ~div_le_0);             
+            mk_axiom(q_ge_0, p_le_0, ~div_ge_0);
+#endif
  
             std::function<void(void)> log = [&,this]() {
                 th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var()))); 
                 th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var()))); 
                 th.log_axiom_unit(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_sub(mod, q), zero)));
                 th.log_axiom_unit(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_add(mod, q), zero)));
+#if 0
                 th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var())));
                 th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var())));
                 th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var())));
                 th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var())));
+#endif
             };
             if_trace_stream _ts(m, log);
         }