A more informative error message when a theory is not yet supported by the proof infrastructure (e.g., quantifiers)

1 files changed, 6 insertions, 1 deletions

diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index c684aa6bc..1d694c947 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -118,7 +118,12 @@ TheoryProof* TheoryProofEngine::getTheoryProof(theory::TheoryId id) {
     id = theory::THEORY_UF;
   }
 
-  Assert (d_theoryProofTable.find(id) != d_theoryProofTable.end());
+  if (d_theoryProofTable.find(id) == d_theoryProofTable.end()) {
+    std::stringstream ss;
+    ss << "Error! Proofs not yet supported for the following theory: " << id << std::endl;
+    InternalError(ss.str().c_str());
+  }
+
   return d_theoryProofTable[id];
 }