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

clean m_nla_lemma_vector in nla_solver

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2023-09-25 12:10:59 -07:00
parent 87a839c794
commit 26a9b776c6
5 changed files with 7 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2027,11 +2027,12 @@ void core::add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std:
}
}
void core::init_bound_propagation() {
void core::init_bound_propagation(vector<nla::lemma>& lemma_vector) {
m_implied_bounds.clear();
m_improved_lower_bounds.reset();
m_improved_upper_bounds.reset();
m_column_types = &lra.get_column_types();
lemma_vector.clear();
}
} // namespace nla