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<numeral>& 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";