diff --git a/test/regress/cli/regress0/auflia/bug336.smt2 b/test/regress/cli/regress0/auflia/bug336.smt2 index 34af91c6cdf..a93f79668c1 100644 --- 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 index e73e42fb57e..7aca12c60d9 100644 --- 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 index f2110a3f7be..8fed8280d8f 100644 --- 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 index 055a98dc8e8..7b43649bfd0 100644 --- 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 index 10012202887..042adf1ccd9 100644 --- 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 index d81c3723d1e..be3126b7956 100644 --- 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 index 4a9dfce0a4b..94a49ca0a69 100644 --- 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 index 8ce18634490..f572b83cb9f 100644 --- 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 index 378c87560f2..aa2591ab144 100644 --- 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 index 44fee2acb46..5b348ee9189 100644 --- 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 index 56bd79a47f1..cd8fa6c932e 100644 --- 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 index 89d63eb0633..5e6b6efbcbf 100644 --- 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 index 518df8e65c0..4a7b1cab33d 100644 --- 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 index 4b0aa59fff1..df28c558bdb 100644 --- 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 index ea2913eec4a..f1f66c53551 100644 --- 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 index adc7ad95ac6..dd971446bdf 100644 --- 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 index 178f1a000e1..4a1e20f7504 100644 --- 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 index a202e80585e..89e451dc603 100644 --- 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 index c7f2fda2633..7bf11e816c8 100644 --- 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 index db0c389d5cc..31f8334d13a 100644 --- 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 index b6d4ba58e19..a0cecaff104 100644 --- 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 index 59451624673..356bdc6e22b 100644 --- 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 index 7fa37011b0f..6bfd0b5130d 100644 --- 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 index 76f39e66e0f..6f98dc62f37 100644 --- 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 index 5ef10166238..3aad7e2ff7a 100644 --- 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 index 0c5ce70b5a9..5c92166d805 100644 --- 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 index 81890f6af81..0a88e6f3a83 100644 --- 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 index c9ce01ccf54..46356a7b748 100644 --- 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 index 6ed774840f2..56574909357 100644 --- 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 index 96a50854c39..8ad8bc3bb5a 100644 --- 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 index d54e69d7610..105bb4d12a6 100644 --- 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 index b45175a741b..ad588f38bed 100644 --- 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 index c8f3c8a6ce1..a346dc6f079 100644 --- 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 index bf7028f52b7..eca0e5f8036 100644 --- 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 index efddbc88bbd..dfa6ce06ef3 100644 --- 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 index 26c9b423f9d..e6913888b13 100644 --- 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 index b07c53077d5..82044f51857 100644 --- 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 index 404b3abeaaa..8e83edccdd7 100644 --- 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 index e110c4e465a..b255abf38e1 100644 --- 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 index 7ceb74ad38e..cd945d3dd86 100644 --- 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 index 3040f9ba95e..b8182ec9ef0 100644 --- 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 index 62314f2846c..12f2d92b4de 100644 --- 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 index 88090daeccc..9298ff81117 100644 --- 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 index 226d6589c13..f115ef3bff6 100644 --- 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 index 6939e478ad5..75b95465885 100644 --- 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 index f5f2024c013..1eaca034886 100644 --- 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 index c06cdb1105d..ff1b099cbf2 100644 --- 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 index 8907fd846bb..682275c3ee3 100644 --- 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 index c2144dfc4d1..804c0ae709c 100644 --- 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 index 754186943dc..82aefc088c5 100644 --- 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 index 1e8ae7320d3..0b0389c3917 100644 --- 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 index 45eeb23a70c..0a9fc62ef0e 100644 --- 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 index f8cafab02af..e56250b1a77 100644 --- 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 index 5e847b1f76e..eb5e1f86ca1 100644 --- 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 index 81af169a7d6..712465c435b 100644 --- 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) diff --git a/test/regress/cli/regress0/ho/ext-finite-unsat.smt2 b/test/regress/cli/regress0/ho/ext-finite-unsat.smt2 index 282cc3bda03..32a64ba944b 100644 --- a/test/regress/cli/regress0/ho/ext-finite-unsat.smt2 +++ b/test/regress/cli/regress0/ho/ext-finite-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/finite-fun-ext.smt2 b/test/regress/cli/regress0/ho/finite-fun-ext.smt2 index 63e25cb039f..af413a76b6d 100644 --- a/test/regress/cli/regress0/ho/finite-fun-ext.smt2 +++ b/test/regress/cli/regress0/ho/finite-fun-ext.smt2 @@ -1,4 +1,6 @@ ; EXPECT: unsat +;; HO not supported in Alethe +; DISABLE-TESTER: alethe (set-logic HO_ALL) (declare-datatype Unit ((unit))) diff --git a/test/regress/cli/regress0/ho/fta0144-alpha-eq.smt2 b/test/regress/cli/regress0/ho/fta0144-alpha-eq.smt2 index c3b0e73872a..5395cab7078 100644 --- a/test/regress/cli/regress0/ho/fta0144-alpha-eq.smt2 +++ b/test/regress/cli/regress0/ho/fta0144-alpha-eq.smt2 @@ -1,4 +1,6 @@ ; EXPECT: unsat +;; HO not supported in Alethe +; DISABLE-TESTER: alethe (set-logic HO_ALL) (declare-sort Nat$ 0) (declare-sort Complex$ 0) diff --git a/test/regress/cli/regress0/ho/fta0210.smt2 b/test/regress/cli/regress0/ho/fta0210.smt2 index 864bb985926..226f8ea3411 100644 --- a/test/regress/cli/regress0/ho/fta0210.smt2 +++ b/test/regress/cli/regress0/ho/fta0210.smt2 @@ -1,5 +1,7 @@ ; EXPECT: unsat -(set-logic HO_ALL) +;; HO not supported in Alethe +; DISABLE-TESTER: alethe + (set-logic HO_ALL) (declare-sort A$ 0) (declare-sort Nat$ 0) (declare-sort A_poly$ 0) diff --git a/test/regress/cli/regress0/ho/ho-match-fun-suffix.smt2 b/test/regress/cli/regress0/ho/ho-match-fun-suffix.smt2 index 4418b156f9f..8116ed130b6 100644 --- a/test/regress/cli/regress0/ho/ho-match-fun-suffix.smt2 +++ b/test/regress/cli/regress0/ho/ho-match-fun-suffix.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) diff --git a/test/regress/cli/regress0/ho/ho-matching-enum-2.smt2 b/test/regress/cli/regress0/ho/ho-matching-enum-2.smt2 index e73afdce241..8b694c1b6d5 100644 --- a/test/regress/cli/regress0/ho/ho-matching-enum-2.smt2 +++ b/test/regress/cli/regress0/ho/ho-matching-enum-2.smt2 @@ -1,4 +1,6 @@ ; EXPECT: unsat +;; HO not supported in Alethe +; DISABLE-TESTER: alethe (set-logic HO_ALL) (set-info :status unsat) diff --git a/test/regress/cli/regress0/ho/ho-matching-enum.smt2 b/test/regress/cli/regress0/ho/ho-matching-enum.smt2 index df3a920ec0e..14c99606d59 100644 --- a/test/regress/cli/regress0/ho/ho-matching-enum.smt2 +++ b/test/regress/cli/regress0/ho/ho-matching-enum.smt2 @@ -1,4 +1,6 @@ ; EXPECT: unsat +;; HO not supported in Alethe +; DISABLE-TESTER: alethe (set-logic HO_ALL) (set-info :status unsat) diff --git a/test/regress/cli/regress0/ho/ho-matching-nested-app.smt2 b/test/regress/cli/regress0/ho/ho-matching-nested-app.smt2 index 506cd55cf12..e9d3f73ce4b 100644 --- a/test/regress/cli/regress0/ho/ho-matching-nested-app.smt2 +++ b/test/regress/cli/regress0/ho/ho-matching-nested-app.smt2 @@ -1,4 +1,6 @@ ; EXPECT: unsat +;; HO not supported in Alethe +; DISABLE-TESTER: alethe (set-logic HO_ALL) (set-info :status unsat) diff --git a/test/regress/cli/regress0/ho/hoa0008.smt2 b/test/regress/cli/regress0/ho/hoa0008.smt2 index b43920c2175..f28c33c17ee 100644 --- a/test/regress/cli/regress0/ho/hoa0008.smt2 +++ b/test/regress/cli/regress0/ho/hoa0008.smt2 @@ -1,4 +1,6 @@ ; EXPECT: unsat +;; HO not supported in Alethe +; DISABLE-TESTER: alethe (set-logic HO_ALL) (declare-sort A$ 0) (declare-sort Com$ 0) diff --git a/test/regress/cli/regress0/ho/lambda-test-deps-simple.smt2 b/test/regress/cli/regress0/ho/lambda-test-deps-simple.smt2 index 876dc95340a..961d0b83ccb 100644 --- a/test/regress/cli/regress0/ho/lambda-test-deps-simple.smt2 +++ b/test/regress/cli/regress0/ho/lambda-test-deps-simple.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --enum-inst ; EXPECT: unsat +;; HO not supported in Alethe +; DISABLE-TESTER: alethe (set-logic HO_ALL) (declare-fun f (Int Int) Int) (assert (= f (lambda ((x Int) (y Int)) (+ 1 (f x y))))) diff --git a/test/regress/cli/regress0/ho/lambda-test-deps.smt2 b/test/regress/cli/regress0/ho/lambda-test-deps.smt2 index e05539f90df..e08e616b9dd 100644 --- a/test/regress/cli/regress0/ho/lambda-test-deps.smt2 +++ b/test/regress/cli/regress0/ho/lambda-test-deps.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --enum-inst ; EXPECT: unsat +;; HO not supported in Alethe +; DISABLE-TESTER: alethe (set-logic HO_ALL) (declare-fun f (Int Int) Int) (declare-fun g (Int Int) Int) diff --git a/test/regress/cli/regress0/ho/match-middle.smt2 b/test/regress/cli/regress0/ho/match-middle.smt2 index 225faa1a542..ae5b2607e1c 100644 --- a/test/regress/cli/regress0/ho/match-middle.smt2 +++ b/test/regress/cli/regress0/ho/match-middle.smt2 @@ -1,4 +1,6 @@ ; EXPECT: unsat +;; HO not supported in Alethe +; DISABLE-TESTER: alethe (set-logic HO_UFLIA) (set-info :status unsat) (declare-fun f (Int Int Int) Int) diff --git a/test/regress/cli/regress0/ho/simple-conf-lazy-lambda-lift-app.smt2 b/test/regress/cli/regress0/ho/simple-conf-lazy-lambda-lift-app.smt2 index ab949c40cea..7e22049d53e 100644 --- a/test/regress/cli/regress0/ho/simple-conf-lazy-lambda-lift-app.smt2 +++ b/test/regress/cli/regress0/ho/simple-conf-lazy-lambda-lift-app.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --uf-lazy-ll ; EXPECT: unsat +;; HO not supported in Alethe +; DISABLE-TESTER: alethe (set-logic HO_ALL) (set-info :status unsat) (define-fun f ((x Int)) Int (+ x 1)) diff --git a/test/regress/cli/regress0/ho/simple-conf-lazy-lambda-lift.smt2 b/test/regress/cli/regress0/ho/simple-conf-lazy-lambda-lift.smt2 index d11a4418b3c..c7e71bbfee3 100644 --- a/test/regress/cli/regress0/ho/simple-conf-lazy-lambda-lift.smt2 +++ b/test/regress/cli/regress0/ho/simple-conf-lazy-lambda-lift.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --uf-lazy-ll ; EXPECT: unsat +;; HO not supported in Alethe +; DISABLE-TESTER: alethe (set-logic HO_ALL) (set-info :status unsat) (define-fun f ((x Int)) Int (+ x 1)) diff --git a/test/regress/cli/regress0/ho/simple-matching-partial.smt2 b/test/regress/cli/regress0/ho/simple-matching-partial.smt2 index 18c578367e1..1e25a81288f 100644 --- a/test/regress/cli/regress0/ho/simple-matching-partial.smt2 +++ b/test/regress/cli/regress0/ho/simple-matching-partial.smt2 @@ -1,4 +1,6 @@ ; EXPECT: unsat +;; HO not supported in Alethe +; DISABLE-TESTER: alethe (set-logic HO_ALL) (set-info :status unsat) (declare-sort U 0) diff --git a/test/regress/cli/regress0/ho/simple-matching.smt2 b/test/regress/cli/regress0/ho/simple-matching.smt2 index cbd70f0726c..9476b573f00 100644 --- a/test/regress/cli/regress0/ho/simple-matching.smt2 +++ b/test/regress/cli/regress0/ho/simple-matching.smt2 @@ -1,4 +1,6 @@ ; EXPECT: unsat +;; HO not supported in Alethe +; DISABLE-TESTER: alethe (set-logic HO_ALL) (set-info :status unsat) (declare-sort U 0) diff --git a/test/regress/cli/regress0/proofs/unused-def1.smt2 b/test/regress/cli/regress0/proofs/unused-def1.smt2 index 04b5e0f39fa..136611ec5ec 100644 --- a/test/regress/cli/regress0/proofs/unused-def1.smt2 +++ b/test/regress/cli/regress0/proofs/unused-def1.smt2 @@ -1,6 +1,6 @@ -; DISABLE-TESTER: alethe ; EXPECT: unsat - +;; define-const is not supported in Alethe +; DISABLE-TESTER: alethe (set-logic UF) (declare-const x Bool) (define-const p Bool x) diff --git a/test/regress/cli/regress0/proofs/unused-def2.smt2 b/test/regress/cli/regress0/proofs/unused-def2.smt2 index 7f2b94e23f1..1cd20705cd4 100644 --- a/test/regress/cli/regress0/proofs/unused-def2.smt2 +++ b/test/regress/cli/regress0/proofs/unused-def2.smt2 @@ -1,7 +1,8 @@ ; COMMAND-LINE: --proof-prune-input --dump-proof --proof-format=lfsc ; SCRUBBER: grep -E "define|unsat" ; EXPECT: unsat - +;; define-const is not supported in Alethe +; DISABLE-TESTER: alethe (set-logic UF) (declare-const x Bool) (define-const p Bool x) diff --git a/test/regress/cli/regress0/smtlib/issue4552.smt2 b/test/regress/cli/regress0/smtlib/issue4552.smt2 index 8fcfabd5e05..5aa33ca38e8 100644 --- a/test/regress/cli/regress0/smtlib/issue4552.smt2 +++ b/test/regress/cli/regress0/smtlib/issue4552.smt2 @@ -2,6 +2,8 @@ ; EXPECT: unsat ; EXPECT: unsat ; EXPECT: unsat +;; define-const is not supported in Alethe +; DISABLE-TESTER: alethe (set-logic UF) (set-option :global-declarations true)