mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix wrong check
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
19b858dbea
commit
5206e29bdd
|
@ -2672,11 +2672,11 @@ namespace sat {
|
|||
return;
|
||||
}
|
||||
|
||||
VERIFY(c.size() - c.k() >= sz - k);
|
||||
VERIFY(!all_units || c.size() - c.k() >= sz - k);
|
||||
c.set_size(sz);
|
||||
c.set_k(k);
|
||||
|
||||
if (clausify(c)) {
|
||||
if (all_units && clausify(c)) {
|
||||
return;
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue