mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 14:53:40 +00:00
Code Activity

Prefer larger masks for justifications

Browse source
This commit is contained in:
Clemens Eisenhofer 2023-02-16 07:31:13 +01:00
parent 5fbfa0be8f
commit 0dae2d40b5
1 changed files with 10 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -772,6 +772,8 @@ namespace {
add_entry(e); add_entry(e);
}; };
unsigned largest_mask = 0;
do { do {
single_bit bit; single_bit bit;
trailing_bits mask; trailing_bits mask;
@ -808,6 +810,14 @@ namespace {
s.set_conflict(*builder.build()); s.set_conflict(*builder.build());
return false; return false;
} }
else {
// Prefer justifications from larger masks (less premisses)
if (largest_mask < mask.length) {
largest_mask = mask.length;
justifications[i].clear();
justifications[i].push_back(e);
}
}
} }
else { else {
SASSERT(justifications[i].empty()); SASSERT(justifications[i].empty());