diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index d61789992..f3897f552 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -63,6 +63,7 @@ namespace dd {
     pdd pdd_manager::mk_val(rational const& r) { return pdd(imk_val(r), this); }
     pdd pdd_manager::mul(rational const& r, pdd const& b) { pdd c(mk_val(r)); return pdd(apply(c.root, b.root, pdd_mul_op), this); }
     pdd pdd_manager::add(rational const& r, pdd const& b) { pdd c(mk_val(r)); return pdd(apply(c.root, b.root, pdd_add_op), this); }
+    pdd pdd_manager::minus(pdd const& b) { return pdd(apply(zero_pdd, b.root, pdd_sub_op), this); }
     
     pdd_manager::PDD pdd_manager::apply(PDD arg1, PDD arg2, pdd_op op) {
         bool first = true;
@@ -422,44 +423,8 @@ namespace dd {
 
     pdd pdd_manager::mk_var(unsigned i) {
         reserve_var(i);
-        std::cout << m_var2pdd[i] << "\n";
         return pdd(m_var2pdd[i], this);        
     }
-
-    pdd pdd_manager::minus(pdd const &b) {
-        bool first = true;
-        while (true) {
-            try {
-                return pdd(minus_rec(b.root), this);
-            }
-            catch (const mem_out &) {
-                if (!first) throw;
-                try_gc();
-                first = false;
-            }
-        }
-    }
-
-    pdd_manager::PDD pdd_manager::minus_rec(PDD b) {
-        if (is_zero(b)) {
-            return zero_pdd;
-        }
-
-        if (is_val(b)) {
-            return imk_val(-val(b));
-        }
-
-        op_entry* e1 = pop_entry(b, b, pdd_minus_op);
-        op_entry const* e2 = m_op_cache.insert_if_not_there(e1);
-        if (check_result(e1, e2, b, b, pdd_minus_op)) 
-            return e2->m_result;
-        push(minus_rec(lo(b)));
-        push(minus_rec(hi(b)));
-        PDD r = make_node(level(b), read(2), read(1));
-        pop(2);
-        e1->m_result = r;
-        return r;
-    }
     
     unsigned pdd_manager::pdd_size(pdd const& b) {
         init_mark();
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index 6f9834469..3dddb7401 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -45,9 +45,8 @@ namespace dd {
             pdd_add_op = 2,
             pdd_sub_op = 3,
             pdd_mul_op = 4,
-            pdd_minus_op = 5,
-            pdd_reduce_op = 6,
-            pdd_no_op = 7
+            pdd_reduce_op = 5,
+            pdd_no_op = 6
         };
 
         struct pdd_node {
@@ -147,14 +146,13 @@ namespace dd {
         bool is_new_node() const { return m_is_new_node; }
 
         PDD apply(PDD arg1, PDD arg2, pdd_op op);
+        PDD apply_rec(PDD arg1, PDD arg2, pdd_op op);
+
         PDD reduce_on_match(PDD a, PDD b);
         bool lm_divides(PDD p, PDD q) const;
         PDD lt_quotient(PDD p, PDD q);
 
-        PDD apply_rec(PDD arg1, PDD arg2, pdd_op op);
-        PDD imk_val(rational const& r);
-        PDD minus_rec(PDD a);
-        
+        PDD imk_val(rational const& r);        
 
         void push(PDD b);
         void pop(unsigned num_scopes);