mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

fix #3824

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

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

@ -518,6 +518,10 @@ namespace datalog {
b.m_rule_trace.push_back(r);
rm.to_formula(*r, fml);
IF_VERBOSE(1, verbose_stream() << mk_pp(fml, m) << "\n";);
if (!r->get_proof()) {
IF_VERBOSE(0, r->display(b.m_ctx, verbose_stream() << "no proof associated with rule"));
throw default_exception("no proof associated with rule");
}
prs.push_back(r->get_proof());
unsigned sz = r->get_uninterpreted_tail_size();