diff --git a/README b/README
index 1ca0cd577..074abd2a3 100644
--- a/README
+++ b/README
@@ -41,3 +41,5 @@ Remark: clang does not support OpenMP yet.
    cd build
    make
 
+
+To clean Z3 you can delete the build directory and run the mk_make.py script again.
\ No newline at end of file
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index f3f2d4948..957d5ebe7 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3321,13 +3321,13 @@ namespace smt {
                 CASSERT("dyn_ack", check_clauses(m_lemmas) && check_clauses(m_aux_clauses));
             }
             
-            if (resource_limits_exceeded()) {
-                SASSERT(!inconsistent());
+            if (resource_limits_exceeded() && !inconsistent()) {
                 return l_undef;
             }
 
             if (m_base_lvl == m_scope_lvl && m_fparams.m_simplify_clauses)
                 simplify_clauses();
+
             
             if (!decide()) {
                 final_check_status fcs = final_check();
@@ -3342,8 +3342,7 @@ namespace smt {
                 }
             }
 
-            if (resource_limits_exceeded()) {
-                SASSERT(!inconsistent());
+            if (resource_limits_exceeded() && !inconsistent()) {
                 return l_undef;
             }
         }
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 66d232227..a7f442e1f 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -336,8 +336,9 @@ namespace smt {
     theory_var theory_arith<Ext>::internalize_rem(app * n) {
         theory_var s  = mk_binary_op(n);
         context & ctx = get_context();
-        if (!ctx.relevancy())
+        if (!ctx.relevancy()) {
             mk_rem_axiom(n->get_arg(0), n->get_arg(1));
+        }
         return s;
     }
 
@@ -456,22 +457,20 @@ namespace smt {
 
     template<typename Ext>
     void theory_arith<Ext>::mk_rem_axiom(expr * dividend, expr * divisor) {
-        if (!m_util.is_zero(divisor)) {
-            // if divisor is zero, then rem is an uninterpreted function.
-            ast_manager & m    = get_manager();
-            expr * zero        = m_util.mk_numeral(rational(0), true);
-            expr * rem         = m_util.mk_rem(dividend, divisor);
-            expr * mod         = m_util.mk_mod(dividend, divisor);
-            expr_ref dltz(m), eq1(m), eq2(m);
-            dltz               = m_util.mk_lt(divisor, zero);
-            eq1                = m.mk_eq(rem, mod);
-            eq2                = m.mk_eq(rem, m_util.mk_sub(zero, mod));
-            // n < 0 || rem(a,n) = mod(a, n)
-            mk_axiom(dltz, eq1);
-            dltz               = m.mk_not(dltz);
-            // !n < 0 || rem(a,n) = -mod(a, n)
-            mk_axiom(dltz, eq2);
-        }
+        // if divisor is zero, then rem is an uninterpreted function.
+        ast_manager & m    = get_manager();
+        expr * zero        = m_util.mk_numeral(rational(0), true);
+        expr * rem         = m_util.mk_rem(dividend, divisor);
+        expr * mod         = m_util.mk_mod(dividend, divisor);
+        expr_ref dltz(m), eq1(m), eq2(m);
+        dltz               = m_util.mk_lt(divisor, zero);
+        eq1                = m.mk_eq(rem, mod);
+        eq2                = m.mk_eq(rem, m_util.mk_sub(zero, mod));
+        // n < 0 || rem(a,n) = mod(a, n)
+        mk_axiom(dltz, eq1);
+        dltz               = m.mk_not(dltz);
+        // !n < 0 || rem(a,n) = -mod(a, n)
+        mk_axiom(dltz, eq2);        
     }
 
     //