mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix soundness bug in disabled code
This commit is contained in:
parent
b75d81f3c2
commit
97b66d13c0
|
@ -390,6 +390,7 @@ int gomory::find_basic_var() {
|
|||
const row_strip<mpq>& row = lra.get_row(lia.row_of_basic_column(result));
|
||||
if (is_gomory_cut_target(row))
|
||||
return result;
|
||||
result = -1;
|
||||
#endif
|
||||
|
||||
for (unsigned j : lra.r_basis()) {
|
||||
|
|
Loading…
Reference in a new issue