1 files changed, 17 insertions, 3 deletions
diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index fd7cd467e..e23262746 100644
--- a/src/theory/uf/ho_extension.cpp
+++ b/src/theory/uf/ho_extension.cpp
@@ -200,7 +200,11 @@ Node HoExtension::getApplyUfForHoApply(Node node)
 
 unsigned HoExtension::checkExtensionality(TheoryModel* m)
 {
-  eq::EqualityEngine* ee = d_state.getEqualityEngine();
+  // if we are in collect model info, we require looking at the model's
+  // equality engine, so that we only consider "relevant" (see
+  // Theory::computeRelevantTerms) function terms.
+  eq::EqualityEngine* ee =
+      m != nullptr ? m->getEqualityEngine() : d_state.getEqualityEngine();
   NodeManager* nm = NodeManager::currentNM();
   unsigned num_lemmas = 0;
   bool isCollectModel = (m != nullptr);
@@ -247,8 +251,13 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m)
       for (unsigned k = (j + 1), sizek = itf->second.size(); k < sizek; k++)
       {
         // if these equivalence classes are not explicitly disequal, do
-        // extensionality to ensure distinctness
-        if (!ee->areDisequal(itf->second[j], itf->second[k], false))
+        // extensionality to ensure distinctness. Notice that we always use
+        // the (local) equality engine for this check via the state, since the
+        // model's equality engine does not store any disequalities. This is
+        // an optimization to introduce fewer equalities during model
+        // construction, since we know such disequalities have already been
+        // witness via assertions.
+        if (!d_state.areDisequal(itf->second[j], itf->second[k]))
         {
           Node deq =
               Rewriter::rewrite(itf->second[j].eqNode(itf->second[k]).negate());
@@ -450,6 +459,11 @@ bool HoExtension::collectModelInfoHo(TheoryModel* m,
       return false;
     }
   }
+  // We apply an explicit extensionality technique for asserting
+  // disequalities to the model to ensure that function values are distinct
+  // in the curried HO_APPLY version of model construction. This is a
+  // non-standard alternative to using a type enumerator over function
+  // values to assign unique values.
   int addedLemmas = checkExtensionality(m);
   return addedLemmas == 0;
 }