diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index b69c628c4..071496577 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1396,6 +1396,11 @@ public:
         }
         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
@@ -1411,12 +1416,10 @@ 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
-            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));
 
             mk_axiom(q_le_0, ~p_ge_0, div_ge_0); 
             mk_axiom(q_le_0, ~p_le_0, div_le_0);