diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 8f1718141..cfad0d394 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1322,7 +1322,7 @@ void cmd_context::restore_func_decls(unsigned old_sz) {
         sf_pair const & p = *it;
         erase_func_decl_core(p.first, p.second);
     }
-    m_func_decls_stack.shrink(old_sz);
+    m_func_decls_stack.resize(old_sz);
 }
 
 void cmd_context::restore_psort_decls(unsigned old_sz) {
@@ -1389,7 +1389,7 @@ void cmd_context::restore_assertions(unsigned old_sz) {
     if (produce_unsat_cores())
         restore(m(), m_assertion_names, old_sz);
     if (m_interactive_mode)
-        m_assertion_strings.shrink(old_sz);
+        m_assertion_strings.resize(old_sz);
 }
 
 void cmd_context::pop(unsigned n) {
@@ -1724,8 +1724,8 @@ void cmd_context::display_statistics(bool show_total_time, double total_time) {
 void cmd_context::display_assertions() {
     if (!m_interactive_mode)
         throw cmd_exception("command is only available in interactive mode, use command (set-option :interactive-mode true)");
-    vector<std::string>::const_iterator it  = m_assertion_strings.begin();
-    vector<std::string>::const_iterator end = m_assertion_strings.end();
+    std::vector<std::string>::const_iterator it  = m_assertion_strings.begin();
+    std::vector<std::string>::const_iterator end = m_assertion_strings.end();
     regular_stream() << "(";
     for (bool first = true; it != end; ++it) {
         std::string const & s = *it;
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 865999042..be3a1f4f8 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -22,6 +22,7 @@ Notes:
 #define CMD_CONTEXT_H_
 
 #include<sstream>
+#include<vector>
 #include"ast.h"
 #include"ast_printer.h"
 #include"pdecl.h"
@@ -38,6 +39,7 @@ Notes:
 #include"scoped_ptr_vector.h"
 #include"context_params.h"
 
+
 class func_decls {
     func_decl * m_decls;
 public:
@@ -189,7 +191,7 @@ protected:
     // 
     ptr_vector<pdecl>            m_aux_pdecls;
     ptr_vector<expr>             m_assertions;
-    vector<std::string>          m_assertion_strings;
+    std::vector<std::string>     m_assertion_strings;
     ptr_vector<expr>             m_assertion_names; // named assertions are represented using boolean variables.
 
     struct scope {