Commit 8dadb815 authored by Daniel Le Berre's avatar Daniel Le Berre

Merge branch 'fix-sat-155' into 'master'

Fix sat 155

See merge request !4
parents 4c8d6b14 05d6d9e1
Pipeline #4758 failed with stages
in 161 minutes and 41 seconds
......@@ -361,7 +361,7 @@ public abstract class WatchPb
for (j = i + 1; j < to; j++) {
if (this.coefs[j].compareTo(this.coefs[bestIndex]) > 0
|| this.coefs[j].equals(this.coefs[bestIndex])
&& this.lits[j] > this.lits[bestIndex]) {
&& this.lits[j] < this.lits[bestIndex]) {
bestIndex = j;
}
}
......@@ -447,12 +447,12 @@ public abstract class WatchPb
i++;
} while (this.coefs[i].compareTo(pivot) > 0
|| this.coefs[i].equals(pivot)
&& this.lits[i] > litPivot);
&& this.lits[i] < litPivot);
do {
j--;
} while (pivot.compareTo(this.coefs[j]) > 0
|| this.coefs[j].equals(pivot)
&& this.lits[j] < litPivot);
&& this.lits[j] > litPivot);
if (i >= j) {
break;
......
......@@ -361,7 +361,7 @@ public abstract class WatchPbLong
for (j = i + 1; j < to; j++) {
if (this.coefs[j] > this.coefs[bestIndex]
|| this.coefs[j] == this.coefs[bestIndex]
&& this.lits[j] > this.lits[bestIndex]) {
&& this.lits[j] < this.lits[bestIndex]) {
bestIndex = j;
}
}
......@@ -445,11 +445,11 @@ public abstract class WatchPbLong
do {
i++;
} while (this.coefs[i] > pivot
|| this.coefs[i] == pivot && this.lits[i] > litPivot);
|| this.coefs[i] == pivot && this.lits[i] < litPivot);
do {
j--;
} while (pivot > this.coefs[j]
|| this.coefs[j] == pivot && this.lits[j] < litPivot);
|| this.coefs[j] == pivot && this.lits[j] > litPivot);
if (i >= j) {
break;
......
......@@ -388,7 +388,7 @@ public abstract class WatchPbLongCP
for (j = i + 1; j < to; j++) {
if (this.coefs[j] > this.coefs[bestIndex]
|| this.coefs[j] == this.coefs[bestIndex]
&& this.lits[j] > this.lits[bestIndex]) {
&& this.lits[j] < this.lits[bestIndex]) {
bestIndex = j;
}
}
......@@ -474,11 +474,11 @@ public abstract class WatchPbLongCP
do {
i++;
} while (this.coefs[i] > pivot
|| this.coefs[i] == pivot && this.lits[i] > litPivot);
|| this.coefs[i] == pivot && this.lits[i] < litPivot);
do {
j--;
} while (pivot > this.coefs[j]
|| this.coefs[j] == pivot && this.lits[j] < litPivot);
|| this.coefs[j] == pivot && this.lits[j] > litPivot);
if (i >= j) {
break;
......
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