Commit 9e1613b5 authored by Daniel Le Berre's avatar Daniel Le Berre

Fix problem where those constraints are watched even if the

constraint is found to be contradictory.
parent fe04ee6c
......@@ -145,6 +145,11 @@ public final class MaxWatchPbLong extends WatchPbLong {
assert this.watchCumul >= computeLeftSide();
if (!this.learnt && this.watchCumul < this.degree) {
for (int i = 0; i < this.lits.length; i++) {
if (!this.voc.isFalsified(this.lits[i])) {
this.voc.watches(this.lits[i] ^ 1).remove(this);
}
}
throw new ContradictionException("non satisfiable constraint");
}
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment