diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index f15af30c0..2abac41ca 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1418,7 +1418,7 @@ void core::create_vars_used_in_mrows() { } void core::run_pdd_grobner() { - m_pdd_manager.resize(m_lar_solver.number_of_vars()); + // m_pdd_manager.resize(m_lar_solver.number_of_vars()); create_vars_used_in_mrows(); for (unsigned i : m_rows) { add_row_to_pdd_grobner(m_lar_solver.A_r().m_rows[i]);