mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-01 08:53:18 +00:00
Code Activity

#4525 regression in model generation

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-10-12 10:35:33 -07:00
parent e3d1849be2
commit e683f4be21
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_lra.cpp
View file

@ -1565,9 +1565,10 @@ public:
if (m_variable_values.count(t.index()) > 0) if (m_variable_values.count(t.index()) > 0)
return m_variable_values[t.index()]; return m_variable_values[t.index()];
if (!t.is_term()) { if (!t.is_term() && lp().is_fixed(t.id()))
return lp().column_lower_bound(t.id()).x;
if (!t.is_term())
return rational::zero(); return rational::zero();
}
m_todo_terms.push_back(std::make_pair(t, rational::one())); m_todo_terms.push_back(std::make_pair(t, rational::one()));
rational result(0); rational result(0);