mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

model_based_opt: fix enabling complete resolution

Browse source 
a bug prevented an optimization to be enabled
This commit is contained in:
Arie Gurfinkel 2022-08-04 17:49:51 -04:00 • committed by Nikolaj Bjorner
parent 80c516bb50
commit aa0719abae
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/simplex/model_based_opt.cpp
View file

@ -981,7 +981,7 @@ namespace opt {
lub_rows.reset(); lub_rows.reset();
glb_rows.reset(); glb_rows.reset();
mod_rows.reset(); mod_rows.reset();
bool lub_is_unit = false, glb_is_unit = false; bool lub_is_unit = true, glb_is_unit = true;
unsigned eq_row = UINT_MAX; unsigned eq_row = UINT_MAX;
// select the lub and glb. // select the lub and glb.
for (unsigned row_id : row_ids) { for (unsigned row_id : row_ids) {