diff options
author | guykatzz <katz911@gmail.com> | 2017-05-31 11:36:05 -0700 |
---|---|---|
committer | guykatzz <katz911@gmail.com> | 2017-05-31 11:36:05 -0700 |
commit | d121faf54238a0859cdc2cf1d3d2889631cbfa3a (patch) | |
tree | c6313c3e5ace4aa9afec2423658511dc0f9fe41a /src/proof | |
parent | b9f47b4c948e2aab68303a14903e60bee0a449b8 (diff) |
A more informative error message when a theory is not yet supported by the proof infrastructure (e.g., quantifiers)
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/theory_proof.cpp | 7 |
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]; } |