diff options
Diffstat (limited to 'test/regress/regress2')
5 files changed, 5 insertions, 5 deletions
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) |