mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

fix term_is_int

Browse source 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
This commit is contained in:
Lev Nachmanson 2017-07-17 16:08:20 -07:00
parent 77171f4af8
commit 729644a2b6
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/util/lp/lar_solver.cpp
View file

@ -1413,7 +1413,7 @@ bool lar_solver::model_is_int_feasible() const {
bool lar_solver::term_is_int(const lar_term * t) const { bool lar_solver::term_is_int(const lar_term * t) const {
for (auto const & p : t->m_coeffs) for (auto const & p : t->m_coeffs)
if (!column_is_int(p.first) || p.second.is_int()) if (! (column_is_int(p.first) && p.second.is_int()))
return false; return false;
return t->m_v.is_int(); return t->m_v.is_int();
} }