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 #3801

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-07 11:34:51 -07:00
parent 889a7ad3f2
commit 87a2a3410c
1 changed files with 6 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/muz/bmc/dl_bmc_engine.cpp
View file

@ -502,13 +502,18 @@ namespace datalog {
rule* r = nullptr; rule* r = nullptr;
for (unsigned i = 0; i < rls.size(); ++i) { for (unsigned i = 0; i < rls.size(); ++i) {
func_decl_ref rule_i = mk_level_rule(pred, i, level); func_decl_ref rule_i = mk_level_rule(pred, i, level);
TRACE("bmc", rls[i]->display(b.m_ctx, tout << "Checking rule " << mk_pp(rule_i, m) << " "););
prop_r = m.mk_app(rule_i, prop->get_num_args(), prop->get_args()); prop_r = m.mk_app(rule_i, prop->get_num_args(), prop->get_args());
TRACE("bmc", rls[i]->display(b.m_ctx, tout << "Checking rule " << mk_pp(rule_i, m) << " ");
tout << (*md)(prop_r) << "\n";
tout << *md << "\n";
);
if (md->is_true(prop_r)) { if (md->is_true(prop_r)) {
r = rls[i]; r = rls[i];
break; break;
} }
} }
if (!r)
throw default_exception("could not expand BMC rule");
SASSERT(r); SASSERT(r);
b.m_rule_trace.push_back(r); b.m_rule_trace.push_back(r);
rm.to_formula(*r, fml); rm.to_formula(*r, fml);