3 files changed, 17 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index 573e11426..a8c4cb0d1 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -111,6 +111,13 @@ bool CegisCoreConnective::processInitialize(Node conj,
     Trace("sygus-ccore-init") << "...could not infer predicate." << std::endl;
     return false;
   }
+  if (ti.isTrivial())
+  {
+    // not necessary to use this class if the conjecture is trivial (does
+    // not contain the function-to-synthesize).
+    Trace("sygus-ccore-init") << "...conjecture is trivial." << std::endl;
+    return false;
+  }
   Node trans = ti.getTransitionRelation();
   Trace("sygus-ccore-init") << "  transition relation: " << trans << std::endl;
   if (!trans.isConst() || trans.getConst<bool>())
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();
diff --git a/src/theory/quantifiers/sygus/transition_inference.h b/src/theory/quantifiers/sygus/transition_inference.h
index 8939cf6da..a6276e70d 100644
--- a/src/theory/quantifiers/sygus/transition_inference.h
+++ b/src/theory/quantifiers/sygus/transition_inference.h
@@ -158,6 +158,11 @@ class TransitionInference
    * was called on formula that does not have the shape of a transition system.
    */
   bool isComplete() const { return d_complete; }
+  /**
+   * Was the analysis of the conjecture trivial? This is true if the function
+   * did not occur in the conjecture.
+   */
+  bool isTrivial() const { return d_trivial; }
 
   /**
    * The following two functions are used for computing whether this transition
@@ -212,6 +217,8 @@ class TransitionInference
    * of this class complete?
    */
   bool d_complete;
+  /** Was the analyis trivial? */
+  bool d_trivial;
 
   /** process disjunct
    *