diff --git a/src/muz/ddnf/ddnf.cpp b/src/muz/ddnf/ddnf.cpp
index ad0e0ad34..e80bf144e 100644
--- a/src/muz/ddnf/ddnf.cpp
+++ b/src/muz/ddnf/ddnf.cpp
@@ -945,37 +945,6 @@ namespace datalog {
             // 
 
 -------------------------------
-
-        void add_pos(ddnf_node& n, vector<dot>& active) {
-            for (unsigned i = 0; i < n.pos().size(); ++i) {                
-                active.push_back(n.pos()[i]);
-                // TBD: Garvit; prove (or disprove): there are no repetitions.
-                // the argument may be that the sub-expressions are
-                // traversed in DFS order, and that repeated dots
-                // cannot occur below each-other.
-            }
-            for (unsigned i = 0; i < active.size(); ++i) {
-                m_dots.find(active[i])->insert(&n);
-            }
-            for (unsigned i = 0; i < n.num_children(); ++i) {
-                vector<dot> active1(active);
-                add_pos(*n[i], active1);
-            }            
-        }
-
-        void del_neg(ddnf_node& n, vector<dot>& active) {
-            for (unsigned i = 0; i < n.neg().size(); ++i) {                
-                active.push_back(n.neg()[i]);
-            }
-            for (unsigned i = 0; i < active.size(); ++i) {
-                m_dots.find(active[i])->remove(&n);
-            }
-            for (unsigned i = 0; i < n.num_children(); ++i) {
-                vector<dot> active1(active);
-                del_neg(*n[i], active1);
-            }          
-        } 
-
     class trie {
     public:
         class node {
@@ -1026,71 +995,3 @@ namespace datalog {
     };
 #endif
 
-#if 0
-    class dot {
-        tbv         m_pos;
-        vector<tbv> m_negs;
-    public:
-        dot() {}
-        dot(tbv const& pos): m_pos(pos) {}
-        dot(tbv const& pos, vector<tbv> const& negs):
-            m_pos(pos), m_negs(negs) {
-            DEBUG_CODE(
-                for (unsigned i = 0; i < negs.size(); ++i) {
-                    SASSERT(pos.size() == negs[i].size());
-                }
-                );
-        }
-
-        tbv const& pos() const { return m_pos; }
-        tbv neg(unsigned i) const { return m_negs[i]; }
-        unsigned size() const { return m_negs.size(); }
-        unsigned num_bits() const { return m_pos.size(); }
-
-        bool operator==(dot const& other) const {
-            if (m_pos != other.m_pos) return false;
-            if (m_negs.size() != other.m_negs.size()) return false;
-            for (unsigned i = 0; i < m_negs.size(); ++i) {
-                if (m_negs[i] != other.m_negs[i]) return false;
-            }
-            return true;
-        }
-
-        void display(std::ostream& out) {
-            out << "<";
-            m_pos.display(out);
-            out << "\\";
-            for (unsigned i = 0; i < m_negs.size(); ++i) {
-                m_negs[i].display(out);
-                if (i + 1 < m_negs.size()) out << " u ";
-            }
-            out << ">";
-        }
-
-        struct eq {
-            bool operator()(dot const& d1, dot const& d2) const {
-                return d1 == d2;
-            }
-        };
-
-        struct hash {
-            unsigned operator()(dot const& d) const {
-                unsigned h = d.pos().get_hash();
-                for (unsigned i = 0; i < d.size(); ++i) {
-                    h ^= d.neg(i).get_hash();
-                }
-                return h;
-            }
-        };
-
-    };
-
-        vector<dot>           m_pos;
-        vector<dot>           m_neg;
-        vector<dot> const& pos() const { return m_pos; }
-        vector<dot> const& neg() const { return m_neg; }
-        ddnf_node* add_pos(dot const& d) { m_pos.push_back(d); return this; }
-        ddnf_node* add_neg(dot const& d) { m_neg.push_back(d); return this; }
-
-
-#endif