mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix

Browse source
This commit is contained in:
Jakob Rath 2022-08-19 16:18:13 +02:00
parent c3e7bd34d0
commit ee208efdc5
1 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/math/polysat/solver.cpp
View file

@ -1245,11 +1245,14 @@ namespace polysat {
}
if (all_unit) {
SASSERT(!intersection.is_currently_empty());
// Unit intervals from all constraints
// => build constraint from intersection of forbidden intervals
// z \not\in [l;u[ <=> z - l >= u - l
auto c_new = ule(intersection.hi() - intersection.lo(), z - intersection.lo());
out_lits.push_back(c_new.blit());
if (intersection.is_proper()) {
auto c_new = ule(intersection.hi() - intersection.lo(), z - intersection.lo());
out_lits.push_back(c_new.blit());
}
return;
} else {
out_lits.shrink(out_lits_original_size);