diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp index f2f149971..a03a9c71e 100644 --- a/src/muz/transforms/dl_mk_bit_blast.cpp +++ b/src/muz/transforms/dl_mk_bit_blast.cpp @@ -264,7 +264,6 @@ namespace datalog { } rule_set * operator()(rule_set const & source) { - // TODO pc if (!m_context.xform_bit_blast()) { return nullptr; } @@ -300,8 +299,7 @@ namespace datalog { // copy output predicates without any rule (bit-blasting not really needed) const func_decl_set& decls = source.get_output_predicates(); for (func_decl* p : decls) - if (!source.contains(p)) - result->set_output_predicate(p); + result->set_output_predicate(p); if (m_context.get_model_converter()) { generic_model_converter* fmc = alloc(generic_model_converter, m, "dl_mk_bit_blast"); @@ -314,7 +312,7 @@ namespace datalog { } m_context.add_model_converter(concat(bvmc, fmc)); } - + CTRACE("dl", result, result->display(tout);); return result; } }; diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index 457905a56..dc1f7ba1a 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -112,7 +112,7 @@ namespace datalog { } m_context.add_model_converter(mc0); } - CTRACE("dl", 0 != res, res->display(tout);); + CTRACE("dl", res, res->display(tout);); return res.detach(); }