From a9223283589ab805e7fc54506b0ab46d9a2de7d0 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 27 Dec 2019 11:32:20 -0800 Subject: [PATCH] integrate with Z3Prover Signed-off-by: Lev Nachmanson --- src/math/lp/nla_core.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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]);