Make option names related to CEGQI consistent (#4316)

This updates option names to be consistent across uses of counterexample-guided quantifier instantiation (ceqgi), which was previously called "counterexample-based quantifier instantiation" (cbqi), and sygus.

Notably, the trace "cegqi-engine" is changed to "sygus-engine" by this commit.

The changes were done by these commands in the given directories:

src/:
for f in $(find -name '.'); do sed -i 's/options::cbqi/options::cegqi/g' $f;sed -i 's/cegqi-engine/sygus-engine/g' $f; done;sed -i 's/"cbqi/"cegqi/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/--cbqi/--cegqi/g' $f; done
src/: and test/regress/:
for f in $(find -name '.'); do sed -i 's/cegqi-si/sygus-si/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/no-cbqi/no-cegqi/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/:cbqi/:cegqi/g' $f; done

And a few minor fixes afterwards.

This should be merged close to the time of the next stable release.

19 files changed, 264 insertions, 264 deletions

diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index dbc1e24af..f22e0e6d5 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -1623,26 +1623,26 @@ void SygusExtension::check( std::vector< Node >& lemmas ) {
     return check(lemmas);
   }
 
-  if (Trace.isOn("cegqi-engine") && !d_szinfo.empty())
+  if (Trace.isOn("sygus-engine") && !d_szinfo.empty())
   {
     if (lemmas.empty())
     {
-      Trace("cegqi-engine") << "*** Sygus : passed datatypes check. term size(s) : ";
+      Trace("sygus-engine") << "*** Sygus : passed datatypes check. term size(s) : ";
       for (std::pair<const Node, std::unique_ptr<SygusSizeDecisionStrategy>>&
                p : d_szinfo)
       {
         SygusSizeDecisionStrategy* s = p.second.get();
-        Trace("cegqi-engine") << s->d_curr_search_size << " ";
+        Trace("sygus-engine") << s->d_curr_search_size << " ";
       }
-      Trace("cegqi-engine") << std::endl;
+      Trace("sygus-engine") << std::endl;
     }
     else
     {
-      Trace("cegqi-engine")
+      Trace("sygus-engine")
           << "*** Sygus : produced symmetry breaking lemmas" << std::endl;
       for (const Node& lem : lemmas)
       {
-        Trace("cegqi-engine-debug") << "  " << lem << std::endl;
+        Trace("sygus-engine-debug") << "  " << lem << std::endl;
       }
     }
   }
@@ -1783,7 +1783,7 @@ Node SygusExtension::SygusSizeDecisionStrategy::mkLiteral(unsigned s)
   }
   Assert(!d_this.isNull());
   NodeManager* nm = NodeManager::currentNM();
-  Trace("cegqi-engine") << "******* Sygus : allocate size literal " << s
+  Trace("sygus-engine") << "******* Sygus : allocate size literal " << s
                         << " for " << d_this << std::endl;
   return nm->mkNode(DT_SYGUS_BOUND, d_this, nm->mkConst(Rational(s)));
 }
diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index c349e05b0..3756c6b4b 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -336,7 +336,7 @@ Node BvInverter::solveBvLit(Node sv,
     }
     else if (k == BITVECTOR_CONCAT)
     {
-      if (litk == EQUAL && options::cbqiBvConcInv())
+      if (litk == EQUAL && options::cegqiBvConcInv())
       {
         /* Compute inverse for s1 o x, x o s2, s1 o x o s2
          * (while disregarding that invertibility depends on si)
diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
index 2984c23be..bb59aa766 100644
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
@@ -167,7 +167,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
   }
   // compute how many bounds we will consider
   unsigned rmax = 1;
-  if (atom.getKind() == EQUAL && (pol || !options::cbqiModel()))
+  if (atom.getKind() == EQUAL && (pol || !options::cegqiModel()))
   {
     rmax = 2;
   }
@@ -206,7 +206,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
     {
       // disequalities are either strict upper or lower bounds
       bool is_upper;
-      if (options::cbqiModel())
+      if (options::cegqiModel())
       {
         // disequality is a disjunction : only consider the bound in the
         // direction of the model
@@ -273,7 +273,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
     // take into account delta
     if (uires == CEG_TT_UPPER_STRICT || uires == CEG_TT_LOWER_STRICT)
     {
-      if (options::cbqiModel())
+      if (options::cegqiModel())
       {
         Node delta_coeff =
             nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1));
@@ -295,7 +295,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
         uval = Rewriter::rewrite(uval);
       }
     }
-    if (options::cbqiModel())
+    if (options::cegqiModel())
     {
       // just store bounds, will choose based on tighest bound
       unsigned index = isUpperBoundCTT(uires) ? 0 : 1;
@@ -330,15 +330,15 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
                                           Node pv,
                                           CegInstEffort effort)
 {
-  if (!options::cbqiModel())
+  if (!options::cegqiModel())
   {
     return false;
   }
   NodeManager* nm = NodeManager::currentNM();
   bool use_inf =
-      d_type.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal();
+      d_type.isInteger() ? options::cegqiUseInfInt() : options::cegqiUseInfReal();
   bool upper_first = Random::getRandom().pickWithProb(0.5);
-  if (options::cbqiMinBounds())
+  if (options::cegqiMinBounds())
   {
     upper_first = d_mbp_bounds[1].size() < d_mbp_bounds[0].size();
   }
@@ -370,7 +370,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
         {
           return true;
         }
-        else if (!options::cbqiMultiInst())
+        else if (!options::cegqiMultiInst())
         {
           return false;
         }
@@ -509,7 +509,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
         best_used[rr] = best;
         // if using cbqiMidpoint, only add the instance based on one bound if
         // the bound is non-strict
-        if (!options::cbqiMidpoint() || d_type.isInteger()
+        if (!options::cegqiMidpoint() || d_type.isInteger()
             || d_mbp_vts_coeff[rr][1][best].isNull())
         {
           Node val = d_mbp_bounds[rr][best];
@@ -532,7 +532,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
             {
               return true;
             }
-            else if (!options::cbqiMultiInst())
+            else if (!options::cegqiMultiInst())
             {
               return false;
             }
@@ -563,13 +563,13 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
       {
         return true;
       }
-      else if (!options::cbqiMultiInst())
+      else if (!options::cegqiMultiInst())
       {
         return false;
       }
     }
   }
-  if (options::cbqiMidpoint() && !d_type.isInteger())
+  if (options::cegqiMidpoint() && !d_type.isInteger())
   {
     Node vals[2];
     bool bothBounds = true;
@@ -634,7 +634,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
       {
         return true;
       }
-      else if (!options::cbqiMultiInst())
+      else if (!options::cegqiMultiInst())
       {
         return false;
       }
@@ -643,7 +643,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
   // generally should not make it to this point, unless we are using a
   // non-monotonic selection function
 
-  if (!options::cbqiNopt())
+  if (!options::cegqiNopt())
   {
     // if not trying non-optimal bounds, return
     return false;
@@ -656,7 +656,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
     for (unsigned j = 0, nbounds = d_mbp_bounds[rr].size(); j < nbounds; j++)
     {
       if ((int)j != best_used[rr]
-          && (!options::cbqiMidpoint() || d_mbp_vts_coeff[rr][1][j].isNull()))
+          && (!options::cegqiMidpoint() || d_mbp_vts_coeff[rr][1][j].isNull()))
       {
         Node val = getModelBasedProjectionValue(ci,
                                                 pv,
@@ -677,7 +677,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
           {
             return true;
           }
-          else if (!options::cbqiMultiInst())
+          else if (!options::cegqiMultiInst())
           {
             return false;
           }
@@ -753,7 +753,7 @@ bool ArithInstantiator::postProcessInstantiationForVariable(
         << "...bound type is : " << sf.d_props[index].d_type << std::endl;
     // intger division rounding up if from a lower bound
     if (sf.d_props[index].d_type == CEG_TT_UPPER
-        && options::cbqiRoundUpLowerLia())
+        && options::cegqiRoundUpLowerLia())
     {
       sf.d_subs[index] = nm->mkNode(
           PLUS,
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
index 92f3e6d0d..2d43e63dc 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
@@ -91,7 +91,7 @@ void BvInstantiator::processLiteral(CegInstantiator* ci,
   Node pvs = ci->getModelValue(pv);
   Trace("cegqi-bv") << "Get path to " << pv << " : " << lit << std::endl;
   Node slit =
-      d_inverter->getPathToPv(lit, pv, sv, pvs, path, options::cbqiBvSolveNl());
+      d_inverter->getPathToPv(lit, pv, sv, pvs, path, options::cegqiBvSolveNl());
   if (!slit.isNull())
   {
     CegInstantiatorBvInverterQuery m(ci);
@@ -153,7 +153,7 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci,
   {
     return Node::null();
   }
-  else if (options::cbqiBvIneqMode() == options::CbqiBvIneqMode::KEEP
+  else if (options::cegqiBvIneqMode() == options::CbqiBvIneqMode::KEEP
            || (pol && k == EQUAL))
   {
     return lit;
@@ -172,7 +172,7 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci,
   Trace("cegqi-bv") << "   " << sm << " <> " << tm << std::endl;
 
   Node ret;
-  if (options::cbqiBvIneqMode() == options::CbqiBvIneqMode::EQ_SLACK)
+  if (options::cegqiBvIneqMode() == options::CbqiBvIneqMode::EQ_SLACK)
   {
     // if using slack, we convert constraints to a positive equality based on
     // the current model M, e.g.:
@@ -233,7 +233,7 @@ bool BvInstantiator::processAssertion(CegInstantiator* ci,
 {
   // if option enabled, use approach for word-level inversion for BV
   // instantiation
-  if (options::cbqiBv())
+  if (options::cegqiBv())
   {
     // get the best rewritten form of lit for solving for pv
     //   this should remove instances of non-invertible operators, and
@@ -261,7 +261,7 @@ bool BvInstantiator::useModelValue(CegInstantiator* ci,
                                    Node pv,
                                    CegInstEffort effort)
 {
-  return effort < CEG_INST_EFFORT_FULL || options::cbqiFullEffort();
+  return effort < CEG_INST_EFFORT_FULL || options::cegqiFullEffort();
 }
 
 bool BvInstantiator::processAssertions(CegInstantiator* ci,
@@ -279,7 +279,7 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci,
   Trace("cegqi-bv") << "BvInstantiator::processAssertions for " << pv
                     << std::endl;
   // if interleaving, do not do inversion half the time
-  if (options::cbqiBvInterleaveValue() && Random::getRandom().pickWithProb(0.5))
+  if (options::cegqiBvInterleaveValue() && Random::getRandom().pickWithProb(0.5))
   {
     Trace("cegqi-bv") << "...do not do instantiation for " << pv
                       << " (skip, based on heuristic)" << std::endl;
@@ -341,7 +341,7 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci,
   // for constructing instantiations is exponential on the number of
   // variables in this quantifier prefix.
   bool ret = false;
-  bool tryMultipleInst = firstVar && options::cbqiMultiInst();
+  bool tryMultipleInst = firstVar && options::cegqiMultiInst();
   bool revertOnSuccess = tryMultipleInst;
   for (unsigned j = 0, size = iti->second.size(); j < size; j++)
   {
@@ -557,7 +557,7 @@ Node BvInstantiator::rewriteTermForSolvePv(
           bv::utils::mkConst(BitVector(bv::utils::getSize(pv), Integer(2))));
     }
 
-    if (options::cbqiBvLinearize() && contains_pv[lhs] && contains_pv[rhs])
+    if (options::cegqiBvLinearize() && contains_pv[lhs] && contains_pv[rhs])
     {
       Node result = utils::normalizePvEqual(pv, children, contains_pv);
       if (!result.isNull())
@@ -575,7 +575,7 @@ Node BvInstantiator::rewriteTermForSolvePv(
   }
   else if (n.getKind() == BITVECTOR_MULT || n.getKind() == BITVECTOR_PLUS)
   {
-    if (options::cbqiBvLinearize() && contains_pv[n])
+    if (options::cegqiBvLinearize() && contains_pv[n])
     {
       Node result;
       if (n.getKind() == BITVECTOR_MULT)
@@ -640,7 +640,7 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma(
   // new lemmas
   std::vector<Node> new_lems;
 
-  if (options::cbqiBvRmExtract())
+  if (options::cegqiBvRmExtract())
   {
     NodeManager* nm = NodeManager::currentNM();
     Trace("cegqi-bv-pp") << "-----remove extracts..." << std::endl;
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index e62de0840..6b625fc73 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -294,7 +294,7 @@ CegHandledStatus CegInstantiator::isCbqiTerm(Node n)
           if (curr < ret)
           {
             ret = curr;
-            Trace("cbqi-debug2") << "Non-cbqi kind : " << cur.getKind()
+            Trace("cegqi-debug2") << "Non-cbqi kind : " << cur.getKind()
                                  << " in " << n << std::endl;
             if (curr == CEG_UNHANDLED)
             {
@@ -426,7 +426,7 @@ CegHandledStatus CegInstantiator::isCbqiQuant(Node q, QuantifiersEngine* qe)
   // if quantifier has a non-handled variable, then do not use cbqi
   // if quantifier has an APPLY_UF term, then do not use cbqi unless EPR
   CegHandledStatus ncbqiv = CegInstantiator::isCbqiQuantPrefix(q, qe);
-  Trace("cbqi-quant-debug") << "isCbqiQuantPrefix returned " << ncbqiv
+  Trace("cegqi-quant-debug") << "isCbqiQuantPrefix returned " << ncbqiv
                             << std::endl;
   if (ncbqiv == CEG_UNHANDLED)
   {
@@ -436,7 +436,7 @@ CegHandledStatus CegInstantiator::isCbqiQuant(Node q, QuantifiersEngine* qe)
   else
   {
     CegHandledStatus cbqit = CegInstantiator::isCbqiTerm(q);
-    Trace("cbqi-quant-debug") << "isCbqiTerm returned " << cbqit << std::endl;
+    Trace("cegqi-quant-debug") << "isCbqiTerm returned " << cbqit << std::endl;
     if (cbqit == CEG_UNHANDLED)
     {
       if (ncbqiv == CEG_HANDLED_UNCONDITIONAL)
@@ -457,7 +457,7 @@ CegHandledStatus CegInstantiator::isCbqiQuant(Node q, QuantifiersEngine* qe)
       ret = CEG_PARTIALLY_HANDLED;
     }
   }
-  if (ret == CEG_UNHANDLED && options::cbqiAll())
+  if (ret == CEG_UNHANDLED && options::cegqiAll())
   {
     // try but not exclusively
     ret = CEG_PARTIALLY_HANDLED;
@@ -549,7 +549,7 @@ void CegInstantiator::registerVariable(Node v)
   d_vars.push_back(v);
   d_vars_set.insert(v);
   TypeNode vtn = v.getType();
-  Trace("cbqi-proc-debug") << "Collect theory ids from type " << vtn << " of "
+  Trace("cegqi-proc-debug") << "Collect theory ids from type " << vtn << " of "
                            << v << std::endl;
   // collect relevant theories for this variable
   std::map<TypeNode, bool> visited;
@@ -623,11 +623,11 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
     }
     // If the above call fails, resort to using value in model. We do so if:
     // - we have yet to try an instantiation this round (or we are trying
-    //   multiple instantiations, indicated by options::cbqiMultiInst),
+    //   multiple instantiations, indicated by options::cegqiMultiInst),
     // - the instantiator uses model values at this effort or
     //   if we are solving for a subfield of a datatype (is_sv), and
     // - the instantiator allows model values.
-    if ((options::cbqiMultiInst() || !hasTriedInstantiation(pv))
+    if ((options::cegqiMultiInst() || !hasTriedInstantiation(pv))
         && (vinst->useModelValue(this, sf, pv, d_effort) || is_sv)
         && vinst->allowModelValue(this, sf, pv, d_effort))
     {
@@ -638,16 +638,16 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
       // Quantified Linear Arithmetic by Counterexample Guided Instantiation",
       // FMSD 2017. We throw an assertion failure if we detect a case where the
       // strategy was not monotonic.
-      if (options::cbqiNestedQE() && d_qe->getLogicInfo().isPure(THEORY_ARITH)
+      if (options::cegqiNestedQE() && d_qe->getLogicInfo().isPure(THEORY_ARITH)
           && d_qe->getLogicInfo().isLinear())
       {
-        Trace("cbqi-warn") << "Had to resort to model value." << std::endl;
+        Trace("cegqi-warn") << "Had to resort to model value." << std::endl;
         Assert(false);
       }
 #endif
       Node mv = getModelValue( pv );
       TermProperties pv_prop_m;
-      Trace("cbqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl;
+      Trace("cegqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl;
       d_curr_iphase[pv] = CEG_INST_PHASE_MVALUE;
       CegInstEffort prev = d_effort;
       if (d_effort < CEG_INST_EFFORT_STANDARD_MV)
@@ -662,7 +662,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
       d_effort = prev;
     }
 
-    Trace("cbqi-inst-debug") << "[No instantiation found for " << pv << "]" << std::endl;
+    Trace("cegqi-inst-debug") << "[No instantiation found for " << pv << "]" << std::endl;
     if (is_sv)
     {
       d_stack_vars.push_back( pv );
@@ -684,34 +684,34 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf,
   {
     pvr = d_qe->getMasterEqualityEngine()->getRepresentative(pv);
   }
-  Trace("cbqi-inst-debug") << "[Find instantiation for " << pv
+  Trace("cegqi-inst-debug") << "[Find instantiation for " << pv
                            << "], rep=" << pvr << ", instantiator is "
                            << vinst->identify() << std::endl;
   Node pv_value;
-  if (options::cbqiModel())
+  if (options::cegqiModel())
   {
     pv_value = getModelValue(pv);
-    Trace("cbqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl;
+    Trace("cegqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl;
   }
 
   //[1] easy case : pv is in the equivalence class as another term not
   // containing pv
   if (vinst->hasProcessEqualTerm(this, sf, pv, d_effort))
   {
-    Trace("cbqi-inst-debug")
+    Trace("cegqi-inst-debug")
         << "[1] try based on equivalence class." << std::endl;
     d_curr_iphase[pv] = CEG_INST_PHASE_EQC;
     std::map<Node, std::vector<Node> >::iterator it_eqc = d_curr_eqc.find(pvr);
     if (it_eqc != d_curr_eqc.end())
     {
       // std::vector< Node > eq_candidates;
-      Trace("cbqi-inst-debug2")
+      Trace("cegqi-inst-debug2")
           << "...eqc has size " << it_eqc->second.size() << std::endl;
       for (const Node& n : it_eqc->second)
       {
         if (n != pv)
         {
-          Trace("cbqi-inst-debug")
+          Trace("cegqi-inst-debug")
               << "...try based on equal term " << n << std::endl;
           // must be an eligible term
           if (isEligible(n))
@@ -741,7 +741,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf,
               {
                 return true;
               }
-              else if (!options::cbqiMultiInst() && hasTriedInstantiation(pv))
+              else if (!options::cegqiMultiInst() && hasTriedInstantiation(pv))
               {
                 return false;
               }
@@ -757,14 +757,14 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf,
       {
         return true;
       }
-      else if (!options::cbqiMultiInst() && hasTriedInstantiation(pv))
+      else if (!options::cegqiMultiInst() && hasTriedInstantiation(pv))
       {
         return false;
       }
     }
     else
     {
-      Trace("cbqi-inst-debug2") << "...eqc not found." << std::endl;
+      Trace("cegqi-inst-debug2") << "...eqc not found." << std::endl;
     }
   }
 
@@ -773,7 +773,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf,
   /// the variable
   if (vinst->hasProcessEquality(this, sf, pv, d_effort))
   {
-    Trace("cbqi-inst-debug")
+    Trace("cegqi-inst-debug")
         << "[2] try based on solving equalities." << std::endl;
     d_curr_iphase[pv] = CEG_INST_PHASE_EQUAL;
     std::vector<Node>& cteqc = d_curr_type_eqc[pvtnb];
@@ -787,7 +787,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf,
       Assert(it_reqc != d_curr_eqc.end());
       for (const Node& n : it_reqc->second)
       {
-        Trace("cbqi-inst-debug2") << "...look at term " << n << std::endl;
+        Trace("cegqi-inst-debug2") << "...look at term " << n << std::endl;
         // must be an eligible term
         if (isEligible(n))
         {
@@ -808,7 +808,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf,
           if (!ns.isNull())
           {
             bool hasVar = d_prog_var[ns].find(pv) != d_prog_var[ns].end();
-            Trace("cbqi-inst-debug2") << "... " << ns << " has var " << pv
+            Trace("cegqi-inst-debug2") << "... " << ns << " has var " << pv
                                       << " : " << hasVar << std::endl;
             std::vector<TermProperties> term_props;
             std::vector<Node> terms;
@@ -819,7 +819,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf,
               // if this term or the another has pv in it, try to solve for it
               if (hasVar || lhs_v[j])
               {
-                Trace("cbqi-inst-debug") << "......try based on equality "
+                Trace("cegqi-inst-debug") << "......try based on equality "
                                          << lhs[j] << " = " << ns << std::endl;
                 term_props.push_back(lhs_prop[j]);
                 terms.push_back(lhs[j]);
@@ -828,7 +828,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf,
                 {
                   return true;
                 }
-                else if (!options::cbqiMultiInst() && hasTriedInstantiation(pv))
+                else if (!options::cegqiMultiInst() && hasTriedInstantiation(pv))
                 {
                   return false;
                 }
@@ -842,14 +842,14 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf,
           }
           else
           {
-            Trace("cbqi-inst-debug2")
+            Trace("cegqi-inst-debug2")
                 << "... term " << n << " is ineligible after substitution."
                 << std::endl;
           }
         }
         else
         {
-          Trace("cbqi-inst-debug2")
+          Trace("cegqi-inst-debug2")
               << "... term " << n << " is ineligible." << std::endl;
         }
       }
@@ -860,13 +860,13 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf,
   {
     return false;
   }
-  Trace("cbqi-inst-debug") << "[3] try based on assertions." << std::endl;
+  Trace("cegqi-inst-debug") << "[3] try based on assertions." << std::endl;
   d_curr_iphase[pv] = CEG_INST_PHASE_ASSERTION;
   std::unordered_set<Node, NodeHashFunction> lits;
   for (unsigned r = 0; r < 2; r++)
   {
     TheoryId tid = r == 0 ? Theory::theoryOf(pvtn) : THEORY_UF;
-    Trace("cbqi-inst-debug2") << "  look at assertions of " << tid << std::endl;
+    Trace("cegqi-inst-debug2") << "  look at assertions of " << tid << std::endl;
     std::map<TheoryId, std::vector<Node> >::iterator ita =
         d_curr_asserts.find(tid);
     if (ita != d_curr_asserts.end())
@@ -877,18 +877,18 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf,
         {
           lits.insert(lit);
           Node plit;
-          if (options::cbqiRepeatLit() || !isSolvedAssertion(lit))
+          if (options::cegqiRepeatLit() || !isSolvedAssertion(lit))
           {
             plit = vinst->hasProcessAssertion(this, sf, pv, lit, d_effort);
           }
           if (!plit.isNull())
           {
-            Trace("cbqi-inst-debug2") << "  look at " << lit;
+            Trace("cegqi-inst-debug2") << "  look at " << lit;
             if (plit != lit)
             {
-              Trace("cbqi-inst-debug2") << "...processed to : " << plit;
+              Trace("cegqi-inst-debug2") << "...processed to : " << plit;
             }
-            Trace("cbqi-inst-debug2") << std::endl;
+            Trace("cegqi-inst-debug2") << std::endl;
             // apply substitutions
             Node slit = applySubstitutionToLiteral(plit, sf);
             if (!slit.isNull())
@@ -896,14 +896,14 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf,
               // check if contains pv
               if (hasVariable(slit, pv))
               {
-                Trace("cbqi-inst-debug")
+                Trace("cegqi-inst-debug")
                     << "...try based on literal " << slit << "," << std::endl;
-                Trace("cbqi-inst-debug") << "...from " << lit << std::endl;
+                Trace("cegqi-inst-debug") << "...from " << lit << std::endl;
                 if (vinst->processAssertion(this, sf, pv, slit, lit, d_effort))
                 {
                   return true;
                 }
-                else if (!options::cbqiMultiInst() && hasTriedInstantiation(pv))
+                else if (!options::cegqiMultiInst() && hasTriedInstantiation(pv))
                 {
                   return false;
                 }
@@ -939,14 +939,14 @@ bool CegInstantiator::constructInstantiationInc(Node pv,
   Node cnode = pv_prop.getCacheNode();
   if( d_curr_subs_proc[pv][n].find( cnode )==d_curr_subs_proc[pv][n].end() ){
     d_curr_subs_proc[pv][n][cnode] = true;
-    if( Trace.isOn("cbqi-inst-debug") ){
+    if( Trace.isOn("cegqi-inst-debug") ){
       for( unsigned j=0; j<sf.d_subs.size(); j++ ){
-        Trace("cbqi-inst-debug") << " ";
+        Trace("cegqi-inst-debug") << " ";
       }
-      Trace("cbqi-inst-debug") << sf.d_subs.size() << ": (" << d_curr_iphase[pv]
+      Trace("cegqi-inst-debug") << sf.d_subs.size() << ": (" << d_curr_iphase[pv]
                          << ") ";
       Node mod_pv = pv_prop.getModifiedTerm( pv );
-      Trace("cbqi-inst-debug") << mod_pv << " -> " << n << std::endl;
+      Trace("cegqi-inst-debug") << mod_pv << " -> " << n << std::endl;
       Assert(n.getType().isSubtypeOf(pv.getType()));
     }
     //must ensure variables have been computed for n
@@ -969,9 +969,9 @@ bool CegInstantiator::constructInstantiationInc(Node pv,
     std::map< int, TermProperties > prev_prop;
     std::map< int, Node > prev_sym_subs;
     std::vector< Node > new_non_basic;
-    Trace("cbqi-inst-debug2") << "Applying substitutions to previous substitution terms..." << std::endl;
+    Trace("cegqi-inst-debug2") << "Applying substitutions to previous substitution terms..." << std::endl;
     for( unsigned j=0; j<sf.d_subs.size(); j++ ){
-      Trace("cbqi-inst-debug2") << "  Apply for " << sf.d_subs[j]  << std::endl;
+      Trace("cegqi-inst-debug2") << "  Apply for " << sf.d_subs[j]  << std::endl;
       Assert(d_prog_var.find(sf.d_subs[j]) != d_prog_var.end());
       if( d_prog_var[sf.d_subs[j]].find( pv )!=d_prog_var[sf.d_subs[j]].end() ){
         prev_subs[j] = sf.d_subs[j];
@@ -1014,25 +1014,25 @@ bool CegInstantiator::constructInstantiationInc(Node pv,
             computeProgVars( sf.d_subs[j] );
             Assert(d_inelig.find(sf.d_subs[j]) == d_inelig.end());
           }
-          Trace("cbqi-inst-debug2") << "Subs " << j << " " << sf.d_subs[j] << std::endl;
+          Trace("cegqi-inst-debug2") << "Subs " << j << " " << sf.d_subs[j] << std::endl;
         }else{
-          Trace("cbqi-inst-debug2") << "...failed to apply substitution to " << sf.d_subs[j] << std::endl;
+          Trace("cegqi-inst-debug2") << "...failed to apply substitution to " << sf.d_subs[j] << std::endl;
           success = false;
           break;
         }
       }else{
-        Trace("cbqi-inst-debug2") << "Skip " << j << " " << sf.d_subs[j] << std::endl;
+        Trace("cegqi-inst-debug2") << "Skip " << j << " " << sf.d_subs[j] << std::endl;
       }
     }
     if( success ){
-      Trace("cbqi-inst-debug2") << "Adding to vectors..." << std::endl;
+      Trace("cegqi-inst-debug2") << "Adding to vectors..." << std::endl;
       sf.push_back( pv, n, pv_prop );
-      Trace("cbqi-inst-debug2") << "Recurse..." << std::endl;
+      Trace("cegqi-inst-debug2") << "Recurse..." << std::endl;
       unsigned i = d_curr_index[pv];
       success = constructInstantiation(sf, d_stack_vars.empty() ? i + 1 : i);
       if (!success || revertOnSuccess)
       {
-        Trace("cbqi-inst-debug2") << "Removing from vectors..." << std::endl;
+        Trace("cegqi-inst-debug2") << "Removing from vectors..." << std::endl;
         sf.pop_back( pv, n, pv_prop );
       }
     }
@@ -1040,7 +1040,7 @@ bool CegInstantiator::constructInstantiationInc(Node pv,
     {
       return true;
     }else{
-      Trace("cbqi-inst-debug2") << "Revert substitutions..." << std::endl;
+      Trace("cegqi-inst-debug2") << "Revert substitutions..." << std::endl;
       //revert substitution information
       for (std::map<int, Node>::iterator it = prev_subs.begin();
            it != prev_subs.end();
@@ -1068,7 +1068,7 @@ bool CegInstantiator::constructInstantiationInc(Node pv,
 bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& lemmas ) {
   if (vars.size() > d_input_vars.size() || !d_var_order_index.empty())
   {
-    Trace("cbqi-inst-debug") << "Reconstructing instantiations...." << std::endl;
+    Trace("cegqi-inst-debug") << "Reconstructing instantiations...." << std::endl;
     std::map< Node, Node > subs_map;
     for( unsigned i=0; i<subs.size(); i++ ){
       subs_map[vars[i]] = subs[i];
@@ -1079,24 +1079,24 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector
       std::map<Node, Node>::iterator it = subs_map.find(d_input_vars[i]);
       Assert(it != subs_map.end());
       Node n = it->second;
-      Trace("cbqi-inst-debug") << "  " << d_input_vars[i] << " -> " << n
+      Trace("cegqi-inst-debug") << "  " << d_input_vars[i] << " -> " << n
                                << std::endl;
       Assert(n.getType().isSubtypeOf(d_input_vars[i].getType()));
       subs.push_back( n );
     }
   }
-  if (Trace.isOn("cbqi-inst"))
+  if (Trace.isOn("cegqi-inst"))
   {
-    Trace("cbqi-inst") << "Ceg Instantiator produced : " << std::endl;
+    Trace("cegqi-inst") << "Ceg Instantiator produced : " << std::endl;
     for (unsigned i = 0, size = d_input_vars.size(); i < size; ++i)
     {
       Node v = d_input_vars[i];
-      Trace("cbqi-inst") << i << " (" << d_curr_iphase[v] << ") : " 
+      Trace("cegqi-inst") << i << " (" << d_curr_iphase[v] << ") : " 
                          << v << " -> " << subs[i] << std::endl;
       Assert(subs[i].getType().isSubtypeOf(v.getType()));
     }
   }
-  Trace("cbqi-inst-debug") << "Do the instantiation...." << std::endl;
+  Trace("cegqi-inst-debug") << "Do the instantiation...." << std::endl;
   bool ret = d_parent->doAddInstantiation(subs);
   for( unsigned i=0; i<lemmas.size(); i++ ){
     d_parent->addLemma(lemmas[i]);
@@ -1154,10 +1154,10 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
   n = Rewriter::rewrite(n);
   computeProgVars( n );
   bool is_basic = canApplyBasicSubstitution( n, non_basic );
-  if( Trace.isOn("cegqi-si-apply-subs-debug") ){
-    Trace("cegqi-si-apply-subs-debug") << "is_basic = " << is_basic << "  " << tn << std::endl;
+  if( Trace.isOn("sygus-si-apply-subs-debug") ){
+    Trace("sygus-si-apply-subs-debug") << "is_basic = " << is_basic << "  " << tn << std::endl;
     for( unsigned i=0; i<subs.size(); i++ ){
-      Trace("cegqi-si-apply-subs-debug") << "  " << vars[i] << " -> " << subs[i] << "   types : " << vars[i].getType() << " -> " << subs[i].getType() << std::endl;
+      Trace("sygus-si-apply-subs-debug") << "  " << vars[i] << " -> " << subs[i] << "   types : " << vars[i].getType() << " -> " << subs[i].getType() << std::endl;
       Assert(subs[i].getType().isSubtypeOf(vars[i].getType()));
     }
   }
@@ -1215,7 +1215,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
         //make sum with normalized coefficient
         if( !pv_prop.d_coeff.isNull() ){
           pv_prop.d_coeff = Rewriter::rewrite( pv_prop.d_coeff );
-          Trace("cegqi-si-apply-subs-debug") << "Combined coeff : " << pv_prop.d_coeff << std::endl;
+          Trace("sygus-si-apply-subs-debug") << "Combined coeff : " << pv_prop.d_coeff << std::endl;
           std::vector< Node > children;
           for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
             Node c_coeff;
@@ -1235,7 +1235,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
               c = NodeManager::currentNM()->mkNode( MULT, c_coeff, msum_term[it->first] );
             }
             children.push_back( c );
-            Trace("cegqi-si-apply-subs-debug") << "Add child : " << c << std::endl;
+            Trace("sygus-si-apply-subs-debug") << "Add child : " << c << std::endl;
           }
           Node nretc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children );
           nretc = Rewriter::rewrite( nretc );
@@ -1245,14 +1245,14 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
             //result is ( nret / pv_prop.d_coeff )
             nret = nretc;
           }else{
-            Trace("cegqi-si-apply-subs-debug") << "Failed, since result " << nretc << " contains free variable." << std::endl;
+            Trace("sygus-si-apply-subs-debug") << "Failed, since result " << nretc << " contains free variable." << std::endl;
           }
         }else{
           //implies that we have a monomial that has a free variable
-          Trace("cegqi-si-apply-subs-debug") << "Failed to find coefficient during substitution, implies monomial with free variable." << std::endl;
+          Trace("sygus-si-apply-subs-debug") << "Failed to find coefficient during substitution, implies monomial with free variable." << std::endl;
         }
       }else{
-        Trace("cegqi-si-apply-subs-debug") << "Failed to find monomial sum " << n << std::endl;
+        Trace("sygus-si-apply-subs-debug") << "Failed to find monomial sum " << n << std::endl;
       }
     }
   }
@@ -1324,7 +1324,7 @@ bool CegInstantiator::check() {
       return true;
     }
   }
-  Trace("cbqi-engine") << "  WARNING : unable to find CEGQI single invocation instantiation." << std::endl;
+  Trace("cegqi-engine") << "  WARNING : unable to find CEGQI single invocation instantiation." << std::endl;
   return false;
 }
 
@@ -1344,7 +1344,7 @@ void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq
                  == it->second.end())
       {
         it->second.push_back(nn);
-        Trace("cbqi-presolve") << "  - " << n[i] << " = " << nn << std::endl;
+        Trace("cegqi-presolve") << "  - " << n[i] << " = " << nn << std::endl;
       }
     }
   }
@@ -1393,7 +1393,7 @@ void CegInstantiator::presolve( Node q ) {
       Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj );
       Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() );
       lem = NodeManager::currentNM()->mkNode( OR, g, lem );
-      Trace("cbqi-presolve-debug") << "Presolve lemma : " << lem << std::endl;
+      Trace("cegqi-presolve-debug") << "Presolve lemma : " << lem << std::endl;
       Assert(!expr::hasFreeVar(lem));
       d_qe->getOutputChannel().lemma( lem, false, true );
     }
@@ -1401,7 +1401,7 @@ void CegInstantiator::presolve( Node q ) {
 }
 
 void CegInstantiator::processAssertions() {
-  Trace("cbqi-proc") << "--- Process assertions, #var = " << d_vars.size()
+  Trace("cegqi-proc") << "--- Process assertions, #var = " << d_vars.size()
                      << std::endl;
   d_curr_asserts.clear();
   d_curr_eqc.clear();
@@ -1414,12 +1414,12 @@ void CegInstantiator::processAssertions() {
   for( unsigned i=0; i<d_vars.size(); i++ ){
     Node pv = d_vars[i];
     TypeNode pvtn = pv.getType();
-    Trace("cbqi-proc-debug") << "Collect theory ids from type " << pvtn << " of " << pv << std::endl;
+    Trace("cegqi-proc-debug") << "Collect theory ids from type " << pvtn << " of " << pv << std::endl;
     //collect information about eqc
     if( ee->hasTerm( pv ) ){
       Node pvr = ee->getRepresentative( pv );
       if( d_curr_eqc.find( pvr )==d_curr_eqc.end() ){
-        Trace("cbqi-proc") << "Collect equivalence class " << pvr << std::endl;
+        Trace("cegqi-proc") << "Collect equivalence class " << pvr << std::endl;
         eq::EqClassIterator eqc_i = eq::EqClassIterator( pvr, ee );
         while( !eqc_i.isFinished() ){
           d_curr_eqc[pvr].push_back( *eqc_i );
@@ -1433,7 +1433,7 @@ void CegInstantiator::processAssertions() {
     TheoryId tid = d_tids[i];
     Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid );
     if( theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid) ){
-      Trace("cbqi-proc") << "Collect assertions from theory " << tid << std::endl;
+      Trace("cegqi-proc") << "Collect assertions from theory " << tid << std::endl;
       d_curr_asserts[tid].clear();
       //collect all assertions from theory
       for( context::CDList<Assertion>::const_iterator it = theory->facts_begin(); it != theory->facts_end(); ++ it) {
@@ -1441,15 +1441,15 @@ void CegInstantiator::processAssertions() {
         Node atom = lit.getKind()==NOT ? lit[0] : lit;
         if( d_is_nested_quant || std::find( d_ce_atoms.begin(), d_ce_atoms.end(), atom )!=d_ce_atoms.end() ){
           d_curr_asserts[tid].push_back( lit );
-          Trace("cbqi-proc-debug") << "...add : " << lit << std::endl;
+          Trace("cegqi-proc-debug") << "...add : " << lit << std::endl;
         }else{
-          Trace("cbqi-proc") << "...do not consider literal " << tid << " : " << lit << " since it is not part of CE body." << std::endl;
+          Trace("cegqi-proc") << "...do not consider literal " << tid << " : " << lit << " since it is not part of CE body." << std::endl;
         }
       }
     }
   }
   //collect equivalence classes that correspond to relevant theories
-  Trace("cbqi-proc-debug") << "...collect typed equivalence classes" << std::endl;
+  Trace("cegqi-proc-debug") << "...collect typed equivalence classes" << std::endl;
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
   while( !eqcs_i.isFinished() ){
     Node r = *eqcs_i;
@@ -1460,18 +1460,18 @@ void CegInstantiator::processAssertions() {
       if( rtn.isInteger() || rtn.isReal() ){
         rtn = rtn.getBaseType();
       }
-      Trace("cbqi-proc-debug") << "...type eqc: " << r << std::endl;
+      Trace("cegqi-proc-debug") << "...type eqc: " << r << std::endl;
       d_curr_type_eqc[rtn].push_back( r );
       if( d_curr_eqc.find( r )==d_curr_eqc.end() ){
-        Trace("cbqi-proc") << "Collect equivalence class " << r << std::endl;
-        Trace("cbqi-proc-debug") << "  ";
+        Trace("cegqi-proc") << "Collect equivalence class " << r << std::endl;
+        Trace("cegqi-proc-debug") << "  ";
         eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
         while( !eqc_i.isFinished() ){
-          Trace("cbqi-proc-debug") << *eqc_i << " ";
+          Trace("cegqi-proc-debug") << *eqc_i << " ";
           d_curr_eqc[r].push_back( *eqc_i );
           ++eqc_i;
         }
-        Trace("cbqi-proc-debug") << std::endl;
+        Trace("cegqi-proc-debug") << std::endl;
       }
     }
     ++eqcs_i;
@@ -1486,13 +1486,13 @@ void CegInstantiator::processAssertions() {
       if( isEligible( n ) ){
         //must contain at least one variable
         if( !d_prog_var[n].empty() ){
-          Trace("cbqi-proc") << "...literal[" << it->first << "] : " << n << std::endl;
+          Trace("cegqi-proc") << "...literal[" << it->first << "] : " << n << std::endl;
           akeep.push_back( n );
         }else{
-          Trace("cbqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains no relevant variables." << std::endl;
+          Trace("cegqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains no relevant variables." << std::endl;
         }
       }else{
-        Trace("cbqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains ineligible terms." << std::endl;
+        Trace("cegqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains ineligible terms." << std::endl;
       }
     }
     it->second.clear();
@@ -1564,7 +1564,7 @@ void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited )
       }
     }else{
       if( std::find( d_ce_atoms.begin(), d_ce_atoms.end(), n )==d_ce_atoms.end() ){
-        Trace("cbqi-ce-atoms") << "CE atoms : " << n << std::endl;
+        Trace("cegqi-ce-atoms") << "CE atoms : " << n << std::endl;
         d_ce_atoms.push_back( n );
       }
     }
@@ -1572,7 +1572,7 @@ void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited )
 }
 
 void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) {
-  Trace("cbqi-reg") << "Register counterexample lemma..." << std::endl;
+  Trace("cegqi-reg") << "Register counterexample lemma..." << std::endl;
   d_input_vars.clear();
   d_input_vars.insert(d_input_vars.end(), ce_vars.begin(), ce_vars.end());
 
@@ -1581,12 +1581,12 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
   registerTheoryId(THEORY_UF);
   for (unsigned i = 0; i < ce_vars.size(); i++)
   {
-    Trace("cbqi-reg") << "  register input variable : " << ce_vars[i] << std::endl;
+    Trace("cegqi-reg") << "  register input variable : " << ce_vars[i] << std::endl;
     registerVariable(ce_vars[i]);
   }
 
   // preprocess with all relevant instantiator preprocessors
-  Trace("cbqi-debug") << "Preprocess based on theory-specific methods..."
+  Trace("cegqi-debug") << "Preprocess based on theory-specific methods..."
                       << std::endl;
   std::vector<Node> pvars;
   pvars.insert(pvars.end(), d_vars.begin(), d_vars.end());
@@ -1595,12 +1595,12 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
     p.second->registerCounterexampleLemma(lems, pvars);
   }
   // must register variables generated by preprocessors
-  Trace("cbqi-debug") << "Register variables from theory-specific methods "
+  Trace("cegqi-debug") << "Register variables from theory-specific methods "
                       << d_input_vars.size() << " " << pvars.size() << " ..."
                       << std::endl;
   for (unsigned i = d_input_vars.size(), size = pvars.size(); i < size; ++i)
   {
-    Trace("cbqi-reg") << "  register theory preprocess variable : " << pvars[i]
+    Trace("cegqi-reg") << "  register theory preprocess variable : " << pvars[i]
                       << std::endl;
     registerVariable(pvars[i]);
   }
@@ -1609,21 +1609,21 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
   IteSkolemMap iteSkolemMap;
   d_qe->getTheoryEngine()->getTermFormulaRemover()->run(lems, iteSkolemMap);
   for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) {
-    Trace("cbqi-reg") << "  register aux variable : " << i->first << std::endl;
+    Trace("cegqi-reg") << "  register aux variable : " << i->first << std::endl;
     registerVariable(i->first);
   }
   for( unsigned i=0; i<lems.size(); i++ ){
-    Trace("cbqi-debug") << "Counterexample lemma (pre-rewrite)  " << i << " : " << lems[i] << std::endl;
+    Trace("cegqi-debug") << "Counterexample lemma (pre-rewrite)  " << i << " : " << lems[i] << std::endl;
     Node rlem = lems[i];
     rlem = Rewriter::rewrite( rlem );
     // also must preprocess to ensure that the counterexample atoms we
     // collect below are identical to the atoms that we add to the CNF stream
     rlem = d_qe->getTheoryEngine()->preprocess(rlem);
-    Trace("cbqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl;
+    Trace("cegqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl;
     lems[i] = rlem;
   }
   // determine variable order: must do Reals before Ints
-  Trace("cbqi-debug") << "Determine variable order..." << std::endl;
+  Trace("cegqi-debug") << "Determine variable order..." << std::endl;
   if (!d_vars.empty())
   {
     std::map<Node, unsigned> voo;
@@ -1647,21 +1647,21 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
     }
     if (doSort)
     {
-      Trace("cbqi-debug") << "Sort variables based on ordering." << std::endl;
+      Trace("cegqi-debug") << "Sort variables based on ordering." << std::endl;
       for (std::pair<const TypeNode, std::vector<Node> >& vs : tvars)
       {
         vars.insert(vars.end(), vs.second.begin(), vs.second.end());
       }
 
-      Trace("cbqi-debug") << "Consider variables in this order : " << std::endl;
+      Trace("cegqi-debug") << "Consider variables in this order : " << std::endl;
       for (unsigned i = 0; i < vars.size(); i++)
       {
         d_var_order_index[voo[vars[i]]] = i;
-        Trace("cbqi-debug") << "  " << vars[i] << " : " << vars[i].getType()
+        Trace("cegqi-debug") << "  " << vars[i] << " : " << vars[i].getType()
                             << ", index was : " << voo[vars[i]] << std::endl;
         d_vars[i] = vars[i];
       }
-      Trace("cbqi-debug") << std::endl;
+      Trace("cegqi-debug") << std::endl;
     }
     else
     {
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 8273f2c91..208eb0bf8 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -66,7 +66,7 @@ InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe)
   d_small_const =
       NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000));
   d_check_vts_lemma_lc = false;
-  if (options::cbqiBv())
+  if (options::cegqiBv())
   {
     // if doing instantiation for BV, need the inverter class
     d_bv_invert.reset(new quantifiers::BvInverter);
@@ -96,7 +96,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
   if( !hasAddedCbqiLemma( q ) ){
     NodeManager* nm = NodeManager::currentNM();
     d_added_cbqi_lemma.insert( q );
-    Trace("cbqi-debug") << "Do cbqi for " << q << std::endl;
+    Trace("cegqi-debug") << "Do cbqi for " << q << std::endl;
     //add cbqi lemma
     //get the counterexample literal
     Node ceLit = getCounterexampleLiteral(q);
@@ -106,10 +106,10 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
       Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() );
       //require any decision on cel to be phase=true
       d_quantEngine->addRequirePhase( ceLit, true );
-      Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
+      Debug("cegqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
       //add counterexample lemma
       lem = Rewriter::rewrite( lem );
-      Trace("cbqi-lemma") << "Counterexample lemma : " << lem << std::endl;
+      Trace("cegqi-lemma") << "Counterexample lemma : " << lem << std::endl;
       registerCounterexampleLemma( q, lem );
       
       //totality lemmas for EPR
@@ -129,7 +129,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
                   disj.push_back( ic.eqNode( itc->second[j] ) );
                 }
                 Node tlem = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj );
-                Trace("cbqi-lemma") << "EPR totality lemma : " << tlem << std::endl;
+                Trace("cegqi-lemma") << "EPR totality lemma : " << tlem << std::endl;
                 d_quantEngine->getOutputChannel().lemma( tlem );
               }else{
                 Assert(false);
@@ -162,7 +162,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
       if (!dep.empty())
       {
         Node dep_lemma = nm->mkNode(IMPLIES, ceLit, nm->mkNode(AND, dep));
-        Trace("cbqi-lemma")
+        Trace("cegqi-lemma")
             << "Counterexample dependency lemma : " << dep_lemma << std::endl;
         d_quantEngine->getOutputChannel().lemma(dep_lemma);
       }
@@ -174,14 +174,14 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
         if( doCbqi( quants[i] ) ){
           registerCbqiLemma( quants[i] );
         }
-        if( options::cbqiNestedQE() ){
+        if( options::cegqiNestedQE() ){
           //record these as counterexample quantifiers
           QAttributes qa;
           QuantAttributes::computeQuantAttributes( quants[i], qa );
           if( !qa.d_qid_num.isNull() ){
             d_id_to_ce_quant[ qa.d_qid_num ] = quants[i];
             d_ce_quant_to_id[ quants[i] ] = qa.d_qid_num;
-            Trace("cbqi-nqe") << "CE quant id = " << qa.d_qid_num << " is " << quants[i] << std::endl;
+            Trace("cegqi-nqe") << "CE quant id = " << qa.d_qid_num << " is " << quants[i] << std::endl;
           }
         }
       }
@@ -226,21 +226,21 @@ void InstStrategyCegqi::reset_round(Theory::Effort effort)
       Assert(hasAddedCbqiLemma(q));
       if( d_quantEngine->getModel()->isQuantifierActive( q ) ){
         d_active_quant[q] = true;
-        Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl;
+        Debug("cegqi-debug") << "Check quantified formula " << q << "..." << std::endl;
         Node cel = getCounterexampleLiteral(q);
         bool value;
         if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){
-          Debug("cbqi-debug") << "...CE Literal has value " << value << std::endl;
+          Debug("cegqi-debug") << "...CE Literal has value " << value << std::endl;
           if( !value ){
             if( d_quantEngine->getValuation().isDecision( cel ) ){
-              Trace("cbqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl;
+              Trace("cegqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl;
             }else{
-              Trace("cbqi") << "Inactive : " << q << std::endl;
+              Trace("cegqi") << "Inactive : " << q << std::endl;
               d_quantEngine->getModel()->setQuantifierActive( q, false );
               d_cbqi_set_quant_inactive = true;
               d_active_quant.erase( q );
               d_elim_quants.insert( q );
-              Trace("cbqi-nqe") << "Inactive, waitlist proc/size = " << d_nested_qe_waitlist_proc[q].get() << "/" << d_nested_qe_waitlist_size[q].get() << std::endl;
+              Trace("cegqi-nqe") << "Inactive, waitlist proc/size = " << d_nested_qe_waitlist_proc[q].get() << "/" << d_nested_qe_waitlist_size[q].get() << std::endl;
               //process from waitlist
               while( d_nested_qe_waitlist_proc[q]<d_nested_qe_waitlist_size[q] ){
                 int index = d_nested_qe_waitlist_proc[q];
@@ -249,43 +249,43 @@ void InstStrategyCegqi::reset_round(Theory::Effort effort)
                 Node nq = d_nested_qe_waitlist[q][index];
                 Node nqeqn = doNestedQENode( d_nested_qe_info[nq].d_q, q, nq, d_nested_qe_info[nq].d_inst_terms, d_nested_qe_info[nq].d_doVts );
                 Node dqelem = nq.eqNode( nqeqn ); 
-                Trace("cbqi-lemma") << "Delayed nested quantifier elimination lemma : " << dqelem << std::endl;
+                Trace("cegqi-lemma") << "Delayed nested quantifier elimination lemma : " << dqelem << std::endl;
                 d_quantEngine->getOutputChannel().lemma( dqelem );
                 d_nested_qe_waitlist_proc[q] = index + 1;
               }
             }
           }
         }else{
-          Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl;
+          Debug("cegqi-debug") << "...CE Literal does not have value " << std::endl;
         }
       }
     }
   }
 
   //refinement: only consider innermost active quantified formulas
-  if( options::cbqiInnermost() ){
+  if( options::cegqiInnermost() ){
     if( !d_children_quant.empty() && !d_active_quant.empty() ){
-      Trace("cbqi-debug") << "Find non-innermost quantifiers..." << std::endl;
+      Trace("cegqi-debug") << "Find non-innermost quantifiers..." << std::endl;
       std::vector< Node > ninner;
       for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
         std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( it->first );
         if( itc!=d_children_quant.end() ){
           for( unsigned j=0; j<itc->second.size(); j++ ){
             if( d_active_quant.find( itc->second[j] )!=d_active_quant.end() ){
-              Trace("cbqi-debug") << "Do not consider " << it->first << " since it is not innermost (" << itc->second[j] << std::endl;
+              Trace("cegqi-debug") << "Do not consider " << it->first << " since it is not innermost (" << itc->second[j] << std::endl;
               ninner.push_back( it->first );
               break;
             }
           }
         }
       } 
-      Trace("cbqi-debug") << "Found " << ninner.size() << " non-innermost." << std::endl;
+      Trace("cegqi-debug") << "Found " << ninner.size() << " non-innermost." << std::endl;
       for( unsigned i=0; i<ninner.size(); i++ ){
         Assert(d_active_quant.find(ninner[i]) != d_active_quant.end());
         d_active_quant.erase( ninner[i] );
       }
       Assert(!d_active_quant.empty());
-      Trace("cbqi-debug") << "...done removing." << std::endl;
+      Trace("cegqi-debug") << "...done removing." << std::endl;
     }
   }
   d_check_vts_lemma_lc = false;
@@ -297,9 +297,9 @@ void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e)
   {
     Assert(!d_quantEngine->inConflict());
     double clSet = 0;
-    if( Trace.isOn("cbqi-engine") ){
+    if( Trace.isOn("cegqi-engine") ){
       clSet = double(clock())/double(CLOCKS_PER_SEC);
-      Trace("cbqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl;
+      Trace("cegqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl;
     }
     unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
     for( int ee=0; ee<=1; ee++ ){
@@ -308,14 +308,14 @@ void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e)
       //  if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
       for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
         Node q = it->first;
-        Trace("cbqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl;
+        Trace("cegqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl;
         if( d_nested_qe.find( q )==d_nested_qe.end() ){
           process( q, e, ee );
           if( d_quantEngine->inConflict() ){
             break;
           }
         }else{
-          Trace("cbqi-warn") << "CBQI : Cannot process already eliminated quantified formula " << q << std::endl;
+          Trace("cegqi-warn") << "CBQI : Cannot process already eliminated quantified formula " << q << std::endl;
           Assert(false);
         }
       }
@@ -323,19 +323,19 @@ void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e)
         break;
       }
     }
-    if( Trace.isOn("cbqi-engine") ){
+    if( Trace.isOn("cegqi-engine") ){
       if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
-        Trace("cbqi-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl;
+        Trace("cegqi-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl;
       }
       double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
-      Trace("cbqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl;
+      Trace("cegqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl;
     }
   }
 }
 
 bool InstStrategyCegqi::checkComplete()
 {
-  if( ( !options::cbqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){
+  if( ( !options::cegqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){
     return false;
   }else{
     return true;
@@ -415,7 +415,7 @@ void InstStrategyCegqi::checkOwnership(Node q)
 void InstStrategyCegqi::preRegisterQuantifier(Node q)
 {
   // mark all nested quantifiers with id
-  if (options::cbqiNestedQE())
+  if (options::cegqiNestedQE())
   {
     if( d_quantEngine->getOwner(q)==this )
     {
@@ -436,20 +436,20 @@ void InstStrategyCegqi::preRegisterQuantifier(Node q)
         }
         Node qq = NodeManager::currentNM()->mkNode(FORALL, qqc);
         Node mlem = NodeManager::currentNM()->mkNode(IMPLIES, q, qq);
-        Trace("cbqi-lemma") << "Mark quant id lemma : " << mlem << std::endl;
+        Trace("cegqi-lemma") << "Mark quant id lemma : " << mlem << std::endl;
         d_quantEngine->addLemma(mlem);
       }
     }
   }
   if( doCbqi( q ) ){
     // get the instantiator
-    if (options::cbqiPreRegInst())
+    if (options::cegqiPreRegInst())
     {
       getInstantiator(q);
     }
     // register the cbqi lemma
     if( registerCbqiLemma( q ) ){
-      Trace("cbqi") << "Registered cbqi lemma for quantifier : " << q << std::endl;
+      Trace("cegqi") << "Registered cbqi lemma for quantifier : " << q << std::endl;
     }
   }
 }
@@ -466,7 +466,7 @@ Node InstStrategyCegqi::rewriteInstantiation(Node q,
     inst = d_vtsCache->rewriteVtsSymbols(inst);
     Trace("quant-vts-debug") << "...got " << inst << std::endl;
   }
-  if (options::cbqiNestedQE())
+  if (options::cegqiNestedQE())
   {
     inst = doNestedQE(q, terms, inst, doVts);
   }
@@ -488,9 +488,9 @@ Node InstStrategyCegqi::doNestedQENode(
   // in this case, q is equivalent to the quantifier-free formula C[t].
   if( d_nested_qe.find( ceq )==d_nested_qe.end() ){
     d_nested_qe[ceq] = d_quantEngine->getInstantiatedConjunction( ceq );
-    Trace("cbqi-nqe") << "CE quantifier elimination : " << std::endl;
-    Trace("cbqi-nqe") << "  " << ceq << std::endl; 
-    Trace("cbqi-nqe") << "  " << d_nested_qe[ceq] << std::endl;
+    Trace("cegqi-nqe") << "CE quantifier elimination : " << std::endl;
+    Trace("cegqi-nqe") << "  " << ceq << std::endl; 
+    Trace("cegqi-nqe") << "  " << d_nested_qe[ceq] << std::endl;
     //should not contain quantifiers
     Assert(!expr::hasClosure(d_nested_qe[ceq]));
   }
@@ -505,9 +505,9 @@ Node InstStrategyCegqi::doNestedQENode(
     ret = Rewriter::rewrite( ret );
     ret = d_vtsCache->rewriteVtsSymbols(ret);
   }
-  Trace("cbqi-nqe") << "Nested quantifier elimination: " << std::endl;
-  Trace("cbqi-nqe") << "  " << n << std::endl; 
-  Trace("cbqi-nqe") << "  " << ret << std::endl;
+  Trace("cegqi-nqe") << "Nested quantifier elimination: " << std::endl;
+  Trace("cegqi-nqe") << "  " << n << std::endl; 
+  Trace("cegqi-nqe") << "  " << ret << std::endl;
   return ret;
 }
 
@@ -531,10 +531,10 @@ Node InstStrategyCegqi::doNestedQERec(Node q,
           if( doNestedQe ){
             ret = doNestedQENode( q, ceq, n, inst_terms, doVts );
           }else{
-            Trace("cbqi-nqe") << "Add to nested qe waitlist : " << std::endl;
+            Trace("cegqi-nqe") << "Add to nested qe waitlist : " << std::endl;
             Node nr = Rewriter::rewrite( n );
-            Trace("cbqi-nqe") << "  " << ceq << std::endl;
-            Trace("cbqi-nqe") << "  " << nr << std::endl;
+            Trace("cegqi-nqe") << "  " << ceq << std::endl;
+            Trace("cegqi-nqe") << "  " << nr << std::endl;
             int wlsize = d_nested_qe_waitlist_size[ceq] + 1;
             d_nested_qe_waitlist_size[ceq] = wlsize;
             if( wlsize<(int)d_nested_qe_waitlist[ceq].size() ){
@@ -547,7 +547,7 @@ Node InstStrategyCegqi::doNestedQERec(Node q,
             d_nested_qe_info[nr].d_inst_terms.insert( d_nested_qe_info[nr].d_inst_terms.end(), inst_terms.begin(), inst_terms.end() );
             d_nested_qe_info[nr].d_doVts = doVts;
             //TODO: ensure this holds by restricting prenex when cbqiNestedQe is true.
-            Assert(!options::cbqiInnermost());
+            Assert(!options::cegqiInnermost());
           }
         } 
       } 
@@ -599,7 +599,7 @@ void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem)
   cinst->registerCounterexampleLemma(lems, ce_vars);
   for (unsigned i = 0, size = lems.size(); i < size; i++)
   {
-    Trace("cbqi-debug") << "Counterexample lemma " << i << " : " << lems[i]
+    Trace("cegqi-debug") << "Counterexample lemma " << i << " : " << lems[i]
                         << std::endl;
     d_quantEngine->addLemma(lems[i], false);
   }
@@ -610,7 +610,7 @@ bool InstStrategyCegqi::doCbqi(Node q)
   std::map<Node, CegHandledStatus>::iterator it = d_do_cbqi.find(q);
   if( it==d_do_cbqi.end() ){
     CegHandledStatus ret = CegInstantiator::isCbqiQuant(q, d_quantEngine);
-    Trace("cbqi-quant") << "doCbqi " << q << " returned " << ret << std::endl;
+    Trace("cegqi-quant") << "doCbqi " << q << " returned " << ret << std::endl;
     d_do_cbqi[q] = ret;
     return ret != CEG_UNHANDLED;
   }
@@ -687,7 +687,7 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
       return true;
     }else{
       //this should never happen for monotonic selection strategies
-      Trace("cbqi-warn") << "WARNING: Existing instantiation" << std::endl;
+      Trace("cegqi-warn") << "WARNING: Existing instantiation" << std::endl;
       return false;
     }
   }
@@ -719,13 +719,13 @@ BvInverter* InstStrategyCegqi::getBvInverter() const
 }
 
 void InstStrategyCegqi::presolve() {
-  if (!options::cbqiPreRegInst())
+  if (!options::cegqiPreRegInst())
   {
     return;
   }
   for (std::pair<const Node, std::unique_ptr<CegInstantiator>>& ci : d_cinst)
   {
-    Trace("cbqi-presolve") << "Presolve " << ci.first << std::endl;
+    Trace("cegqi-presolve") << "Presolve " << ci.first << std::endl;
     ci.second->presolve(ci.first);
   }
 }
diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index ee6291564..784453838 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -31,7 +31,7 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::inst;
 
 bool CandidateGenerator::isLegalCandidate( Node n ){
-  return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr(n) );
+  return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(n) );
 }
 
 CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersEngine* qe, Node pat)
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index 964d2e492..a95944bed 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -1053,7 +1053,7 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple(Node q,
   Assert(Trigger::isSimpleTrigger(d_match_pattern));
   for( unsigned i=0; i<d_match_pattern.getNumChildren(); i++ ){
     if( d_match_pattern[i].getKind()==INST_CONSTANT ){
-      if( !options::cbqi() || quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i])==q ){
+      if( !options::cegqi() || quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i])==q ){
         d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
       }else{
         d_var_num[i] = -1;
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index 355375d06..f806234ef 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -230,7 +230,7 @@ int EqualityQueryQuantifiersEngine::getRepScore(Node n,
                                                 int index,
                                                 TypeNode v_tn)
 {
-  if( options::cbqi() && quantifiers::TermUtil::hasInstConstAttr(n) ){  //reject
+  if( options::cegqi() && quantifiers::TermUtil::hasInstConstAttr(n) ){  //reject
     return -2;
   }else if( !n.getType().isSubtypeOf( v_tn ) ){  //reject if incorrect type
     return -2;
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index 6c17746ef..9388f2dba 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -207,7 +207,7 @@ bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd)
         for (unsigned j = 0; j < ts; j++)
         {
           Node gt = tdb->getTypeGroundTerm(ftypes[i], j);
-          if (!options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr(gt))
+          if (!options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(gt))
           {
             Node rep = qy->getRepresentative(gt);
             if (reps_found.find(rep) == reps_found.end())
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 218753308..89e2678fc 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -146,7 +146,7 @@ bool Instantiate::addInstantiation(
                     << std::endl;
       bad_inst = true;
     }
-    else if (options::cbqi())
+    else if (options::cegqi())
     {
       Node icf = quantifiers::TermUtil::getInstConstAttr(terms[i]);
       if (!icf.isNull())
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 511eb6d79..2d1cf6531 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1925,7 +1925,7 @@ void QuantConflictFind::reset_round( Theory::Effort level ) {
     if (tdb->hasTermCurrent(r))
     {
       TypeNode rtn = r.getType();
-      if (!options::cbqi() || !TermUtil::hasInstConstAttr(r))
+      if (!options::cegqi() || !TermUtil::hasInstConstAttr(r))
       {
         d_eqcs[rtn].push_back(r);
       }
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 27d77dfbb..ec1b9e71a 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -56,7 +56,7 @@ void CegSingleInv::initialize(Node q)
   Assert(d_quant.isNull());
   d_quant = q;
   d_simp_quant = q;
-  Trace("cegqi-si") << "CegSingleInv::initialize : " << q << std::endl;
+  Trace("sygus-si") << "CegSingleInv::initialize : " << q << std::endl;
   // infer single invocation-ness
 
   // get the variables
@@ -87,13 +87,13 @@ void CegSingleInv::initialize(Node q)
   // process the single invocation-ness of the property
   if (!d_sip->init(progs, qq))
   {
-    Trace("cegqi-si") << "...not single invocation (type mismatch)"
+    Trace("sygus-si") << "...not single invocation (type mismatch)"
                       << std::endl;
     return;
   }
-  Trace("cegqi-si") << "- Partitioned to single invocation parts : "
+  Trace("sygus-si") << "- Partitioned to single invocation parts : "
                     << std::endl;
-  d_sip->debugPrint("cegqi-si");
+  d_sip->debugPrint("sygus-si");
 
   // map from program to bound variables
   std::vector<Node> funcs;
@@ -142,7 +142,7 @@ void CegSingleInv::initialize(Node q)
     return;
   }
   // if we are doing invariant templates, then construct the template
-  Trace("cegqi-si") << "- Do transition inference..." << std::endl;
+  Trace("sygus-si") << "- Do transition inference..." << std::endl;
   d_ti[q].process(qq, q[0][0]);
   Trace("cegqi-inv") << std::endl;
   Node prog = d_ti[q].getFunction();
@@ -194,7 +194,7 @@ void CegSingleInv::initialize(Node q)
           .negate();
   d_simp_quant = Rewriter::rewrite(d_simp_quant);
   d_simp_quant = nm->mkNode(FORALL, q[0], d_simp_quant, q[2]);
-  Trace("cegqi-si") << "Rewritten quantifier : " << d_simp_quant << std::endl;
+  Trace("sygus-si") << "Rewritten quantifier : " << d_simp_quant << std::endl;
 
   // construct template argument
   d_templ_arg[prog] = nm->mkSkolem("I", invariant.getType());
@@ -273,21 +273,21 @@ void CegSingleInv::initialize(Node q)
 
 void CegSingleInv::finishInit(bool syntaxRestricted)
 {
-  Trace("cegqi-si-debug") << "Single invocation: finish init" << std::endl;
+  Trace("sygus-si-debug") << "Single invocation: finish init" << std::endl;
   // do not do single invocation if grammar is restricted and
   // options::CegqiSingleInvMode::ALL is not enabled
   if (options::cegqiSingleInvMode() == options::CegqiSingleInvMode::USE
       && d_single_invocation && syntaxRestricted)
   {
     d_single_invocation = false;
-    Trace("cegqi-si") << "...grammar is restricted, do not use single invocation techniques." << std::endl;
+    Trace("sygus-si") << "...grammar is restricted, do not use single invocation techniques." << std::endl;
   }
 
   // we now have determined whether we will do single invocation techniques
   if (!d_single_invocation)
   {
     d_single_inv = Node::null();
-    Trace("cegqi-si") << "Formula is not single invocation." << std::endl;
+    Trace("sygus-si") << "Formula is not single invocation." << std::endl;
     if (options::cegqiSingleInvAbort())
     {
       std::stringstream ss;
@@ -320,7 +320,7 @@ void CegSingleInv::finishInit(bool syntaxRestricted)
                                          sivars.end(),
                                          d_single_inv_arg_sk.begin(),
                                          d_single_inv_arg_sk.end());
-  Trace("cegqi-si") << "Single invocation formula is : " << d_single_inv
+  Trace("sygus-si") << "Single invocation formula is : " << d_single_inv
                     << std::endl;
   // check whether we can handle this quantified formula
   CegHandledStatus status = CEG_HANDLED;
@@ -332,10 +332,10 @@ void CegSingleInv::finishInit(bool syntaxRestricted)
       status = CegInstantiator::isCbqiQuant(d_single_inv);
     }
   }
-  Trace("cegqi-si") << "CegHandledStatus is " << status << std::endl;
+  Trace("sygus-si") << "CegHandledStatus is " << status << std::endl;
   if (status < CEG_HANDLED)
   {
-    Trace("cegqi-si") << "...do not invoke single invocation techniques since "
+    Trace("sygus-si") << "...do not invoke single invocation techniques since "
                          "the quantified formula does not have a handled "
                          "counterexample-guided instantiation strategy!"
                       << std::endl;
@@ -356,7 +356,7 @@ bool CegSingleInv::solve()
     // already solved, probably via a call to solveTrivial.
     return true;
   }
-  Trace("cegqi-si") << "Solve using single invocation..." << std::endl;
+  Trace("sygus-si") << "Solve using single invocation..." << std::endl;
   NodeManager* nm = NodeManager::currentNM();
   // Mark the quantified formula with the quantifier elimination attribute to
   // ensure its structure is preserved in the query below.
@@ -378,7 +378,7 @@ bool CegSingleInv::solve()
   siSmt.setLogic(smt::currentSmtEngine()->getLogicInfo());
   siSmt.assertFormula(siq.toExpr());
   Result r = siSmt.checkSat();
-  Trace("cegqi-si") << "Result: " << r << std::endl;
+  Trace("sygus-si") << "Result: " << r << std::endl;
   if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
   {
     // conjecture is infeasible or unknown
@@ -389,7 +389,7 @@ bool CegSingleInv::solve()
   siSmt.getInstantiatedQuantifiedFormulas(qs);
   Assert(qs.size() <= 1);
   // track the instantiations, as solution construction is based on this
-  Trace("cegqi-si") << "#instantiated quantified formulas=" << qs.size()
+  Trace("sygus-si") << "#instantiated quantified formulas=" << qs.size()
                     << std::endl;
   d_inst.clear();
   d_instConds.clear();
@@ -399,7 +399,7 @@ bool CegSingleInv::solve()
     Assert(qn.getKind() == FORALL);
     std::vector<std::vector<Expr> > tvecs;
     siSmt.getInstantiationTermVectors(q, tvecs);
-    Trace("cegqi-si") << "#instantiations of " << q << "=" << tvecs.size()
+    Trace("sygus-si") << "#instantiations of " << q << "=" << tvecs.size()
                       << std::endl;
     std::vector<Node> vars;
     for (const Node& v : qn[0])
@@ -415,14 +415,14 @@ bool CegSingleInv::solve()
       {
         inst.push_back(Node::fromExpr(t));
       }
-      Trace("cegqi-si") << "  Instantiation: " << inst << std::endl;
+      Trace("sygus-si") << "  Instantiation: " << inst << std::endl;
       d_inst.push_back(inst);
       Assert(inst.size() == vars.size());
       Node ilem =
           body.substitute(vars.begin(), vars.end(), inst.begin(), inst.end());
       ilem = Rewriter::rewrite(ilem);
       d_instConds.push_back(ilem);
-      Trace("cegqi-si") << "  Instantiation Lemma: " << ilem << std::endl;
+      Trace("sygus-si") << "  Instantiation Lemma: " << ilem << std::endl;
     }
   }
   d_isSolved = true;
@@ -654,7 +654,7 @@ bool CegSingleInv::solveTrivial(Node q)
   // if we solved all arguments
   if (args.empty() && body.isConst() && !body.getConst<bool>())
   {
-    Trace("cegqi-si-trivial-solve")
+    Trace("sygus-si-trivial-solve")
         << q << " is trivially solvable by substitution " << vars << " -> "
         << subs << std::endl;
     std::map<Node, Node> imap;
@@ -673,7 +673,7 @@ bool CegSingleInv::solveTrivial(Node q)
     d_isSolved = true;
     return true;
   }
-  Trace("cegqi-si-trivial-solve")
+  Trace("sygus-si-trivial-solve")
       << q << " is not trivially solvable." << std::endl;
   return false;
 }
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index dfef0bad4..0c11baecc 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -138,7 +138,7 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
   // constructors.
   if (!d_usingSymCons)
   {
-    Trace("cegqi-engine") << "  *** Do refinement lemma evaluation"
+    Trace("sygus-engine") << "  *** Do refinement lemma evaluation"
                           << (doGen ? " with conjecture-specific refinement"
                                     : "")
                           << "..." << std::endl;
@@ -168,7 +168,7 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
       // just check whether the refinement lemmas are satisfied, fail if not
       if (checkRefinementEvalLemmas(candidates, candidate_values))
       {
-        Trace("cegqi-engine") << "...(actively enumerated) candidate failed "
+        Trace("sygus-engine") << "...(actively enumerated) candidate failed "
                                  "refinement lemma evaluation."
                               << std::endl;
         return true;
@@ -179,7 +179,7 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
   bool doEvalUnfold = (doGen && options::sygusEvalUnfold()) || d_usingSymCons;
   if (doEvalUnfold)
   {
-    Trace("cegqi-engine") << "  *** Do evaluation unfolding..." << std::endl;
+    Trace("sygus-engine") << "  *** Do evaluation unfolding..." << std::endl;
     std::vector<Node> eager_terms, eager_vals, eager_exps;
     for (unsigned i = 0, size = candidates.size(); i < size; ++i)
     {
@@ -627,7 +627,7 @@ bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates,
                                      const std::vector<Node>& vals,
                                      std::vector<Node>& lems)
 {
-  Trace("cegqi-engine") << "  *** Do sample add refinement..." << std::endl;
+  Trace("sygus-engine") << "  *** Do sample add refinement..." << std::endl;
   if (Trace.isOn("cegis-sample"))
   {
     Trace("cegis-sample") << "Check sampling for candidate solution"
@@ -681,7 +681,7 @@ bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates,
             }
             Trace("cegis-sample") << std::endl;
           }
-          Trace("cegqi-engine") << "  *** Refine by sampling" << std::endl;
+          Trace("sygus-engine") << "  *** Refine by sampling" << std::endl;
           addRefinementLemma(rlem);
           // if trust, we are not interested in sending out refinement lemmas
           if (options::cegisSample() != options::CegisSampleMode::TRUST)
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index 3590e76f1..ce3c94914 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -781,7 +781,7 @@ bool SygusEnumerator::TermEnumMaster::incrementInternal()
         }
         if (doTerminate)
         {
-          Trace("cegqi-engine") << "master(" << d_tn << "): complete at size "
+          Trace("sygus-engine") << "master(" << d_tn << "): complete at size "
                                 << d_currSize << std::endl;
           tc.setComplete();
           return false;
@@ -793,12 +793,12 @@ bool SygusEnumerator::TermEnumMaster::incrementInternal()
     d_currSize++;
     Trace("sygus-enum-debug2") << "master(" << d_tn
                                << "): size++ : " << d_currSize << "\n";
-    if (Trace.isOn("cegqi-engine"))
+    if (Trace.isOn("sygus-engine"))
     {
       // am i the master enumerator? if so, print
       if (d_se->d_tlEnum == this)
       {
-        Trace("cegqi-engine") << "SygusEnumerator::size = " << d_currSize
+        Trace("sygus-engine") << "SygusEnumerator::size = " << d_currSize
                               << std::endl;
       }
     }
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index df41672e2..aa0dc8e5e 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -256,7 +256,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
     }
   }
 
-  Trace("cegqi-engine") << "Repairing previous solution..." << std::endl;
+  Trace("sygus-engine") << "Repairing previous solution..." << std::endl;
   // make the satisfiability query
   bool needExport = true;
   ExprManagerMapCollection varMap;
@@ -268,7 +268,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
   if (r.asSatisfiabilityResult().isSat() == Result::UNSAT
       || r.asSatisfiabilityResult().isUnknown())
   {
-    Trace("cegqi-engine") << "...failed" << std::endl;
+    Trace("sygus-engine") << "...failed" << std::endl;
     return false;
   }
   std::vector<Node> sk_sygus_m;
@@ -300,7 +300,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
     Node scsk = csk.substitute(
         sk_vars.begin(), sk_vars.end(), sk_sygus_m.begin(), sk_sygus_m.end());
     repair_cv.push_back(scsk);
-    if (Trace.isOn("sygus-repair-const") || Trace.isOn("cegqi-engine"))
+    if (Trace.isOn("sygus-repair-const") || Trace.isOn("sygus-engine"))
     {
       std::stringstream sss;
       Printer::getPrinter(options::outputLanguage())
@@ -308,8 +308,8 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
       ss << "  * " << candidates[i] << " -> " << sss.str() << std::endl;
     }
   }
-  Trace("cegqi-engine") << "...success:" << std::endl;
-  Trace("cegqi-engine") << ss.str();
+  Trace("sygus-engine") << "...success:" << std::endl;
+  Trace("sygus-engine") << ss.str();
   Trace("sygus-repair-const")
       << "Repaired constants in solution : " << std::endl;
   Trace("sygus-repair-const") << ss.str();
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index e69d746fe..bb5307c79 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -280,12 +280,12 @@ bool SynthConjecture::needsCheck()
   {
     if (!value)
     {
-      Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl;
+      Trace("sygus-engine-debug") << "Conjecture is infeasible." << std::endl;
       return false;
     }
     else
     {
-      Trace("cegqi-engine-debug") << "Feasible guard " << d_feasible_guard
+      Trace("sygus-engine-debug") << "Feasible guard " << d_feasible_guard
                                   << " assigned true." << std::endl;
     }
   }
@@ -366,16 +366,16 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
         Assert(d_repair_index < d_cinfo[cprog].d_inst.size());
         fail_cvs.push_back(d_cinfo[cprog].d_inst[d_repair_index]);
       }
-      if (Trace.isOn("cegqi-engine"))
+      if (Trace.isOn("sygus-engine"))
       {
-        Trace("cegqi-engine") << "CegConjuncture : repair previous solution ";
+        Trace("sygus-engine") << "CegConjuncture : repair previous solution ";
         for (const Node& fc : fail_cvs)
         {
           std::stringstream ss;
           Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, fc);
-          Trace("cegqi-engine") << ss.str() << " ";
+          Trace("sygus-engine") << ss.str() << " ";
         }
-        Trace("cegqi-engine") << std::endl;
+        Trace("sygus-engine") << std::endl;
       }
       d_repair_index++;
       if (d_sygus_rconst->repairSolution(
@@ -397,7 +397,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
     if (!d_master->allowPartialModel() && !fullModel)
     {
       // we retain the values in d_ev_active_gen_waiting
-      Trace("cegqi-engine-debug") << "...partial model, fail." << std::endl;
+      Trace("sygus-engine-debug") << "...partial model, fail." << std::endl;
       // if we are partial due to an active enumerator, we may still succeed
       // on the next call
       return !activeIncomplete;
@@ -416,13 +416,13 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
     }
     if (emptyModel)
     {
-      Trace("cegqi-engine-debug") << "...empty model, fail." << std::endl;
+      Trace("sygus-engine-debug") << "...empty model, fail." << std::endl;
       return !activeIncomplete;
     }
     // debug print
-    if (Trace.isOn("cegqi-engine"))
+    if (Trace.isOn("sygus-engine"))
     {
-      Trace("cegqi-engine") << "  * Value is : ";
+      Trace("sygus-engine") << "  * Value is : ";
       for (unsigned i = 0, size = terms.size(); i < size; i++)
       {
         Node nv = enum_values[i];
@@ -430,23 +430,23 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
         TypeNode tn = onv.getType();
         std::stringstream ss;
         Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, onv);
-        Trace("cegqi-engine") << terms[i] << " -> ";
+        Trace("sygus-engine") << terms[i] << " -> ";
         if (nv.isNull())
         {
-          Trace("cegqi-engine") << "[EXC: " << ss.str() << "] ";
+          Trace("sygus-engine") << "[EXC: " << ss.str() << "] ";
         }
         else
         {
-          Trace("cegqi-engine") << ss.str() << " ";
-          if (Trace.isOn("cegqi-engine-rr"))
+          Trace("sygus-engine") << ss.str() << " ";
+          if (Trace.isOn("sygus-engine-rr"))
           {
             Node bv = d_tds->sygusToBuiltin(nv, tn);
             bv = Rewriter::rewrite(bv);
-            Trace("cegqi-engine-rr") << " -> " << bv << std::endl;
+            Trace("sygus-engine-rr") << " -> " << bv << std::endl;
           }
         }
       }
-      Trace("cegqi-engine") << std::endl;
+      Trace("sygus-engine") << std::endl;
     }
     Assert(candidate_values.empty());
     constructed_cand = d_master->constructCandidates(
@@ -471,7 +471,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
     if (!checkSideCondition(candidate_values))
     {
       excludeCurrentSolution(terms, candidate_values);
-      Trace("cegqi-engine") << "...failed side condition" << std::endl;
+      Trace("sygus-engine") << "...failed side condition" << std::endl;
       return false;
     }
   }
@@ -590,22 +590,22 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
     lem = nm->mkNode(OR, d_quant.negate(), query);
     if (options::sygusVerifySubcall())
     {
-      Trace("cegqi-engine") << "  *** Verify with subcall..." << std::endl;
+      Trace("sygus-engine") << "  *** Verify with subcall..." << std::endl;
 
       Result r =
           checkWithSubsolver(query.toExpr(), d_ce_sk_vars, d_ce_sk_var_mvs);
-      Trace("cegqi-engine") << "  ...got " << r << std::endl;
+      Trace("sygus-engine") << "  ...got " << r << std::endl;
       if (r.asSatisfiabilityResult().isSat() == Result::SAT)
       {
-        if (Trace.isOn("cegqi-engine"))
+        if (Trace.isOn("sygus-engine"))
         {
-          Trace("cegqi-engine") << "  * Verification lemma failed for:\n   ";
+          Trace("sygus-engine") << "  * Verification lemma failed for:\n   ";
           for (unsigned i = 0, size = d_ce_sk_vars.size(); i < size; i++)
           {
-            Trace("cegqi-engine")
+            Trace("sygus-engine")
                 << d_ce_sk_vars[i] << " -> " << d_ce_sk_var_mvs[i] << " ";
           }
-          Trace("cegqi-engine") << std::endl;
+          Trace("sygus-engine") << std::endl;
         }
 #ifdef CVC4_ASSERTIONS
         // the values for the query should be a complete model
@@ -658,7 +658,7 @@ bool SynthConjecture::checkSideCondition(const std::vector<Node>& cvals) const
   {
     Node sc = d_embedSideCondition.substitute(
         d_candidates.begin(), d_candidates.end(), cvals.begin(), cvals.end());
-    Trace("cegqi-engine") << "Check side condition..." << std::endl;
+    Trace("sygus-engine") << "Check side condition..." << std::endl;
     Trace("cegqi-debug") << "Check side condition : " << sc << std::endl;
     Result r = checkWithSubsolver(sc);
     Trace("cegqi-debug") << "...got side condition : " << r << std::endl;
@@ -666,7 +666,7 @@ bool SynthConjecture::checkSideCondition(const std::vector<Node>& cvals) const
     {
       return false;
     }
-    Trace("cegqi-engine") << "...passed side condition" << std::endl;
+    Trace("sygus-engine") << "...passed side condition" << std::endl;
   }
   return true;
 }
@@ -763,7 +763,7 @@ bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n,
       Node gstatus = d_qe->getValuation().getSatValue(g);
       if (gstatus.isNull() || !gstatus.getConst<bool>())
       {
-        Trace("cegqi-engine-debug")
+        Trace("sygus-engine-debug")
             << "Enumerator " << e << " is inactive." << std::endl;
         continue;
       }
@@ -785,7 +785,7 @@ Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete)
     // if the current model value of e was not registered by the datatypes
     // sygus solver, or was excluded by symmetry breaking, then it does not
     // have a proper model value that we should consider, thus we return null.
-    Trace("cegqi-engine-debug")
+    Trace("sygus-engine-debug")
         << "Enumerator " << e << " does not have proper model value."
         << std::endl;
     return Node::null();
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 0c8b8f734..b0a562b42 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -43,12 +43,12 @@ SynthEngine::~SynthEngine() {}
 
 void SynthEngine::presolve()
 {
-  Trace("cegqi-engine") << "SynthEngine::presolve" << std::endl;
+  Trace("sygus-engine") << "SynthEngine::presolve" << std::endl;
   for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
   {
     d_conjs[i]->presolve();
   }
-  Trace("cegqi-engine") << "SynthEngine::presolve finished" << std::endl;
+  Trace("sygus-engine") << "SynthEngine::presolve finished" << std::endl;
 }
 
 bool SynthEngine::needsCheck(Theory::Effort e)
@@ -75,7 +75,7 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e)
   {
     Node q = d_waiting_conj.back();
     d_waiting_conj.pop_back();
-    Trace("cegqi-engine") << "--- Conjecture waiting to assign: " << q
+    Trace("sygus-engine") << "--- Conjecture waiting to assign: " << q
                           << std::endl;
     assignConjecture(q);
   }
@@ -87,9 +87,9 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e)
     return;
   }
 
-  Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---"
+  Trace("sygus-engine") << "---Counterexample Guided Instantiation Engine---"
                         << std::endl;
-  Trace("cegqi-engine-debug") << std::endl;
+  Trace("sygus-engine-debug") << std::endl;
   Valuation& valuation = d_quantEngine->getValuation();
   std::vector<SynthConjecture*> activeCheckConj;
   for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
@@ -103,10 +103,10 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e)
     }
     else
     {
-      Trace("cegqi-engine-debug") << "...no value for quantified formula."
+      Trace("sygus-engine-debug") << "...no value for quantified formula."
                                   << std::endl;
     }
-    Trace("cegqi-engine-debug")
+    Trace("sygus-engine-debug")
         << "Current conjecture status : active : " << active << std::endl;
     if (active && sc->needsCheck())
     {
@@ -116,7 +116,7 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e)
   std::vector<SynthConjecture*> acnext;
   do
   {
-    Trace("cegqi-engine-debug") << "Checking " << activeCheckConj.size()
+    Trace("sygus-engine-debug") << "Checking " << activeCheckConj.size()
                                 << " active conjectures..." << std::endl;
     for (unsigned i = 0, size = activeCheckConj.size(); i < size; i++)
     {
@@ -134,13 +134,13 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e)
     acnext.clear();
   } while (!activeCheckConj.empty()
            && !d_quantEngine->theoryEngineNeedsCheck());
-  Trace("cegqi-engine")
+  Trace("sygus-engine")
       << "Finished Counterexample Guided Instantiation engine." << std::endl;
 }
 
 void SynthEngine::assignConjecture(Node q)
 {
-  Trace("cegqi-engine") << "SynthEngine::assignConjecture " << q << std::endl;
+  Trace("sygus-engine") << "SynthEngine::assignConjecture " << q << std::endl;
   if (options::sygusQePreproc())
   {
     // the following does quantifier elimination as a preprocess step
@@ -307,16 +307,16 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj)
 {
   Node q = conj->getEmbeddedConjecture();
   Node aq = conj->getConjecture();
-  if (Trace.isOn("cegqi-engine-debug"))
+  if (Trace.isOn("sygus-engine-debug"))
   {
-    conj->debugPrint("cegqi-engine-debug");
-    Trace("cegqi-engine-debug") << std::endl;
+    conj->debugPrint("sygus-engine-debug");
+    Trace("sygus-engine-debug") << std::endl;
   }
 
   if (!conj->needsRefinement())
   {
-    Trace("cegqi-engine-debug") << "Do conjecture check..." << std::endl;
-    Trace("cegqi-engine-debug")
+    Trace("sygus-engine-debug") << "Do conjecture check..." << std::endl;
+    Trace("sygus-engine-debug")
         << "  *** Check candidate phase..." << std::endl;
     std::vector<Node> cclems;
     bool ret = conj->doCheck(cclems);
@@ -331,13 +331,13 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj)
       else
       {
         // this may happen if we eagerly unfold, simplify to true
-        Trace("cegqi-engine-debug")
+        Trace("sygus-engine-debug")
             << "  ...FAILED to add candidate!" << std::endl;
       }
     }
     if (addedLemma)
     {
-      Trace("cegqi-engine-debug")
+      Trace("sygus-engine-debug")
           << "  ...check for counterexample." << std::endl;
       return true;
     }
@@ -353,7 +353,7 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj)
   }
   else
   {
-    Trace("cegqi-engine-debug")
+    Trace("sygus-engine-debug")
         << "  *** Refine candidate phase..." << std::endl;
     std::vector<Node> rlems;
     conj->doRefine(rlems);
@@ -377,7 +377,7 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj)
     }
     if (addedLemma)
     {
-      Trace("cegqi-engine-debug") << "  ...refine candidate." << std::endl;
+      Trace("sygus-engine-debug") << "  ...refine candidate." << std::endl;
     }
   }
   return true;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index e4caaa539..ca4768ee4 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -118,7 +118,7 @@ class QuantifiersEnginePrivate
       d_inst_engine.reset(new quantifiers::InstantiationEngine(qe));
       modules.push_back(d_inst_engine.get());
     }
-    if (options::cbqi())
+    if (options::cegqi())
     {
       d_i_cbqi.reset(new quantifiers::InstStrategyCegqi(qe));
       modules.push_back(d_i_cbqi.get());