diff --git a/src/muz/pdr/pdr_manager.cpp b/src/muz/pdr/pdr_manager.cpp
index cc5046fe1..319f38255 100644
--- a/src/muz/pdr/pdr_manager.cpp
+++ b/src/muz/pdr/pdr_manager.cpp
@@ -164,12 +164,11 @@ namespace pdr {
         m(manager),
         m_fparams(fparams),
         m_brwr(m),        
-        m_mux(m, m_state_suffixes),
+        m_mux(m),
         m_background(m.mk_true(), m),
         m_contexts(fparams, max_num_contexts, m),
         m_next_unique_num(0)
     {        
-        m_state_suffixes.push_back("_n");
     }
 
 
diff --git a/src/muz/pdr/pdr_manager.h b/src/muz/pdr/pdr_manager.h
index d36360ef9..790e2465d 100644
--- a/src/muz/pdr/pdr_manager.h
+++ b/src/muz/pdr/pdr_manager.h
@@ -80,8 +80,7 @@ namespace pdr {
         smt_params& m_fparams;
         
         mutable bool_rewriter m_brwr;
-        
-        vector<std::string>   m_state_suffixes;
+               
         sym_mux               m_mux;
         expr_ref              m_background;
         decl_vector           m_o0_preds;
diff --git a/src/muz/pdr/pdr_sym_mux.cpp b/src/muz/pdr/pdr_sym_mux.cpp
index be20c502d..198752846 100644
--- a/src/muz/pdr/pdr_sym_mux.cpp
+++ b/src/muz/pdr/pdr_sym_mux.cpp
@@ -28,9 +28,10 @@ Revision History:
 
 using namespace pdr;
 
-sym_mux::sym_mux(ast_manager & m, vector<std::string> & suffixes)
-    : m(m), m_ref_holder(m), m_next_sym_suffix_idx(0), m_suffixes(suffixes)
-{
+sym_mux::sym_mux(ast_manager & m)
+    : m(m), m_ref_holder(m), 
+      m_next_sym_suffix_idx(0) {
+    m_suffixes.push_back("_n");
     unsigned suf_sz = m_suffixes.size();
     for(unsigned i = 0; i < suf_sz; ++i) {
         symbol suff_sym = symbol(m_suffixes[i].c_str());
@@ -53,7 +54,8 @@ std::string sym_mux::get_suffix(unsigned i) {
         m_used_suffixes.insert(new_syffix_sym);
         m_suffixes.push_back(new_suffix);
     }
-    return m_suffixes[i];
+    std::string result = m_suffixes[i];
+    return result;
 }
 
 void sym_mux::create_tuple(func_decl* prefix, unsigned arity, sort * const * domain, sort * range, 
diff --git a/src/muz/pdr/pdr_sym_mux.h b/src/muz/pdr/pdr_sym_mux.h
index a07b712ca..bc1819539 100644
--- a/src/muz/pdr/pdr_sym_mux.h
+++ b/src/muz/pdr/pdr_sym_mux.h
@@ -46,7 +46,7 @@ private:
     mutable unsigned       m_next_sym_suffix_idx;
     mutable symbols        m_used_suffixes;
     /** Here we have default suffixes for each of the variants */
-    vector<std::string> m_suffixes;
+    vector<std::string>    m_suffixes;
 
 
     /**
@@ -94,7 +94,7 @@ private:
 
     expr_ref isolate_o_idx(expr* e, unsigned idx) const;
 public:
-    sym_mux(ast_manager & m, vector<std::string> & suffixes);
+    sym_mux(ast_manager & m);
 
     ast_manager & get_manager() const { return m; }