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

call m_pdd_grobner.reset()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-27 15:19:34 -08:00
parent a922328358
commit 1cc5935953
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1420,6 +1420,7 @@ void core::create_vars_used_in_mrows() {
void core::run_pdd_grobner() { 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(); create_vars_used_in_mrows();
m_pdd_grobner.reset();
for (unsigned i : m_rows) { for (unsigned i : m_rows) {
add_row_to_pdd_grobner(m_lar_solver.A_r().m_rows[i]); add_row_to_pdd_grobner(m_lar_solver.A_r().m_rows[i]);
} }