diff --git a/src/util/buffer.h b/src/util/buffer.h
index eae5592e1..b562e4f78 100644
--- a/src/util/buffer.h
+++ b/src/util/buffer.h
@@ -153,6 +153,15 @@ public:
         m_pos--;
     }
 
+    void erase_elem(T const & elem) {
+        for (unsigned i = 0; i < size(); i++) {
+            if (m_buffer[i] == elem) {
+                erase(i);
+                return;
+            }
+        }
+    }
+
     void insert(unsigned idx, T const & elem) {
         using std::swap;
         lean_assert(idx <= size());