fix #3941

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Apr 13, 2020 · d3db2af · d3db2af
1 parent b4e7730
commit d3db2af
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 1 deletion.
diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
@@ -569,6 +569,7 @@ namespace datalog {
 
     void context::check_rules(rule_set& r) {
         m_rule_properties.set_generate_proof(generate_proof_trace());
+        TRACE("dl", m_rule_set.display(tout););
         switch(get_engine()) {
         case DATALOG_ENGINE:
             m_rule_properties.collect(r);

diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp
@@ -257,7 +257,6 @@ void rule_properties::reset() {
     m_negative_rules.reset();
     m_inf_sort.reset();
     m_collected = false;
-    m_is_monotone = true;
     m_generate_proof = false;
 }