mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

fix #3811

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-06 17:29:07 -07:00
parent 18b4c7e99b
commit 09c5de7798
2 changed files with 3 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -264,7 +264,6 @@ namespace datalog {
} }
rule_set * operator()(rule_set const & source) { rule_set * operator()(rule_set const & source) {
// TODO pc
if (!m_context.xform_bit_blast()) { if (!m_context.xform_bit_blast()) {
return nullptr; return nullptr;
} }
@ -300,7 +299,6 @@ 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))
result->set_output_predicate(p); result->set_output_predicate(p);
if (m_context.get_model_converter()) { if (m_context.get_model_converter()) {
@ -314,7 +312,7 @@ namespace datalog {
} }
m_context.add_model_converter(concat(bvmc, fmc)); m_context.add_model_converter(concat(bvmc, fmc));
} }
CTRACE("dl", result, result->display(tout););
return result; return result;
} }
}; };

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

@ -112,7 +112,7 @@ namespace datalog {
} }
m_context.add_model_converter(mc0); m_context.add_model_converter(mc0);
} }
CTRACE("dl", 0 != res, res->display(tout);); CTRACE("dl", res, res->display(tout););
return res.detach(); return res.detach();
} }