diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 0168652cb..88db34012 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -3097,6 +3097,8 @@ namespace smt {
         m_stats.m_conflicts++;
         m_num_conflicts++;
         TRACE("arith_conflict",
+              if (proof_rule)
+                  tout << proof_rule << "\n";
               tout << "scope: " << ctx.get_scope_level() << "\n";
               for (unsigned i = 0; i < num_literals; i++) {
                   ctx.display_detailed_literal(tout, lits[i]);
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 94702a32b..67d9988ed 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3159,11 +3159,15 @@ public:
         // lp().shrink_explanation_to_minimum(m_explanation); // todo, enable when perf is fixed
         ++m_num_conflicts;
         ++m_stats.m_conflicts;
-        TRACE("arith", tout << "scope: " << ctx().get_scope_level() << "\n"; display_evidence(tout, m_explanation); );
-        TRACE("arith", display(tout << "is-conflict: " << is_conflict << "\n"););
-        for (auto ev : m_explanation) {
+        TRACE("arith",
+              tout << "lemma scope: " << ctx().get_scope_level();
+              for (auto const& p : m_params) tout << " " << p;
+              tout << "\n";
+              display_evidence(tout, m_explanation);
+              display(tout << "is-conflict: " << is_conflict << "\n"););
+        for (auto ev : m_explanation) 
             set_evidence(ev.ci(), m_core, m_eqs);
-        }
+        
         // SASSERT(validate_conflict(m_core, m_eqs));
         dump_conflict(m_core, m_eqs);
         if (is_conflict) {