From 6761bf149592a6f0b16d1a00f392879823ec627f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 6 Apr 2020 16:33:00 -0700
Subject: [PATCH] fix #3822

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/base/dl_context.cpp | 11 +++++++++++
 src/muz/base/dl_context.h   |  2 ++
 src/muz/fp/horn_tactic.cpp  |  5 ++++-
 3 files changed, 17 insertions(+), 1 deletion(-)

diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index a69c40f1d..68b3f1e4d 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -880,6 +880,17 @@ namespace datalog {
         return r;
     }
 
+    bool context::is_monotone() {
+        try {
+            m_rule_properties.check_for_negated_predicates();
+            return true;
+        }
+        catch (...) {
+            return false;
+        }
+    }
+
+
     lbool context::query_from_lvl (expr* query, unsigned lvl) {
         m_mc = mk_skip_model_converter();
         m_last_status = OK;
diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index adb98592d..5a19bfd43 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -528,6 +528,8 @@ namespace datalog {
          */
         model_ref get_model();
 
+        bool is_monotone();
+
         /**
            \brief retrieve proof from derivation of the query.
 
diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp
index a95fae07a..a50fa692d 100644
--- a/src/muz/fp/horn_tactic.cpp
+++ b/src/muz/fp/horn_tactic.cpp
@@ -266,7 +266,10 @@ class horn_tactic : public tactic {
             switch (is_reachable) {
             case l_true: {
                 // goal is unsat
-                if (produce_proofs) {
+                if (!m_ctx.is_monotone()) {
+                    is_reachable = l_undef;
+                }
+                else if (produce_proofs) {
                     proof_ref proof = m_ctx.get_proof();
                     pc = proof2proof_converter(m, proof);
                     g->assert_expr(m.get_fact(proof), proof, nullptr);