diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp
index 6ffd0f745..560202ab3 100644
--- a/src/muz/fp/horn_tactic.cpp
+++ b/src/muz/fp/horn_tactic.cpp
@@ -241,7 +241,7 @@ class horn_tactic : public tactic {
                 verify(q, g, result, mc, pc);
             }
             g->set(pc.get());
-            g->set(mc.get());
+            g->add(mc.get());
         }
 
         void verify(expr* q,
@@ -282,12 +282,11 @@ 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());
+                    mc = mc2.get();
                     TRACE("dl", mc->display(tout << *md << "\n"););
                 }
                 break;
@@ -345,6 +344,7 @@ class horn_tactic : public tactic {
                 g->assert_expr(fml);
             }
             g->set_prec(goal::UNDER_OVER);
+            mc = g->mc();
         }
 
         void check_parameters() {