From 87a2a3410cc5de793a438d89bb50e197fca03ed7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 7 Apr 2020 11:34:51 -0700 Subject: [PATCH] fix #3801 Signed-off-by: Nikolaj Bjorner --- src/muz/bmc/dl_bmc_engine.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp index 0318d0bdc..d5f30c22e 100644 --- a/src/muz/bmc/dl_bmc_engine.cpp +++ b/src/muz/bmc/dl_bmc_engine.cpp @@ -502,13 +502,18 @@ namespace datalog { rule* r = nullptr; for (unsigned i = 0; i < rls.size(); ++i) { 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()); + 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)) { r = rls[i]; break; } } + if (!r) + throw default_exception("could not expand BMC rule"); SASSERT(r); b.m_rule_trace.push_back(r); rm.to_formula(*r, fml);