mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

fix crash in PDR engine when transformations don't produce output predicates

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-05-25 14:38:02 -07:00
parent 09945dc2cb
commit ccf10d0abe
2 changed files with 12 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/muz_qe/dl_mk_slice.cpp
View file

@ -710,6 +710,7 @@ namespace datalog {
void mk_slice::declare_predicates(rule_set const& src, rule_set& dst) { void mk_slice::declare_predicates(rule_set const& src, rule_set& dst) {
obj_map<func_decl, bit_vector>::iterator it = m_sliceable.begin(), end = m_sliceable.end(); obj_map<func_decl, bit_vector>::iterator it = m_sliceable.begin(), end = m_sliceable.end();
ptr_vector<sort> domain; ptr_vector<sort> domain;
bool has_output = false;
func_decl* f; func_decl* f;
for (; it != end; ++it) { for (; it != end; ++it) {
domain.reset(); domain.reset();
@ -731,8 +732,13 @@ namespace datalog {
} }
else if (src.is_output_predicate(p)) { else if (src.is_output_predicate(p)) {
dst.set_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) { bool mk_slice::rule_updated(rule const& r) {

6
src/muz_qe/pdr_dl_interface.cpp
View file

@ -133,6 +133,12 @@ lbool dl_interface::query(expr * query) {
--num_unfolds; --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(); query_pred = m_ctx.get_rules().get_output_predicate();
IF_VERBOSE(2, m_ctx.display_rules(verbose_stream());); IF_VERBOSE(2, m_ctx.display_rules(verbose_stream()););