diff --git a/buddy/src/bddx.h b/buddy/src/bddx.h
index 0efd3a0a9..b3cb377a1 100644
--- a/buddy/src/bddx.h
+++ b/buddy/src/bddx.h
@@ -501,6 +501,7 @@ BUDDY_API_VAR const BDD bddtrue;
 *************************************************************************/
 #ifdef CPLUSPLUS
 #include <iostream>
+#include <memory>
 
 /*=== User BDD class ===================================================*/
 
@@ -1092,6 +1093,11 @@ inline bddxfalse bdd_false(void)
 { return bddxfalse(); }
 
 
+template<>
+struct std::default_delete<bddPair> {
+    void operator()(bddPair *p) const { bdd_freepair(p); };
+};
+
 /*=== Iostream printing ================================================*/
 
 class BUDDY_API bdd_ioformat