From e93d0be650b9f349fe8be3a56ce2fc7cb20fddf0 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 9 Apr 2014 16:12:19 -0500
Subject: [PATCH] Revert E-matching datatypes fix.

---
 src/theory/quantifiers/term_database.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index c1b3b307d..ea1231e7a 100644
--- 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();
-- 
2.30.2