mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
fix #6648
This commit is contained in:
parent
ce501e0b6e
commit
8a3a3dc91b
|
@ -119,7 +119,7 @@ namespace pb {
|
|||
else {
|
||||
bool_var v = s().add_var(true);
|
||||
literal lit(v, sign);
|
||||
add_pb_ge(v, sign, wlits, k.get_unsigned());
|
||||
add_pb_ge(v, false, wlits, k.get_unsigned());
|
||||
TRACE("ba", tout << "root: " << root << " lit: " << lit << "\n";);
|
||||
return lit;
|
||||
}
|
||||
|
@ -146,7 +146,7 @@ namespace pb {
|
|||
else {
|
||||
sat::bool_var v = s().add_var(true);
|
||||
sat::literal lit(v, sign);
|
||||
add_pb_ge(v, sign, wlits, k.get_unsigned());
|
||||
add_pb_ge(v, false, wlits, k.get_unsigned());
|
||||
TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";);
|
||||
return lit;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue