diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp
index 917a0796d..b7423c106 100644
--- a/src/muz/fp/horn_tactic.cpp
+++ b/src/muz/fp/horn_tactic.cpp
@@ -282,11 +282,13 @@ class horn_tactic : public tactic {
             }
             case l_false: {
                 // goal is sat
+                mc = concat(g->mc(), mc.get());
                 g->reset();
                 if (produce_models) {
                     model_ref md = m_ctx.get_model();
                     model_converter_ref mc2 = model2model_converter(md.get());
                     mc = concat(mc.get(), mc2.get());
+                    TRACE("dl", mc->display(tout << *md << "\n"););
                 }
                 break;
             }
diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp
index cb2888e2f..d95cd129f 100644
--- a/src/tactic/core/reduce_invertible_tactic.cpp
+++ b/src/tactic/core/reduce_invertible_tactic.cpp
@@ -95,6 +95,7 @@ public:
             g->inc_depth();
         }        
         result.push_back(g.get());
+        CTRACE("invertible_tactic", g->mc(), g->mc()->display(tout););
     }
 
     void cleanup() override {}