diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-13 13:36:28 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-13 13:36:28 -0500 |
commit | 5887766342258361d3635a5b29a015dadb9ebe83 (patch) | |
tree | 04a9ce1bceb5e5c4d0a715eda0ca9689ac424c58 /src/theory/sep | |
parent | ca1b17c8bba3681643a1a3de19d32b038c38aceb (diff) |
Minor changes to sep logic, epr, quantifier splitting.
Diffstat (limited to 'src/theory/sep')
-rw-r--r-- | src/theory/sep/theory_sep.cpp | 7 |
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 ); + } + } } } } |