3 files changed, 23 insertions, 11 deletions
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 5428d9f1a..8d29cb8e1 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -328,7 +328,11 @@ Node FirstOrderModel::getModelBasisTerm(TypeNode tn)
       }
       else
       {
-        mbt = d_qe->getTermDatabase()->getOrMakeTypeGroundTerm(tn);
+        // The model basis term cannot be an interpreted function, or else we
+        // may produce an inconsistent model by choosing an arbitrary
+        // equivalence class for it. Hence, we require that it be an existing or
+        // fresh variable.
+        mbt = d_qe->getTermDatabase()->getOrMakeTypeGroundTerm(tn, true);
       }
     }
     ModelBasisAttribute mba;
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index c4b10eb6f..989609a76 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -113,19 +113,26 @@ Node TermDb::getTypeGroundTerm(TypeNode tn, unsigned i) const
   }
 }
 
-Node TermDb::getOrMakeTypeGroundTerm(TypeNode tn)
+Node TermDb::getOrMakeTypeGroundTerm(TypeNode tn, bool reqVar)
 {
   std::map<TypeNode, std::vector<Node> >::const_iterator it =
       d_type_map.find(tn);
   if (it != d_type_map.end())
   {
     Assert(!it->second.empty());
-    return it->second[0];
-  }
-  else
-  {
-    return getOrMakeTypeFreshVariable(tn);
+    if (!reqVar)
+    {
+      return it->second[0];
+    }
+    for (const Node& v : it->second)
+    {
+      if (v.isVar())
+      {
+        return v;
+      }
+    }
   }
+  return getOrMakeTypeFreshVariable(tn);
 }
 
 Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn)
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index cd5c27f0d..d58d33673 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -108,10 +108,11 @@ class TermDb : public QuantifiersUtil {
   */
   Node getTypeGroundTerm(TypeNode tn, unsigned i) const;
   /** get or make ground term
-  * Returns the first ground term of type tn,
-  * or makes one if none exist.
-  */
-  Node getOrMakeTypeGroundTerm(TypeNode tn);
+   *
+   * Returns the first ground term of type tn, or makes one if none exist. If
+   * reqVar is true, then the ground term must be a variable.
+   */
+  Node getOrMakeTypeGroundTerm(TypeNode tn, bool reqVar = false);
   /** make fresh variable
   * Returns a fresh variable of type tn.
   * This will return only a single fresh