From 377dbad3b95a54ec30b36aa0e365153222f1d386 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 3 Jun 2020 10:27:08 -0700
Subject: [PATCH] fix #4435

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/asserted_formulas.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index cba9832d2..576a85a87 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -665,11 +665,12 @@ proof * asserted_formulas::get_inconsistency_proof() const {
         return nullptr;
     if (!m.proofs_enabled())
         return nullptr;
+    if (!m.inc())
+        return nullptr;
     for (justified_expr const& j : m_formulas) {
         if (m.is_false(j.get_fml()))
             return j.get_proof();
     }
-    UNREACHABLE();
     return nullptr;
 }