diff --git a/src/muz/spacer/spacer_sym_mux.cpp b/src/muz/spacer/spacer_sym_mux.cpp
index 5dfb3a531..cfe0908d6 100644
--- a/src/muz/spacer/spacer_sym_mux.cpp
+++ b/src/muz/spacer/spacer_sym_mux.cpp
@@ -57,7 +57,7 @@ void sym_mux::register_decl(func_decl *fdecl) {
     m_muxes.insert(entry->m_variants.get(0), std::make_pair(entry, 0));
     m_muxes.insert(entry->m_variants.get(1), std::make_pair(entry, 1));
 }
-void sym_mux::ensure_capacity(sym_mux_entry &entry, unsigned sz) {
+void sym_mux::ensure_capacity(sym_mux_entry &entry, unsigned sz) const {
     while (entry.m_variants.size() < sz) {
         unsigned idx = entry.m_variants.size();
         entry.m_variants.push_back (mk_variant(entry.m_main, idx));
@@ -71,7 +71,7 @@ bool sym_mux::find_idx(func_decl * sym, unsigned & idx) const {
     return false;
 }
 
-func_decl * sym_mux::find_by_decl(func_decl* fdecl, unsigned idx) {
+func_decl * sym_mux::find_by_decl(func_decl* fdecl, unsigned idx) const {
     sym_mux_entry *entry = nullptr;
     if (m_entries.find(fdecl, entry)) {
         ensure_capacity(*entry, idx+1);
@@ -85,6 +85,7 @@ func_decl * sym_mux::shift_decl(func_decl * decl,
     std::pair<sym_mux_entry*,unsigned> entry;
     if (m_muxes.find(decl, entry)) {
         SASSERT(entry.second == src_idx);
+        ensure_capacity(*entry.first, tgt_idx + 1);
         return entry.first->m_variants.get(tgt_idx);
     }
     UNREACHABLE();
diff --git a/src/muz/spacer/spacer_sym_mux.h b/src/muz/spacer/spacer_sym_mux.h
index 9657b47d9..5690370bd 100644
--- a/src/muz/spacer/spacer_sym_mux.h
+++ b/src/muz/spacer/spacer_sym_mux.h
@@ -42,11 +42,11 @@ private:
     typedef obj_map<func_decl, std::pair<sym_mux_entry*, unsigned> > mux2entry_map;
 
     ast_manager &m;
-    decl2entry_map m_entries;
-    mux2entry_map m_muxes;
+    mutable decl2entry_map m_entries;
+    mutable mux2entry_map m_muxes;
 
     func_decl_ref mk_variant(func_decl *fdecl, unsigned i) const;
-    void ensure_capacity(sym_mux_entry &entry, unsigned sz) ;
+    void ensure_capacity(sym_mux_entry &entry, unsigned sz) const;
 
 public:
     sym_mux(ast_manager & m);
@@ -58,12 +58,13 @@ public:
     bool has_index(func_decl * sym, unsigned idx) const
     {unsigned v; return find_idx(sym, v) && idx == v;}
 
+    bool is_muxed(func_decl *fdecl) const {return m_muxes.contains(fdecl);}
 
     /**
        \brief Return symbol created from prefix, or 0 if the prefix
         was never used.
     */
-    func_decl * find_by_decl(func_decl* fdecl, unsigned idx);
+    func_decl * find_by_decl(func_decl* fdecl, unsigned idx) const;
 
     /**
        \brief Return true if the only multiplexed symbols which e contains are