diff --git a/src/util/vector.h b/src/util/vector.h
index ea621b5fb..d684f43eb 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -30,6 +30,7 @@ Revision History:
 #include <functional>
 #include <memory>
 #include <type_traits>
+#include <utility>
 #include "util/memory_manager.h"
 #include "util/hash.h"
 #include "util/z3_exception.h"
@@ -558,7 +559,7 @@ public:
         for(; pos != e; ++pos, ++prev) {
             *prev = std::move(*pos);
         }
-        reinterpret_cast<SZ *>(m_data)[SIZE_IDX]--;
+        pop_back();
     }
 
     void erase(T const & elem) {
@@ -568,6 +569,20 @@ public:
         }
     }
 
+    /** Erase all elements that satisfy the given predicate. Returns the number of erased elements. */
+    template <typename UnaryPredicate>
+    SZ erase_if(UnaryPredicate should_erase) {
+        iterator i = begin();
+        iterator const e = end();
+        for (iterator j = begin(); j != e; ++j)
+            if (!should_erase(std::as_const(*j)))
+                *(i++) = std::move(*j);
+        SZ const count = e - i;
+        SASSERT_EQ(i - begin(), size() - count);
+        shrink(size() - count);
+        return count;
+    }
+
     void shrink(SZ s) {
         if (m_data) {
             SASSERT(s <= reinterpret_cast<SZ *>(m_data)[SIZE_IDX]);
@@ -756,7 +771,8 @@ using bool_vector        = svector<bool>;
 
 template<typename T>
 inline std::ostream& operator<<(std::ostream& out, svector<T> const& v) {
-    for (unsigned u : v) out << u << " ";
+    for (auto const& x : v)
+        out << x << " ";
     return out;
 }