diff options
Diffstat (limited to 'test/regress/regress2/ho')
| -rw-r--r-- | test/regress/regress2/ho/auth0068.smt2 | 3 | ||||
| -rw-r--r-- | test/regress/regress2/ho/bug_instfalse_SEU882^5.p | 2 | ||||
| -rw-r--r-- | test/regress/regress2/ho/fta0409.smt2 | 3 | ||||
| -rw-r--r-- | test/regress/regress2/ho/involved_parsing_ALG248^3.p | 2 | ||||
| -rw-r--r-- | test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p | 2 |
5 files changed, 5 insertions, 7 deletions
diff --git a/test/regress/regress2/ho/auth0068.smt2 b/test/regress/regress2/ho/auth0068.smt2 index eb0bb5d36..fc788a15c 100644 --- a/test/regress/regress2/ho/auth0068.smt2 +++ b/test/regress/regress2/ho/auth0068.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status unsat) (declare-sort Msg$ 0) (declare-sort Nat$ 0) diff --git a/test/regress/regress2/ho/bug_instfalse_SEU882^5.p b/test/regress/regress2/ho/bug_instfalse_SEU882^5.p index a62a2080a..bf58b95d8 100644 --- a/test/regress/regress2/ho/bug_instfalse_SEU882^5.p +++ b/test/regress/regress2/ho/bug_instfalse_SEU882^5.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim +% COMMAND-LINE: --full-saturate-quant --ho-elim % EXPECT: % SZS status Theorem for bug_instfalse_SEU882^5 %------------------------------------------------------------------------------ diff --git a/test/regress/regress2/ho/fta0409.smt2 b/test/regress/regress2/ho/fta0409.smt2 index 51ac5f2da..5516c804a 100644 --- a/test/regress/regress2/ho/fta0409.smt2 +++ b/test/regress/regress2/ho/fta0409.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status unsat) (declare-sort Nat$ 0) (declare-sort Complex$ 0) diff --git a/test/regress/regress2/ho/involved_parsing_ALG248^3.p b/test/regress/regress2/ho/involved_parsing_ALG248^3.p index d0577dd1f..47a89143d 100644 --- a/test/regress/regress2/ho/involved_parsing_ALG248^3.p +++ b/test/regress/regress2/ho/involved_parsing_ALG248^3.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --uf-ho --ho-elim +% COMMAND-LINE: --ho-elim % EXPECT: % SZS status Theorem for involved_parsing_ALG248^3 %------------------------------------------------------------------------------ diff --git a/test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p b/test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p index 37c7a02e8..5f87519d1 100644 --- a/test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p +++ b/test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim +% COMMAND-LINE: --full-saturate-quant --ho-elim % EXPECT: % SZS status Theorem for partial_app_interpreted_SWW474^2 %------------------------------------------------------------------------------ |