lots of disabling

HanielB · Feb 27, 2024 · f8efd04 · f8efd04
1 parent 49b03c6
commit f8efd04
Show file tree

Hide file tree

Showing 184 changed files with 506 additions and 143 deletions.
diff --git a/test/regress/cli/regress1/arith/div.03.smt2 b/test/regress/cli/regress1/arith/div.03.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; introduces div_by_zero Skolem
+; DISABLE-TESTER: alethe
 (set-logic QF_NIA)
 (set-info :smt-lib-version 2.6)
 (set-info :status unsat)

diff --git a/test/regress/cli/regress1/arith/div.08.smt2 b/test/regress/cli/regress1/arith/div.08.smt2
@@ -1,3 +1,5 @@
+;; introduces div_by_zero Skolem
+; DISABLE-TESTER: alethe
 (set-logic QF_NIA)
 (set-info :smt-lib-version 2.6)
 (set-info :status unsat)

diff --git a/test/regress/cli/regress1/arith/mod.02.smt2 b/test/regress/cli/regress1/arith/mod.02.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; introduces mod_by_zero Skolem
+; DISABLE-TESTER: alethe
 (set-logic QF_NIA)
 (set-info :smt-lib-version 2.6)
 (set-info :status unsat)

diff --git a/test/regress/cli/regress1/aufbv/bug348.smtv1.smt2 b/test/regress/cli/regress1/aufbv/bug348.smtv1.smt2
@@ -1,5 +1,7 @@
 ; DISABLE-TESTER: lfsc
 ; COMMAND-LINE: --bv-solver=bitblast
+;; introduces arrays Skolem
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-info :status unsat)
 (set-logic QF_AUFBV)

diff --git a/test/regress/cli/regress1/bags/card3.smt2 b/test/regress/cli/regress1/bags/card3.smt2
@@ -1,3 +1,5 @@
+;; Bags 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/bags/choose2.smt2 b/test/regress/cli/regress1/bags/choose2.smt2
@@ -1,3 +1,5 @@
+;; Bags are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun A () (Bag Int))

diff --git a/test/regress/cli/regress1/bags/duplicate_removal2.smt2 b/test/regress/cli/regress1/bags/duplicate_removal2.smt2
@@ -1,3 +1,5 @@
+;; Bags are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun A () (Bag String))

diff --git a/test/regress/cli/regress1/bags/emptybag1.smt2 b/test/regress/cli/regress1/bags/emptybag1.smt2
@@ -1,3 +1,5 @@
+;; Bags are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun A () (Bag String))

diff --git a/test/regress/cli/regress1/bags/filter3.smt2 b/test/regress/cli/regress1/bags/filter3.smt2
@@ -1,3 +1,5 @@
+;; Bags are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic HO_ALL)
 (set-info :status unsat)
 (set-option :fmf-bound true)

diff --git a/test/regress/cli/regress1/bags/filter4.smt2 b/test/regress/cli/regress1/bags/filter4.smt2
@@ -1,3 +1,5 @@
+;; Bags are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic HO_ALL)
 (set-info :status unsat)
 (declare-fun A () (Bag Int))

diff --git a/test/regress/cli/regress1/bags/filter5.smt2 b/test/regress/cli/regress1/bags/filter5.smt2
@@ -1,3 +1,5 @@
+;; Bags are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic HO_ALL)
 (set-info :status unsat)
 (declare-fun A () (Bag Int))

diff --git a/test/regress/cli/regress1/bags/fol_0000119.smt2 b/test/regress/cli/regress1/bags/fol_0000119.smt2
@@ -1,3 +1,5 @@
+;; Bags are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 
 (set-option :fmf-bound true)

diff --git a/test/regress/cli/regress1/bags/intersection_min2.smt2 b/test/regress/cli/regress1/bags/intersection_min2.smt2
@@ -1,3 +1,5 @@
+;; Bags are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun A () (Bag String))

diff --git a/test/regress/cli/regress1/bags/map3.smt2 b/test/regress/cli/regress1/bags/map3.smt2
@@ -1,3 +1,5 @@
+;; Bags are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic HO_ALL)
 (set-info :status unsat)
 (set-option :fmf-bound true)

diff --git a/test/regress/cli/regress1/bags/murxla6.smt2 b/test/regress/cli/regress1/bags/murxla6.smt2
@@ -1,3 +1,5 @@
+;; Bags are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-const x (Bag Int))

diff --git a/test/regress/cli/regress1/bags/murxla7.smt2 b/test/regress/cli/regress1/bags/murxla7.smt2
@@ -1,3 +1,5 @@
+;; Bags 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/bags/product2.smt2 b/test/regress/cli/regress1/bags/product2.smt2
@@ -1,3 +1,5 @@
+;; Bags are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun A () (Table Int Int Int))

diff --git a/test/regress/cli/regress1/bags/proj-issue584.smt2 b/test/regress/cli/regress1/bags/proj-issue584.smt2
@@ -1,3 +1,5 @@
+;; Bags are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-const x (Bag Bool))

diff --git a/test/regress/cli/regress1/bags/subbag1.smt2 b/test/regress/cli/regress1/bags/subbag1.smt2
@@ -1,3 +1,5 @@
+;; Bags are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun A () (Bag Int))

diff --git a/test/regress/cli/regress1/bags/table_group3.smt2 b/test/regress/cli/regress1/bags/table_group3.smt2
@@ -1,5 +1,7 @@
 ; DISABLE-TESTER: lfsc
 ; Disabled since table.group is not supported in LFSC
+;; Bags are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic HO_ALL)
 
 (set-info :status unsat)

diff --git a/test/regress/cli/regress1/bags/table_group5.smt2 b/test/regress/cli/regress1/bags/table_group5.smt2
@@ -1,5 +1,7 @@
 ; DISABLE-TESTER: lfsc
 ; Disabled since table.group is not supported in LFSC
+;; Bags are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic HO_ALL)
 
 (set-info :status unsat)

diff --git a/test/regress/cli/regress1/bags/union_max2.smt2 b/test/regress/cli/regress1/bags/union_max2.smt2
@@ -1,3 +1,5 @@
+;; Bags are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun A () (Bag Int))

diff --git a/test/regress/cli/regress1/bug296.smt2 b/test/regress/cli/regress1/bug296.smt2
@@ -1,5 +1,7 @@
 ; EXPECT: unsat
 ; DISABLE-TESTER: alf
+;; introduces fresh Skolem in a trusted step
+; DISABLE-TESTER: alethe
 (set-logic QF_ALL)
 (set-info :status unsat)
 (declare-datatypes

diff --git a/test/regress/cli/regress1/bv/bug787.smt2 b/test/regress/cli/regress1/bv/bug787.smt2
@@ -1,5 +1,7 @@
-; COMMAND-LINE: --bitblast=eager 
+; COMMAND-LINE: --bitblast=eager
 ; EXPECT: unsat
+;; eager bit-blasting not supported by Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_BV)
 (set-info :status unsat)
 (define-fun hamming-weight ((bv (_ BitVec 4))) (_ BitVec 4)
@@ -88,4 +90,3 @@
        (centered (index-bit (_ bv3 4) v0) v0))
       (_ bv8 8)))))
 (check-sat)
-
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,5 +1,7 @@
 ; COMMAND-LINE: --solve-bv-as-int=iand
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 
 ;; produced by cvc4_16.drv ;;
 (set-logic AUFBVFPDTNIRA)
@@ -69,4 +71,3 @@
             (=> (f1__function_guard (f1 Tuple0) Tuple0) (= (f1 Tuple0) 1)))))))))
 
 (check-sat)
-
diff --git a/test/regress/cli/regress1/bv/divtest.smt2 b/test/regress/cli/regress1/bv/divtest.smt2
@@ -1,4 +1,6 @@
 ; DISABLE-TESTER: lfsc
+;; unsupported bitblasting of bvurem
+; DISABLE-TESTER: alethe
 (set-logic QF_BV)
 (set-info :status unsat)
 (declare-fun x1 () (_ BitVec 12))
@@ -30,25 +32,25 @@
 (declare-fun a0 () (_ BitVec 10))
 
 (assert
-(or 
-(and 
-	(= a (_ bv0 12))
-	(or (not (= (bvudiv x1 a) (bvudiv x2 a)))
-	    (not (= (bvudiv x1 a) (bvudiv x3 a)))
-	    (not (= (bvudiv x2 a) (bvudiv x3 a))))
-	(or (and (= x1 y1) (= y1 x2))
-	    (and (= x1 z1) (= z1 x2)))
-	(or (and (= x2 y2) (= y2 x3))
-	    (and (= x2 z2) (= z2 x3))))
-
-(and 
-	(= a0 (_ bv0 10))
-	(or (not (= (bvurem x01 a0) (bvurem x02 a0)))
-	    (not (= (bvurem x01 a0) (bvurem x03 a0)))
-	    (not (= (bvurem x02 a0) (bvurem x03 a0))))
-	(or (and (= x01 y01) (= y01 x02))
-	    (and (= x01 z01) (= z01 x02)))
-	(or (and (= x02 y02) (= y02 x03))
-	    (and (= x02 z02) (= z02 x03))))))
-	    
+(or
+(and
+  (= a (_ bv0 12))
+  (or (not (= (bvudiv x1 a) (bvudiv x2 a)))
+      (not (= (bvudiv x1 a) (bvudiv x3 a)))
+      (not (= (bvudiv x2 a) (bvudiv x3 a))))
+  (or (and (= x1 y1) (= y1 x2))
+      (and (= x1 z1) (= z1 x2)))
+  (or (and (= x2 y2) (= y2 x3))
+      (and (= x2 z2) (= z2 x3))))
+
+(and
+  (= a0 (_ bv0 10))
+  (or (not (= (bvurem x01 a0) (bvurem x02 a0)))
+      (not (= (bvurem x01 a0) (bvurem x03 a0)))
+      (not (= (bvurem x02 a0) (bvurem x03 a0))))
+  (or (and (= x01 y01) (= y01 x02))
+      (and (= x01 z01) (= z01 x02)))
+  (or (and (= x02 y02) (= y02 x03))
+      (and (= x02 z02) (= z02 x03))))))
+
 (check-sat)
diff --git a/test/regress/cli/regress1/bv/fuzz18.smtv1.smt2 b/test/regress/cli/regress1/bv/fuzz18.smtv1.smt2
@@ -1,3 +1,5 @@
+;; unsupported bitblasting of bvashr
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-info :status unsat)
 (set-logic QF_BV)

diff --git a/test/regress/cli/regress1/bv/fuzz19.smtv1.smt2 b/test/regress/cli/regress1/bv/fuzz19.smtv1.smt2
@@ -1,3 +1,5 @@
+;; unsupported bitblasting of bvlshr
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-info :status unsat)
 (set-logic QF_BV)

diff --git a/test/regress/cli/regress1/bv/fuzz34.smtv1.smt2 b/test/regress/cli/regress1/bv/fuzz34.smtv1.smt2
@@ -1,3 +1,5 @@
+;; unsupported bitblasting of bvlshr
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-info :status unsat)
 (set-logic QF_BV)

diff --git a/test/regress/cli/regress1/bv/fuzz38.smtv1.smt2 b/test/regress/cli/regress1/bv/fuzz38.smtv1.smt2
@@ -1,4 +1,6 @@
 ; DISABLE-TESTER: lfsc
+;; unsupported bitblasting of bvshl
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-info :status unsat)
 (set-logic QF_BV)

diff --git a/test/regress/cli/regress1/bv/incorrect1.smtv1.smt2 b/test/regress/cli/regress1/bv/incorrect1.smtv1.smt2
@@ -1,4 +1,6 @@
 ; DISABLE-TESTER: lfsc
+;; unsupported bitblasting of bvudiv
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-info :status unsat)
 (set-logic QF_BV)

diff --git a/test/regress/cli/regress1/bvdiv2.smt2 b/test/regress/cli/regress1/bvdiv2.smt2
@@ -1,4 +1,6 @@
 ; DISABLE-TESTER: lfsc
+;; unsupported bitblasting of bvudiv
+; DISABLE-TESTER: alethe
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/cli/regress1/datatypes/acyclicity-sr-ground096.smt2 b/test/regress/cli/regress1/datatypes/acyclicity-sr-ground096.smt2
@@ -1,3 +1,5 @@
+;; 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,6 +1,8 @@
 ; COMMAND-LINE: --ee-mode=distributed
 ; COMMAND-LINE: --ee-mode=central
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-datatypes ((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,5 +1,7 @@
 ; 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,4 +1,6 @@
 ; 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,4 +1,6 @@
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-datatypes ((tuple2!879 0)) (((tuple2!879!880 (_1!881 Int) (_2!882 Int)))))

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,3 +1,5 @@
+;; 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,5 +1,7 @@
 ; COMMAND-LINE: --dt-nested-rec
 ; EXPECT: unsat
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-datatypes ((E 0)(T 0)) (

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,4 +1,6 @@
 ; DISABLE-TESTER: lfsc
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic HO_ALL)
 (set-info :status unsat)
 (assert (= (nullable.lift (lambda ((x Bool) (y Bool)) (and x y)) (nullable.some false) (nullable.some false)) (nullable.some true)))

diff --git a/test/regress/cli/regress1/datatypes/nullables/nullables2.smt2 b/test/regress/cli/regress1/datatypes/nullables/nullables2.smt2
@@ -1,3 +1,5 @@
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (set-option :produce-models true)

diff --git a/test/regress/cli/regress1/datatypes/nullables/nullables3.smt2 b/test/regress/cli/regress1/datatypes/nullables/nullables3.smt2
@@ -1,4 +1,6 @@
 ; DISABLE-TESTER: alf
+;; Datatypes are not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun x () (Nullable Int))

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,3 +1,5 @@
+;; 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/decision/error3.smtv1.smt2 b/test/regress/cli/regress1/decision/error3.smtv1.smt2
@@ -1,3 +1,5 @@
+;; unsupported bitblasting of bvshl
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-info :status unsat)
 (set-logic QF_AUFBV)

diff --git a/test/regress/cli/regress1/fmf/agree467.smt2 b/test/regress/cli/regress1/fmf/agree467.smt2
@@ -1,6 +1,8 @@
 ; COMMAND-LINE: --finite-model-find
 ; EXPECT: unsat
 ; DISABLE-TESTER: alf
+;; introduces fresh Skolem in a trusted step
+; DISABLE-TESTER: alethe
 ; Preamble  --------------
 (set-logic AUFDTLIA)
 (set-info :status unsat)

diff --git a/test/regress/cli/regress1/fmf/bug0909.smt2 b/test/regress/cli/regress1/fmf/bug0909.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --finite-model-find
 ; EXPECT: unsat
+;; introduces fresh Skolem in a trusted step
+; DISABLE-TESTER: alethe
 ; Preamble  --------------
 (set-option :produce-models true)
 (set-logic ALL)

diff --git a/test/regress/cli/regress1/fmf/fc-pigeonhole19.smt2 b/test/regress/cli/regress1/fmf/fc-pigeonhole19.smt2
@@ -1,3 +1,5 @@
+;; introduces fresh Skolem in a trusted step
+; DISABLE-TESTER: alethe
 (set-logic UFC)
 (set-info :status unsat)
 

diff --git a/test/regress/cli/regress1/fmf/fmf-fun-divisor-pp.smt2 b/test/regress/cli/regress1/fmf/fmf-fun-divisor-pp.smt2
@@ -1,10 +1,12 @@
 ; COMMAND-LINE: --fmf-fun
 ; EXPECT: unsat
+;; introduces div_by_zero Skolem
+; DISABLE-TESTER: alethe
 (set-logic UFNIA)
 (set-info :status unsat)
-(define-fun-rec pow ((a Int)(b Int)) Int 
-    (ite (<= b 0) 
-         1 
+(define-fun-rec pow ((a Int)(b Int)) Int
+    (ite (<= b 0)
+         1
          (* a (pow a (- b 1)))))
 
 (declare-fun x () Int)

diff --git a/test/regress/cli/regress1/fmf/fore19-exp2-core.smt2 b/test/regress/cli/regress1/fmf/fore19-exp2-core.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-datatypes ((St 0) (Ex 0) (List!2293 0))