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.

61 files changed, 61 insertions, 61 deletions

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