diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-20 19:47:35 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-20 19:47:35 -0500 |
commit | ad7907adff119a6e25fe3c229663afecb15db7c4 (patch) | |
tree | 0cf0c1931db8d4529127806eca03cd014fcb6a42 /test/regress/regress0 | |
parent | 6255c0356bd78140a9cf075491c1d4608ac27704 (diff) |
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.
Diffstat (limited to 'test/regress/regress0')
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) |