diff options
Diffstat (limited to 'test/regress/regress0/ho')
33 files changed, 33 insertions, 67 deletions
diff --git a/test/regress/regress0/ho/apply-collapse-sat.smt2 b/test/regress/regress0/ho/apply-collapse-sat.smt2 index 74a9df660..64aaa797d 100644 --- a/test/regress/regress0/ho/apply-collapse-sat.smt2 +++ b/test/regress/regress0/ho/apply-collapse-sat.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic UF) +(set-logic HO_UF) (set-info :status sat) (declare-sort U 0) (declare-fun f (U U) U) diff --git a/test/regress/regress0/ho/apply-collapse-unsat.smt2 b/test/regress/regress0/ho/apply-collapse-unsat.smt2 index 101de9081..45eeb23a7 100644 --- a/test/regress/regress0/ho/apply-collapse-unsat.smt2 +++ b/test/regress/regress0/ho/apply-collapse-unsat.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic UF) +(set-logic HO_UF) (set-info :status unsat) (declare-sort U 0) (declare-fun f (U U) U) diff --git a/test/regress/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p b/test/regress/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p index 0ed7fe44b..c4b517e56 100644 --- a/test/regress/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p +++ b/test/regress/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p @@ -1,4 +1,3 @@ -% COMMAND-LINE: --uf-ho % EXPECT: % SZS status Unsatisfiable for bug_nodbuilding_interpreted_SYO042^1 %------------------------------------------------------------------------------ diff --git a/test/regress/regress0/ho/cong-full-apply.smt2 b/test/regress/regress0/ho/cong-full-apply.smt2 index 0ff147b97..493bbf140 100644 --- a/test/regress/regress0/ho/cong-full-apply.smt2 +++ b/test/regress/regress0/ho/cong-full-apply.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic UFLIA) +(set-logic HO_UFLIA) (set-info :status unsat) (declare-fun f (Int) Int) (declare-fun g (Int) Int) diff --git a/test/regress/regress0/ho/cong.smt2 b/test/regress/regress0/ho/cong.smt2 index 531356568..b1feafe3e 100644 --- a/test/regress/regress0/ho/cong.smt2 +++ b/test/regress/regress0/ho/cong.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic UF) +(set-logic HO_UF) (set-info :status unsat) (declare-sort U 0) (declare-fun f (U) U) diff --git a/test/regress/regress0/ho/declare-fun-variants.smt2 b/test/regress/regress0/ho/declare-fun-variants.smt2 index 990423fb3..de37f7044 100644 --- a/test/regress/regress0/ho/declare-fun-variants.smt2 +++ b/test/regress/regress0/ho/declare-fun-variants.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status sat) (declare-fun f (Int Int) Int) (declare-fun g (Int) (-> Int Int)) diff --git a/test/regress/regress0/ho/def-fun-flatten.smt2 b/test/regress/regress0/ho/def-fun-flatten.smt2 index af33098f5..81af169a7 100644 --- a/test/regress/regress0/ho/def-fun-flatten.smt2 +++ b/test/regress/regress0/ho/def-fun-flatten.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status unsat) (declare-fun f (Int Int) Int) (define-fun g ((x Int)) (-> Int Int) (f x)) diff --git a/test/regress/regress0/ho/ext-finite-unsat.smt2 b/test/regress/regress0/ho/ext-finite-unsat.smt2 index 1719d5ad1..282cc3bda 100644 --- a/test/regress/regress0/ho/ext-finite-unsat.smt2 +++ b/test/regress/regress0/ho/ext-finite-unsat.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic UF) +(set-logic HO_UF) (set-info :status unsat) (declare-sort U 0) (declare-fun f (U) U) diff --git a/test/regress/regress0/ho/ext-ho-nested-lambda-model.smt2 b/test/regress/regress0/ho/ext-ho-nested-lambda-model.smt2 index 7031829d4..175ced858 100644 --- a/test/regress/regress0/ho/ext-ho-nested-lambda-model.smt2 +++ b/test/regress/regress0/ho/ext-ho-nested-lambda-model.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status sat) (declare-sort U 0) (declare-fun f ((-> U U)) U) diff --git a/test/regress/regress0/ho/ext-ho.smt2 b/test/regress/regress0/ho/ext-ho.smt2 index 02e51654e..613533ebd 100644 --- a/test/regress/regress0/ho/ext-ho.smt2 +++ b/test/regress/regress0/ho/ext-ho.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status sat) (declare-sort U 0) (declare-fun f ((-> U U)) U) diff --git a/test/regress/regress0/ho/ext-sat-partial-eval.smt2 b/test/regress/regress0/ho/ext-sat-partial-eval.smt2 index f3392f1ba..cc63c52ea 100644 --- a/test/regress/regress0/ho/ext-sat-partial-eval.smt2 +++ b/test/regress/regress0/ho/ext-sat-partial-eval.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic UF) +(set-logic HO_UF) (set-info :status sat) (declare-sort U 0) (declare-fun f (U U) U) diff --git a/test/regress/regress0/ho/ext-sat.smt2 b/test/regress/regress0/ho/ext-sat.smt2 index 772b6eaa0..f91fb8240 100644 --- a/test/regress/regress0/ho/ext-sat.smt2 +++ b/test/regress/regress0/ho/ext-sat.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic UF) +(set-logic HO_UF) (set-info :status sat) (declare-sort U 0) (declare-fun f (U U) U) diff --git a/test/regress/regress0/ho/finite-fun-ext.smt2 b/test/regress/regress0/ho/finite-fun-ext.smt2 index 005a2109a..63e25cb03 100644 --- a/test/regress/regress0/ho/finite-fun-ext.smt2 +++ b/test/regress/regress0/ho/finite-fun-ext.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (declare-datatype Unit ((unit))) diff --git a/test/regress/regress0/ho/fta0144-alpha-eq.smt2 b/test/regress/regress0/ho/fta0144-alpha-eq.smt2 index 0fc536bd9..747bfd48e 100644 --- a/test/regress/regress0/ho/fta0144-alpha-eq.smt2 +++ b/test/regress/regress0/ho/fta0144-alpha-eq.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (declare-sort Nat$ 0) (declare-sort Complex$ 0) (declare-sort Real_set$ 0) diff --git a/test/regress/regress0/ho/fta0210.smt2 b/test/regress/regress0/ho/fta0210.smt2 index 9f0a39f25..864bb9859 100644 --- a/test/regress/regress0/ho/fta0210.smt2 +++ b/test/regress/regress0/ho/fta0210.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (declare-sort A$ 0) (declare-sort Nat$ 0) (declare-sort A_poly$ 0) diff --git a/test/regress/regress0/ho/fun-subtyping.smt2 b/test/regress/regress0/ho/fun-subtyping.smt2 index 8eae3d073..e7cc01772 100644 --- a/test/regress/regress0/ho/fun-subtyping.smt2 +++ b/test/regress/regress0/ho/fun-subtyping.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic ALL) +(set-logic HO_ALL) (declare-fun g (Int) Real) (declare-fun h (Int) Real) (assert (not (= g h))) diff --git a/test/regress/regress0/ho/ho-exponential-model.smt2 b/test/regress/regress0/ho/ho-exponential-model.smt2 index 3f0011828..964a45f77 100644 --- a/test/regress/regress0/ho/ho-exponential-model.smt2 +++ b/test/regress/regress0/ho/ho-exponential-model.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic UFLIA) +(set-logic HO_UFLIA) (set-info :status sat) (declare-fun f1 (Int Int Int Int) Int) (declare-fun f2 (Int Int Int) Int) diff --git a/test/regress/regress0/ho/ho-match-fun-suffix.smt2 b/test/regress/regress0/ho/ho-match-fun-suffix.smt2 index 1e4ad243c..4418b156f 100644 --- a/test/regress/regress0/ho/ho-match-fun-suffix.smt2 +++ b/test/regress/regress0/ho/ho-match-fun-suffix.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status unsat) (declare-fun f (Int Int) Int) (declare-fun a () Int) diff --git a/test/regress/regress0/ho/ho-matching-enum-2.smt2 b/test/regress/regress0/ho/ho-matching-enum-2.smt2 index 9581e4c4f..e73afdce2 100644 --- a/test/regress/regress0/ho/ho-matching-enum-2.smt2 +++ b/test/regress/regress0/ho/ho-matching-enum-2.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status unsat) (declare-sort U 0) diff --git a/test/regress/regress0/ho/ho-matching-enum.smt2 b/test/regress/regress0/ho/ho-matching-enum.smt2 index bd1d2837f..df3a920ec 100644 --- a/test/regress/regress0/ho/ho-matching-enum.smt2 +++ b/test/regress/regress0/ho/ho-matching-enum.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status unsat) (declare-sort U 0) diff --git a/test/regress/regress0/ho/ho-matching-nested-app.smt2 b/test/regress/regress0/ho/ho-matching-nested-app.smt2 index d6de559e6..506cd55cf 100644 --- a/test/regress/regress0/ho/ho-matching-nested-app.smt2 +++ b/test/regress/regress0/ho/ho-matching-nested-app.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status unsat) (declare-sort U 0) diff --git a/test/regress/regress0/ho/ho-std-fmf.smt2 b/test/regress/regress0/ho/ho-std-fmf.smt2 index 61d82d00c..1b23fdb6f 100644 --- a/test/regress/regress0/ho/ho-std-fmf.smt2 +++ b/test/regress/regress0/ho/ho-std-fmf.smt2 @@ -1,6 +1,6 @@ -; COMMAND-LINE: --uf-ho --finite-model-find +; COMMAND-LINE: --finite-model-find ; EXPECT: sat -(set-logic UF) +(set-logic HO_UF) (set-info :status sat) (declare-sort U 0) (declare-fun P (U U) Bool) diff --git a/test/regress/regress0/ho/hoa0008.smt2 b/test/regress/regress0/ho/hoa0008.smt2 index f4833aadf..b43920c21 100644 --- a/test/regress/regress0/ho/hoa0008.smt2 +++ b/test/regress/regress0/ho/hoa0008.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (declare-sort A$ 0) (declare-sort Com$ 0) (declare-sort Loc$ 0) diff --git a/test/regress/regress0/ho/issue4990-care-graph.smt2 b/test/regress/regress0/ho/issue4990-care-graph.smt2 index 6c44a94a8..93c87d3c9 100644 --- a/test/regress/regress0/ho/issue4990-care-graph.smt2 +++ b/test/regress/regress0/ho/issue4990-care-graph.smt2 @@ -1,7 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic QF_AUFBVLIA) -(set-option :uf-ho true) +(set-logic HO_QF_AUFBVLIA) (declare-fun a () Int) (declare-fun b () Int) (declare-fun c (Int) Int) diff --git a/test/regress/regress0/ho/issue5233-part1-usort-owner.smt2 b/test/regress/regress0/ho/issue5233-part1-usort-owner.smt2 index e97b914a2..9091cf8bd 100644 --- a/test/regress/regress0/ho/issue5233-part1-usort-owner.smt2 +++ b/test/regress/regress0/ho/issue5233-part1-usort-owner.smt2 @@ -1,7 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic QF_AUFBVLIA) -(set-option :uf-ho true) +(set-logic HO_QF_AUFBVLIA) (declare-fun a (Int) Int) (declare-fun b (Int) Int) (assert (distinct a b)) diff --git a/test/regress/regress0/ho/ite-apply-eq.smt2 b/test/regress/regress0/ho/ite-apply-eq.smt2 index 474f6887e..2e21d3081 100644 --- a/test/regress/regress0/ho/ite-apply-eq.smt2 +++ b/test/regress/regress0/ho/ite-apply-eq.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic UFLIA) +(set-logic HO_UFLIA) (set-info :status sat) (declare-fun x () Int) (declare-fun f (Int) Int) diff --git a/test/regress/regress0/ho/lambda-equality-non-canon.smt2 b/test/regress/regress0/ho/lambda-equality-non-canon.smt2 index 80f3db417..61753d90a 100644 --- a/test/regress/regress0/ho/lambda-equality-non-canon.smt2 +++ b/test/regress/regress0/ho/lambda-equality-non-canon.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: sat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status sat) (declare-fun f (Int) Int) diff --git a/test/regress/regress0/ho/match-middle.smt2 b/test/regress/regress0/ho/match-middle.smt2 index 0485f9a6f..225faa1a5 100644 --- a/test/regress/regress0/ho/match-middle.smt2 +++ b/test/regress/regress0/ho/match-middle.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic UFLIA) +(set-logic HO_UFLIA) (set-info :status unsat) (declare-fun f (Int Int Int) Int) (declare-fun h (Int Int Int) Int) diff --git a/test/regress/regress0/ho/modulo-func-equality.smt2 b/test/regress/regress0/ho/modulo-func-equality.smt2 index 8e300ac72..984835be7 100644 --- a/test/regress/regress0/ho/modulo-func-equality.smt2 +++ b/test/regress/regress0/ho/modulo-func-equality.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic UFLIA) +(set-logic HO_UFLIA) (set-info :status unsat) (declare-fun P (Int) Bool) (declare-fun Q (Int) Bool) diff --git a/test/regress/regress0/ho/shadowing-defs.smt2 b/test/regress/regress0/ho/shadowing-defs.smt2 index 722e970b6..fb5ac3ec6 100644 --- a/test/regress/regress0/ho/shadowing-defs.smt2 +++ b/test/regress/regress0/ho/shadowing-defs.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unknown -(set-logic ALL) +(set-logic HO_ALL) (declare-sort $$unsorted 0) (declare-sort mu 0) diff --git a/test/regress/regress0/ho/simple-matching-partial.smt2 b/test/regress/regress0/ho/simple-matching-partial.smt2 index 41b2a0bca..18c578367 100644 --- a/test/regress/regress0/ho/simple-matching-partial.smt2 +++ b/test/regress/regress0/ho/simple-matching-partial.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status unsat) (declare-sort U 0) (declare-fun f (U U) U) diff --git a/test/regress/regress0/ho/simple-matching.smt2 b/test/regress/regress0/ho/simple-matching.smt2 index 8e2315b2f..cbd70f072 100644 --- a/test/regress/regress0/ho/simple-matching.smt2 +++ b/test/regress/regress0/ho/simple-matching.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status unsat) (declare-sort U 0) (declare-fun f (U) U) diff --git a/test/regress/regress0/ho/trans.smt2 b/test/regress/regress0/ho/trans.smt2 index 088abbab1..b33644db3 100644 --- a/test/regress/regress0/ho/trans.smt2 +++ b/test/regress/regress0/ho/trans.smt2 @@ -1,6 +1,5 @@ -; COMMAND-LINE: --uf-ho ; EXPECT: unsat -(set-logic UF) +(set-logic HO_UF) (set-info :status unsat) (declare-sort U 0) (declare-fun f (U) U) |