Always split on constructor types for datatypes involving uninterpreted sorts when finite model finding is enabled, add regressions.

2 files changed, 2 insertions, 1 deletions

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 095e7868e..027a4573b 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -688,6 +688,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
     }else{
       //make the condition
       Node cond = d_models[op]->d_cond[i];
+      Trace("fmc-model-func") << "...cond : " << cond << std::endl;
       std::vector< Node > children;
       for( unsigned j=0; j<cond.getNumChildren(); j++) {
         TypeNode tn = vars[j].getType();
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 5ccb794f7..36b24c51b 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1029,7 +1029,7 @@ Node TermDb::getEnumerateTerm( TypeNode tn, unsigned index ) {
 bool TermDb::isClosedEnumerableType( TypeNode tn ) {
   std::map< TypeNode, bool >::iterator it = d_typ_closed_enum.find( tn );
   if( it==d_typ_closed_enum.end() ){
-    d_typ_closed_enum[tn] = false;
+    d_typ_closed_enum[tn] = true;
     bool ret = true;
     if( tn.isArray() || tn.isSort() || tn.isCodatatype() ){
       ret = false;