From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 22 Nov 2021 00:49:57 +0000 (-0600)
Subject: Improve error for check theory assertions with model (#7679)
X-Git-Tag: cvc5-1.0.0~790
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2edfb432a4802281c0d45f741f8b844936ea6632;p=cvc5.git

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 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<bool, Node> TheoryEngine::entailmentCheck(options::TheoryOfMode mode,