diff options
author | lianah <lianahady@gmail.com> | 2014-06-13 19:53:03 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2014-06-13 19:53:03 -0400 |
commit | 8c45a2ef94d68ceff7c0997e80d5b573895f2f69 (patch) | |
tree | 190bf91ec726b97f4f3995d6304593d50e06b21b /src/prop | |
parent | f6dd7379078de253a6ec5cc3302f78010dbfccc3 (diff) |
fixed BVMinisat bug due to not clearing seen properly
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/bvminisat/core/Solver.cc | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index 8833eec78..e54c8d174 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -489,13 +489,12 @@ void Solver::analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict) { Var x = var(trail[i]); if (seen[x]) { if (reason(x) == CRef_Undef) { - // this is the case when p was a unit - if (x == var(p)) - continue; - - assert (marker[x] == 2); - assert (level(x) > 0); - out_conflict.push(~trail[i]); + // we skip p if was a learnt unit + if (x != var(p)) { + assert (marker[x] == 2); + assert (level(x) > 0); + out_conflict.push(~trail[i]); + } } else { Clause& c = ca[reason(x)]; for (int j = 1; j < c.size(); j++) @@ -504,6 +503,7 @@ void Solver::analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict) { } seen[x] = 0; } + assert (seen[x] == 0); } assert (out_conflict.size()); } |