diff --git a/src/ast/polymorphism_inst.cpp b/src/ast/polymorphism_inst.cpp
index c34f03585c..5070f66d67 100644
--- a/src/ast/polymorphism_inst.cpp
+++ b/src/ast/polymorphism_inst.cpp
@@ -57,9 +57,11 @@ namespace polymorphism {
         m_assertions.push_back(e);
         t.push(push_back_vector(m_assertions));
         u.collect_type_vars(e, inst.m_tvs);
+        auto* init = alloc(substitution, m);
         inst.m_subst = alloc(substitutions);
-        inst.m_subst->insert(alloc(substitution, m));
+        inst.m_subst->insert(init);
         m_instances.insert(e, inst);            
+        t.push(new_obj_trail(init));
         t.push(new_obj_trail(inst.m_subst));
         t.push(insert_map(m_instances, e));        
     }
diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp
index 8ab6b31672..ff656b7ef4 100644
--- a/src/cmd_context/tptp_frontend.cpp
+++ b/src/cmd_context/tptp_frontend.cpp
@@ -553,8 +553,10 @@ class tptp_parser {
     // Multi-argument A * B > C is represented as Array(A, Array(B, C)) (curried).
     sort* get_ho_sort(ptr_vector<sort> const& domain, sort* range) {
         sort* s = range;
-        for (int i = (int)domain.size() - 1; i >= 0; --i)
+        for (int i = (int)domain.size() - 1; i >= 0; --i) {
             s = m_array.mk_array_sort(domain[i], s);
+            m_pinned_sorts.push_back(s);
+        }
         return s;
     }
 
@@ -1369,6 +1371,7 @@ class tptp_parser {
                 sort* arg_sort = arg->get_sort();
                 sort* result_sort = m.is_bool(arg_sort) ? m.mk_bool_sort() : m_univ;
                 sort* arr_sort = m_array.mk_array_sort(arg_sort, result_sort);
+                m_pinned_sorts.push_back(arr_sort);
                 e = coerce_arg(e, arr_sort);
             } else {
                 // Array but domain may not match arg sort — coerce arg
@@ -2217,6 +2220,7 @@ class tptp_parser {
                     // If arg is Bool-sorted, result is likely Bool too (modal/connective application)
                     sort* result_sort = m.is_bool(arg_sort) ? m.mk_bool_sort() : m_univ;
                     sort* arr_sort = m_array.mk_array_sort(arg_sort, result_sort);
+                    m_pinned_sorts.push_back(arr_sort);
                     e = coerce_arg(e, arr_sort);
                 } else {
                     // Array but domain may not match arg sort — coerce arg
diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg
index 782e281b77..29a10c2d52 100644
--- a/src/math/lp/lp_params_helper.pyg
+++ b/src/math/lp/lp_params_helper.pyg
@@ -14,6 +14,6 @@ def_module_params(module_name='lp',
                           ('lcube', BOOL, True, 'use the largest cube test for integer feasibility'),
                           ('lcube_flips', UINT, 16, 'maximal number of coordinate flips when repairing the rounded largest cube center, only relevant when lcube is true'),
                           ('int_hammer_period', UINT, 4, 'period (in final_check calls) for the integer cut/cube heuristics (find_cube, hnf, gomory); a smaller value calls them more often'),
-                         ('random_hammers', BOOL, True, 'draw the periodic integer heuristic gates (find_cube, lcube, hnf, gomory, dio) at random with the same 1/period rate instead of a deterministic every-k-th-call modulus'),
+                          ('random_hammers', BOOL, True, 'draw the periodic integer heuristic gates (find_cube, lcube, hnf, gomory, dio) at random with the same 1/period rate instead of a deterministic every-k-th-call modulus'),
                          ))