Merge branch 'master' into fix2002fix2002

1 files changed, 4 insertions, 7 deletions

diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index d96fb4e05..b493d6a0c 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -384,10 +384,11 @@ void BoundedIntegers::setBoundedVar( Node q, Node v, unsigned bound_type ) {
   Trace("bound-int-var") << "Bound variable #" << d_set_nums[q][v] << " : " << v << std::endl; 
 }
 
-void BoundedIntegers::preRegisterQuantifier( Node f ) {
+void BoundedIntegers::checkOwnership(Node f)
+{
   //this needs to be done at preregister since it affects e.g. QuantDSplit's preregister
-  Trace("bound-int") << "preRegister quantifier " << f << std::endl;
-  
+  Trace("bound-int") << "check ownership quantifier " << f << std::endl;
+
   bool success;
   do{
     std::map< Node, unsigned > bound_lit_type_map;
@@ -546,10 +547,6 @@ void BoundedIntegers::preRegisterQuantifier( Node f ) {
   }
 }
 
-void BoundedIntegers::registerQuantifier( Node q ) {
-
-}
-
 void BoundedIntegers::assertNode( Node n ) {
   Trace("bound-int-assert") << "Assert " << n << std::endl;
   Node nlit = n.getKind()==NOT ? n[0] : n;