summaryrefslogtreecommitdiff
path: root/test/regress/regress1/ho
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress1/ho')
-rw-r--r--test/regress/regress1/ho/NUM638^1.smt24
-rw-r--r--test/regress/regress1/ho/NUM925^1.p2
-rw-r--r--test/regress/regress1/ho/SYO056^1.p2
-rw-r--r--test/regress/regress1/ho/bound_var_bug.p1
-rw-r--r--test/regress/regress1/ho/bug_freeVar_BDD_General_data_270.p2
-rw-r--r--test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt24
-rw-r--r--test/regress/regress1/ho/fta0328.lfho.p2
-rw-r--r--test/regress/regress1/ho/hoa0102.smt24
-rw-r--r--test/regress/regress1/ho/issue3136-fconst-bool-bool.smt24
-rw-r--r--test/regress/regress1/ho/issue4065-no-rep.smt23
-rw-r--r--test/regress/regress1/ho/issue4092-sinf.smt213
-rw-r--r--test/regress/regress1/ho/issue4134-sinf.smt25
-rw-r--r--test/regress/regress1/ho/nested_lambdas-AGT034^2.smt24
-rw-r--r--test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt25
-rw-r--r--test/regress/regress1/ho/soundness_fmf_SYO362^5-delta.p2
-rw-r--r--test/regress/regress1/ho/store-ax-min.p4
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)).
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback