diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 97c780de6..dfe5b8fc4 100644
--- a/src/muz/base/dl_context.cpp
+++ b/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;
     }
 
 
diff --git a/src/muz/base/dl_util.cpp b/src/muz/base/dl_util.cpp
index fdafea924..83902846c 100644
--- a/src/muz/base/dl_util.cpp
+++ b/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());
diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp
index a50fa692d..4077bc7c5 100644
--- a/src/muz/fp/horn_tactic.cpp
+++ b/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);
             }