diff --git a/src/math/interval/dep_intervals.cpp b/src/math/interval/dep_intervals.cpp index f3aa33680..3381f9440 100644 --- a/src/math/interval/dep_intervals.cpp +++ b/src/math/interval/dep_intervals.cpp @@ -38,6 +38,7 @@ void dep_intervals::set_interval_for_scalar(interval& a, const rational& v) { + void dep_intervals::set_zero_interval(interval& i, u_dependency* dep) const { auto val = rational(0); m_config.set_lower(i, val); diff --git a/src/math/interval/dep_intervals.h b/src/math/interval/dep_intervals.h index 9d7c5de20..4b1357656 100644 --- a/src/math/interval/dep_intervals.h +++ b/src/math/interval/dep_intervals.h @@ -332,5 +332,5 @@ public: copy_upper_bound(b, i); } - typedef im_config::interval interv; + }; diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index 43e6f2ba8..5141924e0 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -34,7 +34,7 @@ class intervals { core* m_core; public: - typedef dep_intervals::interv interval; + typedef dep_intervals::interval interval; private: u_dependency* mk_dep(lp::constraint_index ci); u_dependency* mk_dep(lp::explanation const&);