1 files changed, 12 insertions, 5 deletions
diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp
index 1377ad23d..d23ff060a 100644
--- a/src/theory/quantifiers/term_registry.cpp
+++ b/src/theory/quantifiers/term_registry.cpp
@@ -22,19 +22,26 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-TermRegistry::TermRegistry(QuantifiersState& qs,
-                           QuantifiersInferenceManager& qim,
-                           QuantifiersRegistry& qr)
+TermRegistry::TermRegistry(QuantifiersState& qs, QuantifiersRegistry& qr)
     : d_presolve(qs.getUserContext(), true),
       d_presolveCache(qs.getUserContext()),
       d_termEnum(new TermEnumeration),
-      d_termDb(new TermDb(qs, qim, qr)),
+      d_termDb(new TermDb(qs, qr)),
       d_sygusTdb(nullptr)
 {
   if (options::sygus() || options::sygusInst())
   {
     // must be constructed here since it is required for datatypes finistInit
-    d_sygusTdb.reset(new TermDbSygus(qs, qim));
+    d_sygusTdb.reset(new TermDbSygus(qs));
+  }
+}
+
+void TermRegistry::finishInit(QuantifiersInferenceManager* qim)
+{
+  d_termDb->finishInit(qim);
+  if (d_sygusTdb.get())
+  {
+    d_sygusTdb->finishInit(qim);
   }
 }