mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

fix model generation regression exposed in nightly builds

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-13 13:51:07 -07:00
parent 774fa33bfe
commit 88f4ce68fd
1 changed files with 9 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/smt/theory_lra.cpp
View file

@ -1118,7 +1118,7 @@ public:
(v != null_theory_var) &&
(v < static_cast<theory_var>(m_theory_var2var_index.size())) &&
(UINT_MAX != m_theory_var2var_index[v]) &&
!m_variable_values.empty();
(!m_variable_values.empty() || m_solver->is_term(m_theory_var2var_index[v]));
}
bool can_get_bound(theory_var v) const {
@ -1163,13 +1163,19 @@ public:
}
rational get_value(theory_var v) const {
if (!can_get_value(v)) return rational::zero();
if (v == null_theory_var ||
v >= static_cast<theory_var>(m_theory_var2var_index.size()))
return rational::zero();
lp::var_index vi = m_theory_var2var_index[v];
if (m_variable_values.count(vi) > 0)
return m_variable_values[vi];
if(!m_solver->is_term(vi))
if (!m_solver->is_term(vi)) {
TRACE("arith", tout << "not a term v" << v << "\n";);
return rational::zero();
}
m_todo_terms.push_back(std::make_pair(vi, rational::one()));
rational result(0);