mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

Remove unnecessary null pointer checks

Browse source
This commit is contained in:
Lev Nachmanson 2019-03-22 10:47:11 -07:00
parent 61ac006cbe
commit e59d60fbbe
1 changed files with 5 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/util/lp/lar_core_solver.h
View file

@ -235,20 +235,17 @@ public:
m_r_upper_bounds.pop(k); m_r_upper_bounds.pop(k);
m_column_types.pop(k); m_column_types.pop(k);
if (m_r_solver.m_factorization != nullptr) { delete m_r_solver.m_factorization;
delete m_r_solver.m_factorization; m_r_solver.m_factorization = nullptr;
m_r_solver.m_factorization = nullptr;
}
m_r_x.resize(m_r_A.column_count()); m_r_x.resize(m_r_A.column_count());
m_r_solver.m_costs.resize(m_r_A.column_count()); m_r_solver.m_costs.resize(m_r_A.column_count());
m_r_solver.m_d.resize(m_r_A.column_count()); m_r_solver.m_d.resize(m_r_A.column_count());
if(!settings().use_tableau()) if(!settings().use_tableau())
pop_markowitz_counts(k); pop_markowitz_counts(k);
m_d_A.pop(k); m_d_A.pop(k);
if (m_d_solver.m_factorization != nullptr) { // doubles
delete m_d_solver.m_factorization; delete m_d_solver.m_factorization;
m_d_solver.m_factorization = nullptr; m_d_solver.m_factorization = nullptr;
}
m_d_x.resize(m_d_A.column_count()); m_d_x.resize(m_d_A.column_count());
pop_basis(k); pop_basis(k);