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.

133 files changed, 469 insertions, 469 deletions

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
index b46253851..b0bc70cd7 100755
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current
@@ -90,24 +90,24 @@ ABVFP|BVFP|FP)
 UFBV)
   # most problems in UFBV are essentially BV
   trywith 600 --full-saturate-quant --decision=internal
-  trywith 600 --full-saturate-quant --cbqi-nested-qe --decision=internal
-  trywith 60 --full-saturate-quant --no-cbqi-innermost --global-negate
+  trywith 600 --full-saturate-quant --cegqi-nested-qe --decision=internal
+  trywith 60 --full-saturate-quant --no-cegqi-innermost --global-negate
   finishwith --finite-model-find
   ;;
 BV)
   trywith 240 --full-saturate-quant
-  trywith 240 --full-saturate-quant --no-cbqi-innermost
-  trywith 600 --full-saturate-quant --cbqi-nested-qe --decision=internal
-  trywith 60 --full-saturate-quant --no-cbqi-bv
-  trywith 60 --full-saturate-quant --cbqi-bv-ineq=eq-slack
+  trywith 240 --full-saturate-quant --no-cegqi-innermost
+  trywith 600 --full-saturate-quant --cegqi-nested-qe --decision=internal
+  trywith 60 --full-saturate-quant --no-cegqi-bv
+  trywith 60 --full-saturate-quant --cegqi-bv-ineq=eq-slack
   # finish 10min
-  finishwith --full-saturate-quant --no-cbqi-innermost --global-negate
+  finishwith --full-saturate-quant --no-cegqi-innermost --global-negate
   ;;
 LIA|LRA|NIA|NRA)
   trywith 60 --full-saturate-quant --nl-ext-tplanes
-  trywith 600 --full-saturate-quant --no-cbqi-innermost
-  trywith 600 --full-saturate-quant --cbqi-nested-qe
-  finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal
+  trywith 600 --full-saturate-quant --no-cegqi-innermost
+  trywith 600 --full-saturate-quant --cegqi-nested-qe
+  finishwith --full-saturate-quant --cegqi-nested-qe --decision=internal
   ;;
 QF_AUFBV)
   trywith 1200 --ite-simp
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
index 0371d8b42..5e827128e 100755
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
@@ -36,10 +36,10 @@ BV)
   finishwith --full-saturate-quant --decision=internal
   ;;
 LIA|LRA)
-  finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal
+  finishwith --full-saturate-quant --cegqi-nested-qe --decision=internal
   ;;
 NIA|NRA)
-  finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal
+  finishwith --full-saturate-quant --cegqi-nested-qe --decision=internal
   ;;
 QF_AUFBV)
   finishwith --decision=justification-stoponly --ite-simp
diff --git a/src/options/didyoumean_test.cpp b/src/options/didyoumean_test.cpp
index df1dfa5cc..2dd28a40f 100644
--- a/src/options/didyoumean_test.cpp
+++ b/src/options/didyoumean_test.cpp
@@ -165,9 +165,9 @@ set<string> getDebugTags() {
   a.insert("bvminisat");
   a.insert("bvminisat::explain");
   a.insert("bvminisat::search");
-  a.insert("cbqi");
-  a.insert("cbqi-debug");
-  a.insert("cbqi-prop-as-dec");
+  a.insert("cegqi");
+  a.insert("cegqi-debug");
+  a.insert("cegqi-prop-as-dec");
   a.insert("cd_set_collection");
   a.insert("cdlist");
   a.insert("cdlist:cmm");
@@ -605,7 +605,7 @@ set<string> getOptionStrings() {
       "literal-matching",
       "enable-cbqi",
       "no-enable-cbqi",
-      "cbqi-recurse",
+      "cegqi-recurse",
       "no-cbqi-recurse",
       "user-pat",
       "flip-decision",
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 32ae173bd..21cba6abb 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -987,7 +987,7 @@ header = "options/quantifiers_options.h"
 [[option]]
   name       = "cegqiSingleInvMode"
   category   = "regular"
-  long       = "cegqi-si=MODE"
+  long       = "sygus-si=MODE"
   type       = "CegqiSingleInvMode"
   default    = "NONE"
   help       = "mode for processing single invocation synthesis conjectures"
@@ -1005,7 +1005,7 @@ header = "options/quantifiers_options.h"
 [[option]]
   name       = "cegqiSingleInvPartial"
   category   = "regular"
-  long       = "cegqi-si-partial"
+  long       = "sygus-si-partial"
   type       = "bool"
   default    = "false"
   read_only  = true
@@ -1020,7 +1020,7 @@ header = "options/quantifiers_options.h"
 [[option]]
   name       = "cegqiSingleInvReconstruct"
   category   = "regular"
-  long       = "cegqi-si-rcons=MODE"
+  long       = "sygus-si-rcons=MODE"
   type       = "CegqiSingleInvRconsMode"
   default    = "ALL_LIMIT"
   help       = "policy for reconstructing solutions for single invocation conjectures"
@@ -1041,7 +1041,7 @@ header = "options/quantifiers_options.h"
 [[option]]
   name       = "cegqiSingleInvReconstructLimit"
   category   = "regular"
-  long       = "cegqi-si-rcons-limit=N"
+  long       = "sygus-si-rcons-limit=N"
   type       = "int"
   default    = "10000"
   read_only  = true
@@ -1050,7 +1050,7 @@ header = "options/quantifiers_options.h"
 [[option]]
   name       = "cegqiSingleInvReconstructConst"
   category   = "regular"
-  long       = "cegqi-si-reconstruct-const"
+  long       = "sygus-si-reconstruct-const"
   type       = "bool"
   default    = "true"
   read_only  = true
@@ -1059,7 +1059,7 @@ header = "options/quantifiers_options.h"
 [[option]]
   name       = "cegqiSingleInvAbort"
   category   = "regular"
-  long       = "cegqi-si-abort"
+  long       = "sygus-si-abort"
   type       = "bool"
   default    = "false"
   read_only  = true
@@ -1623,73 +1623,73 @@ header = "options/quantifiers_options.h"
 # CEGQI applied to general quantified formulas
 
 [[option]]
-  name       = "cbqi"
+  name       = "cegqi"
   category   = "regular"
-  long       = "cbqi"
+  long       = "cegqi"
   type       = "bool"
   default    = "false"
   help       = "turns on counterexample-based quantifier instantiation"
 
 [[option]]
-  name       = "cbqiFullEffort"
+  name       = "cegqiFullEffort"
   category   = "regular"
-  long       = "cbqi-full"
+  long       = "cegqi-full"
   type       = "bool"
   default    = "false"
   help       = "turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation"
 
 [[option]]
-  name       = "cbqiSat"
+  name       = "cegqiSat"
   category   = "regular"
-  long       = "cbqi-sat"
+  long       = "cegqi-sat"
   type       = "bool"
   default    = "true"
   help       = "answer sat when quantifiers are asserted with counterexample-based quantifier instantiation"
 
 [[option]]
-  name       = "cbqiModel"
+  name       = "cegqiModel"
   category   = "regular"
-  long       = "cbqi-model"
+  long       = "cegqi-model"
   type       = "bool"
   default    = "true"
   help       = "guide instantiations by model values for counterexample-based quantifier instantiation"
 
 [[option]]
-  name       = "cbqiAll"
+  name       = "cegqiAll"
   category   = "regular"
-  long       = "cbqi-all"
+  long       = "cegqi-all"
   type       = "bool"
   default    = "false"
   help       = "apply counterexample-based instantiation to all quantified formulas"
 
 [[option]]
-  name       = "cbqiMultiInst"
+  name       = "cegqiMultiInst"
   category   = "regular"
-  long       = "cbqi-multi-inst"
+  long       = "cegqi-multi-inst"
   type       = "bool"
   default    = "false"
   help       = "when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation"
 
 [[option]]
-  name       = "cbqiRepeatLit"
+  name       = "cegqiRepeatLit"
   category   = "regular"
-  long       = "cbqi-repeat-lit"
+  long       = "cegqi-repeat-lit"
   type       = "bool"
   default    = "false"
   help       = "solve literals more than once in counterexample-based quantifier instantiation"
 
 [[option]]
-  name       = "cbqiInnermost"
+  name       = "cegqiInnermost"
   category   = "regular"
-  long       = "cbqi-innermost"
+  long       = "cegqi-innermost"
   type       = "bool"
   default    = "true"
   help       = "only process innermost quantified formulas in counterexample-based quantifier instantiation"
 
 [[option]]
-  name       = "cbqiNestedQE"
+  name       = "cegqiNestedQE"
   category   = "regular"
-  long       = "cbqi-nested-qe"
+  long       = "cegqi-nested-qe"
   type       = "bool"
   default    = "false"
   help       = "process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation"
@@ -1697,59 +1697,59 @@ header = "options/quantifiers_options.h"
 # CEGQI for arithmetic
 
 [[option]]
-  name       = "cbqiUseInfInt"
+  name       = "cegqiUseInfInt"
   category   = "regular"
-  long       = "cbqi-use-inf-int"
+  long       = "cegqi-use-inf-int"
   type       = "bool"
   default    = "false"
   help       = "use integer infinity for vts in counterexample-based quantifier instantiation"
 
 [[option]]
-  name       = "cbqiUseInfReal"
+  name       = "cegqiUseInfReal"
   category   = "regular"
-  long       = "cbqi-use-inf-real"
+  long       = "cegqi-use-inf-real"
   type       = "bool"
   default    = "false"
   help       = "use real infinity for vts in counterexample-based quantifier instantiation"
 
 [[option]]
-  name       = "cbqiPreRegInst"
+  name       = "cegqiPreRegInst"
   category   = "regular"
-  long       = "cbqi-prereg-inst"
+  long       = "cegqi-prereg-inst"
   type       = "bool"
   default    = "false"
   help       = "preregister ground instantiations in counterexample-based quantifier instantiation"
 
 [[option]]
-  name       = "cbqiMinBounds"
+  name       = "cegqiMinBounds"
   category   = "regular"
-  long       = "cbqi-min-bounds"
+  long       = "cegqi-min-bounds"
   type       = "bool"
   default    = "false"
   read_only  = true
   help       = "use minimally constrained lower/upper bound for counterexample-based quantifier instantiation"
 
 [[option]]
-  name       = "cbqiRoundUpLowerLia"
+  name       = "cegqiRoundUpLowerLia"
   category   = "regular"
-  long       = "cbqi-round-up-lia"
+  long       = "cegqi-round-up-lia"
   type       = "bool"
   default    = "false"
   read_only  = true
   help       = "round up integer lower bounds in substitutions for counterexample-based quantifier instantiation"
 
 [[option]]
-  name       = "cbqiMidpoint"
+  name       = "cegqiMidpoint"
   category   = "regular"
-  long       = "cbqi-midpoint"
+  long       = "cegqi-midpoint"
   type       = "bool"
   default    = "false"
   help       = "choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation"
 
 [[option]]
-  name       = "cbqiNopt"
+  name       = "cegqiNopt"
   category   = "regular"
-  long       = "cbqi-nopt"
+  long       = "cegqi-nopt"
   type       = "bool"
   default    = "true"
   read_only  = true
@@ -1777,25 +1777,25 @@ header = "options/quantifiers_options.h"
 # CEGQI for BV
 
 [[option]]
-  name       = "cbqiBv"
+  name       = "cegqiBv"
   category   = "regular"
-  long       = "cbqi-bv"
+  long       = "cegqi-bv"
   type       = "bool"
   default    = "true"
   help       = "use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors"
 
 [[option]]
-  name       = "cbqiBvInterleaveValue"
+  name       = "cegqiBvInterleaveValue"
   category   = "regular"
-  long       = "cbqi-bv-interleave-value"
+  long       = "cegqi-bv-interleave-value"
   type       = "bool"
   default    = "false"
   help       = "interleave model value instantiation with word-level inversion approach"
 
 [[option]]
-  name       = "cbqiBvIneqMode"
+  name       = "cegqiBvIneqMode"
   category   = "regular"
-  long       = "cbqi-bv-ineq=MODE"
+  long       = "cegqi-bv-ineq=MODE"
   type       = "CbqiBvIneqMode"
   default    = "EQ_BOUNDARY"
   help       = "choose mode for handling bit-vector inequalities with counterexample-guided instantiation"
@@ -1811,33 +1811,33 @@ header = "options/quantifiers_options.h"
   help = "Solve for the inequality directly using side conditions for invertibility."
 
 [[option]]
-  name       = "cbqiBvRmExtract"
+  name       = "cegqiBvRmExtract"
   category   = "regular"
-  long       = "cbqi-bv-rm-extract"
+  long       = "cegqi-bv-rm-extract"
   type       = "bool"
   default    = "true"
   help       = "replaces extract terms with variables for counterexample-guided instantiation for bit-vectors"
 
 [[option]]
-  name       = "cbqiBvLinearize"
+  name       = "cegqiBvLinearize"
   category   = "regular"
-  long       = "cbqi-bv-linear"
+  long       = "cegqi-bv-linear"
   type       = "bool"
   default    = "true"
   help       = "linearize adder chains for variables"
 
 [[option]]
-  name       = "cbqiBvSolveNl"
+  name       = "cegqiBvSolveNl"
   category   = "regular"
-  long       = "cbqi-bv-solve-nl"
+  long       = "cegqi-bv-solve-nl"
   type       = "bool"
   default    = "false"
   help       = "try to solve non-linear bv literals using model value projections"
 
 [[option]]
-  name       = "cbqiBvConcInv"
+  name       = "cegqiBvConcInv"
   category   = "regular"
-  long       = "cbqi-bv-concat-inv"
+  long       = "cegqi-bv-concat-inv"
   type       = "bool"
   default    = "true"
   help       = "compute inverse for concat over equalities rather than producing an invertibility condition"
diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp
index 5e7d42632..59b5ddf6e 100644
--- a/src/preprocessing/passes/global_negate.cpp
+++ b/src/preprocessing/passes/global_negate.cpp
@@ -30,14 +30,14 @@ namespace passes {
 Node GlobalNegate::simplify(std::vector<Node>& assertions, NodeManager* nm)
 {
   Assert(!assertions.empty());
-  Trace("cbqi-gn") << "Global negate : " << std::endl;
+  Trace("cegqi-gn") << "Global negate : " << std::endl;
   // collect free variables in all assertions
   std::vector<Node> free_vars;
   std::vector<TNode> visit;
   std::unordered_set<TNode, TNodeHashFunction> visited;
   for (const Node& as : assertions)
   {
-    Trace("cbqi-gn") << "  " << as << std::endl;
+    Trace("cegqi-gn") << "  " << as << std::endl;
     TNode cur = as;
     // compute free variables
     visit.push_back(cur);
@@ -90,9 +90,9 @@ Node GlobalNegate::simplify(std::vector<Node>& assertions, NodeManager* nm)
     body = nm->mkNode(FORALL, bvl, body);
   }
 
-  Trace("cbqi-gn-debug") << "...got (pre-rewrite) : " << body << std::endl;
+  Trace("cegqi-gn-debug") << "...got (pre-rewrite) : " << body << std::endl;
   body = Rewriter::rewrite(body);
-  Trace("cbqi-gn") << "...got (post-rewrite) : " << body << std::endl;
+  Trace("cegqi-gn") << "...got (post-rewrite) : " << body << std::endl;
   return body;
 }
 
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 7109a3222..f98c9ee84 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -495,7 +495,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
     }
   }
 
-  if (options::cbqiBv() && logic.isQuantified())
+  if (options::cegqiBv() && logic.isQuantified())
   {
     if (options::boolToBitvector() != options::BoolToBVMode::OFF)
     {
@@ -819,11 +819,11 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
   {
     Notice() << "SmtEngine: turning off cbqi to support instMaxLevel"
              << std::endl;
-    options::cbqi.set(false);
+    options::cegqi.set(false);
   }
   // Do we need to track instantiations?
   // Needed for sygus due to single invocation techniques.
-  if (options::cbqiNestedQE()
+  if (options::cegqiNestedQE()
       || (options::proof() && !options::trackInstLemmas.wasSetByUser())
       || is_sygus)
   {
@@ -937,15 +937,15 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
     }
     options::sygus.set(true);
     // must use Ferrante/Rackoff for real arithmetic
-    if (!options::cbqiMidpoint.wasSetByUser())
+    if (!options::cegqiMidpoint.wasSetByUser())
     {
-      options::cbqiMidpoint.set(true);
+      options::cegqiMidpoint.set(true);
     }
     if (options::sygusRepairConst())
     {
-      if (!options::cbqi.wasSetByUser())
+      if (!options::cegqi.wasSetByUser())
       {
-        options::cbqi.set(true);
+        options::cegqi.set(true);
       }
     }
     if (options::sygusInference())
@@ -973,10 +973,10 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
     {
       options::instNoEntail.set(false);
     }
-    if (!options::cbqiFullEffort.wasSetByUser())
+    if (!options::cegqiFullEffort.wasSetByUser())
     {
       // should use full effort cbqi for single invocation and repair const
-      options::cbqiFullEffort.set(true);
+      options::cegqiFullEffort.set(true);
     }
     if (options::sygusRew())
     {
@@ -1085,9 +1085,9 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
     {
       options::macrosQuant.set(false);
     }
-    if (!options::cbqiPreRegInst.wasSetByUser())
+    if (!options::cegqiPreRegInst.wasSetByUser())
     {
-      options::cbqiPreRegInst.set(true);
+      options::cegqiPreRegInst.set(true);
     }
   }
   // counterexample-guided instantiation for non-sygus
@@ -1097,22 +1097,22 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
            || logic.isTheoryEnabled(THEORY_DATATYPES)
            || logic.isTheoryEnabled(THEORY_BV)
            || logic.isTheoryEnabled(THEORY_FP)))
-      || options::cbqiAll())
+      || options::cegqiAll())
   {
-    if (!options::cbqi.wasSetByUser())
+    if (!options::cegqi.wasSetByUser())
     {
-      options::cbqi.set(true);
+      options::cegqi.set(true);
     }
     // check whether we should apply full cbqi
     if (logic.isPure(THEORY_BV))
     {
-      if (!options::cbqiFullEffort.wasSetByUser())
+      if (!options::cegqiFullEffort.wasSetByUser())
       {
-        options::cbqiFullEffort.set(true);
+        options::cegqiFullEffort.set(true);
       }
     }
   }
-  if (options::cbqi())
+  if (options::cegqi())
   {
     // must rewrite divk
     if (!options::rewriteDivk.wasSetByUser())
@@ -1122,8 +1122,8 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
     if (options::incrementalSolving())
     {
       // cannot do nested quantifier elimination in incremental mode
-      options::cbqiNestedQE.set(false);
-      options::cbqiPreRegInst.set(false);
+      options::cegqiNestedQE.set(false);
+      options::cegqiPreRegInst.set(false);
     }
     if (logic.isPure(THEORY_ARITH) || logic.isPure(THEORY_BV))
     {
@@ -1135,7 +1135,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
       {
         options::instNoEntail.set(false);
       }
-      if (!options::instWhenMode.wasSetByUser() && options::cbqiModel())
+      if (!options::instWhenMode.wasSetByUser() && options::cegqiModel())
       {
         // only instantiation should happen at last call when model is avaiable
         options::instWhenMode.set(options::InstWhenMode::LAST_CALL);
@@ -1144,10 +1144,10 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
     else
     {
       // only supported in pure arithmetic or pure BV
-      options::cbqiNestedQE.set(false);
+      options::cegqiNestedQE.set(false);
     }
     // prenexing
-    if (options::cbqiNestedQE())
+    if (options::cegqiNestedQE())
     {
       // only complete with prenex = disj_normal or normal
       if (options::prenexQuant() <= options::PrenexQuantMode::DISJ_NORMAL)
@@ -1175,7 +1175,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
   {
     options::quantConflictFind.set(true);
   }
-  if (options::cbqiNestedQE())
+  if (options::cegqiNestedQE())
   {
     options::prenexQuantUser.set(true);
     if (!options::preSkolemQuant.wasSetByUser())
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());
diff --git a/test/regress/regress0/expect/scrub.08.sy b/test/regress/regress0/expect/scrub.08.sy
index 02879cb8d..592189df2 100644
--- a/test/regress/regress0/expect/scrub.08.sy
+++ b/test/regress/regress0/expect/scrub.08.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --no-sygus-repair-const
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --no-sygus-repair-const
 ; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'
 ; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic.
 ; EXPECT: The fact in question: TERM
diff --git a/test/regress/regress0/quantifiers/ari056.smt2 b/test/regress/regress0/quantifiers/ari056.smt2
index a1f4aef04..aee3cd970 100644
--- a/test/regress/regress0/quantifiers/ari056.smt2
+++ b/test/regress/regress0/quantifiers/ari056.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi
+; COMMAND-LINE: --cegqi
 ; EXPECT: unsat
 (set-logic UFNIRA)
 (set-info :status unsat)
diff --git a/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 b/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2
index fe567f898..7e58ea87c 100644
--- a/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2
+++ b/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi --dt-rewrite-error-sel --lang=smt2.5
+; COMMAND-LINE: --cegqi --dt-rewrite-error-sel --lang=smt2.5
 ; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (declare-datatypes () ((List (cons (head Int) (tail List)) (nil))))
diff --git a/test/regress/regress0/quantifiers/issue4086-infs.smt2 b/test/regress/regress0/quantifiers/issue4086-infs.smt2
index 2ebb45960..faad2cf18 100644
--- a/test/regress/regress0/quantifiers/issue4086-infs.smt2
+++ b/test/regress/regress0/quantifiers/issue4086-infs.smt2
@@ -1,7 +1,7 @@
 (set-logic LIRA)
 (set-info :status unsat)
-(set-option :cbqi-use-inf-int true) 
-(set-option :cbqi-use-inf-real true)
+(set-option :cegqi-use-inf-int true) 
+(set-option :cegqi-use-inf-real true)
 (set-option :var-ineq-elim-quant false) 
 (assert (forall (( b Real )) (forall (( c Int )) (and  (> c (* b 2 ))))))
 (check-sat)    
diff --git a/test/regress/regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2 b/test/regress/regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2
index 51d3e89ea..6caa2b10c 100644
--- a/test/regress/regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2
+++ b/test/regress/regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2
@@ -1,5 +1,5 @@
 (set-logic UFBV)
-(set-option :cbqi-all true)
+(set-option :cegqi-all true)
 (set-info :status unsat)
 (declare-sort S0 0)
 (declare-const S0-0 S0)
diff --git a/test/regress/regress0/quantifiers/mix-complete-strat.smt2 b/test/regress/regress0/quantifiers/mix-complete-strat.smt2
index e75591dec..fd7b3f574 100644
--- a/test/regress/regress0/quantifiers/mix-complete-strat.smt2
+++ b/test/regress/regress0/quantifiers/mix-complete-strat.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi --finite-model-find --no-check-models
+; COMMAND-LINE: --cegqi --finite-model-find --no-check-models
 ; EXPECT: sat
 (set-logic UFLIA)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2
index b196ee262..efac3468c 100644
--- a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2
+++ b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi --no-check-models
+; COMMAND-LINE: --cegqi --no-check-models
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/qbv-inequality2.smt2 b/test/regress/regress0/quantifiers/qbv-inequality2.smt2
index 1486e176d..939918ef7 100644
--- a/test/regress/regress0/quantifiers/qbv-inequality2.smt2
+++ b/test/regress/regress0/quantifiers/qbv-inequality2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 b/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2
index 3c4f93243..b6095fcab 100644
--- a/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2
+++ b/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/qbv-simp.smt2 b/test/regress/regress0/quantifiers/qbv-simp.smt2
index ec4626f52..2bdc2d994 100644
--- a/test/regress/regress0/quantifiers/qbv-simp.smt2
+++ b/test/regress/regress0/quantifiers/qbv-simp.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --no-cegqi-full
 ; EXPECT: unsat
 (set-logic BV)
 (set-info :status unsat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2
index 216a98531..790918675 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: unsat
 (set-logic BV)
 (set-info :status unsat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2
index ad3b9a9e5..ab1d665bb 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2
index 8dd50b1be..80cc8db6d 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2
index e05c3446d..92304674e 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: unsat
 (set-logic BV)
 (set-info :status unsat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2
index 2835e5956..ea778697f 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2
index 537f0ee3d..82efd63bf 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2
index 1018ce72c..cd8d0db2d 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2
index 503bc9852..9287e4c2b 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2
index 74c2891cf..1758bbe38 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2
index 4145c68b1..f5826fcda 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2
index e85ecc7de..5fed3ada8 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2
index abef84da2..d7bd29ba0 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2
index a1dca469a..3d6aec051 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2
index 4f9c6edc3..049df0b27 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: unsat
 (set-logic BV)
 (set-info :status unsat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2
index 69c5def65..3dc095e83 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: unsat
 (set-logic BV)
 (declare-fun a () (_ BitVec 8))
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2
index 769854f6f..4f8983e01 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: unsat
 (set-logic BV)
 (set-info :status unsat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2
index 7b66bd859..81a299b4e 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2
index 7dab5637e..ceda04f35 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: unsat
 (set-logic BV)
 (set-info :status unsat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2
index 13fb3e1c2..d295cfcdc 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2
index 43019c4cb..58b14a564 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress0/sygus/General_plus10.sy b/test/regress/regress0/sygus/General_plus10.sy
index 69bcd0f08..9dee4efdf 100755
--- a/test/regress/regress0/sygus/General_plus10.sy
+++ b/test/regress/regress0/sygus/General_plus10.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
 (set-logic LIA)
 
 (synth-fun fb () Int ((Start Int)) ((Start Int ((Constant Int)))))
diff --git a/test/regress/regress0/sygus/aig-si.sy b/test/regress/regress0/sygus/aig-si.sy
index 9330546d8..9d3af67fb 100644
--- a/test/regress/regress0/sygus/aig-si.sy
+++ b/test/regress/regress0/sygus/aig-si.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --cegqi-si-abort --decision=internal --cbqi --cbqi-prereg-inst --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-si-abort --decision=internal --cegqi --cegqi-prereg-inst --sygus-out=status
 (set-logic BV)
 
 (define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
diff --git a/test/regress/regress0/sygus/c100.sy b/test/regress/regress0/sygus/c100.sy
index 994fb6de3..b0837e341 100644
--- a/test/regress/regress0/sygus/c100.sy
+++ b/test/regress/regress0/sygus/c100.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/check-generic-red.sy b/test/regress/regress0/sygus/check-generic-red.sy
index d593a7d9e..c1ebc52b2 100644
--- a/test/regress/regress0/sygus/check-generic-red.sy
+++ b/test/regress/regress0/sygus/check-generic-red.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --decision=justification
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --decision=justification
 (set-logic LIA)
 
 (synth-fun P ((x Int) (y Int)) Bool
diff --git a/test/regress/regress0/sygus/const-var-test.sy b/test/regress/regress0/sygus/const-var-test.sy
index 31e88f523..78029cbc8 100644
--- a/test/regress/regress0/sygus/const-var-test.sy
+++ b/test/regress/regress0/sygus/const-var-test.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/hd-05-d1-prog-nogrammar.sy b/test/regress/regress0/sygus/hd-05-d1-prog-nogrammar.sy
index b410e5d23..8c77eea61 100644
--- a/test/regress/regress0/sygus/hd-05-d1-prog-nogrammar.sy
+++ b/test/regress/regress0/sygus/hd-05-d1-prog-nogrammar.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-si=none
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none
 ; EXPECT: unsat
 
 (set-logic BV)
diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy
index 9f9eea2a8..9793c927b 100644
--- a/test/regress/regress0/sygus/let-ringer.sy
+++ b/test/regress/regress0/sygus/let-ringer.sy
@@ -1,6 +1,6 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-unif-pi=complete --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-unif-pi=complete --sygus-out=status
 (set-logic LIA)
 (define-fun g ((x Int)) Int (ite (= x 1) 15 19))
 (define-fun letf ((z Int) (w Int) (s Int) (x Int)) Int (+ z (+ x (+ x (+ s (+ 1 (+ (g w) z)))))))
diff --git a/test/regress/regress0/sygus/let-simp.sy b/test/regress/regress0/sygus/let-simp.sy
index 91a865035..19a4e6bc9 100644
--- a/test/regress/regress0/sygus/let-simp.sy
+++ b/test/regress/regress0/sygus/let-simp.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
 (set-logic LIA)
 (define-fun letf ((z Int)) Int (+ z z))
 (synth-fun f ((x Int) (y Int)) Int
diff --git a/test/regress/regress0/sygus/parity-AIG-d0.sy b/test/regress/regress0/sygus/parity-AIG-d0.sy
index 09fae5410..d3ca69e96 100644
--- a/test/regress/regress0/sygus/parity-AIG-d0.sy
+++ b/test/regress/regress0/sygus/parity-AIG-d0.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
 (set-logic BV)
 
 (define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
diff --git a/test/regress/regress0/sygus/pbe-pred-contra.sy b/test/regress/regress0/sygus/pbe-pred-contra.sy
index 99c308173..5bd6ebae4 100644
--- a/test/regress/regress0/sygus/pbe-pred-contra.sy
+++ b/test/regress/regress0/sygus/pbe-pred-contra.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status
 ; EXPECT: unknown
 (set-logic LIA)
 (synth-fun P ((x Int)) Bool)
diff --git a/test/regress/regress1/bug519.smt2 b/test/regress/regress1/bug519.smt2
index 6cabbaa64..2d7d3a9c5 100644
--- a/test/regress/regress1/bug519.smt2
+++ b/test/regress/regress1/bug519.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi -mi --no-check-models
+; COMMAND-LINE: --cegqi -mi --no-check-models
 ; EXPECT: sat
 ; EXPECT: unsat
 
diff --git a/test/regress/regress1/quantifiers/NUM878.smt2 b/test/regress/regress1/quantifiers/NUM878.smt2
index 8d78bf861..6f26e7af2 100644
--- a/test/regress/regress1/quantifiers/NUM878.smt2
+++ b/test/regress/regress1/quantifiers/NUM878.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cegqi-bv
 ; EXPECT: unsat
 (set-logic BV)
 (set-info :status unsat)
diff --git a/test/regress/regress1/quantifiers/RNDPRE_4_1-dd-nqe.smt2 b/test/regress/regress1/quantifiers/RNDPRE_4_1-dd-nqe.smt2
index 6379d6cec..e19532329 100644
--- a/test/regress/regress1/quantifiers/RNDPRE_4_1-dd-nqe.smt2
+++ b/test/regress/regress1/quantifiers/RNDPRE_4_1-dd-nqe.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-nested-qe
+; COMMAND-LINE: --cegqi-nested-qe
 ; EXPECT: unsat
 (set-logic LRA)
 
diff --git a/test/regress/regress1/quantifiers/anti-sk-simp.smt2 b/test/regress/regress1/quantifiers/anti-sk-simp.smt2
index 2ae54a075..a5f576f86 100644
--- a/test/regress/regress1/quantifiers/anti-sk-simp.smt2
+++ b/test/regress/regress1/quantifiers/anti-sk-simp.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi --quant-anti-skolem
+; COMMAND-LINE: --cegqi --quant-anti-skolem
 ; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
diff --git a/test/regress/regress1/quantifiers/ari118-bv-2occ-x.smt2 b/test/regress/regress1/quantifiers/ari118-bv-2occ-x.smt2
index 2d70dfb8e..2372faa1e 100644
--- a/test/regress/regress1/quantifiers/ari118-bv-2occ-x.smt2
+++ b/test/regress/regress1/quantifiers/ari118-bv-2occ-x.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cegqi-bv
 ; EXPECT: unsat
 (set-logic BV)
 (set-info :status unsat)
diff --git a/test/regress/regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 b/test/regress/regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2
index 4d5cf4ec4..cd921419c 100644
--- a/test/regress/regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2
+++ b/test/regress/regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi --decision=internal
+; COMMAND-LINE: --cegqi --decision=internal
 ; EXPECT: unsat
 (set-logic LIA)
 (set-info :status unsat)
diff --git a/test/regress/regress1/quantifiers/extract-nproc.smt2 b/test/regress/regress1/quantifiers/extract-nproc.smt2
index 6072776dc..30b6a300d 100644
--- a/test/regress/regress1/quantifiers/extract-nproc.smt2
+++ b/test/regress/regress1/quantifiers/extract-nproc.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-rm-extract
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-rm-extract
 ; EXPECT: sat
 (set-logic BV)
 (declare-fun k_3 () (_ BitVec 8))
diff --git a/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 b/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2
index 38a4ed127..fdbac9996 100644
--- a/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2
+++ b/test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cegqi-bv
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/issue4243-prereg-inc.smt2 b/test/regress/regress1/quantifiers/issue4243-prereg-inc.smt2
index aa5cbc31e..92c8ac47b 100644
--- a/test/regress/regress1/quantifiers/issue4243-prereg-inc.smt2
+++ b/test/regress/regress1/quantifiers/issue4243-prereg-inc.smt2
@@ -3,7 +3,7 @@
 (set-logic BV)
 (set-info :status sat)
 (declare-fun _substvar_16_ () Bool)
-(set-option :cbqi-prereg-inst true)
+(set-option :cegqi-prereg-inst true)
 (set-option :check-models true)
 (declare-fun v2 () Bool)
 (push 1)
diff --git a/test/regress/regress1/quantifiers/lra-vts-inf.smt2 b/test/regress/regress1/quantifiers/lra-vts-inf.smt2
index 22d6455fb..80315edaf 100644
--- a/test/regress/regress1/quantifiers/lra-vts-inf.smt2
+++ b/test/regress/regress1/quantifiers/lra-vts-inf.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-use-inf-int --cbqi-use-inf-real
+; COMMAND-LINE: --cegqi-use-inf-int --cegqi-use-inf-real
 ; EXPECT: unsat
 (set-info :smt-lib-version 2.6)
 (set-logic LRA)
diff --git a/test/regress/regress1/quantifiers/model_6_1_bv.smt2 b/test/regress/regress1/quantifiers/model_6_1_bv.smt2
index 011430bd6..f2b69974f 100644
--- a/test/regress/regress1/quantifiers/model_6_1_bv.smt2
+++ b/test/regress/regress1/quantifiers/model_6_1_bv.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-nested-qe
+; COMMAND-LINE: --cegqi-nested-qe
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 b/test/regress/regress1/quantifiers/nested9_true-unreach-call.i_575.smt2
index 2a46d2a21..d39ad79f4 100644
--- a/test/regress/regress1/quantifiers/nested9_true-unreach-call.i_575.smt2
+++ b/test/regress/regress1/quantifiers/nested9_true-unreach-call.i_575.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cegqi-bv
 ; EXPECT: unsat
 (set-logic BV)
 (set-info :status unsat)
diff --git a/test/regress/regress1/quantifiers/nl-pow-trick.smt2 b/test/regress/regress1/quantifiers/nl-pow-trick.smt2
index 5152b89c4..82857c50a 100644
--- a/test/regress/regress1/quantifiers/nl-pow-trick.smt2
+++ b/test/regress/regress1/quantifiers/nl-pow-trick.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-all --no-relational-triggers
+; COMMAND-LINE: --cegqi-all --no-relational-triggers
 ; EXPECT: unsat
 (set-logic NIA)
 (declare-fun a () Int)
diff --git a/test/regress/regress1/quantifiers/nra-interleave-inst.smt2 b/test/regress/regress1/quantifiers/nra-interleave-inst.smt2
index 7d981597a..b01860f73 100644
--- a/test/regress/regress1/quantifiers/nra-interleave-inst.smt2
+++ b/test/regress/regress1/quantifiers/nra-interleave-inst.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-multi-inst
+; COMMAND-LINE: --cegqi-multi-inst
 ; EXPECT: unsat
 (set-info :smt-lib-version 2.6)
 (set-logic NRA)
diff --git a/test/regress/regress1/quantifiers/psyco-107-bv.smt2 b/test/regress/regress1/quantifiers/psyco-107-bv.smt2
index 82b54a231..06cec17c1 100644
--- a/test/regress/regress1/quantifiers/psyco-107-bv.smt2
+++ b/test/regress/regress1/quantifiers/psyco-107-bv.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=eq-boundary
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=eq-boundary
 ; EXPECT: unsat
 (set-logic BV)
 (set-info :status unsat)
diff --git a/test/regress/regress1/quantifiers/qbv-disequality3.smt2 b/test/regress/regress1/quantifiers/qbv-disequality3.smt2
index d16157509..78f5b7c88 100644
--- a/test/regress/regress1/quantifiers/qbv-disequality3.smt2
+++ b/test/regress/regress1/quantifiers/qbv-disequality3.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/qbv-simple-2vars-vo.smt2 b/test/regress/regress1/quantifiers/qbv-simple-2vars-vo.smt2
index c36322aac..31cc96325 100644
--- a/test/regress/regress1/quantifiers/qbv-simple-2vars-vo.smt2
+++ b/test/regress/regress1/quantifiers/qbv-simple-2vars-vo.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvashr-0.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvashr-0.smt2
index 30e7c2f8b..18eee2027 100644
--- a/test/regress/regress1/quantifiers/qbv-test-invert-bvashr-0.smt2
+++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvashr-0.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvashr-1.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvashr-1.smt2
index c3de64c4c..f639a129e 100644
--- a/test/regress/regress1/quantifiers/qbv-test-invert-bvashr-1.smt2
+++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvashr-1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvcomp.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvcomp.smt2
index 6bcc6501b..ed9c9880f 100644
--- a/test/regress/regress1/quantifiers/qbv-test-invert-bvcomp.smt2
+++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvcomp.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: unsat
 (set-logic BV)
 (declare-fun a () (_ BitVec 8))
diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvlshr-1.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvlshr-1.smt2
index 08479d90e..b098cc49e 100644
--- a/test/regress/regress1/quantifiers/qbv-test-invert-bvlshr-1.smt2
+++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvlshr-1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvmul-neq.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvmul-neq.smt2
index 9dc9f98ac..71795cfde 100644
--- a/test/regress/regress1/quantifiers/qbv-test-invert-bvmul-neq.smt2
+++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvmul-neq.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvmul.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvmul.smt2
index f3dad679b..adcd5dfa8 100644
--- a/test/regress/regress1/quantifiers/qbv-test-invert-bvmul.smt2
+++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvmul.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2
index 3748eca24..751c5d6bb 100644
--- a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2
+++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: unsat
 (set-logic BV)
 (set-info :status unsat)
diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2
index 2cabb502e..9e8cd6586 100644
--- a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2
+++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2
index a0e1b62c2..5c2c42202 100644
--- a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2
+++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full --bv-div-zero-const
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full --bv-div-zero-const
 ; EXPECT: unsat
 (set-logic BV)
 (set-info :status unsat)
diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2
index 2690a0ac9..e9883297e 100644
--- a/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2
+++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full --bv-div-zero-const
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full --bv-div-zero-const
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2
index 871df4827..2c42744ac 100644
--- a/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2
+++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2 b/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2
index 22bd306ee..f24aa6b1b 100644
--- a/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2
+++ b/test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2 b/test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2
index e57352b8f..dbb653351 100644
--- a/test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2
+++ b/test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/small-pipeline-fixpoint-3.smt2 b/test/regress/regress1/quantifiers/small-pipeline-fixpoint-3.smt2
index 378912490..05bcb762f 100644
--- a/test/regress/regress1/quantifiers/small-pipeline-fixpoint-3.smt2
+++ b/test/regress/regress1/quantifiers/small-pipeline-fixpoint-3.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --no-check-models
+; COMMAND-LINE: --cegqi-bv --no-check-models
 ; EXPECT: unsat
 (set-logic BV)
 (set-info :status unsat)
diff --git a/test/regress/regress1/sygus/Base16_1.sy b/test/regress/regress1/sygus/Base16_1.sy
index b84e5bb48..b47060bf8 100644
--- a/test/regress/regress1/sygus/Base16_1.sy
+++ b/test/regress/regress1/sygus/Base16_1.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-qe-preproc --cbqi-full --sygus-out=status --cegqi-si=all
+; COMMAND-LINE: --lang=sygus2 --sygus-qe-preproc --cegqi-full --sygus-out=status --sygus-si=all
 (set-logic BV)
 
 (define-fun B ((h (_ BitVec 8)) (l (_ BitVec 8)) (v (_ BitVec 8))) (_ BitVec 8) (bvlshr (bvshl v (bvsub #x07 h)) (bvsub #x07 (bvsub h l))))
diff --git a/test/regress/regress1/sygus/array_search_2.sy b/test/regress/regress1/sygus/array_search_2.sy
index 1a7c5888c..b519c570f 100644
--- a/test/regress/regress1/sygus/array_search_2.sy
+++ b/test/regress/regress1/sygus/array_search_2.sy
@@ -1,6 +1,6 @@
 ; REQUIRES: proof
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --cegqi-si-sol-min-core --proof
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --sygus-si-sol-min-core --proof
 (set-logic LIA)
 (synth-fun findIdx ((y1 Int) (y2 Int) (k1 Int)) Int ((Start Int) (BoolExpr Bool)) ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
 (declare-var x1 Int)
diff --git a/test/regress/regress1/sygus/array_search_5-Q-easy.sy b/test/regress/regress1/sygus/array_search_5-Q-easy.sy
index dd1783d85..fb1c10337 100644
--- a/test/regress/regress1/sygus/array_search_5-Q-easy.sy
+++ b/test/regress/regress1/sygus/array_search_5-Q-easy.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --decision=justification
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --decision=justification
 (set-logic LIA)
 
 (synth-fun findIdx  ((y1 Int) (y2 Int) (y3 Int) (y4 Int) (y5 Int) (k1 Int)) Int
diff --git a/test/regress/regress1/sygus/array_sum_2_5.sy b/test/regress/regress1/sygus/array_sum_2_5.sy
index 84046f30a..9490f73b6 100644
--- a/test/regress/regress1/sygus/array_sum_2_5.sy
+++ b/test/regress/regress1/sygus/array_sum_2_5.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
 (set-logic LIA)
 (synth-fun findSum ( (y1 Int) (y2 Int) )Int ((Start Int) (BoolExpr Bool)) ((Start Int ( 0 1 2 y1 y2 (+ Start Start)    (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
 (declare-var x1 Int)
diff --git a/test/regress/regress1/sygus/clock-inc-tuple.sy b/test/regress/regress1/sygus/clock-inc-tuple.sy
index c9705f7b8..b5d7bff91 100644
--- a/test/regress/regress1/sygus/clock-inc-tuple.sy
+++ b/test/regress/regress1/sygus/clock-inc-tuple.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --decision=justification
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --decision=justification
 
 (set-logic ALL_SUPPORTED)
 (declare-var m Int)
diff --git a/test/regress/regress1/sygus/crcy-si-rcons.sy b/test/regress/regress1/sygus/crcy-si-rcons.sy
index 70aec7c4c..177a33274 100644
--- a/test/regress/regress1/sygus/crcy-si-rcons.sy
+++ b/test/regress/regress1/sygus/crcy-si-rcons.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --cegqi-si-abort --decision=internal --cegqi-si-rcons=try --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-si-abort --decision=internal --sygus-si-rcons=try --sygus-out=status
 
 (set-logic BV)
 
diff --git a/test/regress/regress1/sygus/dt-test-ns.sy b/test/regress/regress1/sygus/dt-test-ns.sy
index 90fa57827..f67784002 100644
--- a/test/regress/regress1/sygus/dt-test-ns.sy
+++ b/test/regress/regress1/sygus/dt-test-ns.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
 (set-logic DTLIA)
 
 (declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil))))
diff --git a/test/regress/regress1/sygus/dup-op.sy b/test/regress/regress1/sygus/dup-op.sy
index 517849b2a..dfd99f55d 100644
--- a/test/regress/regress1/sygus/dup-op.sy
+++ b/test/regress/regress1/sygus/dup-op.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int) (Con Int))
diff --git a/test/regress/regress1/sygus/enum-test.sy b/test/regress/regress1/sygus/enum-test.sy
index 55b2eb69e..b5fbe4306 100644
--- a/test/regress/regress1/sygus/enum-test.sy
+++ b/test/regress/regress1/sygus/enum-test.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
 (set-logic LIA)
 ;; this is the custom enumeration datatype syntax from an early proposal of the sygus standard
 (define-sort D (Enum (a b)))
diff --git a/test/regress/regress1/sygus/error1-dt.sy b/test/regress/regress1/sygus/error1-dt.sy
index 1ae8cabd9..d0027d685 100644
--- a/test/regress/regress1/sygus/error1-dt.sy
+++ b/test/regress/regress1/sygus/error1-dt.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-si=none --sygus-active-gen=enum
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none --sygus-active-gen=enum
 
 (set-logic ALL_SUPPORTED)
 
diff --git a/test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy b/test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy
index 089a8f11f..ab8852d2e 100644
--- a/test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy
+++ b/test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
 
 (set-logic BV)
 
diff --git a/test/regress/regress1/sygus/hd-sdiv.sy b/test/regress/regress1/sygus/hd-sdiv.sy
index c4c90c6f6..2fdfb1c43 100644
--- a/test/regress/regress1/sygus/hd-sdiv.sy
+++ b/test/regress/regress1/sygus/hd-sdiv.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status
 (set-logic BV)
 
 (define-fun hd01 ((x (_ BitVec 32))) (_ BitVec 32) (bvand x #x00000001))
diff --git a/test/regress/regress1/sygus/int-any-const.sy b/test/regress/regress1/sygus/int-any-const.sy
index 18e7ed06e..f377b23c1 100644
--- a/test/regress/regress1/sygus/int-any-const.sy
+++ b/test/regress/regress1/sygus/int-any-const.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term-concise
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-si=none --sygus-grammar-cons=any-term-concise
 
 (set-logic LIA)
 (synth-fun f ((x Int) (y Int)) Int)
diff --git a/test/regress/regress1/sygus/large-const-simp.sy b/test/regress/regress1/sygus/large-const-simp.sy
index d93644197..08f280a4b 100644
--- a/test/regress/regress1/sygus/large-const-simp.sy
+++ b/test/regress/regress1/sygus/large-const-simp.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --sygus-add-const-grammar
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --sygus-add-const-grammar
 (set-logic LIA)
 
 (synth-fun lc ((x Int)) Int)
diff --git a/test/regress/regress1/sygus/list-head-x.sy b/test/regress/regress1/sygus/list-head-x.sy
index ae2bcc00e..c6b7d032a 100644
--- a/test/regress/regress1/sygus/list-head-x.sy
+++ b/test/regress/regress1/sygus/list-head-x.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
 (set-logic ALL_SUPPORTED)
 
 (declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil))))
diff --git a/test/regress/regress1/sygus/max.sy b/test/regress/regress1/sygus/max.sy
index f191d784f..e753277cc 100644
--- a/test/regress/regress1/sygus/max.sy
+++ b/test/regress/regress1/sygus/max.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
 (set-logic LIA)
 
 (synth-fun max ((x Int) (y Int)) Int
diff --git a/test/regress/regress1/sygus/nia-max-square-ns.sy b/test/regress/regress1/sygus/nia-max-square-ns.sy
index 5d63ab023..1177be5e7 100644
--- a/test/regress/regress1/sygus/nia-max-square-ns.sy
+++ b/test/regress/regress1/sygus/nia-max-square-ns.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --nl-ext-tplanes
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --nl-ext-tplanes
 (set-logic NIA)
 
 (synth-fun max ((x Int) (y Int)) Int)
diff --git a/test/regress/regress1/sygus/parity-si-rcons.sy b/test/regress/regress1/sygus/parity-si-rcons.sy
index 850cc6610..aea7e32f3 100644
--- a/test/regress/regress1/sygus/parity-si-rcons.sy
+++ b/test/regress/regress1/sygus/parity-si-rcons.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --cegqi-si-abort --decision=internal --cbqi-prereg-inst --cegqi-si-rcons=try --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-si-abort --decision=internal --cegqi-prereg-inst --sygus-si-rcons=try --sygus-out=status
 
 (set-logic BV)
 
diff --git a/test/regress/regress1/sygus/phone-1-long.sy b/test/regress/regress1/sygus/phone-1-long.sy
index 0b402acf5..6d89a4e6c 100644
--- a/test/regress/regress1/sygus/phone-1-long.sy
+++ b/test/regress/regress1/sygus/phone-1-long.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --sygus-fair=direct

+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --sygus-fair=direct

 ; EXPECT: unsat

 (set-logic SLIA)

 

diff --git a/test/regress/regress1/sygus/process-10-vars.sy b/test/regress/regress1/sygus/process-10-vars.sy
index 6a9a80a49..86fac86cd 100644
--- a/test/regress/regress1/sygus/process-10-vars.sy
+++ b/test/regress/regress1/sygus/process-10-vars.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --sygus-arg-relevant
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --sygus-arg-relevant
 ; EXPECT: unsat
 (set-logic LIA)
 
diff --git a/test/regress/regress1/sygus/qe.sy b/test/regress/regress1/sygus/qe.sy
index c8d56229a..eba30350d 100644
--- a/test/regress/regress1/sygus/qe.sy
+++ b/test/regress/regress1/sygus/qe.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --sygus-qe-preproc
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --sygus-qe-preproc
 (set-logic LIA)
 
 (synth-fun f ((x Int)) Int)
diff --git a/test/regress/regress1/sygus/real-any-const.sy b/test/regress/regress1/sygus/real-any-const.sy
index 431d0c1b0..53db26910 100644
--- a/test/regress/regress1/sygus/real-any-const.sy
+++ b/test/regress/regress1/sygus/real-any-const.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term-concise
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-si=none --sygus-grammar-cons=any-term-concise
 
 (set-logic LRA)
 (synth-fun f ((x Real) (y Real)) Real)
diff --git a/test/regress/regress1/sygus/real-grammar.sy b/test/regress/regress1/sygus/real-grammar.sy
index 128a94c1d..d664bf2a2 100644
--- a/test/regress/regress1/sygus/real-grammar.sy
+++ b/test/regress/regress1/sygus/real-grammar.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-si=none
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none
 
 (set-logic LRA)
 
diff --git a/test/regress/regress1/sygus/repair-const-rl.sy b/test/regress/regress1/sygus/repair-const-rl.sy
index 6477de3fc..3374d6a8a 100644
--- a/test/regress/regress1/sygus/repair-const-rl.sy
+++ b/test/regress/regress1/sygus/repair-const-rl.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --cegqi-si=none --sygus-repair-const --lang=sygus2
+; COMMAND-LINE: --sygus-out=status --sygus-si=none --sygus-repair-const --lang=sygus2
 (set-logic LIA)
 
 (synth-fun f ((x Int) (y Int)) Int
diff --git a/test/regress/regress1/sygus/strings-any-term1.sy b/test/regress/regress1/sygus/strings-any-term1.sy
index cca2edb2c..2c3eaac33 100644
--- a/test/regress/regress1/sygus/strings-any-term1.sy
+++ b/test/regress/regress1/sygus/strings-any-term1.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-si=none --sygus-grammar-cons=any-term
 (set-logic ALL)
 (synth-fun f ((x String) (y String)) Int)
 (declare-var x String)
diff --git a/test/regress/regress1/sygus/tl-type-0.sy b/test/regress/regress1/sygus/tl-type-0.sy
index 0beea8056..3da21f6dc 100644
--- a/test/regress/regress1/sygus/tl-type-0.sy
+++ b/test/regress/regress1/sygus/tl-type-0.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int) (Term Int))
diff --git a/test/regress/regress1/sygus/tl-type-4x.sy b/test/regress/regress1/sygus/tl-type-4x.sy
index 7c4403397..7d6fa778e 100644
--- a/test/regress/regress1/sygus/tl-type-4x.sy
+++ b/test/regress/regress1/sygus/tl-type-4x.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int) (Term Int))
diff --git a/test/regress/regress1/sygus/tl-type.sy b/test/regress/regress1/sygus/tl-type.sy
index fe39ddd8e..8be604b23 100644
--- a/test/regress/regress1/sygus/tl-type.sy
+++ b/test/regress/regress1/sygus/tl-type.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int) (Term Int))
diff --git a/test/regress/regress1/sygus/twolets1.sy b/test/regress/regress1/sygus/twolets1.sy
index b78bf7647..7f3fed923 100644
--- a/test/regress/regress1/sygus/twolets1.sy
+++ b/test/regress/regress1/sygus/twolets1.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
 (set-logic LIA)
 
 ;; f1 is x plus 2 ;; f2 is 2x plus 5
diff --git a/test/regress/regress1/sygus/twolets2-orig.sy b/test/regress/regress1/sygus/twolets2-orig.sy
index ca1e512a1..16b3e27aa 100644
--- a/test/regress/regress1/sygus/twolets2-orig.sy
+++ b/test/regress/regress1/sygus/twolets2-orig.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
 (set-logic LIA)
 (define-fun letf ((x Int) (y Int) (z Int)) Int (+ (+ y x) z))
 (synth-fun f1 ((x Int)) Int
diff --git a/test/regress/regress2/quantifiers/small-bug1-fixpoint-3.smt2 b/test/regress/regress2/quantifiers/small-bug1-fixpoint-3.smt2
index c26cde173..72743693a 100644
--- a/test/regress/regress2/quantifiers/small-bug1-fixpoint-3.smt2
+++ b/test/regress/regress2/quantifiers/small-bug1-fixpoint-3.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-all --no-check-models
+; COMMAND-LINE: --cegqi-all --no-check-models
 ; EXPECT: sat
 ;AJR:BROKEN
 (set-logic UFBV)
diff --git a/test/regress/regress2/sygus/lustre-real.sy b/test/regress/regress2/sygus/lustre-real.sy
index 99d682bcc..b7637567f 100644
--- a/test/regress/regress2/sygus/lustre-real.sy
+++ b/test/regress/regress2/sygus/lustre-real.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status
 (set-logic LIRA)
 (define-fun
 __node_init_top_0 (
diff --git a/test/regress/regress2/sygus/process-10-vars-2fun.sy b/test/regress/regress2/sygus/process-10-vars-2fun.sy
index fe6f5cd0c..00a0099b0 100644
--- a/test/regress/regress2/sygus/process-10-vars-2fun.sy
+++ b/test/regress/regress2/sygus/process-10-vars-2fun.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --no-sygus-repair-const --sygus-arg-relevant
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --no-sygus-repair-const --sygus-arg-relevant
 ; EXPECT: unsat
 (set-logic LIA)
 
diff --git a/test/regress/regress2/sygus/process-arg-invariance.sy b/test/regress/regress2/sygus/process-arg-invariance.sy
index a50cec2d8..15bffb073 100644
--- a/test/regress/regress2/sygus/process-arg-invariance.sy
+++ b/test/regress/regress2/sygus/process-arg-invariance.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --no-sygus-add-const-grammar --sygus-arg-relevant
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --no-sygus-add-const-grammar --sygus-arg-relevant
 ; EXPECT: unsat
 (set-logic LIA)
 
diff --git a/test/regress/regress2/sygus/real-grammar-neg.sy b/test/regress/regress2/sygus/real-grammar-neg.sy
index 0891e57bf..d9a66bcce 100644
--- a/test/regress/regress2/sygus/real-grammar-neg.sy
+++ b/test/regress/regress2/sygus/real-grammar-neg.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-si=none --no-sygus-pbe
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none --no-sygus-pbe
 
 (set-logic LRA)
 
diff --git a/test/regress/regress3/strings-any-term.sy b/test/regress/regress3/strings-any-term.sy
index 3827585ec..b84252d6c 100644
--- a/test/regress/regress3/strings-any-term.sy
+++ b/test/regress/regress3/strings-any-term.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term --sygus-active-gen=none
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-si=none --sygus-grammar-cons=any-term --sygus-active-gen=none
 (set-logic ALL)
 (synth-fun f ((x String) (y String)) Int)
 (declare-var x String)
diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.h b/test/unit/theory/theory_quantifiers_bv_inverter_white.h
index 03fcaab69..74041295d 100644
--- a/test/unit/theory/theory_quantifiers_bv_inverter_white.h
+++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.h
@@ -223,7 +223,7 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
     d_smt = new SmtEngine(d_em);
-    d_smt->setOption("cbqi-full", CVC4::SExpr(true));
+    d_smt->setOption("cegqi-full", CVC4::SExpr(true));
     d_smt->setOption("produce-models", CVC4::SExpr(true));
     d_scope = new SmtScope(d_smt);