Add unprocessed theory conflict check (cvc5#10248)

This adds an extra safeguard to when we answer "sat" to check if any theory believes there is a conflict. In this case, we should answer "unknown" (in production) and give an assertion failure in debug.

This would have caught previous issues with HO+quantifiers.

src/theory/incomplete_id.cpp

@@ -53,6 +53,8 @@ const char* toString(IncompleteId i)
     case IncompleteId::UF_HO_EXT_DISABLED: return "UF_HO_EXT_DISABLED";
     case IncompleteId::UF_CARD_DISABLED: return "UF_CARD_DISABLED";
     case IncompleteId::UF_CARD_MODE: return "UF_CARD_MODE";
+    case IncompleteId::UNPROCESSED_THEORY_CONFLICT:
+      return "UNPROCESSED_THEORY_CONFLICT";
     case IncompleteId::STOP_SEARCH: return "STOP_SEARCH";
     case IncompleteId::UNKNOWN: return "UNKNOWN";
     default:

src/theory/incomplete_id.h

@@ -80,7 +80,9 @@ enum class IncompleteId
   // UF+cardinality solver used in an incomplete mode
   UF_CARD_MODE,
 
-  //------------------- other causes external to theory engine
+  //------------------- other causes external to theories
+  // unprocessed theory conflict
+  UNPROCESSED_THEORY_CONFLICT,
   // the prop layer stopped search
   STOP_SEARCH,
   //------------------- unknown

src/theory/theory_engine.cpp

@@ -554,6 +554,23 @@ void TheoryEngine::check(Theory::Effort effort) {
     {
       if (!d_inConflict && !needCheck())
       {
+        // if some theory believes there is a conflict, but it is was not
+        // processed, we mark incomplete.
+        for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST;
+             ++theoryId)
+        {
+          Theory* theory = d_theoryTable[theoryId];
+          if (theory && theory->getTheoryState() != nullptr)
+          {
+            if (theory->getTheoryState()->isInConflict())
+            {
+              setModelUnsound(theoryId,
+                              IncompleteId::UNPROCESSED_THEORY_CONFLICT);
+              Assert(false) << "Unprocessed theory conflict from " << theoryId;
+              break;
+            }
+          }
+        }
         // Do post-processing of model from the theories (e.g. used for
         // THEORY_SEP to construct heap model)
         d_tc->postProcessModel(d_modelUnsound.get());