diff --git a/src/math/automata/symbolic_automata_def.h b/src/math/automata/symbolic_automata_def.h
index 3be6a1da0..be38a60bc 100644
--- a/src/math/automata/symbolic_automata_def.h
+++ b/src/math/automata/symbolic_automata_def.h
@@ -24,6 +24,7 @@ Revision History:
 
 #include "math/automata/symbolic_automata.h"
 #include "util/hashtable.h"
+#include "util/vector.h"
 
 
 
@@ -311,7 +312,7 @@ symbolic_automata<T, M>::mk_determinstic_param(automaton_t& a, bool flip_accepta
     s2id.insert(set, p_state_id++);               // the index to the initial state is 0
     id2s.push_back(set);
     
-    svector<uint_set> todo; //States to visit
+    ::vector<uint_set> todo; //States to visit
     todo.push_back(set);
     
     uint_set state;
diff --git a/src/util/scoped_ptr_vector.h b/src/util/scoped_ptr_vector.h
index a9ef92766..0bd0fd47e 100644
--- a/src/util/scoped_ptr_vector.h
+++ b/src/util/scoped_ptr_vector.h
@@ -42,7 +42,7 @@ public:
     bool empty() const { return m_vector.empty(); }
     void resize(unsigned sz) { 
         if (sz < m_vector.size()) {
-            for (unsigned i = m_vector.size(); i < sz; i++)
+            for (unsigned i = m_vector.size(); i-- > sz; )
                 dealloc(m_vector[i]);
             m_vector.shrink(sz); 
         }