From a3f940c14708813018c21792d3e3be3636ca1ebf Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Wed, 28 Feb 2024 13:37:22 -0300 Subject: [PATCH] more disabling --- .../proofs/qgu-fuzz-1-strings-pp.smt2 | 2 + .../cli/regress1/quantifiers/bug822.smt2 | 3 +- .../cli/regress1/quantifiers/bug_743.smt2 | 2 + .../cli/regress1/quantifiers/cdt-0208-to.smt2 | 3 +- .../cli/regress1/quantifiers/cee-npnt-dd.smt2 | 2 + ...ees.adb_1105_16_loop_invariant_init_1.smt2 | 2 + .../regress1/quantifiers/ddatv-delta2.smt2 | 4 +- .../regress1/quantifiers/eqrange_ex_1.smt2 | 2 + .../regress1/quantifiers/f993-loss-easy.smt2 | 4 +- .../regress1/quantifiers/fp-cegqi-unsat.smt2 | 2 + .../quantifiers/ho-seu-sygus-inst.smt2 | 3 +- .../quantifiers/isaplanner-goal20.smt2 | 3 +- .../cli/regress1/quantifiers/issue3481.smt2 | 76 ++++++++++--------- .../regress1/quantifiers/issue3724-quant.smt2 | 2 + .../quantifiers/issue4400-2-already-conf.smt2 | 2 + .../issue4420-order-sensitive.smt2 | 2 + .../quantifiers/issue5288-vts-real-int.smt2 | 2 + .../regress1/quantifiers/issue5471-aext.smt2 | 2 + .../quantifiers/issue5482-rtf-no-fv.smt2 | 2 + .../quantifiers/issue5735-subtypes.smt2 | 2 + .../quantifiers/issue6642-em-types.smt2 | 2 + .../cli/regress1/quantifiers/issue993.smt2 | 6 +- .../quantifiers/issue9989-syqi-nwf.smt2 | 2 + .../cli/regress1/quantifiers/lra-vts-inf.smt2 | 2 + .../quantifiers/min-ppgt-em-incomplete.smt2 | 3 +- .../quantifiers/min-ppgt-em-incomplete2.smt2 | 21 ++--- .../regress1/quantifiers/nl-pow-trick.smt2 | 4 +- .../quantifiers/nra-interleave-inst.smt2 | 2 + .../quantifiers/parametric-lists.smt2 | 2 + ...prenex-scholl-smt08_RNDPRE_RNDPRE_4_6.smt2 | 2 + .../regress1/quantifiers/proj-issue564.smt2 | 2 + .../regress1/quantifiers/proj-issue602.smt2 | 2 + .../quantifiers/quant-wf-int-ind.smt2 | 2 + .../regress1/quantifiers/seq-solved-enum.smt2 | 2 + .../quantifiers/seq-unsolved-ematch.smt2 | 2 + .../seqa-unsat-unknown-110921.smt2 | 2 + .../set-choice-koikonomou.cvc.smt2 | 2 + .../quantifiers/stream-x2014-09-18-unsat.smt2 | 2 + .../quantifiers/sygus-inst-lambda.smt2 | 10 ++- .../quantifiers/tpp-unit-fail-qbv.smt2 | 2 + .../cli/regress1/sep/wand-simp-unsat.smt2 | 2 + .../strings/cee-norn-aes-trivially.smt2 | 2 + .../regress1/strings/instance3303-delta.smt2 | 2 + .../instance6561-dd-concat-unify-char.smt2 | 2 + .../cli/regress1/strings/issue10058.smt2 | 2 + .../cli/regress1/strings/issue10196.smt2 | 3 +- .../cli/regress1/strings/issue2982.smt2 | 2 + .../cli/regress1/strings/issue3090.smt2 | 2 + .../cli/regress1/strings/issue3357.smt2 | 10 ++- .../strings/issue4759-comp-delta.smt2 | 2 + .../issue6057-replace-re-all-jiwonparc.smt2 | 2 + .../strings/issue6180-2-proxy-vars.smt2 | 2 + .../strings/issue6184-unsat-core.smt2 | 2 + .../strings/issue6214-2-sym-re-inc.smt2 | 2 + .../strings/issue6214-3-sym-re-inc.smt2 | 2 + .../strings/issue6214-4-sym-re-inc.smt2 | 2 + .../cli/regress1/strings/issue6271-2-rnf.smt2 | 2 + .../cli/regress1/strings/issue6635-rre.smt2 | 2 + .../strings/issue6973-dup-lemma-conc.smt2 | 2 + .../strings/issue8918-str-nth-crange-red.smt2 | 2 + .../strings/issue9287-trivial-deq-disl.smt2 | 2 + .../regress/cli/regress1/strings/norn-ab.smt2 | 2 + .../cli/regress1/strings/proj-issue331.smt2 | 2 + .../cli/regress1/strings/re-agg-total1.smt2 | 2 + .../cli/regress1/strings/re-agg-total2.smt2 | 2 + .../cli/regress1/strings/re-mod-eq.smt2 | 2 + .../regress1/strings/regexp-strat-fix.smt2 | 2 + .../regress/cli/regress1/strings/rev-ex2.smt2 | 2 + .../regress/cli/regress1/strings/rev-ex3.smt2 | 2 + .../regress/cli/regress1/strings/rev-ex4.smt2 | 2 + .../cli/regress1/strings/seq-cardinality.smt2 | 2 + .../strings/seq-quant-infinite-branch.smt2 | 2 + .../regress1/strings/slent-re-pos-eager.smt2 | 2 + .../strings/strings-leq-trans-unsat.smt2 | 2 + .../cli/regress1/strings/update-ex2.smt2 | 2 + .../strings/username_checker_min.smt2 | 2 + test/regress/cli/regress1/sym/sym5.smt2 | 2 + 77 files changed, 213 insertions(+), 66 deletions(-) diff --git a/test/regress/cli/regress1/proofs/qgu-fuzz-1-strings-pp.smt2 b/test/regress/cli/regress1/proofs/qgu-fuzz-1-strings-pp.smt2 index c0c1f16f712..07e668fe574 100644 --- a/test/regress/cli/regress1/proofs/qgu-fuzz-1-strings-pp.smt2 +++ b/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) diff --git a/test/regress/cli/regress1/quantifiers/bug822.smt2 b/test/regress/cli/regress1/quantifiers/bug822.smt2 index 8bcbb364c13..fe523af94d9 100644 --- a/test/regress/cli/regress1/quantifiers/bug822.smt2 +++ b/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) - diff --git a/test/regress/cli/regress1/quantifiers/bug_743.smt2 b/test/regress/cli/regress1/quantifiers/bug_743.smt2 index 0432509b218..f42b52d8f73 100644 --- a/test/regress/cli/regress1/quantifiers/bug_743.smt2 +++ b/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) diff --git a/test/regress/cli/regress1/quantifiers/cdt-0208-to.smt2 b/test/regress/cli/regress1/quantifiers/cdt-0208-to.smt2 index 5a04e239457..629ace1b700 100644 --- a/test/regress/cli/regress1/quantifiers/cdt-0208-to.smt2 +++ b/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) - diff --git a/test/regress/cli/regress1/quantifiers/cee-npnt-dd.smt2 b/test/regress/cli/regress1/quantifiers/cee-npnt-dd.smt2 index b497ad688a7..256776dd5be 100644 --- a/test/regress/cli/regress1/quantifiers/cee-npnt-dd.smt2 +++ b/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) 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 2253b8cde8c..cd1a88cc552 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,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) diff --git a/test/regress/cli/regress1/quantifiers/ddatv-delta2.smt2 b/test/regress/cli/regress1/quantifiers/ddatv-delta2.smt2 index 7940927ec51..6cd0a0c67b2 100644 --- a/test/regress/cli/regress1/quantifiers/ddatv-delta2.smt2 +++ b/test/regress/cli/regress1/quantifiers/ddatv-delta2.smt2 @@ -1,3 +1,5 @@ +;; Datatypes are not supported in Alethe +; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (declare-sort U 0) @@ -5,7 +7,7 @@ (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) diff --git a/test/regress/cli/regress1/quantifiers/eqrange_ex_1.smt2 b/test/regress/cli/regress1/quantifiers/eqrange_ex_1.smt2 index 5ea87939c4f..1382c0b608e 100644 --- a/test/regress/cli/regress1/quantifiers/eqrange_ex_1.smt2 +++ b/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) diff --git a/test/regress/cli/regress1/quantifiers/f993-loss-easy.smt2 b/test/regress/cli/regress1/quantifiers/f993-loss-easy.smt2 index 775b633384b..c4dfc007bad 100644 --- a/test/regress/cli/regress1/quantifiers/f993-loss-easy.smt2 +++ b/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$)) diff --git a/test/regress/cli/regress1/quantifiers/fp-cegqi-unsat.smt2 b/test/regress/cli/regress1/quantifiers/fp-cegqi-unsat.smt2 index 1fa6225c75c..025bcb344d3 100644 --- a/test/regress/cli/regress1/quantifiers/fp-cegqi-unsat.smt2 +++ b/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) diff --git a/test/regress/cli/regress1/quantifiers/ho-seu-sygus-inst.smt2 b/test/regress/cli/regress1/quantifiers/ho-seu-sygus-inst.smt2 index bb73cdaa3ce..2e633fed748 100644 --- a/test/regress/cli/regress1/quantifiers/ho-seu-sygus-inst.smt2 +++ b/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) - diff --git a/test/regress/cli/regress1/quantifiers/isaplanner-goal20.smt2 b/test/regress/cli/regress1/quantifiers/isaplanner-goal20.smt2 index d3e54e0af6a..ce851c3e4f7 100644 --- a/test/regress/cli/regress1/quantifiers/isaplanner-goal20.smt2 +++ b/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) - diff --git a/test/regress/cli/regress1/quantifiers/issue3481.smt2 b/test/regress/cli/regress1/quantifiers/issue3481.smt2 index 3a8c5350a03..78a006ceb27 100644 --- a/test/regress/cli/regress1/quantifiers/issue3481.smt2 +++ b/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,7 +164,7 @@ (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) @@ -170,18 +172,18 @@ (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)) @@ -189,7 +191,7 @@ (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,14 +344,14 @@ (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)) @@ -357,14 +359,14 @@ (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 diff --git a/test/regress/cli/regress1/quantifiers/issue3724-quant.smt2 b/test/regress/cli/regress1/quantifiers/issue3724-quant.smt2 index 21494ec39cb..1cb94dfb193 100644 --- a/test/regress/cli/regress1/quantifiers/issue3724-quant.smt2 +++ b/test/regress/cli/regress1/quantifiers/issue3724-quant.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --mbqi ; EXPECT: unsat +;; HO not supported in Alethe +; DISABLE-TESTER: alethe (set-logic HO_ALL) (assert (forall ((BOUND_VARIABLE_313 Bool) (BOUND_VARIABLE_314 (-> Int Bool)) (BOUND_VARIABLE_315 (-> Int Int)) (BOUND_VARIABLE_316 Int) (BOUND_VARIABLE_317 (-> Int Bool)) (BOUND_VARIABLE_318 Int)) (! (not (and (not (and (= (ite (and (not (= BOUND_VARIABLE_318 0)) (BOUND_VARIABLE_314 (BOUND_VARIABLE_315 (ite (not (BOUND_VARIABLE_314 0)) 0 (ite BOUND_VARIABLE_313 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (BOUND_VARIABLE_314 0)) 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (or (not BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 (ite (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 9)))))))) (ite (BOUND_VARIABLE_317 (BOUND_VARIABLE_315 (ite (not (BOUND_VARIABLE_314 0)) 0 (ite BOUND_VARIABLE_313 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (BOUND_VARIABLE_314 0)) 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (or (not BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 (ite (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 9))))))) BOUND_VARIABLE_316 0) 0) 0) (not (BOUND_VARIABLE_314 (BOUND_VARIABLE_315 (ite (not (BOUND_VARIABLE_314 0)) 0 (ite BOUND_VARIABLE_313 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (BOUND_VARIABLE_314 0)) 0 (ite (and (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) (or (not BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 (ite (not (or (and BOUND_VARIABLE_313 BOUND_VARIABLE_313) BOUND_VARIABLE_313)) 0 9)))))))))) true)) :pattern (true))) diff --git a/test/regress/cli/regress1/quantifiers/issue4400-2-already-conf.smt2 b/test/regress/cli/regress1/quantifiers/issue4400-2-already-conf.smt2 index b5dc7a598c6..28df68931f8 100644 --- a/test/regress/cli/regress1/quantifiers/issue4400-2-already-conf.smt2 +++ b/test/regress/cli/regress1/quantifiers/issue4400-2-already-conf.smt2 @@ -1,4 +1,6 @@ ; DISABLE-TESTER: alf +;; introduces fresh Skolem in a trusted step +; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (declare-datatypes ((ap 0)) (((bp) (cp (p (_ BitVec 2)) (dp (_ BitVec 2)) diff --git a/test/regress/cli/regress1/quantifiers/issue4420-order-sensitive.smt2 b/test/regress/cli/regress1/quantifiers/issue4420-order-sensitive.smt2 index d30bd563df3..d7378507580 100644 --- a/test/regress/cli/regress1/quantifiers/issue4420-order-sensitive.smt2 +++ b/test/regress/cli/regress1/quantifiers/issue4420-order-sensitive.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --no-jh-rlv-order ; EXPECT: unsat +;; introduces div_by_zero Skolem +; DISABLE-TESTER: alethe (set-logic AUFBVFPDTNIRA) (set-info :status unsat) (set-info :smt-lib-version 2.6) diff --git a/test/regress/cli/regress1/quantifiers/issue5288-vts-real-int.smt2 b/test/regress/cli/regress1/quantifiers/issue5288-vts-real-int.smt2 index d99cb51d0b8..1031c7d9b6a 100644 --- a/test/regress/cli/regress1/quantifiers/issue5288-vts-real-int.smt2 +++ b/test/regress/cli/regress1/quantifiers/issue5288-vts-real-int.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --strings-exp ; EXPECT: unsat +;; introduces div_by_zero Skolem +; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (assert diff --git a/test/regress/cli/regress1/quantifiers/issue5471-aext.smt2 b/test/regress/cli/regress1/quantifiers/issue5471-aext.smt2 index c420359fcce..50324de70bd 100644 --- a/test/regress/cli/regress1/quantifiers/issue5471-aext.smt2 +++ b/test/regress/cli/regress1/quantifiers/issue5471-aext.smt2 @@ -1,3 +1,5 @@ +;; introduces div_by_zero Skolem +; DISABLE-TESTER: alethe (set-logic NRA) (set-option :sygus-inst true) (set-option :strings-exp true) diff --git a/test/regress/cli/regress1/quantifiers/issue5482-rtf-no-fv.smt2 b/test/regress/cli/regress1/quantifiers/issue5482-rtf-no-fv.smt2 index b1e6911cd9c..a617239fc91 100644 --- a/test/regress/cli/regress1/quantifiers/issue5482-rtf-no-fv.smt2 +++ b/test/regress/cli/regress1/quantifiers/issue5482-rtf-no-fv.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --fmf-bound ; EXPECT: unsat +;; introduces div_by_zero Skolem +; DISABLE-TESTER: alethe (set-logic AUFNIA) (declare-fun a () Int) (declare-fun b () (Array Int Int)) diff --git a/test/regress/cli/regress1/quantifiers/issue5735-subtypes.smt2 b/test/regress/cli/regress1/quantifiers/issue5735-subtypes.smt2 index 78eb57c95bb..d42d43a4fcd 100644 --- a/test/regress/cli/regress1/quantifiers/issue5735-subtypes.smt2 +++ b/test/regress/cli/regress1/quantifiers/issue5735-subtypes.smt2 @@ -1,3 +1,5 @@ +;; introduces div_by_zero Skolem +; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (declare-fun a () Bool) diff --git a/test/regress/cli/regress1/quantifiers/issue6642-em-types.smt2 b/test/regress/cli/regress1/quantifiers/issue6642-em-types.smt2 index 19dc1122759..72c0c0792a5 100644 --- a/test/regress/cli/regress1/quantifiers/issue6642-em-types.smt2 +++ b/test/regress/cli/regress1/quantifiers/issue6642-em-types.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --full-saturate-quant ; EXPECT: unsat +;; Logic not supported in Alethe +; DISABLE-TESTER: alethe (set-logic ALL) (declare-fun b () String) (assert (forall ((c (Seq Int))) (exists ((a String)) (and (= 1 (seq.len c)) (not (= b a)))))) diff --git a/test/regress/cli/regress1/quantifiers/issue993.smt2 b/test/regress/cli/regress1/quantifiers/issue993.smt2 index aa0c29f5eea..310ddfe8912 100644 --- a/test/regress/cli/regress1/quantifiers/issue993.smt2 +++ b/test/regress/cli/regress1/quantifiers/issue993.smt2 @@ -1,3 +1,5 @@ +;; Datatypes are not supported in Alethe +; DISABLE-TESTER: alethe (set-logic AUFBVDTNIRA) (set-info :smt-lib-version 2.6) (set-info :status unsat) @@ -10,7 +12,7 @@ (declare-datatypes ((us_split_fields 0)) (((mk___split_fields (rec__unit1__t1__c1 integer) (rec__ext__ us_private))))) (declare-datatypes ((us_split_fields__ref 0)) (((mk___split_fields__ref (us_split_fields__content us_split_fields))))) -(define-fun us_split_fields__ref___projection ((a us_split_fields__ref)) us_split_fields +(define-fun us_split_fields__ref___projection ((a us_split_fields__ref)) us_split_fields (us_split_fields__content a)) (declare-datatypes ((us_rep 0)) (((mk___rep (us_split_fields1 us_split_fields) (attr__tag Int))))) @@ -32,7 +34,7 @@ (declare-datatypes ((us_split_fields2 0)) (((mk___split_fields1 (rec__unit2__t2__c2 integer) (rec__unit1__t1__c11 integer) (rec__ext__1 us_private))))) (declare-datatypes ((us_split_fields__ref1 0)) (((mk___split_fields__ref1 (us_split_fields__content1 us_split_fields2))))) -(define-fun us_split_fields__ref_2__projection ((a us_split_fields__ref1)) us_split_fields2 +(define-fun us_split_fields__ref_2__projection ((a us_split_fields__ref1)) us_split_fields2 (us_split_fields__content1 a)) (declare-datatypes ((us_rep1 0)) (((mk___rep1 (us_split_fields3 us_split_fields2) (attr__tag1 Int))))) diff --git a/test/regress/cli/regress1/quantifiers/issue9989-syqi-nwf.smt2 b/test/regress/cli/regress1/quantifiers/issue9989-syqi-nwf.smt2 index d455629f41d..e5e9a7df90a 100644 --- a/test/regress/cli/regress1/quantifiers/issue9989-syqi-nwf.smt2 +++ b/test/regress/cli/regress1/quantifiers/issue9989-syqi-nwf.smt2 @@ -1,5 +1,7 @@ ; 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/lra-vts-inf.smt2 b/test/regress/cli/regress1/quantifiers/lra-vts-inf.smt2 index 9fb4f7b4476..16ad59de8a9 100644 --- a/test/regress/cli/regress1/quantifiers/lra-vts-inf.smt2 +++ b/test/regress/cli/regress1/quantifiers/lra-vts-inf.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --cegqi-inf-int --cegqi-inf-real ; EXPECT: unsat +;; introduces fresh Skolem in a trusted step +; DISABLE-TESTER: alethe (set-info :smt-lib-version 2.6) (set-logic LRA) (set-info :source | 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 2f86a2764be..9bb8c333cf8 100644 --- a/test/regress/cli/regress1/quantifiers/min-ppgt-em-incomplete.smt2 +++ b/test/regress/cli/regress1/quantifiers/min-ppgt-em-incomplete.smt2 @@ -1,3 +1,5 @@ +;; Datatypes are not supported in Alethe +; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (declare-sort S 0) @@ -22,4 +24,3 @@ (assert (forall ((i Int)) (! (not (s e (j (R (vec (j (R (vec l)) c))) i))) :qid Q2))) (assert (exists ((z Int)) (! (B (b (s e (j (R (vec (j (R (vec (j (R (vec (h (cm a) (t (K (O err) 0 n) 1) (add (D 1))))) r))) c))) z)))) :qid Q3))) (check-sat) - 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 c34fbbee461..67b7bed1ad5 100644 --- a/test/regress/cli/regress1/quantifiers/min-ppgt-em-incomplete2.smt2 +++ b/test/regress/cli/regress1/quantifiers/min-ppgt-em-incomplete2.smt2 @@ -1,3 +1,5 @@ +;; Datatypes are not supported in Alethe +; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (declare-sort U 0) @@ -21,17 +23,16 @@ (assert (forall ((?x0 V) (?x1 Int) (?x2 T)) (! (= ?x2 (s (sto ?x0 ?x1 ?x2) ?x1)) :qid Q2))) (declare-fun k1 () Bool) (declare-fun k2 () Bool) -(assert (and -(is-Vec ex) -(not - (and - (not (= ex E)) - (or - (not (= rdv (b false))) - (not (= ivp (Vec (Var (sto (R (vec cdv)) (|l#Var| (vec cdv)) c) 0)))) - (not (= rdv (b k1))) +(assert (and +(is-Vec ex) +(not + (and + (not (= ex E)) + (or + (not (= rdv (b false))) + (not (= ivp (Vec (Var (sto (R (vec cdv)) (|l#Var| (vec cdv)) c) 0)))) + (not (= rdv (b k1))) (not (B (b k2)))))))) (assert (= k1 (not (forall ((j Int)) (! (not (eq c (s (R (vec ivp)) j))) :qid Q3))))) (assert (= k2 (not (forall (($i_0 Int)) (! (not (B (b (eq c (s (R (vec (s (R (vec (s (R (vec (sel (cm in) (t (mc err) 1) (add (A 0))))) 0))) 0))) $i_0))))) :qid Q4))))) (check-sat) - diff --git a/test/regress/cli/regress1/quantifiers/nl-pow-trick.smt2 b/test/regress/cli/regress1/quantifiers/nl-pow-trick.smt2 index a6dfc9f9260..443a894c7a1 100644 --- a/test/regress/cli/regress1/quantifiers/nl-pow-trick.smt2 +++ b/test/regress/cli/regress1/quantifiers/nl-pow-trick.smt2 @@ -1,12 +1,14 @@ ; COMMAND-LINE: --cegqi-all --no-relational-triggers --no-sygus-inst ; EXPECT: unsat +;; introduces mod_by_zero Skolem +; DISABLE-TESTER: alethe (set-logic NIA) (declare-fun a () Int) (declare-fun b () Int) (declare-fun c () Int) (define-fun s ((x Int)) Int (+ x 1)) (define-fun seq ((a Int) (b Int) (k Int) (x Int)) Bool ( = x (mod (+ 1 (* b (+ 1 k))) a))) -(define-fun power ((a Int) (b Int) (c Int)) Bool +(define-fun power ((a Int) (b Int) (c Int)) Bool (exists ((x Int) (y Int)) (and (seq x y 0 1) (seq x y b c) (forall ((k Int) (z Int)) (=> (and (< k b) (seq x y k z)) (seq x y (+ 1 k) (* a z)))))) ) (assert (power 2 3 8)) diff --git a/test/regress/cli/regress1/quantifiers/nra-interleave-inst.smt2 b/test/regress/cli/regress1/quantifiers/nra-interleave-inst.smt2 index b01860f73b3..a8cd8a21af0 100644 --- a/test/regress/cli/regress1/quantifiers/nra-interleave-inst.smt2 +++ b/test/regress/cli/regress1/quantifiers/nra-interleave-inst.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --cegqi-multi-inst ; EXPECT: unsat +;; introduces div_by_zero Skolem +; DISABLE-TESTER: alethe (set-info :smt-lib-version 2.6) (set-logic NRA) (set-info :status unsat) diff --git a/test/regress/cli/regress1/quantifiers/parametric-lists.smt2 b/test/regress/cli/regress1/quantifiers/parametric-lists.smt2 index 89744cded09..6f1e988e0ff 100644 --- a/test/regress/cli/regress1/quantifiers/parametric-lists.smt2 +++ b/test/regress/cli/regress1/quantifiers/parametric-lists.smt2 @@ -1,5 +1,7 @@ ; 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))))) diff --git a/test/regress/cli/regress1/quantifiers/prenex-scholl-smt08_RNDPRE_RNDPRE_4_6.smt2 b/test/regress/cli/regress1/quantifiers/prenex-scholl-smt08_RNDPRE_RNDPRE_4_6.smt2 index f0a4560d1ee..4f1e4378f87 100644 --- a/test/regress/cli/regress1/quantifiers/prenex-scholl-smt08_RNDPRE_RNDPRE_4_6.smt2 +++ b/test/regress/cli/regress1/quantifiers/prenex-scholl-smt08_RNDPRE_RNDPRE_4_6.smt2 @@ -1,3 +1,5 @@ +;; introduces fresh Skolem in a trusted step +; DISABLE-TESTER: alethe (set-info :smt-lib-version 2.6) (set-logic LRA) (set-info :source | diff --git a/test/regress/cli/regress1/quantifiers/proj-issue564.smt2 b/test/regress/cli/regress1/quantifiers/proj-issue564.smt2 index 05623bd6a6b..a070290d798 100644 --- a/test/regress/cli/regress1/quantifiers/proj-issue564.smt2 +++ b/test/regress/cli/regress1/quantifiers/proj-issue564.smt2 @@ -1,5 +1,7 @@ ; EXPECT: unsat ; DISABLE-TESTER: lfsc +;; Logic not supported in Alethe +; DISABLE-TESTER: alethe (set-logic ALL) (set-option :sets-ext true) (set-option :ieval use-learn) diff --git a/test/regress/cli/regress1/quantifiers/proj-issue602.smt2 b/test/regress/cli/regress1/quantifiers/proj-issue602.smt2 index 902301b52fd..58c9bc33599 100644 --- a/test/regress/cli/regress1/quantifiers/proj-issue602.smt2 +++ b/test/regress/cli/regress1/quantifiers/proj-issue602.smt2 @@ -1,4 +1,6 @@ ; EXPECT: unsat +;; Logic not supported in Alethe +; DISABLE-TESTER: alethe (set-logic ALL) (set-option :ieval use) (assert (forall ((x RoundingMode)) (distinct (= RTZ x) (distinct x roundNearestTiesToEven)))) diff --git a/test/regress/cli/regress1/quantifiers/quant-wf-int-ind.smt2 b/test/regress/cli/regress1/quantifiers/quant-wf-int-ind.smt2 index 49ca4ffc507..536d559f127 100644 --- a/test/regress/cli/regress1/quantifiers/quant-wf-int-ind.smt2 +++ b/test/regress/cli/regress1/quantifiers/quant-wf-int-ind.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --int-wf-ind ; EXPECT: unsat +;; introduces fresh Skolem in a trusted step +; DISABLE-TESTER: alethe (set-logic UFLIA) (declare-fun P (Int) Bool) (assert (forall ((x Int)) (=> (P x) (P (+ x 1))))) diff --git a/test/regress/cli/regress1/quantifiers/seq-solved-enum.smt2 b/test/regress/cli/regress1/quantifiers/seq-solved-enum.smt2 index cff3d3ca0a2..7bfc3e75adf 100644 --- a/test/regress/cli/regress1/quantifiers/seq-solved-enum.smt2 +++ b/test/regress/cli/regress1/quantifiers/seq-solved-enum.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --strings-exp --full-saturate-quant ; EXPECT: unsat +;; Logic not supported in Alethe +; DISABLE-TESTER: alethe (set-logic ALL) (declare-fun s () (Seq Int)) diff --git a/test/regress/cli/regress1/quantifiers/seq-unsolved-ematch.smt2 b/test/regress/cli/regress1/quantifiers/seq-unsolved-ematch.smt2 index 044607dfecf..e19ccfb9f58 100644 --- a/test/regress/cli/regress1/quantifiers/seq-unsolved-ematch.smt2 +++ b/test/regress/cli/regress1/quantifiers/seq-unsolved-ematch.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --strings-exp --full-saturate-quant ; EXPECT: unsat +;; Logic not supported in Alethe +; DISABLE-TESTER: alethe (set-logic ALL) (declare-fun s () (Seq Int)) diff --git a/test/regress/cli/regress1/quantifiers/seqa-unsat-unknown-110921.smt2 b/test/regress/cli/regress1/quantifiers/seqa-unsat-unknown-110921.smt2 index b50d6dd25cf..8a6a821d65c 100644 --- a/test/regress/cli/regress1/quantifiers/seqa-unsat-unknown-110921.smt2 +++ b/test/regress/cli/regress1/quantifiers/seqa-unsat-unknown-110921.smt2 @@ -2,6 +2,8 @@ ; DISABLE-TESTER: alf ; COMMAND-LINE: --strings-exp --seq-array=eager ; EXPECT: unsat +;; Logic not supported in Alethe +; DISABLE-TESTER: alethe (set-logic ALL) (declare-sort T 0) (declare-sort T@ 0) diff --git a/test/regress/cli/regress1/quantifiers/set-choice-koikonomou.cvc.smt2 b/test/regress/cli/regress1/quantifiers/set-choice-koikonomou.cvc.smt2 index 8e5598b6c1b..77be19f9183 100644 --- a/test/regress/cli/regress1/quantifiers/set-choice-koikonomou.cvc.smt2 +++ b/test/regress/cli/regress1/quantifiers/set-choice-koikonomou.cvc.smt2 @@ -1,4 +1,6 @@ ; EXPECT: unsat +;; Logic not supported in Alethe +; DISABLE-TESTER: alethe (set-logic ALL) (set-option :incremental false) (set-option :finite-model-find true) diff --git a/test/regress/cli/regress1/quantifiers/stream-x2014-09-18-unsat.smt2 b/test/regress/cli/regress1/quantifiers/stream-x2014-09-18-unsat.smt2 index 953589cc97b..5360a6bfc39 100644 --- a/test/regress/cli/regress1/quantifiers/stream-x2014-09-18-unsat.smt2 +++ b/test/regress/cli/regress1/quantifiers/stream-x2014-09-18-unsat.smt2 @@ -1,4 +1,6 @@ ; EXPECT: unsat +;; introduces fresh Skolem in a trusted step +; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (declare-sort A$ 0) diff --git a/test/regress/cli/regress1/quantifiers/sygus-inst-lambda.smt2 b/test/regress/cli/regress1/quantifiers/sygus-inst-lambda.smt2 index 8ab3bcef052..f7dd5e311c5 100644 --- a/test/regress/cli/regress1/quantifiers/sygus-inst-lambda.smt2 +++ b/test/regress/cli/regress1/quantifiers/sygus-inst-lambda.smt2 @@ -1,16 +1,18 @@ ; COMMAND-LINE: --sygus-inst ; EXPECT: unsat +;; HO not supported in Alethe +; DISABLE-TESTER: alethe (set-logic HO_ALL) (define-sort a () Int) (declare-fun z ((-> a a)) a) (declare-fun g (a) Bool) -(assert - (forall ((H (-> a a))) +(assert + (forall ((H (-> a a))) (g (z H)) ) ) -(assert - (forall ((H (-> a a))) +(assert + (forall ((H (-> a a))) (not (g (H (z H)))) ) ) diff --git a/test/regress/cli/regress1/quantifiers/tpp-unit-fail-qbv.smt2 b/test/regress/cli/regress1/quantifiers/tpp-unit-fail-qbv.smt2 index 0b46717ec5b..50a4e17298f 100644 --- a/test/regress/cli/regress1/quantifiers/tpp-unit-fail-qbv.smt2 +++ b/test/regress/cli/regress1/quantifiers/tpp-unit-fail-qbv.smt2 @@ -1,4 +1,6 @@ ; DISABLE-TESTER: lfsc +;; unsupported bitblasting of bvurem +; DISABLE-TESTER: alethe (set-logic BV) (set-info :status unsat) (declare-fun t () (_ BitVec 4)) diff --git a/test/regress/cli/regress1/sep/wand-simp-unsat.smt2 b/test/regress/cli/regress1/sep/wand-simp-unsat.smt2 index b974b9a3207..af70c82b70e 100644 --- a/test/regress/cli/regress1/sep/wand-simp-unsat.smt2 +++ b/test/regress/cli/regress1/sep/wand-simp-unsat.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: ; EXPECT: unsat +;; Logic not supported in Alethe +; DISABLE-TESTER: alethe (set-logic QF_ALL) (declare-fun x () Int) (declare-heap (Int Int)) diff --git a/test/regress/cli/regress1/strings/cee-norn-aes-trivially.smt2 b/test/regress/cli/regress1/strings/cee-norn-aes-trivially.smt2 index 5d59358c8ae..d4b48bf27e5 100644 --- a/test/regress/cli/regress1/strings/cee-norn-aes-trivially.smt2 +++ b/test/regress/cli/regress1/strings/cee-norn-aes-trivially.smt2 @@ -1,6 +1,8 @@ ; COMMAND-LINE: --arith-eq-solver --ee-mode=distributed --strings-exp ; COMMAND-LINE: --arith-eq-solver --ee-mode=central --strings-exp ; EXPECT: unsat +;; introduces RE Skolem +; DISABLE-TESTER: alethe (set-logic ALL) (declare-fun v () String) (assert (str.in_re (str.++ "" v) (re.* (str.to_re "z")))) diff --git a/test/regress/cli/regress1/strings/instance3303-delta.smt2 b/test/regress/cli/regress1/strings/instance3303-delta.smt2 index b4297477449..0c9a706162b 100644 --- a/test/regress/cli/regress1/strings/instance3303-delta.smt2 +++ b/test/regress/cli/regress1/strings/instance3303-delta.smt2 @@ -1,3 +1,5 @@ +;; introduces RE Skolem +; DISABLE-TESTER: alethe (set-logic QF_S) (set-info :status unsat) (declare-const X String) diff --git a/test/regress/cli/regress1/strings/instance6561-dd-concat-unify-char.smt2 b/test/regress/cli/regress1/strings/instance6561-dd-concat-unify-char.smt2 index 13bb64e5c8e..f6f75dbb556 100644 --- a/test/regress/cli/regress1/strings/instance6561-dd-concat-unify-char.smt2 +++ b/test/regress/cli/regress1/strings/instance6561-dd-concat-unify-char.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --strings-exp ; EXPECT: unsat +;; introduces RE Skolem +; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (declare-const X String) diff --git a/test/regress/cli/regress1/strings/issue10058.smt2 b/test/regress/cli/regress1/strings/issue10058.smt2 index 78da2256aa6..ad37f142d89 100644 --- a/test/regress/cli/regress1/strings/issue10058.smt2 +++ b/test/regress/cli/regress1/strings/issue10058.smt2 @@ -1,3 +1,5 @@ +;; introduces STRINGS_OCCUR_INDEX Skolem +; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (assert (distinct false (exists ((v String)) (distinct true (str.< (str.replace_all v v "") (str.replace (str.++ v "fi") "fi" "if")))))) diff --git a/test/regress/cli/regress1/strings/issue10196.smt2 b/test/regress/cli/regress1/strings/issue10196.smt2 index 90fd061f8bd..eb2280ef31c 100644 --- a/test/regress/cli/regress1/strings/issue10196.smt2 +++ b/test/regress/cli/regress1/strings/issue10196.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --sygus-inst ; EXPECT: unsat +;; unsupported str.to_upper operator +; DISABLE-TESTER: alethe (set-logic QF_SLIA) (declare-const x Bool) (declare-fun T () String) @@ -7,4 +9,3 @@ (assert (= (str.++ v v) (str.to_upper (str.to_lower T)))) (assert (= T (str.++ "b" (ite x "_" (str.replace_re_all "c" re.allchar T))))) (check-sat) - diff --git a/test/regress/cli/regress1/strings/issue2982.smt2 b/test/regress/cli/regress1/strings/issue2982.smt2 index 289ea093126..b3b55c0fe82 100644 --- a/test/regress/cli/regress1/strings/issue2982.smt2 +++ b/test/regress/cli/regress1/strings/issue2982.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --strings-exp --re-elim=agg ; EXPECT: unsat +;; introduces fresh Skolem in a trusted step +; DISABLE-TESTER: alethe (set-logic QF_SLIA) (declare-fun var_0 () String) diff --git a/test/regress/cli/regress1/strings/issue3090.smt2 b/test/regress/cli/regress1/strings/issue3090.smt2 index dc89ea65030..5ad12863262 100644 --- a/test/regress/cli/regress1/strings/issue3090.smt2 +++ b/test/regress/cli/regress1/strings/issue3090.smt2 @@ -1,3 +1,5 @@ +;; introduces RE Skolem +; DISABLE-TESTER: alethe (set-logic ALL) (set-option :strings-exp true) (set-info :status unsat) diff --git a/test/regress/cli/regress1/strings/issue3357.smt2 b/test/regress/cli/regress1/strings/issue3357.smt2 index ca80f7f8175..f9fcf2cbe3e 100644 --- a/test/regress/cli/regress1/strings/issue3357.smt2 +++ b/test/regress/cli/regress1/strings/issue3357.smt2 @@ -1,3 +1,5 @@ +;; introduces RE Skolem +; DISABLE-TESTER: alethe (set-logic ALL) (set-option :strings-exp true) (set-info :status unsat) @@ -8,10 +10,10 @@ (declare-const g String) (declare-const e String) (declare-const f String) -(assert (or - (and (= d (str.++ e g)) (str.in_re e (re.* (str.to_re "HG4"))) (> 0 (str.to_int g)) (= 1 (str.len e)) (= 2 (str.len (str.substr b 0 (str.len d))))) - (and - (str.in_re (str.replace (str.replace a c "") "T" "") (re.* (re.union (str.to_re "a") (str.to_re "")))) +(assert (or + (and (= d (str.++ e g)) (str.in_re e (re.* (str.to_re "HG4"))) (> 0 (str.to_int g)) (= 1 (str.len e)) (= 2 (str.len (str.substr b 0 (str.len d))))) + (and + (str.in_re (str.replace (str.replace a c "") "T" "") (re.* (re.union (str.to_re "a") (str.to_re "")))) (= 0 (str.to_int (str.replace (str.replace a c "") "T" ""))))) ) (assert (= b (str.++ d f))) diff --git a/test/regress/cli/regress1/strings/issue4759-comp-delta.smt2 b/test/regress/cli/regress1/strings/issue4759-comp-delta.smt2 index 2b6d73279e2..68f9264afe2 100644 --- a/test/regress/cli/regress1/strings/issue4759-comp-delta.smt2 +++ b/test/regress/cli/regress1/strings/issue4759-comp-delta.smt2 @@ -1,3 +1,5 @@ +;; introduces RE Skolem +; DISABLE-TESTER: alethe (set-logic QF_S) (set-info :status unsat) (declare-fun a () String) diff --git a/test/regress/cli/regress1/strings/issue6057-replace-re-all-jiwonparc.smt2 b/test/regress/cli/regress1/strings/issue6057-replace-re-all-jiwonparc.smt2 index c9d93d02447..73090a1218f 100644 --- a/test/regress/cli/regress1/strings/issue6057-replace-re-all-jiwonparc.smt2 +++ b/test/regress/cli/regress1/strings/issue6057-replace-re-all-jiwonparc.smt2 @@ -1,4 +1,6 @@ ; COMMAND-LINE: --strings-exp +;; introduces RE Skolem +; DISABLE-TESTER: alethe (set-logic QF_SLIA) (declare-fun a () String) ; A complicated way of saying a = "b" diff --git a/test/regress/cli/regress1/strings/issue6180-2-proxy-vars.smt2 b/test/regress/cli/regress1/strings/issue6180-2-proxy-vars.smt2 index eb991433fec..40167ead79c 100644 --- a/test/regress/cli/regress1/strings/issue6180-2-proxy-vars.smt2 +++ b/test/regress/cli/regress1/strings/issue6180-2-proxy-vars.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --strings-exp ; EXPECT: unsat +;; unsupported str.update operator +; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (declare-fun a () String) diff --git a/test/regress/cli/regress1/strings/issue6184-unsat-core.smt2 b/test/regress/cli/regress1/strings/issue6184-unsat-core.smt2 index 8dcfe81f891..04c9a84209f 100644 --- a/test/regress/cli/regress1/strings/issue6184-unsat-core.smt2 +++ b/test/regress/cli/regress1/strings/issue6184-unsat-core.smt2 @@ -4,6 +4,8 @@ ;; The second command line option is to test unsat core checking with ;; proofs, which at one point had issues for this benchmark due to ;; cycle detection in LazyCDProofChain +;; Logic not supported in Alethe +; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (set-option :check-unsat-cores true) diff --git a/test/regress/cli/regress1/strings/issue6214-2-sym-re-inc.smt2 b/test/regress/cli/regress1/strings/issue6214-2-sym-re-inc.smt2 index 0e74394eedf..b2401baeee8 100644 --- a/test/regress/cli/regress1/strings/issue6214-2-sym-re-inc.smt2 +++ b/test/regress/cli/regress1/strings/issue6214-2-sym-re-inc.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --strings-exp ; EXPECT: unsat +;; introduces RE Skolem +; DISABLE-TESTER: alethe (set-logic ALL) (declare-fun a () String) (declare-fun b () String) diff --git a/test/regress/cli/regress1/strings/issue6214-3-sym-re-inc.smt2 b/test/regress/cli/regress1/strings/issue6214-3-sym-re-inc.smt2 index c203c256f50..79bd6b80070 100644 --- a/test/regress/cli/regress1/strings/issue6214-3-sym-re-inc.smt2 +++ b/test/regress/cli/regress1/strings/issue6214-3-sym-re-inc.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --strings-exp ; EXPECT: unsat +;; introduces fresh Skolem in a trusted step +; DISABLE-TESTER: alethe (set-logic ALL) (declare-fun a () String) (declare-fun b () String) diff --git a/test/regress/cli/regress1/strings/issue6214-4-sym-re-inc.smt2 b/test/regress/cli/regress1/strings/issue6214-4-sym-re-inc.smt2 index c203c256f50..79bd6b80070 100644 --- a/test/regress/cli/regress1/strings/issue6214-4-sym-re-inc.smt2 +++ b/test/regress/cli/regress1/strings/issue6214-4-sym-re-inc.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --strings-exp ; EXPECT: unsat +;; introduces fresh Skolem in a trusted step +; DISABLE-TESTER: alethe (set-logic ALL) (declare-fun a () String) (declare-fun b () String) diff --git a/test/regress/cli/regress1/strings/issue6271-2-rnf.smt2 b/test/regress/cli/regress1/strings/issue6271-2-rnf.smt2 index 78832216605..2c52a32ce85 100644 --- a/test/regress/cli/regress1/strings/issue6271-2-rnf.smt2 +++ b/test/regress/cli/regress1/strings/issue6271-2-rnf.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --strings-exp ; EXPECT: unsat +;; introduces RE Skolem +; DISABLE-TESTER: alethe (set-logic ALL) (declare-fun str4 () String) (declare-fun str5 () String) diff --git a/test/regress/cli/regress1/strings/issue6635-rre.smt2 b/test/regress/cli/regress1/strings/issue6635-rre.smt2 index 368b4fc87f5..6fafe8438a6 100644 --- a/test/regress/cli/regress1/strings/issue6635-rre.smt2 +++ b/test/regress/cli/regress1/strings/issue6635-rre.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --strings-exp --re-elim=agg ; EXPECT: unsat +;; introduces RE Skolem +; DISABLE-TESTER: alethe (set-logic ALL) (declare-fun a () String) (assert (str.in_re (str.replace_re a (re.++ (str.to_re "A") (re.union (str.to_re "") (str.to_re (str.from_code (str.len a))))) "AB") (re.+ (str.to_re "A")))) diff --git a/test/regress/cli/regress1/strings/issue6973-dup-lemma-conc.smt2 b/test/regress/cli/regress1/strings/issue6973-dup-lemma-conc.smt2 index c6fa580f00e..1826bbc21be 100644 --- a/test/regress/cli/regress1/strings/issue6973-dup-lemma-conc.smt2 +++ b/test/regress/cli/regress1/strings/issue6973-dup-lemma-conc.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --strings-exp ; COMMAND-LINE: --strings-exp --re-elim=agg +;; introduces RE Skolem +; DISABLE-TESTER: alethe (set-logic QF_SLIA) (set-info :status unsat) (declare-fun a () String) diff --git a/test/regress/cli/regress1/strings/issue8918-str-nth-crange-red.smt2 b/test/regress/cli/regress1/strings/issue8918-str-nth-crange-red.smt2 index 168648a4fe5..2a6609ec5c3 100644 --- a/test/regress/cli/regress1/strings/issue8918-str-nth-crange-red.smt2 +++ b/test/regress/cli/regress1/strings/issue8918-str-nth-crange-red.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --strings-exp --no-strings-lazy-pp ; EXPECT: unsat +;; introduces STRINGS_STOI_NON_DIGIT Skolem +; DISABLE-TESTER: alethe (set-logic ALL) (declare-fun a () String) (assert (<= (str.to_int (str.++ "0" (str.from_int (ite (str.prefixof "-" (str.at a 2)) 0 (str.to_int (str.at a 2)))))) (- 1))) diff --git a/test/regress/cli/regress1/strings/issue9287-trivial-deq-disl.smt2 b/test/regress/cli/regress1/strings/issue9287-trivial-deq-disl.smt2 index 2c02546b502..28aaf0665e2 100644 --- a/test/regress/cli/regress1/strings/issue9287-trivial-deq-disl.smt2 +++ b/test/regress/cli/regress1/strings/issue9287-trivial-deq-disl.smt2 @@ -1,4 +1,6 @@ ; EXPECT: unsat +;; introduces STRINGS_REPLACE_ALL_RESULT Skolem +; DISABLE-TESTER: alethe (set-logic QF_S) (declare-fun v () String) (assert (distinct true (str.< (str.replace (str.replace_all v v "") (str.++ v "fi") (str.from_int 0)) (str.to_lower (str.replace (str.++ v "fi") "fi" (str.rev "fi")))))) diff --git a/test/regress/cli/regress1/strings/norn-ab.smt2 b/test/regress/cli/regress1/strings/norn-ab.smt2 index 6109a01dd66..a42659834a5 100644 --- a/test/regress/cli/regress1/strings/norn-ab.smt2 +++ b/test/regress/cli/regress1/strings/norn-ab.smt2 @@ -1,3 +1,5 @@ +;; introduces RE Skolem +; DISABLE-TESTER: alethe (set-info :smt-lib-version 2.6) (set-logic SLIA) (set-info :status unsat) diff --git a/test/regress/cli/regress1/strings/proj-issue331.smt2 b/test/regress/cli/regress1/strings/proj-issue331.smt2 index 49ceea42bb7..e9b06bb7d56 100644 --- a/test/regress/cli/regress1/strings/proj-issue331.smt2 +++ b/test/regress/cli/regress1/strings/proj-issue331.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --strings-exp ; EXPECT: unsat +;; introduces STRINGS_ITOS_RESULT Skolem +; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (declare-const x Int) diff --git a/test/regress/cli/regress1/strings/re-agg-total1.smt2 b/test/regress/cli/regress1/strings/re-agg-total1.smt2 index 8090d650877..a8fc8aee47d 100644 --- a/test/regress/cli/regress1/strings/re-agg-total1.smt2 +++ b/test/regress/cli/regress1/strings/re-agg-total1.smt2 @@ -1,3 +1,5 @@ +;; introduces fresh Skolem in a trusted step +; DISABLE-TESTER: alethe (set-info :smt-lib-version 2.6) (set-logic QF_SLIA) (set-info :status unsat) diff --git a/test/regress/cli/regress1/strings/re-agg-total2.smt2 b/test/regress/cli/regress1/strings/re-agg-total2.smt2 index f1bad3defdb..a98d3544456 100644 --- a/test/regress/cli/regress1/strings/re-agg-total2.smt2 +++ b/test/regress/cli/regress1/strings/re-agg-total2.smt2 @@ -1,3 +1,5 @@ +;; introduces fresh Skolem in a trusted step +; DISABLE-TESTER: alethe (set-info :smt-lib-version 2.6) (set-logic ALL) (set-info :status unsat) diff --git a/test/regress/cli/regress1/strings/re-mod-eq.smt2 b/test/regress/cli/regress1/strings/re-mod-eq.smt2 index ff20ec9d47b..b9007cbb177 100644 --- a/test/regress/cli/regress1/strings/re-mod-eq.smt2 +++ b/test/regress/cli/regress1/strings/re-mod-eq.smt2 @@ -1,3 +1,5 @@ +;; introduces RE Skolem +; DISABLE-TESTER: alethe (set-info :smt-lib-version 2.6) (set-logic QF_SLIA) (set-option :strings-exp true) diff --git a/test/regress/cli/regress1/strings/regexp-strat-fix.smt2 b/test/regress/cli/regress1/strings/regexp-strat-fix.smt2 index 34977466321..3b4ab43b60a 100644 --- a/test/regress/cli/regress1/strings/regexp-strat-fix.smt2 +++ b/test/regress/cli/regress1/strings/regexp-strat-fix.smt2 @@ -1,3 +1,5 @@ +;; introduces RE Skolem +; DISABLE-TESTER: alethe (set-info :smt-lib-version 2.6) (set-logic QF_S) (set-info :status unsat) diff --git a/test/regress/cli/regress1/strings/rev-ex2.smt2 b/test/regress/cli/regress1/strings/rev-ex2.smt2 index 163785bdcbc..1b65bb95b1d 100644 --- a/test/regress/cli/regress1/strings/rev-ex2.smt2 +++ b/test/regress/cli/regress1/strings/rev-ex2.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --strings-exp ; EXPECT: unsat +;; unsupported str.rev operator +; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (declare-fun x () String) diff --git a/test/regress/cli/regress1/strings/rev-ex3.smt2 b/test/regress/cli/regress1/strings/rev-ex3.smt2 index e317191ad33..562f9c974b7 100644 --- a/test/regress/cli/regress1/strings/rev-ex3.smt2 +++ b/test/regress/cli/regress1/strings/rev-ex3.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --strings-exp ; EXPECT: unsat +;; unsupported str.rev operator +; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (declare-fun x () String) diff --git a/test/regress/cli/regress1/strings/rev-ex4.smt2 b/test/regress/cli/regress1/strings/rev-ex4.smt2 index a3eed8e351f..9f8bdc9777d 100644 --- a/test/regress/cli/regress1/strings/rev-ex4.smt2 +++ b/test/regress/cli/regress1/strings/rev-ex4.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --strings-exp --strings-fmf ; EXPECT: unsat +;; unsupported str.rev operator +; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (declare-fun x () String) diff --git a/test/regress/cli/regress1/strings/seq-cardinality.smt2 b/test/regress/cli/regress1/strings/seq-cardinality.smt2 index 93a4985d4e4..fd3cbd7a7b8 100644 --- a/test/regress/cli/regress1/strings/seq-cardinality.smt2 +++ b/test/regress/cli/regress1/strings/seq-cardinality.smt2 @@ -1,3 +1,5 @@ +;; Logic not supported in Alethe +; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (declare-fun x () (Seq (_ BitVec 1))) diff --git a/test/regress/cli/regress1/strings/seq-quant-infinite-branch.smt2 b/test/regress/cli/regress1/strings/seq-quant-infinite-branch.smt2 index 9816301d419..33dd9797939 100644 --- a/test/regress/cli/regress1/strings/seq-quant-infinite-branch.smt2 +++ b/test/regress/cli/regress1/strings/seq-quant-infinite-branch.smt2 @@ -1,3 +1,5 @@ +;; Logic not supported in Alethe +; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (declare-const x8 Bool) diff --git a/test/regress/cli/regress1/strings/slent-re-pos-eager.smt2 b/test/regress/cli/regress1/strings/slent-re-pos-eager.smt2 index 108b4ab4827..43c44f50a33 100644 --- a/test/regress/cli/regress1/strings/slent-re-pos-eager.smt2 +++ b/test/regress/cli/regress1/strings/slent-re-pos-eager.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --strings-re-posc-eager ; EXPECT: unsat +;; introduces RE Skolem +; DISABLE-TESTER: alethe (set-logic QF_SLIA) (set-info :status unsat) (declare-fun sigmaStar_safe_50 () String) diff --git a/test/regress/cli/regress1/strings/strings-leq-trans-unsat.smt2 b/test/regress/cli/regress1/strings/strings-leq-trans-unsat.smt2 index c5188e27dd4..3f1ba914d20 100644 --- a/test/regress/cli/regress1/strings/strings-leq-trans-unsat.smt2 +++ b/test/regress/cli/regress1/strings/strings-leq-trans-unsat.smt2 @@ -2,6 +2,8 @@ ; EXPECT: unsat ; DISABLE-TESTER: unsat-core ; timeout with unsat cores +;; introduces fresh Skolem in a trusted step +; DISABLE-TESTER: alethe (set-logic QF_SLIA) (set-info :status unsat) (declare-fun x () String) diff --git a/test/regress/cli/regress1/strings/update-ex2.smt2 b/test/regress/cli/regress1/strings/update-ex2.smt2 index dedba68b26d..70f4b6810a1 100644 --- a/test/regress/cli/regress1/strings/update-ex2.smt2 +++ b/test/regress/cli/regress1/strings/update-ex2.smt2 @@ -1,3 +1,5 @@ +;; unsupported str.update operator +; DISABLE-TESTER: alethe (set-logic QF_SLIA) (set-option :strings-exp true) (set-info :status unsat) diff --git a/test/regress/cli/regress1/strings/username_checker_min.smt2 b/test/regress/cli/regress1/strings/username_checker_min.smt2 index c4c21dface0..a6dcb754a14 100644 --- a/test/regress/cli/regress1/strings/username_checker_min.smt2 +++ b/test/regress/cli/regress1/strings/username_checker_min.smt2 @@ -1,3 +1,5 @@ +;; introduces RE Skolem +; DISABLE-TESTER: alethe (set-info :smt-lib-version 2.6) (set-logic QF_S) (set-option :strings-exp true) diff --git a/test/regress/cli/regress1/sym/sym5.smt2 b/test/regress/cli/regress1/sym/sym5.smt2 index 16b44d11554..fc44104d50b 100644 --- a/test/regress/cli/regress1/sym/sym5.smt2 +++ b/test/regress/cli/regress1/sym/sym5.smt2 @@ -1,3 +1,5 @@ +;; Logic not supported in Alethe +; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (declare-fun A () (Set Int))