Fix infinite loop in datatype enumerator. Minor fixes and improvements to cbqi, full saturate. Add option --purify-quant. Use disequality triggers when using relational triggers. Add regressions.

1 files changed, 0 insertions, 13 deletions

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index e513666a4..e41af5e2d 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -699,19 +699,6 @@ bool TermDb::hasInstConstAttr( Node n ) {
   return !getInstConstAttr(n).isNull();
 }
 
-void TermDb::getBoundVars( Node n, std::vector< Node >& bvs) {
-  if (n.getKind()==BOUND_VARIABLE ){
-    if ( std::find( bvs.begin(), bvs.end(), n)==bvs.end() ){
-      bvs.push_back( n );
-    }
-  }else{
-    for( unsigned i=0; i<n.getNumChildren(); i++) {
-      getBoundVars(n[i], bvs);
-    }
-  }
-}
-
-
 /** get the i^th instantiation constant of q */
 Node TermDb::getInstantiationConstant( Node q, int i ) const {
   std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q );