Minor changes to sep logic, epr, quantifier splitting.

1 files changed, 7 insertions, 0 deletions

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 714688142..e96badfd3 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -1028,6 +1028,13 @@ void TheorySep::initializeBounds() {
           qepr->d_consts[tn].push_back( e );
         }
       }
+      //EPR must include nil ref    
+      if( qepr && qepr->isEPR( tn ) ){
+        Node nr = getNilRef( tn );
+        if( !qepr->isEPRConstant( tn, nr ) ){
+          qepr->d_consts[tn].push_back( nr );
+        }
+      }      
     }
   }
 }