From 077a2cf6f7b229e9bf286b5e4b9d2ce6c5f37209 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 6 Apr 2020 12:27:53 -0700 Subject: [PATCH] fix #3784 Signed-off-by: Nikolaj Bjorner --- src/smt/arith_eq_solver.cpp | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/src/smt/arith_eq_solver.cpp b/src/smt/arith_eq_solver.cpp index 677132804..8f330fa23 100644 --- a/src/smt/arith_eq_solver.cpp +++ b/src/smt/arith_eq_solver.cpp @@ -76,17 +76,16 @@ void arith_eq_solver::prop_mod_const(expr * e, unsigned depth, numeral const& k, void arith_eq_solver::gcd_normalize(vector& values) { numeral g(0); - for (unsigned i = 0; !g.is_one() && i < values.size(); ++i) { - SASSERT(values[i].is_int()); - if (!values[i].is_zero()) { - if (g.is_zero()) { - g = abs(values[i]); - } - else { - g = gcd(abs(values[i]), g); - } - } + for (auto const& n : values) { + SASSERT(n.is_int()); + if (g.is_zero()) + g = abs(n); + else + g = gcd(abs(n), g); + if (g.is_one()) + break; } + if (g.is_zero() || g.is_one()) { return; } @@ -197,6 +196,9 @@ bool arith_eq_solver::solve_integer_equation( // Instead used the coefficient 'm' at position 'index'. // + for (auto const& n : values) + if (!n.is_int()) + return false; gcd_normalize(values); if (!gcd_test(values)) { TRACE("arith_eq_solver", tout << "not sat\n";