fixes #1171

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/simplex/model_based_opt.cpp

@@ -18,8 +18,9 @@ Revision History:
 
 --*/
 
-#include "model_based_opt.h"
-#include "uint_set.h"
+#include "math/simplex/model_based_opt.h"
+#include "util/uint_set.h"
+#include "util/z3_exception.h"
 
 std::ostream& operator<<(std::ostream& out, opt::ineq_type ie) {
     switch (ie) {
@@ -868,6 +869,9 @@ namespace opt {
         for (unsigned i = 0; i < mod_rows.size(); ++i) {
             D = lcm(D, m_rows[mod_rows[i]].m_mod);            
         }
+        if (D.is_zero()) {
+            throw default_exception("modulo 0 is not defined");
+        }
         TRACE("opt", display(tout << "lcm: " << D << " tableau\n"););
         rational val_x = m_var2value[x];
         rational u = mod(val_x, D);

src/qe/qe_arith.cpp

@@ -90,8 +90,8 @@ namespace qe {
                 rational r1, r2;
                 expr_ref val1 = eval(e1); 
                 expr_ref val2 = eval(e2);
-                VERIFY(a.is_numeral(val1, r1));
-                VERIFY(a.is_numeral(val2, r2));
+                if (!a.is_numeral(val1, r1)) return false;
+                if (!a.is_numeral(val2, r2)) return false;
                 SASSERT(r1 != r2);
                 if (r1 < r2) {
                     std::swap(e1, e2);
@@ -107,7 +107,7 @@ namespace qe {
                 vector<std::pair<expr*,rational> > nums;
                 for (unsigned i = 0; i < alit->get_num_args(); ++i) {
                     val = eval(alit->get_arg(i));
-                    VERIFY(a.is_numeral(val, r));
+                    if (!a.is_numeral(val, r)) return false;
                     nums.push_back(std::make_pair(alit->get_arg(i), r));
                 }
                 std::sort(nums.begin(), nums.end(), compare_second());
@@ -129,7 +129,7 @@ namespace qe {
                     expr* arg1 = to_app(lit)->get_arg(i), *arg2 = 0;
                     rational r;
                     expr_ref val = eval(arg1);
-                    VERIFY(a.is_numeral(val, r));
+                    if (!a.is_numeral(val, r)) return false;
                     if (values.find(r, arg2)) {
                         ty = opt::t_eq;
                         linearize(mbo, eval,  mul, arg1, c, fmls, ts, tids);
@@ -196,7 +196,7 @@ namespace qe {
                     linearize(mbo, eval, mul, t3, c, fmls, ts, tids);
                 }
             }
-            else if (a.is_mod(t, t1, t2) && is_numeral(t2, mul1)) {
+            else if (a.is_mod(t, t1, t2) && is_numeral(t2, mul1) && !mul1.is_zero()) {
                 rational r;
                 val = eval(t);
                 VERIFY(a.is_numeral(val, r));

src/test/mpff.cpp

@@ -317,9 +317,7 @@ static void tst_power(unsigned prec = 2) {
     ENSURE(m.eq(a, b));
 
     // checking special support for powers of 2 
-#ifdef Z3DEBUG
     unsigned k;
-#endif
     m.set(a, 1);
     ENSURE(m.is_power_of_two(a, k) && k == 0);
     m.set(a, 2);

src/test/symbol_table.cpp

@@ -26,9 +26,7 @@ static void tst1() {
     t.begin_scope();
     t.insert(symbol("boo"), 20);
     ENSURE(t.contains(symbol("boo")));
-#ifdef Z3DEBUG
     int tmp;
-#endif
     ENSURE(t.find(symbol("boo"), tmp) && tmp == 20);
     ENSURE(t.find(symbol("foo"), tmp) && tmp == 35);
     t.insert(symbol("foo"), 100);

src/util/heap.h

@@ -52,7 +52,6 @@ class heap : private LT {
         }
     }
 
-#ifdef Z3DEBUG
     // Return true if the value can be inserted in the heap. That is, the vector m_value2indices is big enough to store this value.
     bool is_valid_value(int v) const { 
         SASSERT(v >= 0 && v < static_cast<int>(m_value2indices.size())); 
@@ -75,7 +74,6 @@ public:
         return check_invariant_core(1); 
     }
 
-#endif
 private:
 
     void move_up(int idx) {