1 files changed, 20 insertions, 19 deletions
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index cbe907d41..4a708e66c 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -276,28 +276,29 @@ void SynthEngine::registerQuantifier(Node q)
 {
   Trace("cegqi-debug") << "SynthEngine: Register quantifier : " << q
                        << std::endl;
-  if (d_quantEngine->getOwner(q) == this)
+  if (d_quantEngine->getOwner(q) != this)
   {
-    Trace("cegqi") << "Register conjecture : " << q << std::endl;
-    if (options::sygusQePreproc())
-    {
-      d_waiting_conj.push_back(q);
-    }
-    else
-    {
-      // assign it now
-      assignConjecture(q);
-    }
+    return;
   }
-  if (options::sygusRecFun())
+  if (d_quantEngine->getQuantAttributes()->isFunDef(q))
   {
-    if (d_quantEngine->getQuantAttributes()->isFunDef(q))
-    {
-      // If it is a recursive function definition, add it to the function
-      // definition evaluator class.
-      FunDefEvaluator* fde = d_tds->getFunDefEvaluator();
-      fde->assertDefinition(q);
-    }
+    Assert(options::sygusRecFun());
+    // If it is a recursive function definition, add it to the function
+    // definition evaluator class.
+    Trace("cegqi") << "Registering function definition : " << q << "\n";
+    FunDefEvaluator* fde = d_tds->getFunDefEvaluator();
+    fde->assertDefinition(q);
+    return;
+  }
+  Trace("cegqi") << "Register conjecture : " << q << std::endl;
+  if (options::sygusQePreproc())
+  {
+    d_waiting_conj.push_back(q);
+  }
+  else
+  {
+    // assign it now
+    assignConjecture(q);
   }
 }