From 6d6881c87a207b518d2847b05343be29250c6833 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 7 Apr 2020 11:40:12 -0700
Subject: [PATCH] fix #3824

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/bmc/dl_bmc_engine.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp
index d5f30c22e..12ff2157c 100644
--- a/src/muz/bmc/dl_bmc_engine.cpp
+++ b/src/muz/bmc/dl_bmc_engine.cpp
@@ -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();