diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp
index a3e48256d..783f268bd 100644
--- a/src/sat/smt/arith_diagnostics.cpp
+++ b/src/sat/smt/arith_diagnostics.cpp
@@ -136,9 +136,22 @@ namespace arith {
     arith_proof_hint const* solver::explain_conflict(sat::literal_vector const& core, euf::enode_pair_vector const& eqs) {
         arith_proof_hint* hint = nullptr;
         if (ctx.use_drat()) {
+            m_coeffs.reset();
+            for (auto const& e : m_explanation) {
+                if (inequality_source == m_constraint_sources[e.ci()])
+                    m_coeffs.push_back(e.coeff());
+            }
+                
             m_arith_hint.set_type(ctx, hint_type::farkas_h);
-            for (auto lit : core)
-                m_arith_hint.add_lit(rational::one(), lit);
+            if (m_coeffs.size() == core.size()) {
+                unsigned i = 0;
+                for (auto lit : core)
+                    m_arith_hint.add_lit(m_coeffs[i], lit), ++i;
+            }
+            else {
+                for (auto lit : core)
+                    m_arith_hint.add_lit(rational::one(), lit);
+            }
             for (auto const& [a,b] : eqs)
                 m_arith_hint.add_eq(a, b);
             hint = m_arith_hint.mk(ctx);
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index 522867a0d..2364bb16e 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -251,6 +251,7 @@ namespace arith {
         lp::explanation     m_explanation;
         vector<nla::lemma>  m_nla_lemma_vector;
         literal_vector      m_core, m_core2;
+        vector<rational>    m_coeffs;
         svector<enode_pair> m_eqs;
         vector<parameter>   m_params;
         nla::lemma          m_lemma;
diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp
index 781ed7c49..ca83c68c8 100644
--- a/src/smt/qi_queue.cpp
+++ b/src/smt/qi_queue.cpp
@@ -398,6 +398,8 @@ namespace smt {
     bool qi_queue::final_check_eh() {
         TRACE("qi_queue", display_delayed_instances_stats(tout); tout << "lazy threshold: " << m_params.m_qi_lazy_threshold
               << ", scope_level: " << m_context.get_scope_level() << "\n";);
+
+        verbose_stream() << "delayed entries " << m_delayed_entries.size() << "\n";
         if (m_params.m_qi_conservative_final_check) {
             bool  init = false;
             float min_cost = 0.0;