diff --git a/src/muz/base/dl_engine_base.h b/src/muz/base/dl_engine_base.h
index d6099e04c..2a5b91387 100644
--- a/src/muz/base/dl_engine_base.h
+++ b/src/muz/base/dl_engine_base.h
@@ -102,7 +102,7 @@ namespace datalog {
             throw default_exception(std::string("get_rules_along_trace is not supported for ") + m_name);
         }
         virtual proof_ref get_proof() {
-            return proof_ref(m.mk_asserted(m.mk_true()), m);
+            return proof_ref(m.mk_asserted(m.mk_false()), m);
         }
         virtual void add_callback(void *state,
                                   const t_new_lemma_eh new_lemma_eh,
diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp
index 7cc0fe58c..0c356b5ff 100644
--- a/src/muz/fp/horn_tactic.cpp
+++ b/src/muz/fp/horn_tactic.cpp
@@ -269,7 +269,7 @@ class horn_tactic : public tactic {
                 if (produce_proofs) {
                     proof_ref proof = m_ctx.get_proof();
                     pc = proof2proof_converter(m, proof);
-                    g->assert_expr(m.mk_false(), proof, nullptr);
+                    g->assert_expr(m.get_fact(proof), proof, nullptr);
                 }
                 else {
                     g->assert_expr(m.mk_false());