From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 4 Apr 2018 00:30:41 +0000 (-0700)
Subject: [BVMiniSat] Avoid duplicates in conflicts (#1745)
X-Git-Tag: cvc5-1.0.0~5184
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fee2021bb7419630853cbd0b20afa1af5e2eb1e9;p=cvc5.git

[BVMiniSat] Avoid duplicates in conflicts (#1745)

If analyzeFinal() in BVMiniSat was called with a literal that also
occurred in the trail, it could happen that the set of assumptions that
led to the assignment of `p` contained `p` twice.
BitVectorProof::endBVConflict would then register that conflict with the
duplicate literal but at the same time compute a conflict expression
with the duplicate removed. LFSCSatProof::printAssumptionsResolution
would then output two resolutions for the same literal, which made the
simplify_clause side condition fail because it couldn't find the literal
in the clause anymore after the first removal.

The fix simply avoid adding `p` to the set of assumptions if it is found
in the trail. In this situation, `p` is guaranteed to be in the set of
assumptions already because it has been added at the beginning of
analyzeFinal(). This issue originally came up in PR #1384. With this fix
the regression tests pass in #1384.
---

diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 2d6e318f2..885e429f0 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -675,7 +675,10 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
             if (reason(x) == CRef_Undef) {
               assert(marker[x] == 2);
               assert(level(x) > 0);
-              out_conflict.push(~trail[i]);
+              if (~trail[i] != p)
+              {
+                out_conflict.push(~trail[i]);
+              }
             } else {
               Clause& c = ca[reason(x)];
               if(d_bvp){