diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp
index bdcddc03d..77c51d87c 100644
--- a/src/sat/smt/arith_diagnostics.cpp
+++ b/src/sat/smt/arith_diagnostics.cpp
@@ -209,12 +209,6 @@ namespace arith {
         rational lc(1);
         for (unsigned i = m_lit_head; i < m_lit_tail; ++i) 
             lc = lcm(lc, denominator(a.m_arith_hint.lit(i).first));
-
-        for (unsigned i = m_lit_head; i < m_lit_tail; ++i) {
-            auto const& [coeff, lit] = a.m_arith_hint.lit(i);
-            args.push_back(arith.mk_int(abs(coeff*lc)));
-            args.push_back(s.literal2expr(lit));
-        }
         for (unsigned i = m_eq_head; i < m_eq_tail; ++i) {
             auto [x, y, is_eq] = a.m_arith_hint.eq(i);    
             if (x->get_id() > y->get_id())
@@ -224,6 +218,11 @@ namespace arith {
             args.push_back(arith.mk_int(1));
             args.push_back(eq);
         }
+        for (unsigned i = m_lit_head; i < m_lit_tail; ++i) {
+            auto const& [coeff, lit] = a.m_arith_hint.lit(i);
+            args.push_back(arith.mk_int(abs(coeff*lc)));
+            args.push_back(s.literal2expr(lit));
+        }
         return m.mk_app(symbol(name), args.size(), args.data(), m.mk_proof_sort());
     }
 }