diff --git a/src/theory/incomplete_id.cpp b/src/theory/incomplete_id.cpp
index 9e945e6f342..e962df2a576 100644
--- a/src/theory/incomplete_id.cpp
+++ b/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:
diff --git a/src/theory/incomplete_id.h b/src/theory/incomplete_id.h
index fd3980e2b00..f24bf2fe8d9 100644
--- a/src/theory/incomplete_id.h
+++ b/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
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 8792ead674a..88bde9e2acd 100644
--- a/src/theory/theory_engine.cpp
+++ b/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());