Improve error for check theory assertions with model (#7679)

Makes it so that we report *all* unsatisfied assertions, not just the first one.

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 9b65a3e1c9bb3579cc98b453dc0b09394e588547..8622c86aae0f8bb8e69fd434d50aa1d73ca814cc 100644 (file)
--- 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<bool, Node> TheoryEngine::entailmentCheck(options::TheoryOfMode mode,