mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

missing pb cases

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-12 14:50:40 -08:00
parent dfe2b27f9a
commit 366cd9b16d
1 changed files with 9 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/sat/smt/pb_solver.cpp
View file

@ -1370,6 +1370,15 @@ namespace pb {
s().mk_clause(_lits.size(), _lits.data(), sat::status::th(learned, get_id()));
return nullptr;
}
if (k == 0 && lit == sat::null_literal)
return nullptr;
if (k == 0) {
s().assign_unit(lit);
return nullptr;
}
if (!learned && clausify(lit, lits.size(), lits.data(), k)) {
return nullptr;
}