diff --git a/src/math/dd/pdd_interval.h b/src/math/dd/pdd_interval.h index d797bb8b6..2972e0086 100644 --- a/src/math/dd/pdd_interval.h +++ b/src/math/dd/pdd_interval.h @@ -59,7 +59,6 @@ public: m_dep_intervals.mul(hi, a, t); m_dep_intervals.add(t, lo, ret); } - m().del(a); } // f meant to be called when the separation happens template