From 465eafbf45ae107a40f8ec45a030938d8597fdb7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 9 Jul 2014 05:04:00 +0200 Subject: [PATCH] fix assertion for integrality, lax noprogress bail out code Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_aux.h | 6 +++++- src/smt/theory_arith_inv.h | 2 +- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 1e2a6c238..7178834fa 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1449,6 +1449,8 @@ namespace smt { /** Move the variable x_i maximally towards its bound as long as bounds of other variables are not violated. + Returns false if an integer bound was truncated and no + progress was made. */ template @@ -1492,7 +1494,9 @@ namespace smt { } } + bool truncated = false; if (is_int(x_i)) { + truncated = !delta_abs.is_int(); delta_abs = floor(delta_abs); } @@ -1505,7 +1509,7 @@ namespace smt { TRACE("opt", tout << "Safe delta: " << delta << "\n";); update_value(x_i, delta); - return !delta.is_zero(); + return !truncated || !delta.is_zero(); } /** diff --git a/src/smt/theory_arith_inv.h b/src/smt/theory_arith_inv.h index f6270e664..99e4303ff 100644 --- a/src/smt/theory_arith_inv.h +++ b/src/smt/theory_arith_inv.h @@ -204,7 +204,7 @@ namespace smt { bool theory_arith::satisfy_integrality() const { int num = get_num_vars(); for (theory_var v = 0; v < num; v++) { - if (!(is_int(v) && get_value(v).is_int())) { + if (is_int(v) && !get_value(v).is_int()) { TRACE("bound_bug", display_var(tout, v); display(tout);); return false; }