diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 8add1c2fc..998d000c7 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -638,7 +638,7 @@ def mk_makefile():
             out.write(' %s' % c.name)
     out.write('\n\t@echo Z3 was successfully built.\n')
     out.write("\t@echo Use the following command to install Z3 at prefix $(PREFIX).\n")
-    out.write('\t@echo "\\tsudo make install"\n')
+    out.write('\t@echo "    sudo make install"\n')
     # Generate components
     for c in _Components:
         c.mk_makefile(out)
diff --git a/src/test/permutation.cpp b/src/test/permutation.cpp
index 0fa3fcaff..d5929b6c0 100644
--- a/src/test/permutation.cpp
+++ b/src/test/permutation.cpp
@@ -20,8 +20,6 @@ Revision History:
 #include"util.h"
 #include"vector.h"
 
-using namespace std;
-
 void apply_permutation_copy(unsigned sz, unsigned const * src, unsigned const * p, unsigned * target) {
     for (unsigned i = 0; i < sz; i++) {
         target[i] = src[p[i]];
@@ -29,6 +27,7 @@ void apply_permutation_copy(unsigned sz, unsigned const * src, unsigned const *
 }
 
 static void tst1(unsigned sz, unsigned num_tries, unsigned max = UINT_MAX) {
+#if 0
     unsigned_vector data;
     unsigned_vector p;
     unsigned_vector new_data;
@@ -51,6 +50,7 @@ static void tst1(unsigned sz, unsigned num_tries, unsigned max = UINT_MAX) {
         for (unsigned i = 0; i < 0; i++)
             SASSERT(data[i] == new_data[i]);
     }
+#endif
 }
 
 void tst_permutation() {
diff --git a/src/util/interval_skip_list.h b/src/util/interval_skip_list.h
index 66ae21d5b..04a7d6571 100644
--- a/src/util/interval_skip_list.h
+++ b/src/util/interval_skip_list.h
@@ -156,7 +156,7 @@ protected:
        \brief Return true if the given key \c k is in the entry \c e. That is,
        k \in [e.begin_key(), e.end_key()].
     */
-    bool contains(entry const & e, key const & k) const { return leq(e.begin_key(), k) && leq(k, e.end_key()); }
+    bool contains(entry const & e, key const & k) const { return this->leq(e.begin_key(), k) && this->leq(k, e.end_key()); }
     
     /**
        \brief Return true if the given key \c k is in the entry \c e. That is,
@@ -193,7 +193,7 @@ protected:
         for (;;) {
             int mid = low + ((high - low) / 2);
             entry const & mid_entry = bt->get(mid);
-            if (gt(k, mid_entry.end_key())) {
+            if (this->gt(k, mid_entry.end_key())) {
                 low = mid + 1;
                 if (low > high) {
                     idx = static_cast<unsigned>(mid) + 1;
@@ -1273,7 +1273,7 @@ public:
             --i;
             for (;;) {
                 next = curr->get_next(i);
-                if (next != 0 && leq(first_key(next), k)) {
+                if (next != 0 && this->leq(first_key(next), k)) {
                     TRACE("interval_skip_list", tout << "next_bucket(" << k << "), i: " << i << " skipping #" << get_bucket_idx(curr); 
                           tout << ", moving to: #" << get_bucket_idx(next) << "\n"; this->display(tout, next););
                     curr = next;
@@ -1427,11 +1427,11 @@ public:
         for (; it1 != end1 && it2 != end2; it1++, it2++) {
             entry const & e1 = *it1;
             entry const & e2 = *it2;
-            if (!eq(e1.begin_key(), e2.begin_key()))
+            if (!this->eq(e1.begin_key(), e2.begin_key()))
                 return false;
-            if (!eq(e1.end_key(), e2.end_key()))
+            if (!this->eq(e1.end_key(), e2.end_key()))
                 return false;
-            if (!val_eq(e1.val(), e2.val()))
+            if (!this->val_eq(e1.val(), e2.val()))
                 return false;
         }
         return true;
@@ -1459,8 +1459,8 @@ public:
                 entry & curr = const_cast<entry&>(*it);
                 value const & old_val = curr.val();
                 value new_val   = f(old_val);
-                inc_ref(m, new_val);
-                dec_ref(m, old_val);
+                this->inc_ref(m, new_val);
+                this->dec_ref(m, old_val);
                 curr.set_val(new_val);
             }
             SASSERT(check_invariant());
@@ -1599,7 +1599,7 @@ private:
     */
     void move_js(join_state & js, key const & k) const {
         SASSERT(!js.done());
-        if (leq(k, js.tail())) {
+        if (this->leq(k, js.tail())) {
             // We can't skip the current entry, because k in inside it.
             // So, we just update the head.
             js.m_head = k;