1 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 5aff1a848..df8533135 100755
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -48,7 +48,7 @@ void QuantDSplit::preRegisterQuantifier( Node q ) {
       }else{
         int score = -1;
         if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){
-          score = dt.isInterpretedFinite() ? 1 : -1;
+          score = dt.isInterpretedFinite() ? 1 : 0;
         }else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){
           score = dt.isInterpretedFinite() ? 1 : -1;
         }
@@ -73,6 +73,11 @@ bool QuantDSplit::needsCheck( Theory::Effort e ) {
   return e>=Theory::EFFORT_FULL && !d_quant_to_reduce.empty();
 }
 
+bool QuantDSplit::checkCompleteFor( Node q ) {
+  // true if we split q
+  return d_added_split.find( q )!=d_added_split.end();
+}
+
 /* Call during quantifier engine's check */
 void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) {
   //add lemmas ASAP (they are a reduction)