From d121faf54238a0859cdc2cf1d3d2889631cbfa3a Mon Sep 17 00:00:00 2001 From: guykatzz Date: Wed, 31 May 2017 11:36:05 -0700 Subject: [PATCH] A more informative error message when a theory is not yet supported by the proof infrastructure (e.g., quantifiers) --- src/proof/theory_proof.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) 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]; } -- 2.30.2