diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp
index 893af7106..82d56f491 100644
--- a/src/ast/simplifiers/model_reconstruction_trail.cpp
+++ b/src/ast/simplifiers/model_reconstruction_trail.cpp
@@ -69,7 +69,7 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt
                     args.push_back(m.mk_var(i, d->get_domain(i)));
                 head = m.mk_app(d, args);
                 mrp.insert(head, def, dep);
-                TRACE("simplifier", tout << d << " " << def << " " << dep << "\n");
+                TRACE("simplifier", tout << mk_pp(d, m) << " " << mk_pp(def,m) << " " << "\n");
                 dependent_expr de(m, def, nullptr, dep);
                 add_vars(de, free_vars);
             }
diff --git a/src/ast/simplifiers/reduce_args_simplifier.cpp b/src/ast/simplifiers/reduce_args_simplifier.cpp
index 4ebd49127..f9c788792 100644
--- a/src/ast/simplifiers/reduce_args_simplifier.cpp
+++ b/src/ast/simplifiers/reduce_args_simplifier.cpp
@@ -328,7 +328,6 @@ class reduce_args_simplifier : public dependent_expr_simplifier {
         ptr_buffer<expr> new_args;
         var_ref_vector   new_vars(m);
         ptr_buffer<expr> new_eqs;
-        generic_model_converter * f_mc = alloc(generic_model_converter, m, "reduce_args");
         for (auto const& [f, map] : decl2arg2funcs)
             for (auto const& [t, new_def] : *map)
                 m_fmls.model_trail().hide(new_def);