diff --git a/src/muz_qe/heap_trie.h b/src/muz_qe/heap_trie.h
index 04b7f08d2..25689e930 100644
--- a/src/muz_qe/heap_trie.h
+++ b/src/muz_qe/heap_trie.h
@@ -29,6 +29,9 @@ Notes:
 
     Maintaining sorted ranges for larger domains is another option.
 
+    Another possible enhancement is to resplay the tree. 
+    Keep current key index in the nodes.
+
 --*/
 
 #ifndef _HEAP_TRIE_H_
@@ -36,10 +39,12 @@ Notes:
 
 #include "map.h"
 #include "vector.h"
+#include "buffer.h"
 #include "statistics.h"
+#include "small_object_allocator.h"
 
 
-template<typename Key, typename Value>
+template<typename Key, typename KeyLE, typename Value>
 class heap_trie {
 
     struct stats {
@@ -68,7 +73,8 @@ class heap_trie {
         void dec_ref() { SASSERT(m_ref > 0); --m_ref; }
         unsigned ref_count() const { return m_ref; }
         virtual void display(std::ostream& out, unsigned indent) const = 0;
-        virtual unsigned size() const = 0;
+        virtual unsigned num_nodes() const = 0;
+        virtual unsigned num_leaves() const = 0;
     };
 
     class leaf : public node {
@@ -81,19 +87,19 @@ class heap_trie {
         virtual void display(std::ostream& out, unsigned indent) const {
             out << " value: " << m_value;
         }
-        virtual unsigned size() const { return 1; }
+        virtual unsigned num_nodes() const { return 1; }
+        virtual unsigned num_leaves() const { return ref_count()>0?1:0; }
     };
 
+    typedef buffer<std::pair<Key,node*>, true, 2> children_t;
+
     // lean trie node
     class trie : public node {
-        vector<std::pair<Key,node*> > m_nodes;
+        children_t m_nodes;
     public:
         trie(): node(trie_t) {}
 
         virtual ~trie() {
-            for (unsigned i = 0; i < m_nodes.size(); ++i) {
-                dealloc(m_nodes[i].second);
-            }
         }
 
         node* find_or_insert(Key k, node* n) {
@@ -119,7 +125,7 @@ class heap_trie {
         // push nodes whose keys are <= key into vector.
         void find_le(Key key, ptr_vector<node>& nodes) {
             for (unsigned i = 0; i < m_nodes.size(); ++i) {
-                if (m_nodes[i].first <= key) {
+                if (KeyLE::le(m_nodes[i].first, key)) {
                     node* n = m_nodes[i].second;
                     if (n->ref_count() > 0){
                         nodes.push_back(n);
@@ -128,22 +134,35 @@ class heap_trie {
             }
         }
 
+        children_t const& nodes() const { return m_nodes; }
+        children_t & nodes() { return m_nodes; }
+
         virtual void display(std::ostream& out, unsigned indent) const {
             for (unsigned j = 0; j < m_nodes.size(); ++j) {
-                out << "\n";
+                if (j != 0 || indent > 0) {
+                    out << "\n";
+                }
                 for (unsigned i = 0; i < indent; ++i) {
                     out << " ";
                 }
                 node* n = m_nodes[j].second;
-                out << m_nodes[j].first << " count: " << n->ref_count();
+                out << m_nodes[j].first << " refs: " << n->ref_count();
                 n->display(out, indent + 1);
             }
         }
 
-        virtual unsigned size() const {
+        virtual unsigned num_nodes() const {
             unsigned sz = 1;
             for (unsigned j = 0; j < m_nodes.size(); ++j) {
-                sz += m_nodes[j].second->size();
+                sz += m_nodes[j].second->num_nodes();
+            }
+            return sz;
+        }
+
+        virtual unsigned num_leaves() const {
+            unsigned sz = 0;
+            for (unsigned j = 0; j < m_nodes.size(); ++j) {
+                sz += m_nodes[j].second->num_leaves();
             }
             return sz;
         }
@@ -157,18 +176,19 @@ class heap_trie {
             }
             return false;
         }
-
     };
 
+    small_object_allocator m_alloc;
     unsigned m_num_keys;
     node*    m_root;
     stats    m_stats;
     node*    m_spare_leaf;
     node*    m_spare_trie;
-    vector<ptr_vector<node> > m_children;
+
 public:
 
-    heap_trie():         
+    heap_trie():     
+        m_alloc("heap_trie"),
         m_num_keys(0),
         m_root(0),
         m_spare_leaf(0),
@@ -176,19 +196,19 @@ public:
     {}
 
     ~heap_trie() {
-        dealloc(m_root);
-        dealloc(m_spare_leaf);
-        dealloc(m_spare_trie);
+        del_node(m_root);
+        del_node(m_spare_leaf);
+        del_node(m_spare_trie);
     }
 
     unsigned size() const {
-        return m_root->size();
+        return m_root->num_leaves();
     }
 
     void reset(unsigned num_keys) {
-        dealloc(m_root);
-        dealloc(m_spare_leaf);
-        dealloc(m_spare_trie);
+        del_node(m_root);
+        del_node(m_spare_leaf);
+        del_node(m_spare_trie);
         m_num_keys = num_keys;
         m_root = mk_trie();
         m_spare_trie = mk_trie();
@@ -214,7 +234,7 @@ public:
         return true;
     }
 
-    void find_le(Key const* keys, vector<Value>& values) {
+    void find_all_le(Key const* keys, vector<Value>& values) {
         ++m_stats.m_num_find_le;
         ptr_vector<node> todo[2];
         todo[0].push_back(m_root);
@@ -232,7 +252,6 @@ public:
         }
     }
 
-
     // callback based find function
     class check_value {
     public:
@@ -241,28 +260,8 @@ public:
 
     bool find_le(Key const* keys, check_value& check) {
         ++m_stats.m_num_find_le;
-        if (m_children.size() < num_keys()) {
-            m_children.resize(num_keys());
-        }
-        return find_le(m_root, 0, keys, check);
-    }
-
-    bool find_le(node* n, unsigned index, Key const* keys, check_value& check) {
         ++m_stats.m_num_find_le_nodes;
-        if (index == num_keys()) {
-            SASSERT(n->ref_count() > 0);
-            return check(to_leaf(n)->get_value());
-        }
-        else {
-            m_children[index].reset();
-            to_trie(n)->find_le(keys[index], m_children[index]);
-            for (unsigned i = 0; i < m_children[index].size(); ++i) {
-                if (find_le(m_children[index][i], index + 1, keys, check)) {
-                    return true;
-                }
-            }
-            return false;
-        }
+        return find_le(m_root, 0, keys, check);
     }
 
     void remove(Key const* keys) {
@@ -288,9 +287,49 @@ public:
         st.update("heap_trie.num_find_eq", m_stats.m_num_find_eq);
         st.update("heap_trie.num_find_le", m_stats.m_num_find_le);
         st.update("heap_trie.num_find_le_nodes", m_stats.m_num_find_le_nodes);
+        st.update("heap_trie.num_nodes", m_root->num_nodes());
+        unsigned_vector nums;
+        ptr_vector<node> todo;
+        todo.push_back(m_root);
+        while (!todo.empty()) {
+            node* n = todo.back();
+            todo.pop_back();
+            if (n->type() == trie_t) {
+                trie* t = to_trie(n);
+                unsigned sz = t->nodes().size();
+                if (nums.size() <= sz) {
+                    nums.resize(sz+1);
+                }
+                ++nums[sz];
+                for (unsigned i = 0; i < sz; ++i) {
+                    todo.push_back(t->nodes()[i].second);
+                }
+            }
+        }
+        if (nums.size() < 16) nums.resize(16);
+        st.update("heap_trie.num_1_children", nums[1]);
+        st.update("heap_trie.num_2_children", nums[2]);
+        st.update("heap_trie.num_3_children", nums[3]);
+        st.update("heap_trie.num_4_children", nums[4]);
+        st.update("heap_trie.num_5_children", nums[5]);
+        st.update("heap_trie.num_6_children", nums[6]);
+        st.update("heap_trie.num_7_children", nums[7]);
+        st.update("heap_trie.num_8_children", nums[8]);
+        st.update("heap_trie.num_9_children", nums[9]);
+        st.update("heap_trie.num_10_children", nums[10]);
+        st.update("heap_trie.num_11_children", nums[11]);
+        st.update("heap_trie.num_12_children", nums[12]);
+        st.update("heap_trie.num_13_children", nums[13]);
+        st.update("heap_trie.num_14_children", nums[14]);
+        st.update("heap_trie.num_15_children", nums[15]);
+        unsigned sz = 0;
+        for (unsigned i = 16; i < nums.size(); ++i) {
+            sz += nums[i];
+        }
+        st.update("heap_trie.num_16+_children", sz);
     }
 
-    void display(std::ostream& out) {
+    void display(std::ostream& out) const {
         m_root->display(out, 0);
         out << "\n";
     }
@@ -300,23 +339,37 @@ private:
     unsigned num_keys() const { 
         return m_num_keys;
     }
+
+    bool find_le(node* n, unsigned index, Key const* keys, check_value& check) {
+        if (index == num_keys()) {
+            SASSERT(n->ref_count() > 0);
+            return check(to_leaf(n)->get_value());
+        }
+        else {
+            Key key = keys[index];
+            children_t const& nodes = to_trie(n)->nodes();
+            for (unsigned i = 0; i < nodes.size(); ++i) {
+                ++m_stats.m_num_find_le_nodes;
+                if (KeyLE::le(nodes[i].first, key)) {
+                    node* m = nodes[i].second;
+                    if (m->ref_count() > 0 && find_le(m, index+1, keys, check)) {
+                        return true;
+                    }
+                }
+            }
+            return false;
+        }
+    }
     
     void insert(node* n, unsigned num_keys, Key const* keys, Value const& val) {
         // assumption: key is not in table.
-
-        while (true) {
+        for (unsigned i = 0; i < num_keys; ++i) {
             n->inc_ref();
-            if (num_keys == 0) {
-                to_leaf(n)->set_value(val);
-                SASSERT(n->ref_count() == 1);
-                break;
-            }
-            else {
-                n = insert_key(to_trie(n), (num_keys == 1), keys[0]);
-                --num_keys;
-                ++keys;       
-            } 
+            n = insert_key(to_trie(n), (i + 1 == num_keys), keys[i]);
         }
+        n->inc_ref();
+        to_leaf(n)->set_value(val);
+        SASSERT(n->ref_count() == 1);
     }
 
     node* insert_key(trie* n, bool is_leaf, Key const& key) {
@@ -334,19 +387,40 @@ private:
     }       
 
     leaf* mk_leaf() {
-        return alloc(leaf);
+        void* mem = m_alloc.allocate(sizeof(leaf));
+        return new (mem) leaf();
     }
 
     trie* mk_trie() {
-        return alloc(trie);
+        void* mem = m_alloc.allocate(sizeof(trie));
+        return new (mem) trie();
     }
 
-    trie* to_trie(node* n) {
+    void del_node(node* n) {
+        if (!n) {
+            return;
+        }
+        if (n->type() == trie_t) {
+            trie* t = to_trie(n);
+            for (unsigned i = 0; i < t->nodes().size(); ++i) {
+                del_node(t->nodes()[i].second);
+            }            
+            t->~trie();
+            m_alloc.deallocate(sizeof(trie), t);
+        }
+        else {
+            leaf* l = to_leaf(n);
+            l->~leaf();
+            m_alloc.deallocate(sizeof(leaf), l);
+        }
+    }
+
+    trie* to_trie(node* n) const {
         SASSERT(n->type() == trie_t);
         return static_cast<trie*>(n);
     }
 
-    leaf* to_leaf(node* n) {
+    leaf* to_leaf(node* n) const {
         SASSERT(n->type() == leaf_t);
         return static_cast<leaf*>(n);
     }
diff --git a/src/muz_qe/hilbert_basis.cpp b/src/muz_qe/hilbert_basis.cpp
index 10e222fcf..7d15a1958 100644
--- a/src/muz_qe/hilbert_basis.cpp
+++ b/src/muz_qe/hilbert_basis.cpp
@@ -87,7 +87,39 @@ public:
     unsigned size() const {
         return m_table.size();
     }
+
+    void display(std::ostream& out) const {
+        int_table::iterator it = m_table.begin(), end = m_table.end();
+        for (; it != end; ++it) {
+            offset_t offs(*it);
+            hb.display(out, offs);            
+        }
+        display_profile(out);
+    }
+
 private:
+
+    typedef hashtable<numeral, numeral::hash_proc, numeral::eq_proc> numeral_set;
+
+    void display_profile(std::ostream& out) const {
+        vector<numeral_set> weights;
+        weights.resize(hb.get_num_vars()+1);
+        int_table::iterator it = m_table.begin(), end = m_table.end();
+        for (; it != end; ++it) {
+            offset_t offs(*it);
+            values const& ws = hb.vec(offs);
+            weights[0].insert(ws.weight());
+            for (unsigned i = 0; i < hb.get_num_vars(); ++i) {
+                weights[i+1].insert(ws[i]);
+            }            
+        }
+        out << "profile: "; 
+        for (unsigned i = 0; i < weights.size(); ++i) {
+            out << weights[i].size() << " ";
+        }
+        out << "\n";
+    }
+
     void display_profile(offset_t idx, std::ostream& out) {
         unsigned_vector leq;
         unsigned nv = hb.get_num_vars();
@@ -130,14 +162,19 @@ private:
 };
 
 class hilbert_basis::value_index2 {
-    struct checker : public heap_trie<numeral, unsigned>::check_value {
+    struct key_le {
+        static bool le(numeral const& n1, numeral const& n2) {
+            return hilbert_basis::is_abs_geq(n2, n1);
+        }
+    };
+    struct checker : public heap_trie<numeral, key_le, unsigned>::check_value {
         hilbert_basis* hb;
-        offset_t m_value;
-        offset_t m_found;
-        checker(): hb(0) {}
+        offset_t  m_value;
+        offset_t* m_found;
+        checker(): hb(0), m_found(0) {}
         virtual bool operator()(unsigned const& v) {
             if (m_value.m_offset != v && hb->is_subsumed(m_value, offset_t(v))) {
-                m_found = offset_t(v);
+                *m_found = offset_t(v);
                 return true;
             }
             else {
@@ -146,11 +183,25 @@ class hilbert_basis::value_index2 {
         }
     };
     hilbert_basis&               hb;
-    heap_trie<numeral, unsigned> m_trie;
+    heap_trie<numeral, key_le, unsigned> m_trie;
     vector<unsigned>             m_found;
     bool                         m_init;
     checker                      m_checker;
-    
+    vector<numeral>              m_keys;
+
+#if 1    
+    numeral const* get_keys(values const& vs) {
+        return vs()-1;
+    }
+#else
+    numeral const* get_keys(values const& vs) {
+        unsigned sz = m_keys.size();
+        for (unsigned i = 0; i < sz; ++i) {
+            m_keys[sz-i-1] = vs()[i-1];
+        }
+        return m_keys.c_ptr();
+    }
+#endif
 
 public:
     value_index2(hilbert_basis& hb): hb(hb), m_init(false) {
@@ -159,50 +210,23 @@ public:
 
     void insert(offset_t idx, values const& vs) {
         init();
-        m_trie.insert(vs()-1, idx.m_offset);
+        m_trie.insert(get_keys(vs), idx.m_offset);
     }
 
     void remove(offset_t idx, values const& vs) {
-        m_trie.remove(vs()-1);
+        m_trie.remove(get_keys(vs));
     }
 
     void reset() {
-        m_trie.reset(hb.get_num_vars());
+        m_trie.reset(hb.get_num_vars()+1);
+        m_keys.resize(hb.get_num_vars()+1);
     }
 
     bool find(offset_t idx, values const& vs, offset_t& found_idx) {
         init();
-        m_found.reset();
         m_checker.m_value = idx;
-        if (!m_trie.find_le(vs()-1, m_checker)) {
-            return false;
-        }
-        else {
-            found_idx = m_checker.m_found;
-            return true;
-        }        
-    }
-
-    bool find_old(offset_t idx, values const& vs, offset_t& found_idx) {
-        init();
-        m_found.reset();
-        m_trie.find_le(vs()-1, m_found);
-        std::cout << m_found.size() << " - ";
-        for (unsigned i = 0; i < m_found.size(); ++i) {
-            found_idx = offset_t(m_found[i]);
-            std::cout << i << " ";
-            if (m_found[i] != idx.m_offset && hb.is_subsumed(idx, found_idx)) {
-                TRACE("hilbert_basis", 
-                      hb.display(tout << "found:" , idx);
-                      hb.display(tout << "-> ", found_idx);
-                      m_trie.display(tout););       
-                std::cout << "\n";
-                return true;
-            }
-        }
-        std::cout << "\n";
-        TRACE("hilbert_basis", tout << "not found: "; hb.display(tout, idx); );
-        return false;
+        m_checker.m_found = &found_idx;
+        return m_trie.find_le(get_keys(vs), m_checker);
     }
 
     void collect_statistics(statistics& st) const {
@@ -217,6 +241,10 @@ public:
         return m_trie.size();
     }
 
+    void display(std::ostream& out) const {
+        // m_trie.display(out);
+    }
+
 private:
     void init() {
         if (!m_init) {
@@ -232,8 +260,8 @@ class hilbert_basis::index {
     // for each non-positive weight a separate index.
     // for positive weights a shared value index.
 
-    typedef value_index1 value_index;
-    // typedef value_index2 value_index;
+    // typedef value_index1 value_index;
+    typedef value_index2 value_index;
 
     struct stats {
         unsigned m_num_find;
@@ -328,6 +356,15 @@ public:
             it->m_value->reset_statistics();
         }
     }
+
+    void display(std::ostream& out) const {
+        m_pos.display(out);
+        m_zero.display(out);
+        value_map::iterator it = m_neg.begin(), end = m_neg.end();
+        for (; it != end; ++it) {
+            it->m_value->display(out);
+        }
+    }
     
 private:
     unsigned size() const {
@@ -347,15 +384,16 @@ private:
 
 class hilbert_basis::passive {
     struct lt {
-        passive& p;
-        lt(passive& p): p(p) {}
+        passive** p;
+        lt(passive** p): p(p) {}
         bool operator()(int v1, int v2) const {
-            return p(v1, v2);
+            return (**p)(v1, v2);
         }
     };
     hilbert_basis&      hb;
     svector<offset_t>   m_passive;
     unsigned_vector     m_free_list;
+    passive*            m_this;
     lt                  m_lt;
     heap<lt>            m_heap;    // binary heap over weights
 
@@ -371,10 +409,11 @@ class hilbert_basis::passive {
 public:
     
     passive(hilbert_basis& hb): 
-        hb(hb) ,
-        m_lt(*this),
+        hb(hb),
+        m_lt(&m_this),
         m_heap(10, m_lt)
     {
+        m_this = this;
     }
 
     void reset() {
@@ -529,7 +568,7 @@ void hilbert_basis::add_eq(num_vector const& v) {
 
 void hilbert_basis::set_is_int(unsigned var_index) {
     //
-    // The 0't index is reserved for the constant
+    // The 0'th index is reserved for the constant
     // coefficient. Shift indices by 1.
     //
     m_ints.push_back(var_index+1);
@@ -550,7 +589,7 @@ unsigned hilbert_basis::get_num_vars() const {
 }
 
 hilbert_basis::values hilbert_basis::vec(offset_t offs) const {
-    return values(m_store.c_ptr() + offs.m_offset);
+    return values(m_store.c_ptr() + (get_num_vars() + 1)*offs.m_offset);
 }
 
 void hilbert_basis::init_basis() {
@@ -680,7 +719,7 @@ void hilbert_basis::select_inequality() {
     for (unsigned j = best+1; prod != 0 && j < m_ineqs.size(); ++j) {
         unsigned non_zeros2 = get_num_nonzeros(m_ineqs[j]);
         unsigned prod2 = get_ineq_product(m_ineqs[j]);
-        if (prod2 < prod || (prod2 == prod && non_zeros2 < non_zeros)) {
+        if (non_zeros2 < non_zeros || (non_zeros2 == non_zeros && prod2 < prod)) {
             prod = prod2;
             non_zeros = non_zeros2;
             best = j;
@@ -733,7 +772,6 @@ void hilbert_basis::resolve(offset_t i, offset_t j, offset_t r) {
         u[k] = v[k] + w[k];
     }
     u.weight() = v.weight() + w.weight();
-    // std::cout << "resolve: " << v.weight() << " + " << w.weight() << " = " << u.weight() << "\n";
     TRACE("hilbert_basis_verbose",
           display(tout, i); 
           display(tout, j); 
@@ -747,7 +785,7 @@ hilbert_basis::offset_t hilbert_basis::alloc_vector() {
         unsigned num_vars = get_num_vars();
         unsigned idx =  m_store.size();
         m_store.resize(idx + 1 + num_vars);
-        return offset_t(idx);
+        return offset_t(idx/(1+num_vars));
     }
     else {
         offset_t result = m_free_list.back();
@@ -757,6 +795,7 @@ hilbert_basis::offset_t hilbert_basis::alloc_vector() {
 }
 
 void hilbert_basis::add_goal(offset_t idx) {
+    TRACE("hilbert_basis", display(tout, idx););
     values v = vec(idx);
     if (is_subsumed(idx)) {
         return;
@@ -852,6 +891,9 @@ void hilbert_basis::display(std::ostream& out) const {
             display(out, m_zero[i]);
         }
     }
+    if (m_index) {
+        m_index->display(out);
+    }
 }
 
 void hilbert_basis::display(std::ostream& out, offset_t o) const {
@@ -954,7 +996,7 @@ bool hilbert_basis::is_geq(values const& v, values const& w) const {
     return true;
 }
 
-bool hilbert_basis::is_abs_geq(numeral const& v, numeral const& w) const {
+bool hilbert_basis::is_abs_geq(numeral const& v, numeral const& w) {
     if (w.is_neg()) {
         return v <= w;
     }
diff --git a/src/muz_qe/hilbert_basis.h b/src/muz_qe/hilbert_basis.h
index 09839fc03..567d72fbc 100644
--- a/src/muz_qe/hilbert_basis.h
+++ b/src/muz_qe/hilbert_basis.h
@@ -100,7 +100,7 @@ private:
     unsigned get_num_vars() const;
     numeral get_weight(values const & val, num_vector const& ineq) const;
     bool is_geq(values const& v, values const& w) const;
-    bool is_abs_geq(numeral const& v, numeral const& w) const;
+    static bool is_abs_geq(numeral const& v, numeral const& w);
     bool is_subsumed(offset_t idx);
     bool is_subsumed(offset_t i, offset_t j) const;
     void recycle(offset_t idx);
diff --git a/src/test/heap_trie.cpp b/src/test/heap_trie.cpp
index 648a7662e..ad3cd0a8d 100644
--- a/src/test/heap_trie.cpp
+++ b/src/test/heap_trie.cpp
@@ -1,12 +1,15 @@
 #include "heap_trie.h"
 
+struct unsigned_le {
+    static bool le(unsigned i, unsigned j) { return i <= j; }
+};
 
-typedef heap_trie<unsigned, unsigned > heap_trie_t;
+typedef heap_trie<unsigned, unsigned_le, unsigned > heap_trie_t;
 
 static void find_le(heap_trie_t& ht, unsigned num_keys, unsigned const* keys) {
     statistics st;
     vector<unsigned> vals;
-    ht.find_le(keys, vals);
+    ht.find_all_le(keys, vals);
     std::cout << "find_le: ";
     for (unsigned i = 0; i < num_keys; ++i) {
         std::cout << keys[i] << " ";
diff --git a/src/test/hilbert_basis.cpp b/src/test/hilbert_basis.cpp
index d372572bd..b02c8c90c 100644
--- a/src/test/hilbert_basis.cpp
+++ b/src/test/hilbert_basis.cpp
@@ -510,7 +510,7 @@ void tst_hilbert_basis() {
         tst1();
         tst2();
         tst3();
-        // tst4();
+        tst4();
         tst5();
         tst6();
         tst7();
@@ -530,6 +530,5 @@ void tst_hilbert_basis() {
     }
     else {
         gorrila_test(0, 10, 7, 20, 11);
-        tst4();
     }
 }