diff --git a/test/regress/cli/regress1/bv/bv_to_int_10084_forall.smt2 b/test/regress/cli/regress1/bv/bv_to_int_10084_forall.smt2 index e2cf5759413..32772368512 100644 --- a/test/regress/cli/regress1/bv/bv_to_int_10084_forall.smt2 +++ b/test/regress/cli/regress1/bv/bv_to_int_10084_forall.smt2 @@ -1,8 +1,7 @@ ; COMMAND-LINE: --solve-bv-as-int=iand ; EXPECT: unsat -;; Datatypes are not supported in Alethe +;; Instantiation with fresh constants not supported in Alethe ; DISABLE-TESTER: alethe - ;; produced by cvc4_16.drv ;; (set-logic AUFBVFPDTNIRA) ;; produced by cvc4_16.drv diff --git a/test/regress/cli/regress1/datatypes/acyclicity-sr-ground096.smt2 b/test/regress/cli/regress1/datatypes/acyclicity-sr-ground096.smt2 index c368e0db5b9..1da69b279f7 100644 --- a/test/regress/cli/regress1/datatypes/acyclicity-sr-ground096.smt2 +++ b/test/regress/cli/regress1/datatypes/acyclicity-sr-ground096.smt2 @@ -1,5 +1,3 @@ -;; Datatypes are not supported in Alethe -; DISABLE-TESTER: alethe (set-logic QF_DT) (set-info :status unsat) (declare-datatypes ((T 0)) (( (f0) (f1 (proj0f1 T) (proj1f1 T) (proj2f1 T) (proj3f1 T)) (f2 (proj0f2 T) (proj1f2 T) (proj2f2 T)) (f3 (proj0f3 T) (proj1f3 T)) ))) diff --git a/test/regress/cli/regress1/datatypes/cee-prs-small-dd2.smt2 b/test/regress/cli/regress1/datatypes/cee-prs-small-dd2.smt2 index 87cc3a247fa..0e892ecd06f 100644 --- a/test/regress/cli/regress1/datatypes/cee-prs-small-dd2.smt2 +++ b/test/regress/cli/regress1/datatypes/cee-prs-small-dd2.smt2 @@ -1,8 +1,6 @@ ; 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 ((r 0)) (((R1 (x1 Int))))) diff --git a/test/regress/cli/regress1/datatypes/dt-color-2.6.smt2 b/test/regress/cli/regress1/datatypes/dt-color-2.6.smt2 index e9a565f2ba9..f74bfd704d7 100644 --- a/test/regress/cli/regress1/datatypes/dt-color-2.6.smt2 +++ b/test/regress/cli/regress1/datatypes/dt-color-2.6.smt2 @@ -1,7 +1,5 @@ ; COMMAND-LINE: --lang=smt2.6 ; EXPECT: unsat -;; Datatypes are not supported in Alethe -; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (declare-datatype Color ( ( red ) ( green ) ( blue ) )) diff --git a/test/regress/cli/regress1/datatypes/dt-param-card4-unsat.smt2 b/test/regress/cli/regress1/datatypes/dt-param-card4-unsat.smt2 index a9703ef5f5c..269bc515b8e 100644 --- a/test/regress/cli/regress1/datatypes/dt-param-card4-unsat.smt2 +++ b/test/regress/cli/regress1/datatypes/dt-param-card4-unsat.smt2 @@ -1,6 +1,4 @@ ; EXPECT: unsat -;; Datatypes are not supported in Alethe -; DISABLE-TESTER: alethe (set-logic QF_ALL) (set-info :status unsat) (declare-datatypes ((Pair 2)) ((par (T S) ((pair (first T) (second S)))))) diff --git a/test/regress/cli/regress1/datatypes/manos-model.smt2 b/test/regress/cli/regress1/datatypes/manos-model.smt2 index 1e0b160dc99..2c7dc2b7a7d 100644 --- a/test/regress/cli/regress1/datatypes/manos-model.smt2 +++ b/test/regress/cli/regress1/datatypes/manos-model.smt2 @@ -1,6 +1,4 @@ ; EXPECT: unsat -;; Datatypes are not supported in Alethe -; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (declare-datatypes ((tuple2!879 0)) ( diff --git a/test/regress/cli/regress1/datatypes/nested-rec-array-aa.smt2 b/test/regress/cli/regress1/datatypes/nested-rec-array-aa.smt2 index 0905874ff58..aafd02d04d4 100644 --- a/test/regress/cli/regress1/datatypes/nested-rec-array-aa.smt2 +++ b/test/regress/cli/regress1/datatypes/nested-rec-array-aa.smt2 @@ -1,5 +1,3 @@ -;; Datatypes are not supported in Alethe -; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (set-option :dt-nested-rec true) diff --git a/test/regress/cli/regress1/datatypes/non-simple-rec-mut-unsat.smt2 b/test/regress/cli/regress1/datatypes/non-simple-rec-mut-unsat.smt2 index f411d92ab01..93d0a36b560 100644 --- a/test/regress/cli/regress1/datatypes/non-simple-rec-mut-unsat.smt2 +++ b/test/regress/cli/regress1/datatypes/non-simple-rec-mut-unsat.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --dt-nested-rec ; EXPECT: unsat -;; Datatypes are not supported in Alethe +;; introduces arrays Skolem ; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) diff --git a/test/regress/cli/regress1/datatypes/nullables/nullable-lift-unsat.smt2 b/test/regress/cli/regress1/datatypes/nullables/nullable-lift-unsat.smt2 index 8305fe699f7..0fbb1309895 100644 --- a/test/regress/cli/regress1/datatypes/nullables/nullable-lift-unsat.smt2 +++ b/test/regress/cli/regress1/datatypes/nullables/nullable-lift-unsat.smt2 @@ -1,5 +1,5 @@ ; DISABLE-TESTER: lfsc -;; Datatypes are not supported in Alethe +;; Nullables are not supported in Alethe ; DISABLE-TESTER: alethe (set-logic HO_ALL) (set-info :status unsat) diff --git a/test/regress/cli/regress1/datatypes/nullables/nullables2.smt2 b/test/regress/cli/regress1/datatypes/nullables/nullables2.smt2 index 50cad2557ff..2c7ebf03118 100644 --- a/test/regress/cli/regress1/datatypes/nullables/nullables2.smt2 +++ b/test/regress/cli/regress1/datatypes/nullables/nullables2.smt2 @@ -1,4 +1,4 @@ -;; Datatypes are not supported in Alethe +;; Nullables are not supported in Alethe ; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) diff --git a/test/regress/cli/regress1/datatypes/nullables/nullables3.smt2 b/test/regress/cli/regress1/datatypes/nullables/nullables3.smt2 index 078d6e55383..39804c8fdc2 100644 --- a/test/regress/cli/regress1/datatypes/nullables/nullables3.smt2 +++ b/test/regress/cli/regress1/datatypes/nullables/nullables3.smt2 @@ -1,5 +1,5 @@ ; DISABLE-TESTER: alf -;; Datatypes are not supported in Alethe +;; Nullables are not supported in Alethe ; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) diff --git a/test/regress/cli/regress1/datatypes/proj-issue433-tester-merge-pf.smt2 b/test/regress/cli/regress1/datatypes/proj-issue433-tester-merge-pf.smt2 index f56a7b2e4d4..7a6fd8a933c 100644 --- a/test/regress/cli/regress1/datatypes/proj-issue433-tester-merge-pf.smt2 +++ b/test/regress/cli/regress1/datatypes/proj-issue433-tester-merge-pf.smt2 @@ -1,5 +1,3 @@ -;; Datatypes are not supported in Alethe -; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (declare-datatypes ((L 0)) (((i)))) diff --git a/test/regress/cli/regress1/quantifiers/bug822.smt2 b/test/regress/cli/regress1/quantifiers/bug822.smt2 index fe523af94d9..39b2c593f09 100644 --- a/test/regress/cli/regress1/quantifiers/bug822.smt2 +++ b/test/regress/cli/regress1/quantifiers/bug822.smt2 @@ -1,5 +1,3 @@ -;; Datatypes are not supported in Alethe -; DISABLE-TESTER: alethe (set-logic UFDT) (set-info :source | Generated by: Andrew Reynolds diff --git a/test/regress/cli/regress1/quantifiers/bug_743.smt2 b/test/regress/cli/regress1/quantifiers/bug_743.smt2 index f42b52d8f73..0432509b218 100644 --- a/test/regress/cli/regress1/quantifiers/bug_743.smt2 +++ b/test/regress/cli/regress1/quantifiers/bug_743.smt2 @@ -1,8 +1,6 @@ ; COMMAND-LINE: --lang=smt2.6 ; EXPECT: unsat ; DISABLE-TESTER: alf -;; Datatypes are not supported in Alethe -; DISABLE-TESTER: alethe ;; produced by cvc4_14.drv ;; (set-logic AUFBVDTNIRA) diff --git a/test/regress/cli/regress1/quantifiers/cdt-0208-to.smt2 b/test/regress/cli/regress1/quantifiers/cdt-0208-to.smt2 index 629ace1b700..9da540e3063 100644 --- a/test/regress/cli/regress1/quantifiers/cdt-0208-to.smt2 +++ b/test/regress/cli/regress1/quantifiers/cdt-0208-to.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --full-saturate-quant ; EXPECT: unsat -;; Datatypes are not supported in Alethe +;; Codatatypes are not supported in Alethe ; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) diff --git a/test/regress/cli/regress1/quantifiers/cee-npnt-dd.smt2 b/test/regress/cli/regress1/quantifiers/cee-npnt-dd.smt2 index 256776dd5be..b497ad688a7 100644 --- a/test/regress/cli/regress1/quantifiers/cee-npnt-dd.smt2 +++ b/test/regress/cli/regress1/quantifiers/cee-npnt-dd.smt2 @@ -1,8 +1,6 @@ ; 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) (set-option :fmf-bound true) diff --git a/test/regress/cli/regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2 b/test/regress/cli/regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2 index cd1a88cc552..2253b8cde8c 100644 --- a/test/regress/cli/regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2 +++ b/test/regress/cli/regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2 @@ -1,7 +1,5 @@ ; COMMAND-LINE: -q ; EXPECT: unsat -;; Datatypes are not supported in Alethe -; DISABLE-TESTER: alethe (set-logic ALL) (declare-sort e 0) (declare-sort p 0) diff --git a/test/regress/cli/regress1/quantifiers/ddatv-delta2.smt2 b/test/regress/cli/regress1/quantifiers/ddatv-delta2.smt2 index 6cd0a0c67b2..de60d9640a0 100644 --- a/test/regress/cli/regress1/quantifiers/ddatv-delta2.smt2 +++ b/test/regress/cli/regress1/quantifiers/ddatv-delta2.smt2 @@ -1,5 +1,3 @@ -;; Datatypes 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/regress1/quantifiers/example10714-core-no-miniscope-user.smt2 b/test/regress/cli/regress1/quantifiers/example10714-core-no-miniscope-user.smt2 index d773013b31d..9df906730ee 100644 --- a/test/regress/cli/regress1/quantifiers/example10714-core-no-miniscope-user.smt2 +++ b/test/regress/cli/regress1/quantifiers/example10714-core-no-miniscope-user.smt2 @@ -1,6 +1,4 @@ ; EXPECT: unsat -;; Datatypes are not supported in Alethe -; DISABLE-TESTER: alethe (set-logic ALL) (declare-sort integer 0) (declare-datatypes ((t 0)) (((tqtmk (rec__first integer) (rec__last integer))))) diff --git a/test/regress/cli/regress1/quantifiers/f993-loss-easy.smt2 b/test/regress/cli/regress1/quantifiers/f993-loss-easy.smt2 index c4dfc007bad..f73c55fc07f 100644 --- a/test/regress/cli/regress1/quantifiers/f993-loss-easy.smt2 +++ b/test/regress/cli/regress1/quantifiers/f993-loss-easy.smt2 @@ -1,5 +1,3 @@ -;; Datatypes are not supported in Alethe -; DISABLE-TESTER: alethe (set-info :smt-lib-version 2.6) (set-logic UFDT) (set-info :status unsat) diff --git a/test/regress/cli/regress1/quantifiers/isaplanner-goal20.smt2 b/test/regress/cli/regress1/quantifiers/isaplanner-goal20.smt2 index ce851c3e4f7..0a054b6cf11 100644 --- a/test/regress/cli/regress1/quantifiers/isaplanner-goal20.smt2 +++ b/test/regress/cli/regress1/quantifiers/isaplanner-goal20.smt2 @@ -1,7 +1,5 @@ ; COMMAND-LINE: --quant-ind --conjecture-gen ; EXPECT: unsat -;; Datatypes are not supported in Alethe -; DISABLE-TESTER: alethe (set-logic UFDTLIA) (set-info :status unsat) (declare-datatypes ((Nat 0)) (((succ (pred Nat)) (zero)) diff --git a/test/regress/cli/regress1/quantifiers/issue3481.smt2 b/test/regress/cli/regress1/quantifiers/issue3481.smt2 index 78a006ceb27..1c59996b58b 100644 --- a/test/regress/cli/regress1/quantifiers/issue3481.smt2 +++ b/test/regress/cli/regress1/quantifiers/issue3481.smt2 @@ -1,7 +1,5 @@ ; COMMAND-LINE: --enum-inst --enum-inst-limit=2 ; EXPECT: unsat -;; Datatypes are not supported in Alethe -; DISABLE-TESTER: alethe ;; produced by cvc4_16.drv ;; (set-info :smt-lib-version 2.6) diff --git a/test/regress/cli/regress1/quantifiers/issue993.smt2 b/test/regress/cli/regress1/quantifiers/issue993.smt2 index 310ddfe8912..6b8d8eaf9b0 100644 --- a/test/regress/cli/regress1/quantifiers/issue993.smt2 +++ b/test/regress/cli/regress1/quantifiers/issue993.smt2 @@ -1,5 +1,3 @@ -;; Datatypes are not supported in Alethe -; DISABLE-TESTER: alethe (set-logic AUFBVDTNIRA) (set-info :smt-lib-version 2.6) (set-info :status unsat) diff --git a/test/regress/cli/regress1/quantifiers/issue9989-syqi-nwf.smt2 b/test/regress/cli/regress1/quantifiers/issue9989-syqi-nwf.smt2 index e5e9a7df90a..d455629f41d 100644 --- a/test/regress/cli/regress1/quantifiers/issue9989-syqi-nwf.smt2 +++ b/test/regress/cli/regress1/quantifiers/issue9989-syqi-nwf.smt2 @@ -1,7 +1,5 @@ ; COMMAND-LINE: --sygus-inst ; EXPECT: unsat -;; Datatypes are not supported in Alethe -; DISABLE-TESTER: alethe (set-logic ALL) (declare-sort a 0) (declare-datatypes ((t 0)) (((L (s a))))) diff --git a/test/regress/cli/regress1/quantifiers/min-ppgt-em-incomplete.smt2 b/test/regress/cli/regress1/quantifiers/min-ppgt-em-incomplete.smt2 index 9bb8c333cf8..e6d8a960950 100644 --- a/test/regress/cli/regress1/quantifiers/min-ppgt-em-incomplete.smt2 +++ b/test/regress/cli/regress1/quantifiers/min-ppgt-em-incomplete.smt2 @@ -1,5 +1,3 @@ -;; Datatypes are not supported in Alethe -; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (declare-sort S 0) diff --git a/test/regress/cli/regress1/quantifiers/min-ppgt-em-incomplete2.smt2 b/test/regress/cli/regress1/quantifiers/min-ppgt-em-incomplete2.smt2 index 67b7bed1ad5..68f49ee8fc4 100644 --- a/test/regress/cli/regress1/quantifiers/min-ppgt-em-incomplete2.smt2 +++ b/test/regress/cli/regress1/quantifiers/min-ppgt-em-incomplete2.smt2 @@ -1,5 +1,3 @@ -;; Datatypes 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/regress1/quantifiers/parametric-lists.smt2 b/test/regress/cli/regress1/quantifiers/parametric-lists.smt2 index 6f1e988e0ff..89744cded09 100644 --- a/test/regress/cli/regress1/quantifiers/parametric-lists.smt2 +++ b/test/regress/cli/regress1/quantifiers/parametric-lists.smt2 @@ -1,7 +1,5 @@ ; DISABLE-TESTER: alf ; EXPECT: unsat -;; Datatypes are not supported in Alethe -; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (declare-datatypes ((List 1)) ((par (T) ((cons (head T) (tail (List T))) (nil)))))