mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

#5324

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-06-06 15:39:23 -07:00
parent ed49c1eae3
commit 9afc59d5b4
1 changed files with 2 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1009,8 +1009,7 @@ namespace opt {
result = solve_for(glb_index, x, true);
}
else {
result = def();
m_var2value[x] = rational::zero();
result = def() + m_var2value[x];
}
SASSERT(eval(result) == eval(x));
}
@ -1130,9 +1129,8 @@ namespace opt {
}
TRACE("opt1", display(tout << "tableau after replace x by y := v" << y << "\n"););
def result = project(y, compute_def);
if (compute_def) {
if (compute_def)
result = (result * D) + u;
}
SASSERT(!compute_def || eval(result) == eval(x));
return result;
}