1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 4619d74e5..0e7b02b53 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -142,7 +142,7 @@ Node CandidateGeneratorQELitEq::getNextCandidate(){
   while( !d_eq.isFinished() ){
     Node n = (*d_eq);
     ++d_eq;
-    if( n.getType().isSubtypeOf( d_match_pattern[0].getType() ) ){
+    if( n.getType().isComparableTo( d_match_pattern[0].getType() ) ){
       //an equivalence class with the same type as the pattern, return reflexive equality
       return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n );
     }
@@ -199,7 +199,7 @@ Node CandidateGeneratorQEAll::getNextCandidate() {
   while( !d_eq.isFinished() ){
     TNode n = (*d_eq);
     ++d_eq;
-    if( n.getType().isSubtypeOf( d_match_pattern_type ) ){
+    if( n.getType().isComparableTo( d_match_pattern_type ) ){
       TNode nh = d_qe->getTermDatabase()->getEligibleTermInEqc( n );
       if( !nh.isNull() ){
         if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){