diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 1bf95ad39..9d2773326 100644 --- 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 index f0998747a..0499097f4 100644 --- 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; }