diff --git a/src/muz/pdr/pdr_manager.cpp b/src/muz/pdr/pdr_manager.cpp
index 1e808c455..cc5046fe1 100644
--- a/src/muz/pdr/pdr_manager.cpp
+++ b/src/muz/pdr/pdr_manager.cpp
@@ -159,22 +159,17 @@ namespace pdr {
             out << "(pop)\n";
         }
     }
-
-    vector<std::string> manager::get_state_suffixes() {
-        vector<std::string> res;
-        res.push_back("_n");
-        return res;
-    }
     
     manager::manager(smt_params& fparams, unsigned max_num_contexts, ast_manager& manager) :
         m(manager),
         m_fparams(fparams),
-        m_brwr(m),
-        m_mux(m, get_state_suffixes()),
+        m_brwr(m),        
+        m_mux(m, m_state_suffixes),
         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 580075b78..d36360ef9 100644
--- a/src/muz/pdr/pdr_manager.h
+++ b/src/muz/pdr/pdr_manager.h
@@ -81,6 +81,7 @@ namespace pdr {
         
         mutable bool_rewriter m_brwr;
         
+        vector<std::string>   m_state_suffixes;
         sym_mux               m_mux;
         expr_ref              m_background;
         decl_vector           m_o0_preds;
@@ -89,9 +90,7 @@ namespace pdr {
         /** whenever we need an unique number, we get this one and increase */
         unsigned m_next_unique_num;
         
-        
-        static vector<std::string> get_state_suffixes();
-        
+               
         unsigned n_index() const { return 0; }
         unsigned o_index(unsigned i) const { return i+1; }