From 299a6f4aeea2c413c427f8ebcd3726a7096e7209 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 13 Apr 2020 14:00:21 -0700
Subject: [PATCH] fix #3939

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/fp/horn_tactic.cpp                   | 2 ++
 src/tactic/core/reduce_invertible_tactic.cpp | 1 +
 2 files changed, 3 insertions(+)

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 {}