diff options
| -rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 5 |
1 files changed, 4 insertions, 1 deletions
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){ |