From 0d6220f383c4e171ee5f19a840a172653cf1eb60 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Dec 2013 21:53:04 +0200 Subject: [PATCH] revert is_all_int bugfix Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_aux.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 7593e9a52..21b892e57 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -476,10 +476,10 @@ namespace smt { typename vector::const_iterator it = r.begin_entries(); typename vector::const_iterator end = r.end_entries(); for (; it != end; ++it) { - if (!it->is_dead() && !it->m_coeff.is_int()) { + if (!it->is_dead() && !it->m_coeff.is_int()) TRACE("gomory_cut", display_row(tout, r, true);); return false; - } + } return true; }