diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 8d643a348..fefb400ed 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -2755,7 +2755,7 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
         app const * cls   = to_app(f1);
         unsigned num_args = cls->get_num_args();
 #ifdef Z3DEBUG
-        vector<bool> found;
+        svector<bool> found;
 #endif
         for (unsigned i = 0; i < num_args; i++) {
             expr * lit = cls->get_arg(i);
diff --git a/src/util/bit_vector.cpp b/src/util/bit_vector.cpp
index e3a2bc331..0d67f1f79 100644
--- a/src/util/bit_vector.cpp
+++ b/src/util/bit_vector.cpp
@@ -208,8 +208,8 @@ void bit_vector::display(std::ostream & out) const {
 
 void fr_bit_vector::reset() {
     unsigned sz = size();
-    vector<unsigned>::const_iterator it  = m_one_idxs.begin();
-    vector<unsigned>::const_iterator end = m_one_idxs.end();
+    unsigned_vector::const_iterator it  = m_one_idxs.begin();
+    unsigned_vector::const_iterator end = m_one_idxs.end();
     for (; it != end; ++it) {
         unsigned idx = *it;
         if (idx < sz)
@@ -217,5 +217,3 @@ void fr_bit_vector::reset() {
     }
     m_one_idxs.reset();
 }
-
-
diff --git a/src/util/bit_vector.h b/src/util/bit_vector.h
index 1d6083717..2c641c5a6 100644
--- a/src/util/bit_vector.h
+++ b/src/util/bit_vector.h
@@ -204,7 +204,7 @@ inline std::ostream & operator<<(std::ostream & out, bit_vector const & b) {
    This class should be used if the reset is frequently called.
 */
 class fr_bit_vector : private bit_vector {
-    svector<unsigned> m_one_idxs;
+    unsigned_vector m_one_idxs;
 public:
     void reset();
 
diff --git a/src/util/mpff.h b/src/util/mpff.h
index de71ec75e..8d4c853af 100644
--- a/src/util/mpff.h
+++ b/src/util/mpff.h
@@ -107,7 +107,7 @@ class mpff_manager {
     
     unsigned          m_precision;      //!< Number of words in the significand. Must be an even number.
     unsigned          m_precision_bits; //!< Number of bits in the significand.  Must be 32*m_precision.
-    vector<unsigned>  m_significands;   //!< Array containing all significands.
+    unsigned_vector   m_significands;   //!< Array containing all significands.
     unsigned          m_capacity;       //!< Number of significands that can be stored in m_significands.
     bool              m_to_plus_inf;    //!< If True, then round to plus infinity, otherwise to minus infinity
     id_gen            m_id_gen;