1 files changed, 8 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 55bf68b9f..3eedfdf53 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1135,6 +1135,14 @@ Result SmtEngine::checkSynth()
    --------------------------------------------------------------------------
 */
 
+void SmtEngine::declarePool(const Node& p, const std::vector<Node>& initValue)
+{
+  Assert(p.isVar() && p.getType().isSet());
+  finishInit();
+  QuantifiersEngine* qe = getAvailableQuantifiersEngine("declareTermPool");
+  qe->declarePool(p, initValue);
+}
+
 Node SmtEngine::simplify(const Node& ex)
 {
   SmtScope smts(this);