diff options
Diffstat (limited to 'src/theory/sep')
-rw-r--r-- | src/theory/sep/theory_sep.cpp | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index dc8ec9203..c9b6a9d89 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -1001,6 +1001,22 @@ void TheorySep::ppNotifyAssertions(const std::vector<Node>& assertions) { d_loc_to_data_type[d_type_ref] = d_type_data; } } + // initialize the EPR utility + QuantifiersEngine* qe = getQuantifiersEngine(); + if (qe != nullptr) + { + quantifiers::QuantEPR* qepr = qe->getQuantEPR(); + if (qepr != nullptr) + { + for (const Node& a : assertions) + { + qepr->registerAssertion(a); + } + // must handle sources of other new constants e.g. separation logic + initializeBounds(); + qepr->finishInit(); + } + } } //return cardinality |