mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-26 18:45:33 +00:00
Code Activity

fixes in cross_nested interval calculations

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-07-27 22:55:55 -07:00
parent 9fb66e9365
commit 9dbd8d3d46
3 changed files with 12 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/nla_intervals.cpp
View file

@ -86,7 +86,7 @@ std::ostream& intervals::display(std::ostream& out, const interval& i) const {
if (m_imanager.upper_is_inf(i)) {
out << "oo)";
} else {
out << rational(m_imanager.upper(i)) << (m_imanager.lower_is_open(i)? ")":"]");
out << rational(m_imanager.upper(i)) << (m_imanager.upper_is_open(i)? ")":"]");
}
svector<lp::constraint_index> expl;
m_dep_manager.linearize(i.m_lower_dep, expl);