diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp index 9182fbc55..ef5ce8be4 100644 --- a/src/muz/transforms/dl_mk_bit_blast.cpp +++ b/src/muz/transforms/dl_mk_bit_blast.cpp @@ -300,7 +300,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)) + if (!source.contains(p) || result->contains(p)) result->set_output_predicate(p); if (m_context.get_model_converter()) {