diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp
index ec9b11e76..f74adf38b 100644
--- a/src/sat/smt/arith_diagnostics.cpp
+++ b/src/sat/smt/arith_diagnostics.cpp
@@ -82,9 +82,9 @@ namespace arith {
         if (m_nla) m_nla->collect_statistics(st);
     }
 
-    void solver::explain_assumptions() {
+    void solver::explain_assumptions(lp::explanation const& e) {
         unsigned i = 0;
-        for (auto const & ev : m_explanation) {
+        for (auto const & ev : e) {
             ++i;
             auto idx = ev.ci();
             if (UINT_MAX == idx)
@@ -118,17 +118,17 @@ namespace arith {
         if (!ctx.use_drat())
             return nullptr;
         m_arith_hint.set_type(ctx, ty);
-        explain_assumptions();
+        explain_assumptions(m_explanation);
         if (lit != sat::null_literal)
             m_arith_hint.add_lit(rational(1), ~lit);
         return m_arith_hint.mk(ctx);
     }
 
-    arith_proof_hint const* solver::explain_implied_eq(euf::enode* a, euf::enode* b) {
+    arith_proof_hint const* solver::explain_implied_eq(lp::explanation const& e, euf::enode* a, euf::enode* b) {
         if (!ctx.use_drat())
             return nullptr;
         m_arith_hint.set_type(ctx, hint_type::implied_eq_h);
-        explain_assumptions();
+        explain_assumptions(e);
         m_arith_hint.set_num_le(1); // TODO
         m_arith_hint.add_diseq(a, b);
         return m_arith_hint.mk(ctx);
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 87e159b87..685d9249a 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -320,7 +320,7 @@ namespace arith {
         reset_evidence();
         for (auto ev : e)
             set_evidence(ev.ci());
-        auto* ex = explain_implied_eq(n1, n2);
+        auto* ex = explain_implied_eq(e, n1, n2);
         auto* jst = euf::th_explain::propagate(*this, m_core, m_eqs, n1, n2, ex); 
         ctx.propagate(n1, n2, jst->to_index());
         return true;
@@ -744,7 +744,7 @@ namespace arith {
         set_evidence(ci4);
         enode* x = var2enode(v1);
         enode* y = var2enode(v2);
-        auto* ex = explain_implied_eq(x, y);
+        auto* ex = explain_implied_eq(m_explanation, x, y);
         auto* jst = euf::th_explain::propagate(*this, m_core, m_eqs, x, y, ex);
         ctx.propagate(x, y, jst->to_index());
     }
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index 4fdb57386..3d3f1ddd7 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -71,10 +71,10 @@ namespace arith {
         unsigned                               m_lit_head = 0, m_lit_tail = 0, m_eq_head = 0, m_eq_tail = 0;
         void reset() { m_lit_head = m_lit_tail; m_eq_head = m_eq_tail; }
         void add(euf::enode* a, euf::enode* b, bool is_eq) {
-            if (m_eq_tail < m_eqs.size()) 
-                m_eqs[m_eq_tail] = std::tuple(a, b, is_eq); 
-            else 
-                m_eqs.push_back(std::tuple(a, b, is_eq)); 
+            if (m_eq_tail < m_eqs.size())
+                m_eqs[m_eq_tail] = { a, b, is_eq };
+            else
+                m_eqs.push_back({a, b, is_eq });
             m_eq_tail++; 
         }
     public:
@@ -476,9 +476,9 @@ namespace arith {
         arith_proof_hint_builder m_arith_hint;
 
         arith_proof_hint const* explain(hint_type ty, sat::literal lit = sat::null_literal);
-        arith_proof_hint const* explain_implied_eq(euf::enode* a, euf::enode* b);
+        arith_proof_hint const* explain_implied_eq(lp::explanation const& e, euf::enode* a, euf::enode* b);
         arith_proof_hint const* explain_trichotomy(sat::literal le, sat::literal ge, sat::literal eq);
-        void explain_assumptions();
+        void explain_assumptions(lp::explanation const& e);
 
 
     public: