diff --git a/src/tests/util/buffer.cpp b/src/tests/util/buffer.cpp
index 6fc3a65ce..71caa5d41 100644
--- a/src/tests/util/buffer.cpp
+++ b/src/tests/util/buffer.cpp
@@ -20,14 +20,32 @@ static void loop(int n) {
         loop<C>(n-1);
 }
 
-void perftest() {
-    for (unsigned i = 0; i < 10000; i++)
-        loop<buffer<int>>(10000);
-//    for (unsigned i = 0; i < 10000; i++)
-//        loop<std::vector<int>>(10000);
+static void tst1() {
+    buffer<int> b1;
+    buffer<int> b2;
+    b1.push_back(10);
+    lean_assert(b1 != b2);
+    b2.push_back(20);
+    lean_assert(b1 != b2);
+    b2.pop_back();
+    b2.push_back(10);
+    lean_assert(b1 == b2);
+    b2.push_back(20);
+    b2.push_back(20);
+    lean_assert(b1 != b2);
+    b2.shrink(1);
+    lean_assert(b1 == b2);
+    b2.push_back(100);
+    lean_assert(b1 != b2);
+    b2 = b1;
+    lean_assert(b1 == b2);
+    buffer<int> b3(b1);
+    lean_assert(b3 == b1);
+    lean_assert(b1.back() == 10);
 }
 
 int main() {
     loop<buffer<int>>(100);
+    tst1();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/util/buffer.h b/src/util/buffer.h
index 6f3003ad8..1ef4537e4 100644
--- a/src/util/buffer.h
+++ b/src/util/buffer.h
@@ -73,7 +73,7 @@ public:
         return *this;
     }
 
-    bool operator==(buffer const & other) {
+    bool operator==(buffer const & other) const {
         if (size() != other.size()) {
             return false;
         } else {
@@ -85,6 +85,10 @@ public:
         }
     }
 
+    bool operator!=(buffer const & other) const {
+        return !operator==(other);
+    }
+
     T const & back() const { lean_assert(!empty() && m_pos > 0); return m_buffer[m_pos - 1]; }
     T & back() { lean_assert(!empty() && m_pos > 0); return m_buffer[m_pos - 1]; }
     T & operator[](unsigned idx) { lean_assert(idx < size());  return m_buffer[idx]; }