diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 45f0ea559..e2713b09d 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -990,7 +990,7 @@ public:
             return true;
         }
         else {
-            TRACE("arith", tout << "Could not internalize " << mk_pp(atom, m) << "\n";);
+			TRACE("arith", tout << "Could not internalize " << mk_pp(atom, m) << "\n";);
             found_not_handled(atom);
             return true;
         }
@@ -1780,6 +1780,12 @@ public:
             for (auto& kv : coeffs) kv.m_value.neg();
         }
 
+		for (auto const& kv : coeffs) {
+			theory_var w = kv.m_key;
+			expr* o = get_enode(w)->get_owner();
+			is_int &= a.is_int(o);
+		}
+
         app_ref atom(m);
         app_ref t = coeffs2app(coeffs, rational::zero(), is_int);
         if (lower_bound) {