1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
index 1e0b36a3c..83a576d37 100644
--- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
@@ -59,10 +59,10 @@ void CegInstantiation::check(Theory::Effort e, QEffort quant_e)
     d_waiting_conj = Node::null();
     if (!d_conj->isAssigned())
     {
-      if (!assignConjecture(q))
-      {
-        return;
-      }
+      assignConjecture(q);
+      // assign conjecture always uses the output channel, we return and
+      // re-check here.
+      return;
     }
   }
   unsigned echeck =