diff options
Diffstat (limited to 'test/regress')
70 files changed, 104 insertions, 151 deletions
diff --git a/test/regress/regress0/declare-fun-is-match.smt2 b/test/regress/regress0/declare-fun-is-match.smt2 index f3877edca..0b69011c8 100644 --- a/test/regress/regress0/declare-fun-is-match.smt2 +++ b/test/regress/regress0/declare-fun-is-match.smt2 @@ -1,7 +1,6 @@ ; EXPECT: sat -; COMMAND-LINE: --uf-ho (set-info :smt-lib-version 2.6) -(set-logic UFIDL) +(set-logic HO_UFIDL) (set-info :status sat) (declare-fun match (Int Int) Int) (declare-fun is (Int Int) Int) diff --git a/test/regress/regress0/fp/issue4277-assign-func.smt2 b/test/regress/regress0/fp/issue4277-assign-func.smt2 index 6a516a3ca..c42bad235 100644 --- a/test/regress/regress0/fp/issue4277-assign-func.smt2 +++ b/test/regress/regress0/fp/issue4277-assign-func.smt2 @@ -1,8 +1,7 @@ ; COMMAND-LINE: -q ; EXPECT: sat ; REQUIRES: symfpu -(set-logic ALL) -(set-option :uf-ho true) +(set-logic HO_ALL) (set-option :assign-function-values false) (set-info :status sat) (declare-fun b () (_ BitVec 1)) 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) diff --git a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy index 848ae0349..6a149cc71 100644 --- a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy +++ b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy @@ -1,16 +1,16 @@ ; REQUIRES: no-competition ; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2 ; EXPECT-ERROR: (error "Parse Error: pLTL-sygus-syntax-err.sy:80.19: number of arguments does not match the constructor type -; EXPECT-ERROR: +; EXPECT-ERROR: ; EXPECT-ERROR: (Op2 <O2> <F>) ; EXPECT-ERROR: ^ ; EXPECT-ERROR: ") ; EXIT: 1 -(set-logic ALL) +(set-logic HO_ALL) (set-option :lang sygus2) ;(set-option :sygus-out status) (set-option :sygus-rec-fun true) -(set-option :uf-ho true) + (define-sort Time () Int) @@ -47,19 +47,19 @@ (and (<= 0 t tn) (match f ( ((P i) (val t i)) - - ((Op1 op g) + + ((Op1 op g) (match op ( - (NOT (not (holds g t))) + (NOT (not (holds g t))) - (Y (and (< 0 t) (holds g (- t 1)))) + (Y (and (< 0 t) (holds g (- t 1)))) (G (and (holds g t) (or (= t tn) (holds f (+ t 1))))) (H (and (holds g t) (or (= t 0) (holds f (- t 1))))) ))) - ((Op2 op f g) + ((Op2 op f g) (match op ( (AND (and (holds f t) (holds g t))) @@ -88,6 +88,3 @@ (constraint (holds (Op1 G (phi X0 X1)) 0)) (check-synth) - - - diff --git a/test/regress/regress0/sygus/sygus-uf.sy b/test/regress/regress0/sygus/sygus-uf.sy index b08aa8929..2f59598ec 100644 --- a/test/regress/regress0/sygus/sygus-uf.sy +++ b/test/regress/regress0/sygus/sygus-uf.sy @@ -1,6 +1,6 @@ -; COMMAND-LINE: --lang=sygus2 --sygus-out=status --uf-ho +; COMMAND-LINE: --lang=sygus2 --sygus-out=status ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (declare-var uf (-> Int Int)) diff --git a/test/regress/regress1/fmf/issue4225-univ-fun.smt2 b/test/regress/regress1/fmf/issue4225-univ-fun.smt2 index 9946a4567..af1f1e1a6 100644 --- a/test/regress/regress1/fmf/issue4225-univ-fun.smt2 +++ b/test/regress/regress1/fmf/issue4225-univ-fun.smt2 @@ -1,6 +1,6 @@ -; COMMAND-LINE: --finite-model-find --uf-ho +; COMMAND-LINE: --finite-model-find ; EXPECT: unknown -(set-logic ALL) +(set-logic HO_ALL) ; this is not handled by fmf (assert (forall ((a (-> Int Int)) (b Int)) (not (= (a b) 0)))) (check-sat) diff --git a/test/regress/regress1/ho/NUM638^1.smt2 b/test/regress/regress1/ho/NUM638^1.smt2 index 59391ce8c..11683b1a7 100644 --- a/test/regress/regress1/ho/NUM638^1.smt2 +++ b/test/regress/regress1/ho/NUM638^1.smt2 @@ -1,8 +1,8 @@ -; COMMAND-LINE: --uf-ho --finite-model-find +; COMMAND-LINE: --finite-model-find ; EXPECT: unsat (set-option :incremental false) -(set-logic ALL) +(set-logic HO_ALL) (declare-sort $$unsorted 0) (declare-sort nat 0) (declare-fun x () nat) diff --git a/test/regress/regress1/ho/NUM925^1.p b/test/regress/regress1/ho/NUM925^1.p index e162a63a4..e07ad784f 100644 --- a/test/regress/regress1/ho/NUM925^1.p +++ b/test/regress/regress1/ho/NUM925^1.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --uf-ho --ho-elim +% COMMAND-LINE: --ho-elim % EXPECT: % SZS status Theorem for NUM925^1 %------------------------------------------------------------------------------ diff --git a/test/regress/regress1/ho/SYO056^1.p b/test/regress/regress1/ho/SYO056^1.p index a8a6bafca..deda234da 100644 --- a/test/regress/regress1/ho/SYO056^1.p +++ b/test/regress/regress1/ho/SYO056^1.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --uf-ho --finite-model-find +% COMMAND-LINE: --finite-model-find % EXPECT: % SZS status CounterSatisfiable for SYO056^1 %------------------------------------------------------------------------------ diff --git a/test/regress/regress1/ho/bound_var_bug.p b/test/regress/regress1/ho/bound_var_bug.p index 0dc946d6a..23bda7fb2 100644 --- a/test/regress/regress1/ho/bound_var_bug.p +++ b/test/regress/regress1/ho/bound_var_bug.p @@ -1,4 +1,3 @@ -% COMMAND-LINE: --uf-ho % EXPECT: % SZS status GaveUp for bound_var_bug % TIMEFORMAT='%3R'; { time (exec 2>&1; /Users/blanchette/misc/leo --foatp e --atp e="$E_HOME"/eprover --atp epclextract="$E_HOME"/epclextract --proofoutput 1 --timeout 30 /Users/blanchette/hgs/afp_mining/tools/judgment_day_2017/data_afp/leo2-mepo/Call_Arity_SestoftGC_data/prob_308__3244432_1 ) ; } diff --git a/test/regress/regress1/ho/bug_freeVar_BDD_General_data_270.p b/test/regress/regress1/ho/bug_freeVar_BDD_General_data_270.p index 6c35270fd..22c1d1dd1 100644 --- a/test/regress/regress1/ho/bug_freeVar_BDD_General_data_270.p +++ b/test/regress/regress1/ho/bug_freeVar_BDD_General_data_270.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --uf-ho --finite-model-find +% COMMAND-LINE: --finite-model-find % EXPECT: % SZS status Satisfiable for bug_freeVar_BDD_General_data_270 thf(ty_n_t__Nat__Onat, type, diff --git a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 index 21405dfdb..7c9de4c49 100644 --- a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 +++ b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 @@ -1,7 +1,7 @@ -; COMMAND-LINE: --uf-ho --finite-model-find -q --decision=justification-old +; COMMAND-LINE: --finite-model-find -q --decision=justification-old ; EXPECT: sat -(set-logic ALL) +(set-logic HO_ALL) (declare-sort $$unsorted 0) (declare-sort qML_mu 0) (declare-sort qML_i 0) diff --git a/test/regress/regress1/ho/fta0328.lfho.p b/test/regress/regress1/ho/fta0328.lfho.p index c33b43ca5..f67c6db58 100644 --- a/test/regress/regress1/ho/fta0328.lfho.p +++ b/test/regress/regress1/ho/fta0328.lfho.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --uf-ho --uf-ho --finite-model-find +% COMMAND-LINE: --finite-model-find % EXPECT: % SZS status CounterSatisfiable for fta0328.lfho % TIMEFORMAT='%3R'; { time (exec 2>&1; /Users/blanchette/.isabelle/contrib/e-2.0-2/x86_64-darwin/eprover --auto-schedule --tstp-in --tstp-out --silent --cpu-limit=2 --proof-object=1 /Users/blanchette/hgs/matryoshka/papers/2019-TACAS-ehoh/eval/judgment_day/judgment_day_lifting_32/fta/prob_804__4064966_1 ) ; } diff --git a/test/regress/regress1/ho/hoa0102.smt2 b/test/regress/regress1/ho/hoa0102.smt2 index 6be063783..c5840e6a9 100644 --- a/test/regress/regress1/ho/hoa0102.smt2 +++ b/test/regress/regress1/ho/hoa0102.smt2 @@ -1,6 +1,6 @@ -; COMMAND-LINE: --uf-ho --full-saturate-quant +; COMMAND-LINE: --full-saturate-quant ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (set-info :status unsat) (declare-sort Com$ 0) (declare-sort Glb$ 0) diff --git a/test/regress/regress1/ho/issue3136-fconst-bool-bool.smt2 b/test/regress/regress1/ho/issue3136-fconst-bool-bool.smt2 index d536e51a1..d15095123 100644 --- a/test/regress/regress1/ho/issue3136-fconst-bool-bool.smt2 +++ b/test/regress/regress1/ho/issue3136-fconst-bool-bool.smt2 @@ -1,7 +1,7 @@ -; COMMAND-LINE: --uf-ho --ho-elim +; COMMAND-LINE: --ho-elim ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (declare-sort $$unsorted 0) (declare-sort num 0) (declare-fun agent_THFTYPE_i () $$unsorted) diff --git a/test/regress/regress1/ho/issue4065-no-rep.smt2 b/test/regress/regress1/ho/issue4065-no-rep.smt2 index 9852150d9..a13aa2bae 100644 --- a/test/regress/regress1/ho/issue4065-no-rep.smt2 +++ b/test/regress/regress1/ho/issue4065-no-rep.smt2 @@ -1,7 +1,6 @@ -(set-logic AUFBV) +(set-logic HO_AUFBV) (set-info :status unsat) (set-option :fmf-bound-int true) -(set-option :uf-ho true) (declare-fun _substvar_20_ () Bool) (declare-sort S4 0) (assert (forall ((q15 S4) (q16 (_ BitVec 20)) (q17 (_ BitVec 13))) (xor (= (_ bv0 13) (_ bv0 13) q17 (bvsrem (_ bv0 13) (_ bv0 13)) q17) _substvar_20_ true))) diff --git a/test/regress/regress1/ho/issue4092-sinf.smt2 b/test/regress/regress1/ho/issue4092-sinf.smt2 index d3066c282..83a3e08b9 100644 --- a/test/regress/regress1/ho/issue4092-sinf.smt2 +++ b/test/regress/regress1/ho/issue4092-sinf.smt2 @@ -1,10 +1,9 @@ -; COMMAND-LINE: --uf-ho --sort-inference +; COMMAND-LINE: --sort-inference ; EXPECT: sat -(set-logic ALL) +(set-logic HO_ALL) (set-option :sort-inference true) -(set-option :uf-ho true) (set-info :status sat) -(declare-fun a ( Int ) Int) -(declare-fun b ( Int ) Int) -(assert (and (distinct 0 (b 5)) (distinct a b ))) -(check-sat) +(declare-fun a ( Int ) Int) +(declare-fun b ( Int ) Int) +(assert (and (distinct 0 (b 5)) (distinct a b ))) +(check-sat) diff --git a/test/regress/regress1/ho/issue4134-sinf.smt2 b/test/regress/regress1/ho/issue4134-sinf.smt2 index 60a754aad..0003bc91e 100644 --- a/test/regress/regress1/ho/issue4134-sinf.smt2 +++ b/test/regress/regress1/ho/issue4134-sinf.smt2 @@ -1,7 +1,6 @@ -; COMMAND-LINE: --uf-ho --sort-inference +; COMMAND-LINE: --sort-inference ; EXPECT: sat -(set-logic ALL) -(set-option :uf-ho true) +(set-logic HO_ALL) (set-option :sort-inference true) (set-info :status sat) (declare-fun a () Int) diff --git a/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 b/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 index 313ff68a1..6a8feba5c 100644 --- a/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 +++ b/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 @@ -1,7 +1,7 @@ -; COMMAND-LINE: --uf-ho --no-check-unsat-cores --no-produce-models --ho-elim +; COMMAND-LINE: --no-check-unsat-cores --no-produce-models --ho-elim ; EXPECT: unsat -(set-logic ALL) +(set-logic HO_ALL) (declare-sort $$unsorted 0) (declare-sort mu 0) (declare-fun meq_ind (mu mu $$unsorted) Bool) diff --git a/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 b/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 index 6743e00d4..3f02e56fd 100644 --- a/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 +++ b/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 @@ -1,8 +1,7 @@ -; COMMAND-LINE: --uf-ho --finite-model-find --no-check-models +; COMMAND-LINE: --finite-model-find --no-check-models ; EXPECT: sat - -(set-logic ALL) +(set-logic HO_ALL) (declare-sort $$unsorted 0) (declare-fun mvalid ((-> $$unsorted Bool)) Bool) diff --git a/test/regress/regress1/ho/soundness_fmf_SYO362^5-delta.p b/test/regress/regress1/ho/soundness_fmf_SYO362^5-delta.p index baabd675a..4068cc42e 100644 --- a/test/regress/regress1/ho/soundness_fmf_SYO362^5-delta.p +++ b/test/regress/regress1/ho/soundness_fmf_SYO362^5-delta.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --uf-ho --finite-model-find +% COMMAND-LINE: --finite-model-find % EXPECT: % SZS status GaveUp for soundness_fmf_SYO362^5-delta %------------------------------------------------------------------------------ diff --git a/test/regress/regress1/ho/store-ax-min.p b/test/regress/regress1/ho/store-ax-min.p index d67eb8dad..d000a17d0 100644 --- a/test/regress/regress1/ho/store-ax-min.p +++ b/test/regress/regress1/ho/store-ax-min.p @@ -1,5 +1,5 @@ -% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim-store-ax -% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim +% COMMAND-LINE: --full-saturate-quant --ho-elim-store-ax +% COMMAND-LINE: --full-saturate-quant --ho-elim % EXPECT: % SZS status Theorem for store-ax-min thf(a, type, (a: $i)). diff --git a/test/regress/regress1/quantifiers/issue3724-quant.smt2 b/test/regress/regress1/quantifiers/issue3724-quant.smt2 index 6dd874fbf..32e82a8b5 100644 --- a/test/regress/regress1/quantifiers/issue3724-quant.smt2 +++ b/test/regress/regress1/quantifiers/issue3724-quant.smt2 @@ -1,6 +1,6 @@ -; COMMAND-LINE: --uf-ho +; COMMAND-LINE: ; EXPECT: unknown -(set-logic ALL) +(set-logic HO_ALL) (assert (forall ((BOUND_VARIABLE_313 Bool) (BOUND_VARIABLE_314 (-> Int Bool)) (BOUND_VARIABLE_315 (-> Int Int)) (BOUND_VARIABLE_316 Int) (BOUND_VARIABLE_317 (-> Int Bool)) (BOUND_VARIABLE_318 Int)) (! (not (and (not (and (= (ite (and (not (= BOUND_VARIABLE_318 0)) (BOUND_VARIABLE_314 (BOUND_VARIABLE_315 (ite (not (BOUND_VARIABLE_314 0)) 0 (ite BOUND_VARIABLE_313 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (BOUND_VARIABLE_314 0)) 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (or (not BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 (ite (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 9)))))))) (ite (BOUND_VARIABLE_317 (BOUND_VARIABLE_315 (ite (not (BOUND_VARIABLE_314 0)) 0 (ite BOUND_VARIABLE_313 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (BOUND_VARIABLE_314 0)) 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (or (not BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 (ite (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 9))))))) BOUND_VARIABLE_316 0) 0) 0) (not (BOUND_VARIABLE_314 (BOUND_VARIABLE_315 (ite (not (BOUND_VARIABLE_314 0)) 0 (ite BOUND_VARIABLE_313 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (BOUND_VARIABLE_314 0)) 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (or (not BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 (ite (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 9)))))))))) true)) :pattern (true))) ) diff --git a/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2 b/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2 index 03bbd9469..9cb5cdac3 100644 --- a/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2 +++ b/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2 @@ -1,9 +1,9 @@ -(set-logic ALL) +; COMMAND-LINE: +(set-logic HO_ALL) (set-option :ag-miniscope-quant true) (set-option :conjecture-gen true) (set-option :int-wf-ind true) (set-option :sygus-inference true) -(set-option :uf-ho true) (set-info :status unsat) (declare-fun a () Real) (declare-fun b () Real) diff --git a/test/regress/regress1/sygus/eval-uc.sy b/test/regress/regress1/sygus/eval-uc.sy index e2bf9d144..e007eec51 100644 --- a/test/regress/regress1/sygus/eval-uc.sy +++ b/test/regress/regress1/sygus/eval-uc.sy @@ -1,6 +1,6 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status --uf-ho -(set-logic ALL) +; COMMAND-LINE: --lang=sygus2 --sygus-out=status +(set-logic HO_ALL) (declare-sort S 0) (declare-var f Bool) (declare-var u (-> S Bool)) @@ -9,7 +9,7 @@ (define-fun init ((f Bool) (u (-> S Bool))) Bool (and f (forall ((x S)) (not (u x))))) (define-fun trans ((f Bool) (u (-> S Bool)) (new_f Bool) (new_u (-> S Bool))) Bool (and (not new_f) (exists ((x S)) (forall ((y S)) (= (new_u y) (or (u y) (= y x))))))) ;(define-fun trans ((f Bool) (u (-> S Bool)) (new_f Bool) (new_u (-> S Bool))) Bool (and new_f (exists ((x S)) (forall ((y S)) (= (new_u y) (or (u y) (= y x))))))) -(synth-fun inv_matrix ((f Bool) (u (-> S Bool)) (x S)) Bool ((Start Bool)) ((Start Bool ( (or (not +(synth-fun inv_matrix ((f Bool) (u (-> S Bool)) (x S)) Bool ((Start Bool)) ((Start Bool ( (or (not (u x)) (not f)))))) (define-fun inv ((f Bool) (u (-> S Bool))) Bool (forall ((x S)) (inv_matrix f u x))) (constraint (=> (and (inv f u) (trans f u new_f new_u)) (inv new_f new_u))) diff --git a/test/regress/regress1/sygus/ho-sygus.sy b/test/regress/regress1/sygus/ho-sygus.sy index 893c2034e..d46d8ecde 100644 --- a/test/regress/regress1/sygus/ho-sygus.sy +++ b/test/regress/regress1/sygus/ho-sygus.sy @@ -1,6 +1,6 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status --uf-ho -(set-logic ALL) +; COMMAND-LINE: --lang=sygus2 --sygus-out=status +(set-logic HO_ALL) (synth-fun f ((y (-> Int Int)) (z Int)) Int) (declare-var z (-> Int Int)) (constraint (= (f z 0) (z 1))) diff --git a/test/regress/regress1/sygus/issue3507.smt2 b/test/regress/regress1/sygus/issue3507.smt2 index c8700f37b..1bbcb2984 100644 --- a/test/regress/regress1/sygus/issue3507.smt2 +++ b/test/regress/regress1/sygus/issue3507.smt2 @@ -1,6 +1,6 @@ ; EXPECT: sat -; COMMAND-LINE: --sygus-inference --uf-ho --quiet -(set-logic ALL) +; COMMAND-LINE: --sygus-inference --quiet +(set-logic HO_ALL) (declare-fun f (Int) Bool) (declare-fun g (Int) Bool) (assert (and (distinct f g) (g 0))) diff --git a/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 b/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 index bc882fc8a..711afb2d8 100644 --- a/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 +++ b/test/regress/regress1/sygus/issue3995-fmf-var-op.smt2 @@ -1,6 +1,6 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-inference --fmf-bound --uf-ho -(set-logic ALL) +; COMMAND-LINE: --sygus-inference --fmf-bound +(set-logic HO_ALL) (declare-fun a () (_ BitVec 1)) (assert (bvsgt (bvsmod a a) #b0)) (check-sat) diff --git a/test/regress/regress1/sygus/list_recursor.sy b/test/regress/regress1/sygus/list_recursor.sy index 2e10a0c71..cb1ae2721 100644 --- a/test/regress/regress1/sygus/list_recursor.sy +++ b/test/regress/regress1/sygus/list_recursor.sy @@ -1,23 +1,23 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --lang=sygus2 --uf-ho +; COMMAND-LINE: --sygus-out=status --lang=sygus2 -(set-logic ALL) +(set-logic HO_ALL) (declare-datatype List ((cons (head Int) (tail List)) (nil))) (define-fun-rec List_rec ((x Int) (y (-> Int List Int Int)) (l List)) Int - (ite ((_ is nil) l) x + (ite ((_ is nil) l) x (y (head l) (tail l) (List_rec x y (tail l))))) (synth-fun f () Int ((I Int)) ((I Int (0 1 (+ I I))))) - + (synth-fun g ((x Int) (y List) (z Int)) Int ((I Int) (L List)) ((I Int (x z (+ I I) (head L) 0 1)) (L List (y (tail y))))) - + (constraint (= (List_rec f g (cons 0 (cons 1 nil))) 2)) (constraint (= (List_rec f g (cons 0 (cons 0 nil))) 2)) diff --git a/test/regress/regress1/sygus/sygus-uf-ex.sy b/test/regress/regress1/sygus/sygus-uf-ex.sy index 7e1cd80b3..c74ce79b7 100644 --- a/test/regress/regress1/sygus/sygus-uf-ex.sy +++ b/test/regress/regress1/sygus/sygus-uf-ex.sy @@ -1,6 +1,6 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status --uf-ho -(set-logic ALL) +; COMMAND-LINE: --lang=sygus2 --sygus-out=status +(set-logic HO_ALL) (declare-var uf (-> Int Int)) diff --git a/test/regress/regress1/sygus/uf-abduct.smt2 b/test/regress/regress1/sygus/uf-abduct.smt2 index 690e57290..bfcfe39fd 100644 --- a/test/regress/regress1/sygus/uf-abduct.smt2 +++ b/test/regress/regress1/sygus/uf-abduct.smt2 @@ -1,7 +1,7 @@ -; COMMAND-LINE: --produce-abducts --uf-ho +; COMMAND-LINE: --produce-abducts ; SCRUBBER: grep -v -E '(\(define-fun)' ; EXIT: 0 -(set-logic UFLIA) +(set-logic HO_UFLIA) (declare-fun f (Int) Int) (declare-fun a () Int) (assert (and (<= 0 a) (< a 4))) 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 %------------------------------------------------------------------------------ diff --git a/test/regress/regress3/ho/SYO362^5.p b/test/regress/regress3/ho/SYO362^5.p index b9537fd0e..41fe3d541 100644 --- a/test/regress/regress3/ho/SYO362^5.p +++ b/test/regress/regress3/ho/SYO362^5.p @@ -1,4 +1,4 @@ -% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim --decision=justification-old +% COMMAND-LINE: --full-saturate-quant --ho-elim --decision=justification-old % EXPECT: % SZS status Theorem for SYO362^5 thf(cK,type,( diff --git a/test/regress/regress3/issue4170.smt2 b/test/regress/regress3/issue4170.smt2 index 0dee146c0..25e0c7f8d 100644 --- a/test/regress/regress3/issue4170.smt2 +++ b/test/regress/regress3/issue4170.smt2 @@ -1,6 +1,5 @@ -(set-logic ALL) +(set-logic HO_ALL) (set-option :sygus-inference true) -(set-option :uf-ho true) (set-option :sygus-ext-rew false) (set-info :status sat) (declare-fun a (Int) Int) |