fix #3791

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

src/muz/base/dl_context.cpp

@@ -885,13 +885,8 @@ namespace datalog {
     }
 
     bool context::is_monotone() {
-        try {
-            m_rule_properties.check_for_negated_predicates();
-            return true;
-        }
-        catch (...) {
-            return false;
-        }
+        // only the spacer engine uses monotone semantics.
+        return get_engine() == SPACER_ENGINE;
     }
 
 

src/muz/base/dl_util.cpp

@@ -348,7 +348,7 @@ namespace datalog {
 
     void resolve_rule(rule_manager& rm, rule const& r1, rule const& r2, unsigned idx, 
                       expr_ref_vector const& s1, expr_ref_vector const& s2, rule& res) {
-        if (!r1.get_proof()) {
+        if (!r1.get_proof() || !r2.get_proof()) {
             return;
         }
         SASSERT(r2.get_proof());

src/muz/fp/horn_tactic.cpp

@@ -249,7 +249,6 @@ class horn_tactic : public tactic {
                     proof_converter_ref & pc) {
 
             lbool is_reachable = l_undef;
-
             try {
                 is_reachable = m_ctx.query(q);
             }