From 2edfb432a4802281c0d45f741f8b844936ea6632 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 21 Nov 2021 18:49:57 -0600 Subject: [PATCH] Improve error for check theory assertions with model (#7679) Makes it so that we report *all* unsatisfied assertions, not just the first one. --- src/theory/theory_engine.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 9b65a3e1c..8622c86aa 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1790,6 +1790,8 @@ TrustNode TheoryEngine::getExplanation( bool TheoryEngine::isProofEnabled() const { return d_pnm != nullptr; } void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) { + bool hasFailure = false; + std::stringstream serror; for(TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { Theory* theory = d_theoryTable[theoryId]; if(theory && d_logicInfo.isTheoryEnabled(theoryId)) { @@ -1816,7 +1818,8 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) { if (val == d_false) { // Always an error if it is false - InternalError() << ss.str(); + hasFailure = true; + serror << ss.str(); } else { @@ -1831,6 +1834,10 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) { } } } + if (hasFailure) + { + InternalError() << serror.str(); + } } std::pair TheoryEngine::entailmentCheck(options::TheoryOfMode mode, -- 2.30.2