From d0d4ab7955d7e5fe61c68da125fd20e3e3702278 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 20 Feb 2022 10:33:29 +0200
Subject: [PATCH] #5820

---
 src/muz/fp/horn_tactic.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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() {