From 357a92dfef8b2b3aafad0763c588bf153709764b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 27 Oct 2015 18:11:31 -0700 Subject: [PATCH] n/a Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_aux.h | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index bad141e94..96133b88e 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1451,6 +1451,11 @@ namespace smt { normalize_gain(min_gain.get_rational(), max_gain); } + if (is_int(x_i) && !max_gain.is_rational()) { + max_gain = inf_numeral(floor(max_gain)); + normalize_gain(min_gain.get_rational(), max_gain); + } + if (!max_inc.is_minus_one()) { if (is_int(x_i)) { TRACE("opt",