1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 8337ba0b0..8730e3a97 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -407,14 +407,15 @@ void QuantifiersEngine::setOwner(Node q, quantifiers::QAttributes& qa)
     // set rewrite engine as owner
     setOwner(q, d_private->d_rr_engine.get(), 2);
   }
-  if (qa.d_sygus)
+  if (qa.d_sygus || (options::sygusRecFun() && !qa.d_fundef_f.isNull()))
   {
     if (d_private->d_synth_e.get() == nullptr)
     {
       Trace("quant-warn") << "WARNING : synth engine is null, and we have : "
                           << q << std::endl;
     }
-    // set synth engine as owner
+    // set synth engine as owner since this is either a conjecture or a function
+    // definition to be used by sygus
     setOwner(q, d_private->d_synth_e.get(), 2);
   }
 }