From d3db2af81d6a9d6fb811c21a0660da8003329720 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Apr 2020 13:15:15 -0700 Subject: [PATCH] fix #3941 Signed-off-by: Nikolaj Bjorner --- src/muz/base/dl_context.cpp | 1 + src/muz/base/rule_properties.cpp | 1 - 2 files changed, 1 insertion(+), 1 deletion(-) 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; }