diff --git a/src/math/dd/pdd_interval.h b/src/math/dd/pdd_interval.h
index 81153e4b5..076e132e7 100644
--- a/src/math/dd/pdd_interval.h
+++ b/src/math/dd/pdd_interval.h
@@ -59,6 +59,7 @@ 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 <typename T>