[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 2d6e318f237e12723f50092b3c199fd422430000..885e429f007ecae9e79a1b1d69d3f9ad7e7ec501 100644 (file)
--- 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){