Revert E-matching datatypes fix.

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index c1b3b307d708235a03079240918bbb616b8cb1d2..ea1231e7a67589ed59e10bd9619389a9aedbdc9d 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -81,7 +81,7 @@ Node TermDb::getOperator( Node n ) {
     }
     d_par_op_map[op][tn1][tn2] = n;
     return n;
-  }else if( n.hasOperator() ){
+  }else if( n.getKind()==APPLY_UF ){
     return n.getOperator();
   }else{
     return Node::null();