more disabling

HanielB · May 27, 2024 · 057014d · 057014d
1 parent b4cf96f
commit 057014d
Show file tree

Hide file tree

Showing 27 changed files with 6 additions and 49 deletions.
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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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)))))