From 176c0a97f762aefcd9bfefe704ec7c21677e0257 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Tue, 26 Jun 2018 21:18:10 -0400
Subject: [PATCH] Gracefully handle absence of a proof

---
 src/solver/solver_pool.cpp | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp
index 9dacfb5ce..598bb6c02 100644
--- a/src/solver/solver_pool.cpp
+++ b/src/solver/solver_pool.cpp
@@ -101,9 +101,11 @@ public:
     proof * get_proof() override {
         scoped_watch _t_(m_pool.m_proof_watch);
         if (!m_proof.get()) {
-            elim_aux_assertions pc(m_pred);
             m_proof = m_base->get_proof();
-            pc(m, m_proof, m_proof);
+            if (m_proof) {
+                elim_aux_assertions pc(m_pred);
+                pc(m, m_proof, m_proof);
+            }
         }
         return m_proof;
     }