mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-14 09:56:15 +00:00
Code Activity

fix #3850

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-07 19:22:50 -07:00
parent 6e7e53e25c
commit 7fc9eb11db
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz/transforms/dl_mk_bit_blast.cpp
View file

@ -300,7 +300,7 @@ namespace datalog {
// copy output predicates without any rule (bit-blasting not really needed) // copy output predicates without any rule (bit-blasting not really needed)
const func_decl_set& decls = source.get_output_predicates(); const func_decl_set& decls = source.get_output_predicates();
for (func_decl* p : decls) for (func_decl* p : decls)
if (!source.contains(p)) if (!source.contains(p) || result->contains(p))
result->set_output_predicate(p); result->set_output_predicate(p);
if (m_context.get_model_converter()) { if (m_context.get_model_converter()) {