mirror of
https://github.com/Z3Prover/z3
synced 2025-04-16 05:48:44 +00:00
start gomory cut
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
This commit is contained in:
parent
fc6a876845
commit
bac16bac85
|
@ -1254,7 +1254,7 @@ namespace smt {
|
||||||
}
|
}
|
||||||
case lp::lia_move::bound: {
|
case lp::lia_move::bound: {
|
||||||
// todo nikolaj
|
// todo nikolaj
|
||||||
// Need to set a bound >= k on the only var from the term
|
// Need to set a bound x[j] >= k where j is the only var from the term
|
||||||
return l_false;
|
return l_false;
|
||||||
}
|
}
|
||||||
case lp::lia_move::cut: {
|
case lp::lia_move::cut: {
|
||||||
|
|
Loading…
Reference in a new issue