diff --git a/src/muz_qe/heap_trie.h b/src/muz_qe/heap_trie.h
index e50a85505..a99861359 100644
--- a/src/muz_qe/heap_trie.h
+++ b/src/muz_qe/heap_trie.h
@@ -518,7 +518,7 @@ private:
         SASSERT(m_keys.size() == num_keys());
         iterator it = begin();
         trie* new_root = mk_trie();
-        IF_VERBOSE(1, verbose_stream() << "before reshuffle: " << m_root->num_nodes() << " nodes\n";);
+        IF_VERBOSE(2, verbose_stream() << "before reshuffle: " << m_root->num_nodes() << " nodes\n";);
         for (; it != end(); ++it) {
             IF_VERBOSE(2, 
                        for (unsigned i = 0; i < num_keys(); ++i) {
@@ -539,7 +539,7 @@ private:
             m_keys[i] = new_keys[i];
         }
         
-        IF_VERBOSE(1, verbose_stream() << "after reshuffle: " << new_root->num_nodes() << " nodes\n";);
+        IF_VERBOSE(2, verbose_stream() << "after reshuffle: " << new_root->num_nodes() << " nodes\n";);
         IF_VERBOSE(2, 
                    it = begin();
                    for (; it != end(); ++it) {                       
@@ -559,7 +559,7 @@ private:
         if (index == num_keys()) {
             SASSERT(n->ref_count() > 0);
             bool r = check(to_leaf(n)->get_value());
-            IF_VERBOSE(1, 
+            IF_VERBOSE(2, 
                        for (unsigned j = 0; j < index; ++j) {
                            verbose_stream() << " ";
                        }
@@ -572,7 +572,7 @@ private:
             for (unsigned i = 0; i < nodes.size(); ++i) {
                 ++m_stats.m_num_find_le_nodes;
                 node* m = nodes[i].second;
-                IF_VERBOSE(1,
+                IF_VERBOSE(2,
                            for (unsigned j = 0; j < index; ++j) {
                                verbose_stream() << " ";
                            }
diff --git a/src/muz_qe/hilbert_basis.cpp b/src/muz_qe/hilbert_basis.cpp
index 49bf20746..bc06aa15e 100644
--- a/src/muz_qe/hilbert_basis.cpp
+++ b/src/muz_qe/hilbert_basis.cpp
@@ -21,6 +21,7 @@ Revision History:
 #include "heap.h"
 #include "map.h"
 #include "heap_trie.h"
+#include "stopwatch.h"
 
 template<typename Value>
 class rational_map : public map<rational, Value, rational::hash_proc, rational::eq_proc> {};
@@ -777,9 +778,18 @@ lbool hilbert_basis::saturate() {
     init_basis();
     m_current_ineq = 0;
     while (!m_cancel && m_current_ineq < m_ineqs.size()) {
-        IF_VERBOSE(1, { statistics st; collect_statistics(st); st.display(verbose_stream()); });
         select_inequality();
+        stopwatch sw;
+        sw.start();
         lbool r = saturate(m_ineqs[m_current_ineq], m_iseq[m_current_ineq]);
+        IF_VERBOSE(1,  
+                   { statistics st; 
+                       collect_statistics(st); 
+                       st.display(verbose_stream()); 
+                       sw.stop(); 
+                       verbose_stream() << "time: " << sw.get_seconds() << "\n";
+                   });
+
         ++m_stats.m_num_saturations;
         if (r != l_true) {
             return r;
@@ -933,14 +943,6 @@ lbool hilbert_basis::saturate(num_vector const& ineq, bool is_eq) {
         m_free_list.push_back(m_basis.back());
         m_basis.pop_back();
     }
-    for (unsigned i = 0; i < init_basis_size; ++i) {
-        offset_t idx = m_basis[i];
-        if (vec(idx).weight().is_neg()) {
-            m_basis[i] = m_basis.back();
-            m_basis.pop_back();
-            
-        }
-    }
     m_basis.append(m_zero);
     std::sort(m_basis.begin(), m_basis.end(), vector_lt_t(*this));
     m_zero.reset();