fix #3822

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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;

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.
 

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);