From: guykatzz <katz911@gmail.com>
Date: Wed, 31 May 2017 18:36:05 +0000 (-0700)
Subject: A more informative error message when a theory is not yet supported by the proof... 
X-Git-Tag: cvc5-1.0.0~5783
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d121faf54238a0859cdc2cf1d3d2889631cbfa3a;p=cvc5.git

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

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