diff --git a/src/test/ast.cpp b/src/test/ast.cpp
index fce8dafc6..b59e2a612 100644
--- a/src/test/ast.cpp
+++ b/src/test/ast.cpp
@@ -62,7 +62,7 @@ static void tst1() {
 //     SASSERT(foo_foo_x2 == foo_foo_x);
 }
 
-void tst2() {
+static void tst2() {
 //     ast_manager m;
 //     ast_vector<ast> m_nodes(m);
 
diff --git a/src/test/main.cpp b/src/test/main.cpp
index 31d71226c..dc253f36d 100644
--- a/src/test/main.cpp
+++ b/src/test/main.cpp
@@ -207,6 +207,7 @@ int main(int argc, char ** argv) {
     TST(horn_subsume_model_converter);
     TST(model2expr);
     TST(rcf);
+    TST(hilbert_basis);
 }
 
 void initialize_mam() {}
diff --git a/src/util/heap.h b/src/util/heap.h
index dfb741e13..75b41e329 100644
--- a/src/util/heap.h
+++ b/src/util/heap.h
@@ -238,6 +238,24 @@ public:
         m_values.swap(other.m_values);
         m_value2indices.swap(other.m_value2indices);
     }
+
+    /**
+       \brief return set of values in heap that are less or equal to val.
+     */
+    void find_le(int val, int_vector& result) {
+        int_vector todo;
+        todo.push_back(1);
+        while (!todo.empty()) {
+            int index = todo.back();
+            todo.pop_back();
+            if (index < static_cast<int>(m_values.size()) &&
+                !less_than(val, m_values[index])) {
+                result.push_back(m_values[index]);
+                todo.push_back(left(index));
+                todo.push_back(right(index));
+            }
+        }
+    }
   
 };
 
diff --git a/src/util/vector.h b/src/util/vector.h
index 484c406c3..a9d36b202 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -179,6 +179,9 @@ public:
     }
 
     vector & operator=(vector const & source) {
+        if (this == &source) {
+            return *this;
+        }
         destroy();
         if (source.m_data) {
             copy_core(source);