From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Wed, 16 May 2012 16:01:48 +0000 (+0000)
Subject: removing duplicate literals in explanations of propagations
X-Git-Tag: cvc5-1.0.0~8166
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6d4822f197ccd235175669f199e922aa12eda4b1;p=cvc5.git

removing duplicate literals in explanations of propagations
---

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 6ee508eba..71f252291 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -199,6 +199,7 @@ CRef Solver::reason(Var x) {
     // Compute the assertion level for this clause
     int explLevel = 0;
     int i, j;
+    Lit prev = lit_Undef;
     for (i = 0, j = 0; i < explanation.size(); ++ i) {
       int varLevel = intro_level(var(explanation[i]));
       if (varLevel > explLevel) {
@@ -207,8 +208,8 @@ CRef Solver::reason(Var x) {
       Assert(value(explanation[i]) != l_Undef);
       Assert(i == 0 || trail_index(var(explanation[0])) > trail_index(var(explanation[i])));
       // ignore zero level literals
-      if (i == 0 || level(var(explanation[i])) > 0) {
-        explanation[j++] = explanation[i];
+      if (i == 0 || (level(var(explanation[i])) > 0 && explanation[i] != prev)) {
+        prev = explanation[j++] = explanation[i];
       }
     }
     explanation.shrink(i - j);