From ccda9d56d7e1b91d9561e88c913b0c7c50d32a6d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 15 May 2020 15:57:38 -0700
Subject: [PATCH] fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/explanation.h | 2 ++
 1 file changed, 2 insertions(+)

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) {