diff options
Diffstat (limited to 'test/regress/regress1/ho')
-rw-r--r-- | test/regress/regress1/ho/NUM638^1.smt2 | 4 | ||||
-rw-r--r-- | test/regress/regress1/ho/NUM925^1.p | 2 | ||||
-rw-r--r-- | test/regress/regress1/ho/SYO056^1.p | 2 | ||||
-rw-r--r-- | test/regress/regress1/ho/bound_var_bug.p | 1 | ||||
-rw-r--r-- | test/regress/regress1/ho/bug_freeVar_BDD_General_data_270.p | 2 | ||||
-rw-r--r-- | test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 | 4 | ||||
-rw-r--r-- | test/regress/regress1/ho/fta0328.lfho.p | 2 | ||||
-rw-r--r-- | test/regress/regress1/ho/hoa0102.smt2 | 4 | ||||
-rw-r--r-- | test/regress/regress1/ho/issue3136-fconst-bool-bool.smt2 | 4 | ||||
-rw-r--r-- | test/regress/regress1/ho/issue4065-no-rep.smt2 | 3 | ||||
-rw-r--r-- | test/regress/regress1/ho/issue4092-sinf.smt2 | 13 | ||||
-rw-r--r-- | test/regress/regress1/ho/issue4134-sinf.smt2 | 5 | ||||
-rw-r--r-- | test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 | 4 | ||||
-rw-r--r-- | test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 | 5 | ||||
-rw-r--r-- | test/regress/regress1/ho/soundness_fmf_SYO362^5-delta.p | 2 | ||||
-rw-r--r-- | test/regress/regress1/ho/store-ax-min.p | 4 |
16 files changed, 28 insertions, 33 deletions
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)). |