From ad7907adff119a6e25fe3c229663afecb15db7c4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 20 Apr 2020 19:47:35 -0500 Subject: 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. --- test/regress/regress0/expect/scrub.08.sy | 2 +- test/regress/regress0/quantifiers/ari056.smt2 | 2 +- test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 | 2 +- test/regress/regress0/quantifiers/issue4086-infs.smt2 | 4 ++-- test/regress/regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2 | 2 +- test/regress/regress0/quantifiers/mix-complete-strat.smt2 | 2 +- test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 | 2 +- test/regress/regress0/quantifiers/qbv-inequality2.smt2 | 2 +- test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 | 2 +- test/regress/regress0/quantifiers/qbv-simp.smt2 | 2 +- test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2 | 2 +- test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2 | 2 +- test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 | 2 +- test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2 | 2 +- test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2 | 2 +- test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 | 2 +- test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 | 2 +- test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2 | 2 +- test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2 | 2 +- test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 | 2 +- test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2 | 2 +- test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2 | 2 +- test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 | 2 +- test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2 | 2 +- test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 | 2 +- test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2 | 2 +- test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 | 2 +- test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2 | 2 +- test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 | 2 +- test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2 | 2 +- test/regress/regress0/sygus/General_plus10.sy | 2 +- test/regress/regress0/sygus/aig-si.sy | 2 +- test/regress/regress0/sygus/c100.sy | 2 +- test/regress/regress0/sygus/check-generic-red.sy | 2 +- test/regress/regress0/sygus/const-var-test.sy | 2 +- test/regress/regress0/sygus/hd-05-d1-prog-nogrammar.sy | 2 +- test/regress/regress0/sygus/let-ringer.sy | 4 ++-- test/regress/regress0/sygus/let-simp.sy | 2 +- test/regress/regress0/sygus/parity-AIG-d0.sy | 2 +- test/regress/regress0/sygus/pbe-pred-contra.sy | 2 +- test/regress/regress1/bug519.smt2 | 2 +- test/regress/regress1/quantifiers/NUM878.smt2 | 2 +- test/regress/regress1/quantifiers/RNDPRE_4_1-dd-nqe.smt2 | 2 +- test/regress/regress1/quantifiers/anti-sk-simp.smt2 | 2 +- test/regress/regress1/quantifiers/ari118-bv-2occ-x.smt2 | 2 +- test/regress/regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 | 2 +- test/regress/regress1/quantifiers/extract-nproc.smt2 | 2 +- .../quantifiers/intersection-example-onelane.proof-node22337.smt2 | 2 +- test/regress/regress1/quantifiers/issue4243-prereg-inc.smt2 | 2 +- test/regress/regress1/quantifiers/lra-vts-inf.smt2 | 2 +- test/regress/regress1/quantifiers/model_6_1_bv.smt2 | 2 +- .../regress/regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 | 2 +- test/regress/regress1/quantifiers/nl-pow-trick.smt2 | 2 +- test/regress/regress1/quantifiers/nra-interleave-inst.smt2 | 2 +- test/regress/regress1/quantifiers/psyco-107-bv.smt2 | 2 +- test/regress/regress1/quantifiers/qbv-disequality3.smt2 | 2 +- test/regress/regress1/quantifiers/qbv-simple-2vars-vo.smt2 | 2 +- test/regress/regress1/quantifiers/qbv-test-invert-bvashr-0.smt2 | 2 +- test/regress/regress1/quantifiers/qbv-test-invert-bvashr-1.smt2 | 2 +- test/regress/regress1/quantifiers/qbv-test-invert-bvcomp.smt2 | 2 +- test/regress/regress1/quantifiers/qbv-test-invert-bvlshr-1.smt2 | 2 +- test/regress/regress1/quantifiers/qbv-test-invert-bvmul-neq.smt2 | 2 +- test/regress/regress1/quantifiers/qbv-test-invert-bvmul.smt2 | 2 +- test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2 | 2 +- test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2 | 2 +- test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 | 2 +- test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 | 2 +- test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 | 2 +- test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2 | 2 +- test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2 | 2 +- test/regress/regress1/quantifiers/small-pipeline-fixpoint-3.smt2 | 2 +- test/regress/regress1/sygus/Base16_1.sy | 2 +- test/regress/regress1/sygus/array_search_2.sy | 2 +- test/regress/regress1/sygus/array_search_5-Q-easy.sy | 2 +- test/regress/regress1/sygus/array_sum_2_5.sy | 2 +- test/regress/regress1/sygus/clock-inc-tuple.sy | 2 +- test/regress/regress1/sygus/crcy-si-rcons.sy | 2 +- test/regress/regress1/sygus/dt-test-ns.sy | 2 +- test/regress/regress1/sygus/dup-op.sy | 2 +- test/regress/regress1/sygus/enum-test.sy | 2 +- test/regress/regress1/sygus/error1-dt.sy | 2 +- test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy | 2 +- test/regress/regress1/sygus/hd-sdiv.sy | 2 +- test/regress/regress1/sygus/int-any-const.sy | 2 +- test/regress/regress1/sygus/large-const-simp.sy | 2 +- test/regress/regress1/sygus/list-head-x.sy | 2 +- test/regress/regress1/sygus/max.sy | 2 +- test/regress/regress1/sygus/nia-max-square-ns.sy | 2 +- test/regress/regress1/sygus/parity-si-rcons.sy | 2 +- test/regress/regress1/sygus/phone-1-long.sy | 2 +- test/regress/regress1/sygus/process-10-vars.sy | 2 +- test/regress/regress1/sygus/qe.sy | 2 +- test/regress/regress1/sygus/real-any-const.sy | 2 +- test/regress/regress1/sygus/real-grammar.sy | 2 +- test/regress/regress1/sygus/repair-const-rl.sy | 2 +- test/regress/regress1/sygus/strings-any-term1.sy | 2 +- test/regress/regress1/sygus/tl-type-0.sy | 2 +- test/regress/regress1/sygus/tl-type-4x.sy | 2 +- test/regress/regress1/sygus/tl-type.sy | 2 +- test/regress/regress1/sygus/twolets1.sy | 2 +- test/regress/regress1/sygus/twolets2-orig.sy | 2 +- test/regress/regress2/quantifiers/small-bug1-fixpoint-3.smt2 | 2 +- test/regress/regress2/sygus/lustre-real.sy | 2 +- test/regress/regress2/sygus/process-10-vars-2fun.sy | 2 +- test/regress/regress2/sygus/process-arg-invariance.sy | 2 +- test/regress/regress2/sygus/real-grammar-neg.sy | 2 +- test/regress/regress3/strings-any-term.sy | 2 +- 107 files changed, 109 insertions(+), 109 deletions(-) (limited to 'test/regress') 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) -- cgit v1.2.3