mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 12:48:53 +00:00
Code Activity

integrate with Z3Prover

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

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

@ -1418,7 +1418,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();
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]);