mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-06 19:21:22 +00:00
Code Activity

fix

Browse source
This commit is contained in:
Jakob Rath 2023-10-23 11:46:43 +02:00
parent 64ac3596bd
commit 83aeba9ef4
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/viable.cpp
View file

@ -1205,7 +1205,7 @@ namespace {
out_fbi.push_from_bit(last_indet, k); out_fbi.push_from_bit(last_indet, k);
} }
} }
out_fbi.push_just(i, neg.first); out_fbi.push_just(last_indet, neg.first);
fixed[last_indet] = neg.second.bits.get_bit(last_indet) ? l_false : l_true; fixed[last_indet] = neg.second.bits.get_bit(last_indet) ? l_false : l_true;
removed[j] = true; removed[j] = true;
LOG("Applying fast BCP on bit " << last_indet << " from constraint " << neg.first->src); LOG("Applying fast BCP on bit " << last_indet << " from constraint " << neg.first->src);