1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/transition_inference.cpp b/src/theory/quantifiers/sygus/transition_inference.cpp
index 7db3f50f8..97dd18492 100644
--- a/src/theory/quantifiers/sygus/transition_inference.cpp
+++ b/src/theory/quantifiers/sygus/transition_inference.cpp
@@ -197,6 +197,7 @@ void TransitionInference::process(Node n)
 {
   NodeManager* nm = NodeManager::currentNM();
   d_complete = true;
+  d_trivial = true;
   std::vector<Node> n_check;
   if (n.getKind() == AND)
   {
@@ -418,8 +419,9 @@ bool TransitionInference::processDisjunct(
   {
     Node op = lit.getOperator();
     // initialize the variables
-    if (d_vars.empty())
+    if (d_trivial)
     {
+      d_trivial = false;
       d_func = op;
       Trace("cegqi-inv-debug") << "Use " << op << " with args ";
       NodeManager* nm = NodeManager::currentNM();