Fixes for quantifiers + incremental (#2009)

2 files changed, 5 insertions, 9 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;
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index 3e990067a..93b6436d5 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -146,8 +146,7 @@ public:
   void presolve() override;
   bool needsCheck(Theory::Effort e) override;
   void check(Theory::Effort e, QEffort quant_e) override;
-  void registerQuantifier(Node q) override;
-  void preRegisterQuantifier(Node q) override;
+  void checkOwnership(Node q) override;
   void assertNode(Node n) override;
   Node getNextDecisionRequest(unsigned& priority) override;
   bool isBoundVar( Node q, Node v ) { return std::find( d_set[q].begin(), d_set[q].end(), v )!=d_set[q].end(); }