mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

assert that the sdi is infinite by default

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-04-02 12:10:31 -07:00
parent b45311cc7c
commit afce09efe4
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -305,8 +305,10 @@ bool intervals::interval_from_term(const nex& e, scoped_dep_interval& i) {
template <e_with_deps wd> template <e_with_deps wd>
void intervals::interval_of_sum_no_term(const nex_sum& e, scoped_dep_interval & sdi) { void intervals::interval_of_sum_no_term(const nex_sum& e, scoped_dep_interval & sdi) {
if (has_inf_interval(e)) if (has_inf_interval(e)) {
SASSERT(m_dep_intervals.lower_is_inf(sdi) && m_dep_intervals.upper_is_inf(sdi));
return; return;
}
interval_of_expr<wd>(e[0], 1, sdi); interval_of_expr<wd>(e[0], 1, sdi);
for (unsigned k = 1; k < e.size(); k++) { for (unsigned k = 1; k < e.size(); k++) {