diff --git a/src/math/lp/explanation.h b/src/math/lp/explanation.h
index c122f9f2b..01853c626 100644
--- a/src/math/lp/explanation.h
+++ b/src/math/lp/explanation.h
@@ -33,6 +33,8 @@ public:
     vector<std::pair<mpq, constraint_index>>::const_iterator begin() const { return m_explanation.begin(); }
     vector<std::pair<mpq, constraint_index>>::const_iterator end() const { return m_explanation.end(); }
     void push_justification(constraint_index j, const mpq& v) {
+        if (m_set_of_ci.find(j) != m_set_of_ci.end()) return;
+        m_set_of_ci.insert(j);
         m_explanation.push_back(std::make_pair(v, j));
     }
     void push_justification(constraint_index j) {