mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-21 11:52:05 +00:00
Code Activity

avoid using not initialized variables in theory_lra

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-09-10 11:02:38 -07:00
parent 67a2a26009
commit 8068c64cab
2 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_lra.cpp
View file

@ -1465,10 +1465,12 @@ public:
if (!m_has_int) { if (!m_has_int) {
return true; return true;
} }
unsigned nv = th.get_num_vars(); unsigned nv = std::min(th.get_num_vars(), m_theory_var2var_index.size());
bool all_bounded = true; bool all_bounded = true;
for (unsigned v = 0; v < nv; ++v) { for (unsigned v = 0; v < nv; ++v) {
lp::var_index vi = m_theory_var2var_index[v]; lp::var_index vi = m_theory_var2var_index[v];
if (vi == UINT_MAX)
continue;
if (!m_solver->is_term(vi) && !var_has_bound(vi, true) && !var_has_bound(vi, false)) { if (!m_solver->is_term(vi) && !var_has_bound(vi, true) && !var_has_bound(vi, false)) {
lp::lar_term term; lp::lar_term term;
term.add_monomial(rational::one(), vi); term.add_monomial(rational::one(), vi);

2
src/util/lp/lp_settings.h
View file

@ -357,7 +357,7 @@ public:
} }
#ifdef Z3DEBUG #ifdef Z3DEBUG
static unsigned ddd; // used for debugging static unsigned ddd; // used for debugging
#endif #endif
}; // end of lp_settings class }; // end of lp_settings class