From 6558999cef58427b0d044194557d800093e5216a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Jul 2017 08:46:20 -0700 Subject: [PATCH] fixes #1171 Signed-off-by: Nikolaj Bjorner --- src/math/simplex/model_based_opt.cpp | 8 ++++++-- src/qe/qe_arith.cpp | 10 +++++----- src/test/mpff.cpp | 2 -- src/test/symbol_table.cpp | 2 -- src/util/heap.h | 2 -- 5 files changed, 11 insertions(+), 13 deletions(-) diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp index 561f4c47a..f12918bfe 100644 --- a/src/math/simplex/model_based_opt.cpp +++ b/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); diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index d98f36d7d..4490d83db 100644 --- a/src/qe/qe_arith.cpp +++ b/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 > 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)); diff --git a/src/test/mpff.cpp b/src/test/mpff.cpp index bb06846d5..af67d9ff5 100644 --- a/src/test/mpff.cpp +++ b/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); diff --git a/src/test/symbol_table.cpp b/src/test/symbol_table.cpp index 8c3c55c9d..626e2a72f 100644 --- a/src/test/symbol_table.cpp +++ b/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); diff --git a/src/util/heap.h b/src/util/heap.h index cde2451db..14e902648 100644 --- a/src/util/heap.h +++ b/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(m_value2indices.size())); @@ -75,7 +74,6 @@ public: return check_invariant_core(1); } -#endif private: void move_up(int idx) {