From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 9 Apr 2014 21:12:19 +0000 (-0500)
Subject: Revert E-matching datatypes fix.
X-Git-Tag: cvc5-1.0.0~6979
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e93d0be650b9f349fe8be3a56ce2fc7cb20fddf0;p=cvc5.git

Revert E-matching datatypes fix.
---

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();