From 7fc9eb11db303c98dcf2616de23ab7a0ad79ea71 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 7 Apr 2020 19:22:50 -0700 Subject: [PATCH] fix #3850 Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_bit_blast.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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()) {