A more informative error message when a theory is not yet supported by the proof...

diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index c684aa6bcfd2db205533a857cd55875f44059127..1d694c947225e82d8d79a384cb4eca4a4e03e903 100644 (file)
--- 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];
 }