more disabling

test/regress/cli/regress1/proofs/qgu-fuzz-1-strings-pp.smt2

@@ -1,3 +1,5 @@
+;; introduces RE Skolem
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun x () String)

test/regress/cli/regress1/quantifiers/bug822.smt2

@@ -1,3 +1,5 @@
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic UFDT)
 (set-info :source |
 Generated by: Andrew Reynolds
@@ -1178,4 +1180,3 @@ Publications: "A Decision Procedure for (Co)Datatypes" by Andrew Reynolds and Ja
 (assert (forall ((?v0 B_tree_a_b_fun_sum_b_tree_a_b_fun_sum_prod$)) (! (= (fun_app$ay (uncurry$a uvq$) ?v0) ?v0) :pattern ((fun_app$ay (uncurry$a uvq$) ?v0)))))
 (check-sat)
 (exit)
-

test/regress/cli/regress1/quantifiers/bug_743.smt2

@@ -1,6 +1,8 @@
 ; 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)

test/regress/cli/regress1/quantifiers/cdt-0208-to.smt2

@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --full-saturate-quant
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-sort A$ 0)
@@ -765,4 +767,3 @@
 (assert (! (forall ((?v0 A_llist$) (?v1 A_llist_a_llist_prod_a_llist_fun$) (?v2 A_llist_a_llist_prod$) (?v3 A_llist$) (?v4 A_llist_a_llist_prod_a_llist_fun$) (?v5 A_llist_a_llist_prod_set$)) (=> (and (= ?v0 (fun_app$cp ?v1 ?v2)) (and (= ?v3 (fun_app$cp ?v4 ?v2)) (fun_app$i (set.member$ ?v2) ?v5))) (fun_app$i (set.member$ (pair$ ?v0 ?v3)) (image2$ ?v5 ?v1 ?v4)))) :named a419))
 (assert (! (forall ((?v0 A_llist$) (?v1 A_llist$)) (= (the$ (fun_app$ad uncurry$a (fun_app$aa (uwt$ ?v0) ?v1))) (pair$ ?v0 ?v1))) :named a420))
 (check-sat)
-

test/regress/cli/regress1/quantifiers/cee-npnt-dd.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)
 (set-option :fmf-bound true)

test/regress/cli/regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2

@@ -1,5 +1,7 @@
 ; 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)

test/regress/cli/regress1/quantifiers/ddatv-delta2.smt2

@@ -1,11 +1,13 @@
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-sort U 0)
 (declare-datatypes ((T 0) (D 0)) (((E) (o (b Bool)) (I (t Int)) (i (v D)) (R (l T) (u T))) ((ic (vc U)))))
 (declare-datatypes ((H 0)) (((M (h T)))))
 (declare-fun S (U Int) T)
 (declare-fun n () H)
-(assert (and 
+(assert (and
 (not (b (o (or (b (o (or (b (o (or (b (o (= (t (S (vc (v (S (vc (v E)) 0))) (t E))) (t (S (vc (v (S (vc (v (h n))) 0))) (t E))))))))))))))))
 (b (o (forall ((i Int)) (or (< i (t (u (R E E)))) (b (o (forall ((z Int)) (! (or (b (o (or (b (o (< (t (S (vc (v (S (vc (v (h n))) z))) (t E))) (t (S (vc (v (S (vc (v (h n))) 0))) (t (I i))))))))))) :qid id))))))))))
 (check-sat)

test/regress/cli/regress1/quantifiers/eqrange_ex_1.smt2

@@ -1,6 +1,8 @@
 ; COMMAND-LINE: --arrays-exp
 ; EXPECT: unsat
 ; DISABLE-TESTER: dsl-proof
+;; unsupported eqrange operator
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (set-option :produce-models true)

test/regress/cli/regress1/quantifiers/f993-loss-easy.smt2

@@ -1,3 +1,5 @@
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-info :smt-lib-version 2.6)
 (set-logic UFDT)
 (set-info :status unsat)
@@ -63,7 +65,7 @@
 (declare-fun case_enat$ (Nat_bool_fun$) Bool_enat_bool_fun_fun$)
 (declare-fun greatest$a () Nat_bool_fun_nat_fun$)
 (declare-fun greatestM$ (Nat_nat_fun$) Nat_bool_fun_nat_fun$)
-(assert (and 
+(assert (and
 (forall ((?v0 Nat$) (?v1 A_stream_bool_fun$) (?v2 A_stream$)) (=> (fun_app$a (less$a (enat$ ?v0)) (sfirst$ ?v1 ?v2)) (not (fun_app$f ?v1 (sdrop$ ?v0 ?v2)))) )
 (not (fun_app$a (less_eq$a (sfirst$ p$ omega$)) (enat$ (suc$ ia$))))
 (fun_app$f p$ (sdrop$ (suc$ ia$) omega$))

test/regress/cli/regress1/quantifiers/fp-cegqi-unsat.smt2

@@ -1,3 +1,5 @@
+;; FP not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-info :smt-lib-version 2.6)
 (set-logic FPLRA)
 (set-info :status unsat)

test/regress/cli/regress1/quantifiers/ho-seu-sygus-inst.smt2

@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --sygus-inst
 ; EXPECT: unsat
+;; introduces fresh Skolem in a trusted step
+; DISABLE-TESTER: alethe
 (set-logic HO_ALL)
 (declare-sort u 0)
 (declare-fun tptp.funcImageSingleton () Bool)
@@ -26,4 +28,3 @@
 (assert (= tptp.funcImageSingleton (forall ((A u) (B u) (Xf u)) (=> (@ (@ (@ tptp.func A) B) Xf) (forall ((Xx u)) (=> (@ (@ tptp.in Xx) A) (@ tptp.singleton (@ (@ tptp.dsetconstr B) (lambda ((Xy u)) (@ (@ tptp.in (@ (@ tptp.kpair Xx) Xy)) Xf))))))))))
 (assert (not (=> tptp.dsetconstrEL (=> tptp.theprop (=> tptp.funcImageSingleton (forall ((A u) (B u) (Xf u)) (=> (@ (@ (@ tptp.func A) B) Xf) (forall ((Xx u)) (=> (@ (@ tptp.in Xx) A) (@ (@ tptp.in (@ tptp.setunion (@ (@ tptp.dsetconstr B) (lambda ((Xy u)) (@ (@ tptp.in (@ (@ tptp.kpair Xx) Xy)) Xf))))) B))))))))))
 (check-sat)
-

test/regress/cli/regress1/quantifiers/isaplanner-goal20.smt2

@@ -1,5 +1,7 @@
 ; 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))
@@ -63,4 +65,3 @@
 (assert (not (forall ((l Lst)) (= (len (sort l)) (len l)) )))
 (check-sat)
 (exit)
-

test/regress/cli/regress1/quantifiers/issue3481.smt2

@@ -1,5 +1,7 @@
 ; 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)
@@ -40,7 +42,7 @@
 
 (define-fun real__ref___projection ((a real__ref)) Real (real__content a))
 
-(define-fun us_private__ref___projection ((a us_private__ref)) us_private 
+(define-fun us_private__ref___projection ((a us_private__ref)) us_private
   (us_private__content a))
 
 (define-fun in_range ((x Int)) Bool (or (= x 0) (= x 1)))
@@ -68,7 +70,7 @@
 
 (declare-datatypes ((integer__ref 0))
 (((integer__refqtmk (integer__content integer)))))
-(define-fun integer__ref_integer__content__projection ((a integer__ref)) integer 
+(define-fun integer__ref_integer__content__projection ((a integer__ref)) integer
   (integer__content a))
 
 (define-fun to_rep ((x integer)) Int (integerqtint x))
@@ -82,26 +84,26 @@
 
 (declare-datatypes ((positive__ref 0))
 (((positive__refqtmk (positive__content positive)))))
-(define-fun positive__ref_positive__content__projection ((a positive__ref)) positive 
+(define-fun positive__ref_positive__content__projection ((a positive__ref)) positive
   (positive__content a))
 
 (declare-datatypes ((us_split_fields 0))
 (((us_split_fieldsqtmk
   (rec__test_route__point__x integer)(rec__test_route__point__y integer)))))
-(define-fun us_split_fields_rec__test_route__point__x__projection ((a us_split_fields)) integer 
+(define-fun us_split_fields_rec__test_route__point__x__projection ((a us_split_fields)) integer
   (rec__test_route__point__x a))
 
-(define-fun us_split_fields_rec__test_route__point__y__projection ((a us_split_fields)) integer 
+(define-fun us_split_fields_rec__test_route__point__y__projection ((a us_split_fields)) integer
   (rec__test_route__point__y a))
 
 (declare-datatypes ((us_split_fields__ref 0))
 (((us_split_fields__refqtmk (us_split_fields__content us_split_fields)))))
-(define-fun us_split_fields__ref___split_fields__content__projection ((a us_split_fields__ref)) us_split_fields 
+(define-fun us_split_fields__ref___split_fields__content__projection ((a us_split_fields__ref)) us_split_fields
   (us_split_fields__content a))
 
 (declare-datatypes ((us_rep 0))
 (((us_repqtmk (us_split_fields1 us_split_fields)))))
-(define-fun us_rep___split_fields__projection ((a us_rep)) us_split_fields 
+(define-fun us_rep___split_fields__projection ((a us_rep)) us_split_fields
   (us_split_fields1 a))
 
 
@@ -129,27 +131,27 @@
 
 (declare-datatypes ((point__ref 0))
 (((point__refqtmk (point__content us_rep)))))
-(define-fun point__ref_point__content__projection ((a point__ref)) us_rep 
+(define-fun point__ref_point__content__projection ((a point__ref)) us_rep
   (point__content a))
 
 (declare-datatypes ((us_rep1 0))
 (((us_repqtmk1
   (rec__test_route__point_acc__is_null_pointer Bool)(rec__test_route__point_acc__pointer_address Int)(rec__test_route__point_acc__pointer_value us_rep)))))
-(define-fun us_rep_rec__test_route__point_acc__is_null_pointer__projection ((a us_rep1)) Bool 
+(define-fun us_rep_rec__test_route__point_acc__is_null_pointer__projection ((a us_rep1)) Bool
   (rec__test_route__point_acc__is_null_pointer a))
 
-(define-fun us_rep_rec__test_route__point_acc__pointer_address__projection ((a us_rep1)) Int 
+(define-fun us_rep_rec__test_route__point_acc__pointer_address__projection ((a us_rep1)) Int
   (rec__test_route__point_acc__pointer_address a))
 
-(define-fun us_rep_rec__test_route__point_acc__pointer_value__projection ((a us_rep1)) us_rep 
+(define-fun us_rep_rec__test_route__point_acc__pointer_value__projection ((a us_rep1)) us_rep
   (rec__test_route__point_acc__pointer_value a))
 
 (declare-datatypes ((us_rep__ref 0))
 (((us_rep__refqtmk (us_rep__content us_rep1)))))
-(define-fun us_rep__ref___rep__content__projection ((a us_rep__ref)) us_rep1 
+(define-fun us_rep__ref___rep__content__projection ((a us_rep__ref)) us_rep1
   (us_rep__content a))
 
-(define-fun rec__test_route__point_acc__pointer_value__pred ((a us_rep1)) Bool 
+(define-fun rec__test_route__point_acc__pointer_value__pred ((a us_rep1)) Bool
   (not (= (rec__test_route__point_acc__is_null_pointer a) true)))
 
 (declare-const us_null_pointer us_rep1)
@@ -162,34 +164,34 @@
 
 (declare-datatypes ((t1b__ref 0))
 (((t1b__refqtmk (t1b__content us_rep1)))))
-(define-fun t1b__ref_t1b__content__projection ((a t1b__ref)) us_rep1 
+(define-fun t1b__ref_t1b__content__projection ((a t1b__ref)) us_rep1
   (t1b__content a))
 
 (declare-sort us_main_type 0)
 
 (declare-datatypes ((us_rep2 0))
 (((us_repqtmk2
   (rec__test_route__route_acc__is_null_pointer Bool)(rec__test_route__route_acc__pointer_address Int)(rec__test_route__route_acc__pointer_value_abstr us_main_type)))))
-(define-fun us_rep_rec__test_route__route_acc__is_null_pointer__projection ((a us_rep2)) Bool 
+(define-fun us_rep_rec__test_route__route_acc__is_null_pointer__projection ((a us_rep2)) Bool
   (rec__test_route__route_acc__is_null_pointer a))
 
-(define-fun us_rep_rec__test_route__route_acc__pointer_address__projection ((a us_rep2)) Int 
+(define-fun us_rep_rec__test_route__route_acc__pointer_address__projection ((a us_rep2)) Int
   (rec__test_route__route_acc__pointer_address a))
 
-(define-fun us_rep_rec__test_route__route_acc__pointer_value_abstr__projection ((a us_rep2)) us_main_type 
+(define-fun us_rep_rec__test_route__route_acc__pointer_value_abstr__projection ((a us_rep2)) us_main_type
   (rec__test_route__route_acc__pointer_value_abstr a))
 
 (declare-datatypes ((us_rep__ref1 0))
 (((us_rep__refqtmk1 (us_rep__content1 us_rep2)))))
-(define-fun us_rep__ref___rep__content__2__projection ((a us_rep__ref1)) us_rep2 
+(define-fun us_rep__ref___rep__content__2__projection ((a us_rep__ref1)) us_rep2
   (us_rep__content1 a))
 
 
 (declare-const dummy4 us_rep2)
 
 (declare-datatypes ((t4b__ref 0))
 (((t4b__refqtmk (t4b__content us_rep2)))))
-(define-fun t4b__ref_t4b__content__projection ((a t4b__ref)) us_rep2 
+(define-fun t4b__ref_t4b__content__projection ((a t4b__ref)) us_rep2
   (t4b__content a))
 
 (declare-fun length (us_rep2) Int)
@@ -218,40 +220,40 @@
 
 (declare-datatypes ((natural__ref 0))
 (((natural__refqtmk (natural__content natural)))))
-(define-fun natural__ref_natural__content__projection ((a natural__ref)) natural 
+(define-fun natural__ref_natural__content__projection ((a natural__ref)) natural
   (natural__content a))
 
 (declare-const dummy6 us_rep1)
 
 (declare-datatypes ((point_acc__ref 0))
 (((point_acc__refqtmk (point_acc__content us_rep1)))))
-(define-fun point_acc__ref_point_acc__content__projection ((a point_acc__ref)) us_rep1 
+(define-fun point_acc__ref_point_acc__content__projection ((a point_acc__ref)) us_rep1
   (point_acc__content a))
 
 (declare-const dummy7 us_rep2)
 
 (declare-datatypes ((route_acc__ref 0))
 (((route_acc__refqtmk (route_acc__content us_rep2)))))
-(define-fun route_acc__ref_route_acc__content__projection ((a route_acc__ref)) us_rep2 
+(define-fun route_acc__ref_route_acc__content__projection ((a route_acc__ref)) us_rep2
   (route_acc__content a))
 
 (declare-datatypes ((us_split_fields2 0))
 (((us_split_fieldsqtmk1
   (rec__test_route__route__current us_rep1)(rec__test_route__route__rest us_rep2)))))
-(define-fun us_split_fields_rec__test_route__route__current__projection ((a us_split_fields2)) us_rep1 
+(define-fun us_split_fields_rec__test_route__route__current__projection ((a us_split_fields2)) us_rep1
   (rec__test_route__route__current a))
 
-(define-fun us_split_fields_rec__test_route__route__rest__projection ((a us_split_fields2)) us_rep2 
+(define-fun us_split_fields_rec__test_route__route__rest__projection ((a us_split_fields2)) us_rep2
   (rec__test_route__route__rest a))
 
 (declare-datatypes ((us_split_fields__ref1 0))
 (((us_split_fields__refqtmk1 (us_split_fields__content1 us_split_fields2)))))
-(define-fun us_split_fields__ref___split_fields__content__2__projection ((a us_split_fields__ref1)) us_split_fields2 
+(define-fun us_split_fields__ref___split_fields__content__2__projection ((a us_split_fields__ref1)) us_split_fields2
   (us_split_fields__content1 a))
 
 (declare-datatypes ((us_rep3 0))
 (((us_repqtmk3 (us_split_fields3 us_split_fields2)))))
-(define-fun us_rep___split_fields__2__projection ((a us_rep3)) us_split_fields2 
+(define-fun us_rep___split_fields__2__projection ((a us_rep3)) us_split_fields2
   (us_split_fields3 a))
 
 (declare-const value__size1 Int)
@@ -280,17 +282,17 @@
 
 (declare-datatypes ((route__ref 0))
 (((route__refqtmk (route__content us_rep3)))))
-(define-fun route__ref_route__content__projection ((a route__ref)) us_rep3 
+(define-fun route__ref_route__content__projection ((a route__ref)) us_rep3
   (route__content a))
 
 (declare-fun us_open (us_main_type) us_rep3)
 
 (declare-fun us_close (us_rep3) us_main_type)
 
-(define-fun rec__test_route__route_acc__pointer_value ((a us_rep2)) us_rep3 
+(define-fun rec__test_route__route_acc__pointer_value ((a us_rep2)) us_rep3
   (us_open (rec__test_route__route_acc__pointer_value_abstr a)))
 
-(define-fun rec__test_route__route_acc__pointer_value__pred ((a us_rep2)) Bool 
+(define-fun rec__test_route__route_acc__pointer_value__pred ((a us_rep2)) Bool
   (not (= (rec__test_route__route_acc__is_null_pointer a) true)))
 
 (declare-const us_null_pointer1 us_rep2)
@@ -304,7 +306,7 @@
 
 (declare-datatypes ((t5b__ref 0))
 (((t5b__refqtmk (t5b__content us_rep2)))))
-(define-fun t5b__ref_t5b__content__projection ((a t5b__ref)) us_rep2 
+(define-fun t5b__ref_t5b__content__projection ((a t5b__ref)) us_rep2
   (t5b__content a))
 
 (declare-fun nth_x (us_rep2 Int) Int)
@@ -342,29 +344,29 @@
 
 (declare-datatypes ((int_array__ref 0))
 (((int_array__refqtmk (int_array__content us_t)))))
-(define-fun int_array__ref_int_array__content__projection ((a int_array__ref)) us_t 
+(define-fun int_array__ref_int_array__content__projection ((a int_array__ref)) us_t
   (int_array__content a))
 
 (declare-const dummy11 us_rep2)
 
 (declare-datatypes ((t9b__ref 0))
 (((t9b__refqtmk (t9b__content us_rep2)))))
-(define-fun t9b__ref_t9b__content__projection ((a t9b__ref)) us_rep2 
+(define-fun t9b__ref_t9b__content__projection ((a t9b__ref)) us_rep2
   (t9b__content a))
 
 
 (declare-const dummy12 us_rep2)
 
 (declare-datatypes ((t21b__ref 0))
 (((t21b__refqtmk (t21b__content us_rep2)))))
-(define-fun t21b__ref_t21b__content__projection ((a t21b__ref)) us_rep2 
+(define-fun t21b__ref_t21b__content__projection ((a t21b__ref)) us_rep2
   (t21b__content a))
 
 (declare-const dummy13 us_rep1)
 
 (declare-datatypes ((t22b__ref 0))
 (((t22b__refqtmk (t22b__content us_rep1)))))
-(define-fun t22b__ref_t22b__content__projection ((a t22b__ref)) us_rep1 
+(define-fun t22b__ref_t22b__content__projection ((a t22b__ref)) us_rep1
   (t22b__content a))
 
 (declare-fun nth_point (us_rep2 Int) us_rep1)
@@ -401,14 +403,14 @@
 
 (declare-datatypes ((t29b__ref 0))
 (((t29b__refqtmk (t29b__content us_rep2)))))
-(define-fun t29b__ref_t29b__content__projection ((a t29b__ref)) us_rep2 
+(define-fun t29b__ref_t29b__content__projection ((a t29b__ref)) us_rep2
   (t29b__content a))
 
 (declare-const dummy15 us_rep1)
 
 (declare-datatypes ((t34b__ref 0))
 (((t34b__refqtmk (t34b__content us_rep1)))))
-(define-fun t34b__ref_t34b__content__projection ((a t34b__ref)) us_rep1 
+(define-fun t34b__ref_t34b__content__projection ((a t34b__ref)) us_rep1
   (t34b__content a))
 
 (declare-const attr__ATTRIBUTE_ADDRESS4 Int)
@@ -476,7 +478,7 @@
         test_route__shift_nth_x__p__assume) (rec__test_route__point_acc__is_null_pointer
                                             temp___brower_235))))
      (= (length temp___borrowed_236) (length o2))))))
-							     
+
 (assert (not (=>
      (and
      (and