From cb136418d513e22269ee2786dd7e1c3dfd336030 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 6 Apr 2020 19:57:07 -0700
Subject: [PATCH] fix #3812

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/proofs/proof_utils.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/ast/proofs/proof_utils.cpp b/src/ast/proofs/proof_utils.cpp
index bd6e6e0b1ec..ba00914ca0f 100644
--- a/src/ast/proofs/proof_utils.cpp
+++ b/src/ast/proofs/proof_utils.cpp
@@ -463,6 +463,8 @@ class reduce_hypotheses0 {
     reduce_hypotheses0(ast_manager& m): m(m), m_refs(m) {}
     
     void operator()(proof_ref& pr) {
+        if (!pr)
+            throw default_exception("proof reduction requires well defined proofs");
         proof_ref tmp(m);
         tmp = pr;
         elim(pr);