mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

#5452

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-08-03 20:03:34 -07:00
parent 2891ac7dec
commit 939860148f
1 changed files with 3 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/tactic/core/pb_preprocess_tactic.cpp
View file

@ -503,10 +503,7 @@ private:
bool found = false; bool found = false;
for (unsigned j = 0; j < args2.size(); ++j) { for (unsigned j = 0; j < args2.size(); ++j) {
if (is_complement(args1.get(i), args2.get(j))) { if (is_complement(args1.get(i), args2.get(j))) {
if (i == 0) { if (i == 0 || min_coeff > coeffs2[j]) {
min_coeff = coeffs2[j];
}
else if (min_coeff > coeffs2[j]) {
min_coeff = coeffs2[j]; min_coeff = coeffs2[j];
min_index = j; min_index = j;
} }
@ -517,9 +514,9 @@ private:
if (!found) if (!found)
return; return;
} }
for (unsigned i = 0; i < indices.size(); ++i) { for (unsigned j : indices) {
unsigned j = indices[i];
expr* arg = args2.get(j); expr* arg = args2.get(j);
TRACE("pb", tout << "j " << j << " " << min_index << "\n";);
if (j == min_index) { if (j == min_index) {
args2[j] = m.mk_false(); args2[j] = m.mk_false();
} }