diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index b5d07ae1e..f04d445e1 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -93,29 +93,29 @@ public:
             }
             if (m.are_distinct(x->get_char(), y->get_char())) {
                 expr_ref fml(m.mk_false(), m);
-                return sym_expr::mk_pred(fml, x->sort());
+                return sym_expr::mk_pred(fml, x->get_sort());
             }
         }
-        var_ref v(m.mk_var(0, x->sort()), m);
+        var_ref v(m.mk_var(0, x->get_sort()), m);
         expr_ref fml1 = x->accept(v);
         expr_ref fml2 = y->accept(v);
         if (m.is_true(fml1)) return y;
         if (m.is_true(fml2)) return x;
         expr_ref fml(m.mk_and(fml1, fml2), m);
-        return sym_expr::mk_pred(fml, x->sort());
+        return sym_expr::mk_pred(fml, x->get_sort());
     }
     virtual T mk_or(T x, T y) {
         if (x->is_char() && y->is_char() &&
             x->get_char() == y->get_char()) {
             return x;
         }
-        var_ref v(m.mk_var(0, x->sort()), m);
+        var_ref v(m.mk_var(0, x->get_sort()), m);
         expr_ref fml1 = x->accept(v);
         expr_ref fml2 = y->accept(v);        
         if (m.is_false(fml1)) return y;
         if (m.is_false(fml2)) return x;
         expr_ref fml(m.mk_or(fml1, fml2), m);
-        return sym_expr::mk_pred(fml, x->sort());
+        return sym_expr::mk_pred(fml, x->get_sort());
     }
 
     virtual T mk_and(unsigned sz, T const* ts) {
@@ -151,7 +151,7 @@ public:
         if (x->is_range()) {
             // TBD check lower is below upper.
         }
-        expr_ref v(m.mk_fresh_const("x", x->sort()), m);
+        expr_ref v(m.mk_fresh_const("x", x->get_sort()), m);
         expr_ref fml = x->accept(v);
         if (m.is_true(fml)) {
             return l_true;
@@ -162,9 +162,9 @@ public:
         return m_solver.check_sat(fml);
     }
     virtual T mk_not(T x) {
-        var_ref v(m.mk_var(0, x->sort()), m);
+        var_ref v(m.mk_var(0, x->get_sort()), m);
         expr_ref fml(m.mk_not(x->accept(v)), m);
-        return sym_expr::mk_pred(fml, x->sort());
+        return sym_expr::mk_pred(fml, x->get_sort());
     }
 };
 
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 718658652..040bae1b4 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -51,7 +51,7 @@ public:
     bool is_char() const { return m_ty == t_char; }
     bool is_pred() const { return !is_char(); }
     bool is_range() const { return m_ty == t_range; }
-    sort* sort() const { return m_sort; }
+    sort* get_sort() const { return m_sort; }
     expr* get_char() const { SASSERT(is_char()); return m_t; }
 
 };
diff --git a/src/math/automata/symbolic_automata_def.h b/src/math/automata/symbolic_automata_def.h
index 90dd98d10..6cb3d6339 100644
--- a/src/math/automata/symbolic_automata_def.h
+++ b/src/math/automata/symbolic_automata_def.h
@@ -32,14 +32,14 @@ typedef std::pair<unsigned, unsigned> unsigned_pair;
 template<class T, class M>
 typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_total(automaton_t& a) {
     unsigned dead_state = a.num_states();
-    moves_t mvs;
+    moves_t mvs, new_mvs;
     for (unsigned i = 0; i < dead_state; ++i) {
         mvs.reset();
         a.get_moves(i, mvs, true);
         refs_t vs(m);
         
         for (unsigned j = 0; j < mvs.size(); ++j) {
-            mv.push_back(mvs[j]());
+            vs.push_back(mvs[j]());
         }
         ref_t cond(m_ba.mk_not(m_ba.mk_or(vs.size(), vs.c_ptr())), m);
         lbool is_sat = m_ba.is_sat(cond);