Handle subtypes in sets. Bug fixes for tuples with subtypes.

1 files changed, 0 insertions, 14 deletions

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 4f58f7a2e..5ac5ae0cc 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1839,20 +1839,6 @@ Node TermDb::ensureType( Node n, TypeNode tn ) {
   }
 }
 
-bool TermDb::getEnsureTypeCondition( Node n, TypeNode tn, std::vector< Node >& cond ) {
-  TypeNode ntn = n.getType();
-  Assert( ntn.isComparableTo( tn ) );
-  if( !ntn.isSubtypeOf( tn ) ){
-    if( tn.isInteger() ){
-      cond.push_back( NodeManager::currentNM()->mkNode( IS_INTEGER, n ) );
-      return true;
-    }
-    return false;
-  }else{
-    return true;
-  }
-}
-
 void TermDb::getRelevancyCondition( Node n, std::vector< Node >& cond ) {
   if( n.getKind()==APPLY_SELECTOR_TOTAL ){
     unsigned scindex = Datatype::cindexOf(n.getOperator().toExpr());