fix #3812

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Apr 7, 2020 · cb13641 · cb13641
1 parent b954e0d
commit cb13641
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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);