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.

40 files changed, 42 insertions, 42 deletions

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)