diff --git a/src/ast/polymorphism_inst.cpp b/src/ast/polymorphism_inst.cpp
index 42dd516f9..4da83ee10 100644
--- a/src/ast/polymorphism_inst.cpp
+++ b/src/ast/polymorphism_inst.cpp
@@ -38,29 +38,30 @@ namespace polymorphism {
 
         if (!u.has_type_vars(e))
             return;
-            // insert e into the occurs list for polymorphic roots
-            ast_mark seen;
-            for (auto* f : inst.m_poly_fns) {
-                f = m.poly_root(f);
-                if (seen.is_marked(f))
-                    continue;
-                seen.mark(f, true);
-                if (!m_occurs.contains(f)) {
-                    m_occurs.insert(f, ptr_vector<expr>());
-                    t.push(insert_map(m_occurs, f));
-                }
-                auto& es = m_occurs.find(f);
-                es.push_back(e);
-                t.push(remove_back(m_occurs, f));
+        
+        // insert e into the occurs list for polymorphic roots
+        ast_mark seen;
+        for (auto* f : inst.m_poly_fns) {
+            f = m.poly_root(f);
+            if (seen.is_marked(f))
+                continue;
+            seen.mark(f, true);
+            if (!m_occurs.contains(f)) {
+                m_occurs.insert(f, ptr_vector<expr>());
+                t.push(insert_map(m_occurs, f));
             }
-            m_assertions.push_back(e);
-            t.push(push_back_vector(m_assertions));
-            u.collect_type_vars(e, inst.m_tvs);
-            inst.m_subst = alloc(substitutions);
-            inst.m_subst->insert(alloc(substitution, m));
-            m_instances.insert(e, inst);            
-            t.push(new_obj_trail(inst.m_subst));
-            t.push(insert_map(m_instances, e));        
+            auto& es = m_occurs.find(f);
+            es.push_back(e);
+            t.push(remove_back(m_occurs, f));
+        }
+        m_assertions.push_back(e);
+        t.push(push_back_vector(m_assertions));
+        u.collect_type_vars(e, inst.m_tvs);
+        inst.m_subst = alloc(substitutions);
+        inst.m_subst->insert(alloc(substitution, m));
+        m_instances.insert(e, inst);            
+        t.push(new_obj_trail(inst.m_subst));
+        t.push(insert_map(m_instances, e));        
     }
 
     void inst::collect_instantiations(expr* e) {
diff --git a/src/ast/polymorphism_util.cpp b/src/ast/polymorphism_util.cpp
index 2fe271fc5..60048fe41 100644
--- a/src/ast/polymorphism_util.cpp
+++ b/src/ast/polymorphism_util.cpp
@@ -41,8 +41,10 @@ namespace polymorphism {
         vector<parameter> ps;
         for (unsigned i = 0; i < n; ++i) {
             auto p = s->get_parameter(i);
-            if (p.is_ast() && is_sort(p.get_ast()))
-                ps.push_back(parameter((*this)(to_sort(p.get_ast()))));
+            if (p.is_ast() && is_sort(p.get_ast())) {
+                sort_ref s = (*this)(to_sort(p.get_ast()));
+                ps.push_back(parameter(s.get()));
+            }
             else
                 ps.push_back(p);
         }
@@ -101,11 +103,11 @@ namespace polymorphism {
                 if (pending)
                     continue;
                 todo.pop_back();
-                ptr_buffer<sort> sorts;
+                domain.reset();
                 for (unsigned i = 0; i < q->get_num_decls(); ++i)
-                    sorts.push_back((*this)(q->get_decl_sort(i)));
+                    domain.push_back((*this)(q->get_decl_sort(i)));
                 quantifier* q2 = 
-                    m.mk_quantifier(q->get_kind(), q->get_num_decls(), sorts.data(), q->get_decl_names(), result.get(q->get_expr()->get_id()),
+                    m.mk_quantifier(q->get_kind(), q->get_num_decls(), domain.data(), q->get_decl_names(), result.get(q->get_expr()->get_id()),
                     q->get_weight(),
                     q->get_qid(), q->get_skid(), 
                     q->get_num_patterns(), patterns.data(), q->get_num_no_patterns(), no_patterns.data()