From fee2021bb7419630853cbd0b20afa1af5e2eb1e9 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 3 Apr 2018 17:30:41 -0700 Subject: [PATCH] [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. --- src/prop/bvminisat/core/Solver.cc | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) 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& 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){ -- 2.30.2