more disabling

HanielB · Feb 25, 2024 · e4322b5 · e4322b5
1 parent 06ec29c
commit e4322b5
Show file tree

Hide file tree

Showing 74 changed files with 150 additions and 7 deletions.
diff --git a/test/regress/cli/regress0/auflia/bug336.smt2 b/test/regress/cli/regress0/auflia/bug336.smt2
@@ -1,3 +1,5 @@
+;; introduces arrays Skolem
+; DISABLE-TESTER: alethe
 (set-logic QF_AUFLIA)
 (set-info :source | This is based on an example in Section 6.2 of "A Decision
 Procedure for an Extensional Theory of Arrays" by Stump, Barrett, Dill, and

diff --git a/test/regress/cli/regress0/bug1247.smt2 b/test/regress/cli/regress0/bug1247.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --incremental
 ; EXPECT: unsat
+;; define-const is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_ABV)
 (set-info :status unsat)
 

diff --git a/test/regress/cli/regress0/bug310.cvc.smt2 b/test/regress/cli/regress0/bug310.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-option :incremental false)
 (declare-fun b () Bool)

diff --git a/test/regress/cli/regress0/bug541.smt2 b/test/regress/cli/regress0/bug541.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (declare-datatypes ((Pair 2)) ((par (T1 T2) ((mk-pair (first T1) (second T2))))))
 (assert (= (mk-pair 0.0 0.0) (mk-pair 1.5 2.5)))

diff --git a/test/regress/cli/regress0/datatypes/4482-unc-simp-one.smt2 b/test/regress/cli/regress0/datatypes/4482-unc-simp-one.smt2
@@ -1,3 +1,5 @@
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun a () UnitTuple)

diff --git a/test/regress/cli/regress0/datatypes/canExp-dtPendingMerge.smt2 b/test/regress/cli/regress0/datatypes/canExp-dtPendingMerge.smt2
@@ -1,6 +1,8 @@
 ; COMMAND-LINE: --ee-mode=distributed
 ; COMMAND-LINE: --ee-mode=central
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-datatypes ((T 0)) (((A) (B (proj0B T) (proj1B T)) (C (proj0C T)) (D (proj0D T) ))))

diff --git a/test/regress/cli/regress0/datatypes/cdt-non-canon-stream.smt2 b/test/regress/cli/regress0/datatypes/cdt-non-canon-stream.smt2
@@ -1,3 +1,5 @@
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-codatatypes ((list 0)) (((cons (head Int) (tail list)))))

diff --git a/test/regress/cli/regress0/datatypes/datatype0.cvc.smt2 b/test/regress/cli/regress0/datatypes/datatype0.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-option :incremental false)
 (declare-datatypes ((nat 0)) (((succ (pred nat)) (zero))))

diff --git a/test/regress/cli/regress0/datatypes/datatype13.cvc.smt2 b/test/regress/cli/regress0/datatypes/datatype13.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-option :incremental false)
 (declare-datatypes ((enum 0)) (((enum1) (enum2) (enum3) (enum4) (enum5) (enum6) (enum7) (enum8) (enum9) (enum10) (enum11) (enum12) (enum13) (enum14) (enum15) (enum16) (enum17) (enum18) (enum19) (enum20) (enum21) (enum22) (enum23) (enum24) (enum25) (enum26) (enum27) (enum28) (enum29) (enum30) (enum31) (enum32) (enum33))))

diff --git a/test/regress/cli/regress0/datatypes/datatype2.cvc.smt2 b/test/regress/cli/regress0/datatypes/datatype2.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-option :incremental false)
 (declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero))((cons (car tree) (cdr list)) (null))((node (data nat) (children list)) (leaf))))

diff --git a/test/regress/cli/regress0/datatypes/dt-different-params.smt2 b/test/regress/cli/regress0/datatypes/dt-different-params.smt2
@@ -1,3 +1,5 @@
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_ALL)
 (set-info :status unsat)
 (declare-datatypes ((Data 1)) ((par (T) ((data (first T))))))

diff --git a/test/regress/cli/regress0/datatypes/dt-sel-2.6.smt2 b/test/regress/cli/regress0/datatypes/dt-sel-2.6.smt2
@@ -1,6 +1,8 @@
 ; COMMAND-LINE: --lang=smt2.6
 ; EXPECT: unsat
 ; DISABLE-TESTER: alf
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-datatypes ((IntList 0)) (

diff --git a/test/regress/cli/regress0/datatypes/empty_tuprec.cvc.smt2 b/test/regress/cli/regress0/datatypes/empty_tuprec.cvc.smt2
@@ -3,6 +3,8 @@
 ; EXPECT: unsat
 ; EXPECT: unsat
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-option :incremental true)
 (declare-fun a1 () UnitTuple)

diff --git a/test/regress/cli/regress0/datatypes/is_test.smt2 b/test/regress/cli/regress0/datatypes/is_test.smt2
@@ -1,3 +1,5 @@
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-datatypes ((Unit 0)) (((u))))

diff --git a/test/regress/cli/regress0/datatypes/issue8883-sort-inf.smt2 b/test/regress/cli/regress0/datatypes/issue8883-sort-inf.smt2
@@ -1,6 +1,8 @@
 ; COMMAND-LINE: --sort-inference
 ; EXPECT: unsat
 ; DISABLE-TESTER: alf
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (declare-datatypes ((Data 1)) ((par (T) ((data)))))
 (declare-fun p2 () (Data Bool))

diff --git a/test/regress/cli/regress0/datatypes/list-bool.smt2 b/test/regress/cli/regress0/datatypes/list-bool.smt2
@@ -1,3 +1,5 @@
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-datatypes ((list 0)) (

diff --git a/test/regress/cli/regress0/datatypes/list-update.smt2 b/test/regress/cli/regress0/datatypes/list-update.smt2
@@ -1,3 +1,5 @@
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-datatypes ((list 0)) (

diff --git a/test/regress/cli/regress0/datatypes/mutually-recursive.cvc.smt2 b/test/regress/cli/regress0/datatypes/mutually-recursive.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-option :incremental false)
 (declare-datatypes ((nat 0)(nat2 0)) (((succ (pred nat2)) (zero))((succ2 (pred2 nat)) (zero2))))

diff --git a/test/regress/cli/regress0/datatypes/par-updater-type-rule.smt2 b/test/regress/cli/regress0/datatypes/par-updater-type-rule.smt2
@@ -1,4 +1,6 @@
 ; DISABLE-TESTER: alf
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :global-declarations true)
 (set-logic ALL)
 (set-info :status unsat)

diff --git a/test/regress/cli/regress0/datatypes/proj-issue578-clash-pf.smt2 b/test/regress/cli/regress0/datatypes/proj-issue578-clash-pf.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-option :check-proofs true)
 (declare-datatypes ((d 0)) (((c (s Bool)) (_c (_s Bool)))))

diff --git a/test/regress/cli/regress0/datatypes/rec1.cvc.smt2 b/test/regress/cli/regress0/datatypes/rec1.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-option :incremental false)
 (declare-fun c () Bool)

diff --git a/test/regress/cli/regress0/datatypes/rec2.cvc.smt2 b/test/regress/cli/regress0/datatypes/rec2.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-option :incremental false)
 (declare-fun c () Bool)

diff --git a/test/regress/cli/regress0/datatypes/rec4.cvc.smt2 b/test/regress/cli/regress0/datatypes/rec4.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-option :incremental false)
 (declare-fun a () Bool)

diff --git a/test/regress/cli/regress0/datatypes/rewriter.cvc.smt2 b/test/regress/cli/regress0/datatypes/rewriter.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-option :incremental false)
 (declare-datatypes ((single_ctor 0)) (((foo (bar Real)))))

diff --git a/test/regress/cli/regress0/datatypes/stream-singleton.smt2 b/test/regress/cli/regress0/datatypes/stream-singleton.smt2
@@ -1,3 +1,5 @@
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_ALL)
 (set-info :status unsat)
 

diff --git a/test/regress/cli/regress0/datatypes/tuple.cvc.smt2 b/test/regress/cli/regress0/datatypes/tuple.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-option :incremental false)
 (define-fun x () (Tuple Real Int Real) (tuple (/ 4 5) 9 (/ 11 9)))

diff --git a/test/regress/cli/regress0/datatypes/typed_v10l30054.cvc.smt2 b/test/regress/cli/regress0/datatypes/typed_v10l30054.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-option :incremental false)
 (declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero))((cons (car tree) (cdr list)) (null))((node (children list)) (leaf (data nat)))))

diff --git a/test/regress/cli/regress0/datatypes/typed_v1l80005.cvc.smt2 b/test/regress/cli/regress0/datatypes/typed_v1l80005.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-option :incremental false)
 (declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero))((cons (car tree) (cdr list)) (null))((node (children list)) (leaf (data nat)))))

diff --git a/test/regress/cli/regress0/datatypes/typed_v3l20092.cvc.smt2 b/test/regress/cli/regress0/datatypes/typed_v3l20092.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-option :incremental false)
 (declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero))((cons (car tree) (cdr list)) (null))((node (children list)) (leaf (data nat)))))

diff --git a/test/regress/cli/regress0/datatypes/typed_v5l30069.cvc.smt2 b/test/regress/cli/regress0/datatypes/typed_v5l30069.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-option :incremental false)
 (declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero))((cons (car tree) (cdr list)) (null))((node (children list)) (leaf (data nat)))))

diff --git a/test/regress/cli/regress0/datatypes/v10l40099.cvc.smt2 b/test/regress/cli/regress0/datatypes/v10l40099.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-option :incremental false)
 (declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero))((cons (car tree) (cdr list)) (null))((node (children list)) (leaf (data nat)))))

diff --git a/test/regress/cli/regress0/datatypes/v2l40025.cvc.smt2 b/test/regress/cli/regress0/datatypes/v2l40025.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-option :incremental false)
 (declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero))((cons (car tree) (cdr list)) (null))((node (children list)) (leaf (data nat)))))

diff --git a/test/regress/cli/regress0/decision/error3.delta01.smtv1.smt2 b/test/regress/cli/regress0/decision/error3.delta01.smtv1.smt2
@@ -1,3 +1,5 @@
+;; unsupported bitblasting of bvshl
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-info :status unsat)
 (set-logic QF_AUFBV)

diff --git a/test/regress/cli/regress0/decision/wchains010ue.delta02.smtv1.smt2 b/test/regress/cli/regress0/decision/wchains010ue.delta02.smtv1.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --decision=justification
 ; EXPECT: unsat
+;; introduces arrays Skolem
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-info :status unsat)
 (set-logic QF_AUFBV)

diff --git a/test/regress/cli/regress0/eqrange2.smt2 b/test/regress/cli/regress0/eqrange2.smt2
@@ -1,3 +1,5 @@
+;; unsupported eqrange operator
+; DISABLE-TESTER: alethe
 (set-logic AUFBV)
 (set-option :arrays-exp true)
 (set-info :status unsat)

diff --git a/test/regress/cli/regress0/fmf/fc-simple.smt2 b/test/regress/cli/regress0/fmf/fc-simple.smt2
@@ -1,3 +1,5 @@
+;; unsupported fmf.card operator
+; DISABLE-TESTER: alethe
 (set-logic QF_UFC)
 (set-info :status unsat)
 

diff --git a/test/regress/cli/regress0/fmf/fc-unsat-pent.smt2 b/test/regress/cli/regress0/fmf/fc-unsat-pent.smt2
@@ -1,3 +1,5 @@
+;; unsupported fmf.card operator
+; DISABLE-TESTER: alethe
 (set-logic QF_UFC)
 (set-info :status unsat)
 

diff --git a/test/regress/cli/regress0/fmf/fc-unsat-tot-2.smt2 b/test/regress/cli/regress0/fmf/fc-unsat-tot-2.smt2
@@ -1,3 +1,5 @@
+;; unsupported fmf.card operator
+; DISABLE-TESTER: alethe
 (set-logic UFC)
 (set-info :status unsat)
 

diff --git a/test/regress/cli/regress0/fmf/fmf-strange-bounds-2.smt2 b/test/regress/cli/regress0/fmf/fmf-strange-bounds-2.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --finite-model-find --fmf-bound
 ; EXPECT: unsat
+;; Sets are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-sort U 0)

diff --git a/test/regress/cli/regress0/fmf/forall_unit_data2.smt2 b/test/regress/cli/regress0/fmf/forall_unit_data2.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --finite-model-find
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (declare-sort a 0)
 (declare-datatypes ((prod 0)) (((Pair (gx a) (gy a)))))

diff --git a/test/regress/cli/regress0/fp/abs-unsound2.smt2 b/test/regress/cli/regress0/fp/abs-unsound2.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --fp-exp
 ; EXPECT: unsat
+;; FP is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_FP)
 (set-info :status unsat)
 (declare-fun x () (_ FloatingPoint 3 5))

diff --git a/test/regress/cli/regress0/fp/down-cast-RNA.smt2 b/test/regress/cli/regress0/fp/down-cast-RNA.smt2
@@ -1,6 +1,7 @@
 ; COMMAND-LINE: --fp-exp
 ; EXPECT: unsat
-
+;; FP is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_FP)
 (set-info :source |Written by Andres Noetzli for issue #2183|)
 (set-info :smt-lib-version 2.6)

diff --git a/test/regress/cli/regress0/fp/ext-rew-test.smt2 b/test/regress/cli/regress0/fp/ext-rew-test.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --ext-rew-prep=agg
 ; EXPECT: unsat
+;; FP is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-info :smt-lib-version 2.6)
 (set-logic QF_FP)
 (set-info :category "crafted")

diff --git a/test/regress/cli/regress0/fp/from_sbv.smt2 b/test/regress/cli/regress0/fp/from_sbv.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --fp-exp
 ; EXPECT: unsat
+;; FP is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_BVFP)
 (declare-const x (_ BitVec 1))
 (declare-const rm RoundingMode)

diff --git a/test/regress/cli/regress0/fp/from_ubv.smt2 b/test/regress/cli/regress0/fp/from_ubv.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; FP is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_FP)
 (declare-const r RoundingMode)
 (assert (distinct ((_ to_fp_unsigned 8 24) r (_ bv0 1)) (fp (_ bv0 1) (_ bv0 8) (_ bv0 23))))

diff --git a/test/regress/cli/regress0/fp/issue-5524.smt2 b/test/regress/cli/regress0/fp/issue-5524.smt2
@@ -1,6 +1,8 @@
 ; DISABLE-TESTER: lfsc
 ; COMMAND-LINE: --bv-solver=bitblast
 ; EXPECT: unsat
+;; FP is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_FPLRA)
 (declare-fun fpv5 () Float32)
 (assert (fp.eq (fp.mul RTP fpv5 fpv5) ((_ to_fp 8 24) RTN 0.04)))

diff --git a/test/regress/cli/regress0/fp/issue3582.smt2 b/test/regress/cli/regress0/fp/issue3582.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; FP is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_FP)
 (declare-fun bv () (_ BitVec 1))
 (define-fun x () (_ FloatingPoint 11 53) ((_ to_fp_unsigned 11 53) RNE bv))

diff --git a/test/regress/cli/regress0/fp/proj-issue509-fp-set-comprehension.smt2 b/test/regress/cli/regress0/fp/proj-issue509-fp-set-comprehension.smt2
@@ -1,4 +1,6 @@
 ; DISABLE-TESTER: lfsc
+;; FP is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-option :sets-ext true)
 (declare-datatype d ((c (s RoundingMode))))

diff --git a/test/regress/cli/regress0/fp/rti_3_5_bug.smt2 b/test/regress/cli/regress0/fp/rti_3_5_bug.smt2
@@ -1,7 +1,8 @@
 ; DISABLE-TESTER: lfsc
 ; COMMAND-LINE: --fp-exp
 ; EXPECT: unsat
-
+;; FP is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_FP)
 (set-info :source |Written by Martin for issue #2932|)
 (set-info :smt-lib-version 2.6)

diff --git a/test/regress/cli/regress0/fp/simple.smt2 b/test/regress/cli/regress0/fp/simple.smt2
@@ -1,5 +1,7 @@
 ; EXPECT: unsat
-(set-logic QF_FP)    
+;; FP is not supported in Alethe
+; DISABLE-TESTER: alethe
+(set-logic QF_FP)
 (declare-const x Float32)
 (assert (not (= x (fp.neg (fp.neg x)))))
 (check-sat)
diff --git a/test/regress/cli/regress0/fp/word-blast.smt2 b/test/regress/cli/regress0/fp/word-blast.smt2
@@ -1,6 +1,8 @@
 ; DISABLE-TESTER: lfsc
 ; COMMAND-LINE: --fp-lazy-wb
 ; EXPECT: unsat
+;; FP is not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_BVFP)
 (declare-fun meters_ackermann!0 () (_ BitVec 64))
 (assert

diff --git a/test/regress/cli/regress0/ho/apply-collapse-unsat.smt2 b/test/regress/cli/regress0/ho/apply-collapse-unsat.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; HO not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic HO_UF)
 (set-info :status unsat)
 (declare-sort U 0)

diff --git a/test/regress/cli/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.smt2 b/test/regress/cli/regress0/ho/bug_nodbuilding_interpreted_SYO042^1.smt2
@@ -1,3 +1,5 @@
+;; introduces fresh Skolem in a trusted step
+; DISABLE-TESTER: alethe
 (set-logic HO_ALL)
 (set-info :status unsat)
 (declare-sort $$unsorted 0)

diff --git a/test/regress/cli/regress0/ho/dd.syo009.smt2 b/test/regress/cli/regress0/ho/dd.syo009.smt2
@@ -1,3 +1,5 @@
+;; HO not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic HO_ALL)
 (set-info :status unsat)
 (declare-sort $ 0)

diff --git a/test/regress/cli/regress0/ho/def-fun-flatten.smt2 b/test/regress/cli/regress0/ho/def-fun-flatten.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; HO not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic HO_ALL)
 (set-info :status unsat)
 (declare-fun f (Int Int) Int)