summaryrefslogtreecommitdiff
path: root/src/theory/sep
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/sep')
-rw-r--r--src/theory/sep/theory_sep.cpp16
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback