3 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index eb6145f9c..6ba459452 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -1432,7 +1432,7 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
     if( lit.getKind()==CARDINALITY_CONSTRAINT || lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){
       // cardinality constraint from user input, set incomplete   
       Trace("uf-ss") << "Literal " << lit << " not handled when uf ss mode is not FULL, set incomplete." << std::endl;
-      d_im.setIncomplete();
+      d_im.setIncomplete(IncompleteId::UF_CARD_MODE);
     }
   }
   Trace("uf-ss") << "Assert: done " << n << " " << isDecision << std::endl;
diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index ee3753e92..78171349d 100644
--- a/src/theory/uf/ho_extension.cpp
+++ b/src/theory/uf/ho_extension.cpp
@@ -227,7 +227,7 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m)
     // are present
     if (hasFunctions)
     {
-      d_im.setIncomplete();
+      d_im.setIncomplete(IncompleteId::UF_HO_EXT_DISABLED);
     }
     return 0;
   }
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 9cb37a26d..e23bc0c45 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -177,7 +177,7 @@ bool TheoryUF::preNotifyFact(
       else
       {
         // support for cardinality constraints is not enabled, set incomplete
-        d_im.setIncomplete();
+        d_im.setIncomplete(IncompleteId::UF_CARD_DISABLED);
       }
     }
     // don't need to assert cardinality constraints if not producing models