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;
 }