diff --git a/src/util/memory_manager.h b/src/util/memory_manager.h
index 7dab520df..af56c4507 100644
--- a/src/util/memory_manager.h
+++ b/src/util/memory_manager.h
@@ -128,6 +128,29 @@ void dealloc_svect(T * ptr) {
     memory::deallocate(ptr);
 }
 
+template <typename T>
+struct std_allocator {
+    using value_type = T;
+    // the constructors must be provided according to cpp docs
+    std_allocator() = default;
+    template <class U> constexpr std_allocator(const std_allocator<U>&) noexcept {}
+ 
+
+    T* allocate(std::size_t n) {
+        return static_cast<T*>(memory::allocate(n * sizeof(T)));
+    }
+
+    void deallocate(T* p, std::size_t n) {
+        memory::deallocate(p);
+    }
+};
+
+// the comparison operators must be provided according to cpp docs
+template <class T, class U>
+bool operator==(const std_allocator<T>&, const std_allocator<U>&) { return true; }
+template <class T, class U>
+bool operator!=(const std_allocator<T>&, const std_allocator<U>&) { return false; }
+
 struct mem_stat {
 };
 
diff --git a/src/util/vector.h b/src/util/vector.h
index 1cb25a8c4..55b52d745 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -33,6 +33,7 @@ Revision History:
 #include "util/memory_manager.h"
 #include "util/hash.h"
 #include "util/z3_exception.h"
+#include <vector>
 
 // disable warning for constant 'if' expressions.
 // these are used heavily in templates.
@@ -40,6 +41,8 @@ Revision History:
 #pragma warning(disable:4127)
 #endif
 
+template <typename T>
+using std_vector = std::vector<T, std_allocator<T>>;
 
 #if 0