diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp
index d46bdde5a..919a3c3af 100644
--- a/src/qe/qe_arith.cpp
+++ b/src/qe/qe_arith.cpp
@@ -67,6 +67,9 @@ namespace qe {
                        CTRACE("qe", !m.is_true(val), tout << mk_pp(lit, m) << " := " << val << "\n";);
                        SASSERT(m.canceled() || m.is_true(val)););
 
+            if (!m.inc()) 
+                return false;
+            
             TRACE("opt", tout << mk_pp(lit, m) << " " << a.is_lt(lit) << " " << a.is_gt(lit) << "\n";);
             bool is_not = m.is_not(lit, lit);
             if (is_not) {