3 files changed, 30 insertions, 5 deletions
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 018a0c3e0..aa2a43fbf 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -669,6 +669,8 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
   for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) {
     Node v = d_models[op]->d_value[i];
     Trace("fmc-model-func") << "Value is : " << v << std::endl;
+    Assert( v.isConst() );
+    /*
     if( !hasTerm( v ) ){
       //can happen when the model basis term does not exist in ground assignment
       TypeNode tn = v.getType();
@@ -685,6 +687,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
       }
     }
     v = getRepresentative( v );
+    */
     if( curr.isNull() ){
       Trace("fmc-model-func") << "base : " << v << std::endl;
       curr = v;
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 56f966426..6dfd4c737 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1605,10 +1605,10 @@ bool TermDb::containsTerm2( Node n, Node t, std::map< Node, bool >& visited ) {
 }
 
 bool TermDb::containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited ) {
-  if( std::find( t.begin(), t.end(), n )!=t.end() ){
-    return true;
-  }else{
-    if( visited.find( n )==visited.end() ){
+  if( visited.find( n )==visited.end() ){
+    if( std::find( t.begin(), t.end(), n )!=t.end() ){
+      return true;
+    }else{
       visited[n] = true;
       for( unsigned i=0; i<n.getNumChildren(); i++ ){
         if( containsTerms2( n[i], t, visited ) ){
@@ -1616,8 +1616,22 @@ bool TermDb::containsTerms2( Node n, std::vector< Node >& t, std::map< Node, boo
         }
       }
     }
-    return false;
   }
+  return false;
+}
+
+bool TermDb::containsUninterpretedConstant2( Node n, std::map< Node, bool >& visited ) {
+  if( n.getKind()==UNINTERPRETED_CONSTANT ){
+    return true;
+  }else if( visited.find( n )==visited.end() ){
+    visited[n] = true;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      if( containsUninterpretedConstant2( n[i], visited ) ){
+        return true;
+      }
+    }
+  }
+  return false;
 }
 
 bool TermDb::containsTerm( Node n, Node t ) {
@@ -1634,6 +1648,11 @@ bool TermDb::containsTerms( Node n, std::vector< Node >& t ) {
   }
 }
 
+bool TermDb::containsUninterpretedConstant( Node n ) {
+  std::map< Node, bool > visited;
+  return containsUninterpretedConstant2( n, visited );
+}
+
 Node TermDb::simpleNegate( Node n ){
   if( n.getKind()==OR || n.getKind()==AND ){
     std::vector< Node > children;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 86b0efbf3..0c4e94517 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -397,12 +397,15 @@ private:
   //helper for contains term
   static bool containsTerm2( Node n, Node t, std::map< Node, bool >& visited );
   static bool containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited );
+  static bool containsUninterpretedConstant2( Node n, std::map< Node, bool >& visited );
 //general utilities
 public:
   /** simple check for whether n contains t as subterm */
   static bool containsTerm( Node n, Node t );
   /** simple check for contains term, true if contains at least one term in t */
   static bool containsTerms( Node n, std::vector< Node >& t );
+  /** contains uninterpreted constant */
+  static bool containsUninterpretedConstant( Node n );
   /** simple negate */
   static Node simpleNegate( Node n );
   /** is assoc */