mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

start porting grobner basis functionality

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-09-05 14:23:05 -07:00
parent 26b4294bce
commit 868ea58aef
1 changed files with 0 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1612,7 +1612,6 @@ void lar_solver::pop_tableau() {
}
void lar_solver::clean_inf_set_of_r_solver_after_pop() {
TRACE("lp_core", tout << ++lp_settings::ddd << "\n";);
vector<unsigned> became_feas;
clean_popped_elements(A_r().column_count(), m_mpq_lar_core_solver.m_r_solver.m_inf_set);
std::unordered_set<unsigned> basic_columns_with_changed_cost;