mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

add to m_touched_rows only when bound

Browse source 
propagation is required
This commit is contained in:
Lev Nachmanson 2023-07-17 08:00:01 -10:00
parent 013d5dc4db
commit bfc37bd266
1 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/math/lp/lar_solver.cpp
View file

@ -619,11 +619,10 @@ namespace lp {
}
void lar_solver::add_touched_row(unsigned rid) {
m_touched_rows.insert(rid);
if (m_settings.bound_propagation())
m_touched_rows.insert(rid);
}
bool lar_solver::use_tableau_costs() const {
return m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs;
}