mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 03:12:03 +00:00
Code Activity

address #3905

Browse source
This commit is contained in:
Arie Gurfinkel 2020-04-11 00:03:13 -04:00
parent d53e30ecbe
commit 136b0b23ce
1 changed files with 4 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -276,9 +276,10 @@ namespace datalog {
rule_manager& rm = m_context.get_rule_manager(); rule_manager& rm = m_context.get_rule_manager();
unsigned sz = source.get_num_rules(); unsigned sz = source.get_num_rules();
expr_ref fml(m); expr_ref fml(m);
rule_set * result = alloc(rule_set, m_context); // scoped_ptr in case exception is thrown from somewhere
scoped_ptr<rule_set> result = alloc(rule_set, m_context);
m_rewriter.m_cfg.set_src(&source); m_rewriter.m_cfg.set_src(&source);
m_rewriter.m_cfg.set_dst(result); m_rewriter.m_cfg.set_dst(result.get());
for (unsigned i = 0; !m_context.canceled() && i < sz; ++i) { for (unsigned i = 0; !m_context.canceled() && i < sz; ++i) {
rule * r = source.get_rule(i); rule * r = source.get_rule(i);
rm.to_formula(*r, fml); rm.to_formula(*r, fml);
@ -319,7 +320,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);); CTRACE("dl", result, result->display(tout););
return result; return result.detach();
} }
}; };