From ccf10d0abe86c86c66bc5e7908d3f5deda042d10 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 25 May 2013 14:38:02 -0700 Subject: [PATCH] fix crash in PDR engine when transformations don't produce output predicates Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_mk_slice.cpp | 6 ++++++ src/muz_qe/pdr_dl_interface.cpp | 6 ++++++ 2 files changed, 12 insertions(+) diff --git a/src/muz_qe/dl_mk_slice.cpp b/src/muz_qe/dl_mk_slice.cpp index 1a97c1b81..5b9d43acc 100644 --- a/src/muz_qe/dl_mk_slice.cpp +++ b/src/muz_qe/dl_mk_slice.cpp @@ -710,6 +710,7 @@ namespace datalog { void mk_slice::declare_predicates(rule_set const& src, rule_set& dst) { obj_map::iterator it = m_sliceable.begin(), end = m_sliceable.end(); ptr_vector domain; + bool has_output = false; func_decl* f; for (; it != end; ++it) { domain.reset(); @@ -731,8 +732,13 @@ namespace datalog { } else if (src.is_output_predicate(p)) { dst.set_output_predicate(p); + has_output = true; } } + // disable slicing if the output predicates don't occur in rules. + if (!has_output) { + m_predicates.reset(); + } } bool mk_slice::rule_updated(rule const& r) { diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp index 3ff54e68e..437c08f6a 100644 --- a/src/muz_qe/pdr_dl_interface.cpp +++ b/src/muz_qe/pdr_dl_interface.cpp @@ -133,6 +133,12 @@ lbool dl_interface::query(expr * query) { --num_unfolds; } } + + if (m_ctx.get_rules().get_output_predicates().empty()) { + m_context->set_unsat(); + return l_false; + } + query_pred = m_ctx.get_rules().get_output_predicate(); IF_VERBOSE(2, m_ctx.display_rules(verbose_stream()););