From 108bbb0597231f965f270b4e310f6f61f619b99d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Nov 2012 11:50:17 +0100 Subject: [PATCH] add missing check for difference logic fragment for clause heads Signed-off-by: Nikolaj Bjorner --- src/api/api_datalog.cpp | 1 - src/muz_qe/pdr_context.cpp | 3 ++- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index 222d91081..394df7a17 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -130,7 +130,6 @@ namespace api { ast_manager& m = m_context.get_manager(); datalog::context ctx(m, m_context.get_fparams()); - // datalog::rule_manager& rm = ctx.get_rule_manager(); for (unsigned i = 0; i < num_rules; ++i) { expr* rule = rules[i], *body, *head; while (true) { diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index c67cc6ad1..922a09448 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -1283,9 +1283,10 @@ namespace pdr { for (it = rules.begin(); it != end; ++it) { datalog::rule& r = *(*it); unsigned utsz = r.get_uninterpreted_tail_size(); + forms.push_back(r.get_head()); for (unsigned i = utsz; i < r.get_tail_size(); ++i) { forms.push_back(r.get_tail(i)); - } + } } m_is_dl = is_difference_logic(m, forms.size(), forms.c_ptr()); }