From 5efdc58194ccc00490772c49ff4ba783fb80d520 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 15 May 2013 13:17:00 -0700 Subject: [PATCH] horn clause bit blasting: propagate output predicates for predicates without rules (most likely an UNSAT prog) Signed-off-by: Nuno Lopes --- src/muz_qe/dl_mk_bit_blast.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/muz_qe/dl_mk_bit_blast.cpp b/src/muz_qe/dl_mk_bit_blast.cpp index a1eeac6f5..136b8ffae 100644 --- a/src/muz_qe/dl_mk_bit_blast.cpp +++ b/src/muz_qe/dl_mk_bit_blast.cpp @@ -279,6 +279,13 @@ namespace datalog { result->add_rule(r); } } + + // copy output predicates without any rule (bit-blasting not really needed) + const func_decl_set& decls = source.get_output_predicates(); + for (func_decl_set::iterator I = decls.begin(), E = decls.end(); I != E; ++I) { + if (!result->contains(*I)) + result->set_output_predicate(*I); + } if (m_context.get_model_converter()) { filter_model_converter* fmc = alloc(filter_model_converter, m);