more disabling

HanielB · Feb 25, 2024 · 022e95d · 022e95d
1 parent e4322b5
commit 022e95d
Show file tree

Hide file tree

Showing 103 changed files with 238 additions and 35 deletions.
diff --git a/test/regress/cli/regress0/ho/SYO372.smt2 b/test/regress/cli/regress0/ho/SYO372.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --mbqi
 ; EXPECT: unsat
+;; introduces fresh Skolem in a trusted step
+; DISABLE-TESTER: alethe
 (set-logic HO_ALL)
 (set-info :status unsat)
 (declare-sort $$unsorted 0)

diff --git a/test/regress/cli/regress0/nl/combined-uf.smt2 b/test/regress/cli/regress0/nl/combined-uf.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_UFNRA)
 (declare-fun a () Real)
 (declare-fun b () Real)

diff --git a/test/regress/cli/regress0/nl/dd.iand-wrong-0513-pp.smt2 b/test/regress/cli/regress0/nl/dd.iand-wrong-0513-pp.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; unsupported iand operator
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (declare-fun x () Int)
 (declare-fun i () Int)

diff --git a/test/regress/cli/regress0/nl/issue5726-downpolys.smt2 b/test/regress/cli/regress0/nl/issue5726-downpolys.smt2
@@ -1,6 +1,8 @@
 ; COMMAND-LINE: --nl-ext=none --nl-cov
 ; REQUIRES: poly
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_NRA)
 (declare-fun x () Real)
 (declare-fun y () Real)

diff --git a/test/regress/cli/regress0/nl/nta/cos-sig-value.smt2 b/test/regress/cli/regress0/nl/nta/cos-sig-value.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_UFNRAT)
 (set-info :status unsat)
 (declare-fun x () Real)

diff --git a/test/regress/cli/regress0/nl/nta/exp-n0.5-lb.smt2 b/test/regress/cli/regress0/nl/nta/exp-n0.5-lb.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_NRAT)
 (declare-fun x () Real)
 

diff --git a/test/regress/cli/regress0/nl/nta/exp-n0.5-ub.smt2 b/test/regress/cli/regress0/nl/nta/exp-n0.5-ub.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_NRAT)
 (declare-fun x () Real)
 

diff --git a/test/regress/cli/regress0/nl/nta/exp1-ub.smt2 b/test/regress/cli/regress0/nl/nta/exp1-ub.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --nl-ext-tf-tplanes
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_NRAT)
 (set-info :status unsat)
 (declare-fun x () Real)

diff --git a/test/regress/cli/regress0/nl/nta/issue4693-5-inc-purify.smt2 b/test/regress/cli/regress0/nl/nta/issue4693-5-inc-purify.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (assert (forall ((t Real)) (= 0.0 (/ t (cos 1.0)))))

diff --git a/test/regress/cli/regress0/nl/nta/issue4693-inc-purify.smt2 b/test/regress/cli/regress0/nl/nta/issue4693-inc-purify.smt2
@@ -1,6 +1,8 @@
 ; COMMAND-LINE: -i
 ; EXPECT: unsat
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_NRAT)
 (declare-const r0 Real)
 (assert (! (>= (sin 97111.0) r0 r0 r0 97111.0) :named IP_3))

diff --git a/test/regress/cli/regress0/nl/nta/issue8415-embed-arg.smt2 b/test/regress/cli/regress0/nl/nta/issue8415-embed-arg.smt2
@@ -1,3 +1,5 @@
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun r8 () Real)

diff --git a/test/regress/cli/regress0/nl/nta/issue8773-phase-shift.smt2 b/test/regress/cli/regress0/nl/nta/issue8773-phase-shift.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_NRAT)
 (assert (= 0.0 (sin 7)))
 (check-sat)
diff --git a/test/regress/cli/regress0/nl/nta/pi-simplest.smt2 b/test/regress/cli/regress0/nl/nta/pi-simplest.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (assert (= real.pi 1.0))
 (check-sat)
diff --git a/test/regress/cli/regress0/nl/nta/proj-issue505-pi-red.smt2 b/test/regress/cli/regress0/nl/nta/proj-issue505-pi-red.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (assert (is_int (arcsin real.pi)))
 (assert (= real.pi (cos real.pi)))

diff --git a/test/regress/cli/regress0/nl/nta/sin-sym-schema.smt2 b/test/regress/cli/regress0/nl/nta/sin-sym-schema.smt2
@@ -1,3 +1,5 @@
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun a () Real)

diff --git a/test/regress/cli/regress0/nl/nta/sin-sym.smt2 b/test/regress/cli/regress0/nl/nta/sin-sym.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --nl-ext=full --nl-ext-tplanes
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_UFNRAT)
 (set-info :status unsat)
 (declare-fun x () Real)

diff --git a/test/regress/cli/regress0/nl/nta/sqrt-simple.smt2 b/test/regress/cli/regress0/nl/nta/sqrt-simple.smt2
@@ -1,3 +1,5 @@
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_NRAT)
 (set-info :status unsat)
 (declare-fun x () Real)

diff --git a/test/regress/cli/regress0/nl/nta/tan-rewrite.smt2 b/test/regress/cli/regress0/nl/nta/tan-rewrite.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_UFNRAT)
 (set-info :status unsat)
 (declare-fun x () Real)

diff --git a/test/regress/cli/regress0/nl/pow2-native-0.smt2 b/test/regress/cli/regress0/nl/pow2-native-0.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; operator pow2 now supported
+; DISABLE-TESTER: alethe
 (set-logic QF_NIA)
 (declare-fun x () Int)
 (assert (< x 0))

diff --git a/test/regress/cli/regress0/nl/pow2-native-2.smt2 b/test/regress/cli/regress0/nl/pow2-native-2.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; operator pow2 now supported
+; DISABLE-TESTER: alethe
 (set-logic QF_NIA)
 (set-info :status unsat)
 (declare-fun x () Int)

diff --git a/test/regress/cli/regress0/nl/pow2-native-3.smt2 b/test/regress/cli/regress0/nl/pow2-native-3.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; operator pow2 now supported
+; DISABLE-TESTER: alethe
 (set-logic QF_NIA)
 (set-info :status unsat)
 (declare-fun x () Int)

diff --git a/test/regress/cli/regress0/nl/pow2-pow-isabelle.smt2 b/test/regress/cli/regress0/nl/pow2-pow-isabelle.smt2
@@ -1,7 +1,9 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --nl-ext-tplanes 
+; COMMAND-LINE: --solve-bv-as-int=sum --nl-ext-tplanes
 ; EXPECT: unsat
 ; causes exception with large exponents on some builds
 ; DISABLE-TESTER: unsat-core
+;; operator pow2 now supported
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (declare-fun x$ () (_ BitVec 32))
 (declare-fun y$ () (_ BitVec 32))

diff --git a/test/regress/cli/regress0/nl/pow2-pow.smt2 b/test/regress/cli/regress0/nl/pow2-pow.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; operator pow2 now supported
+; DISABLE-TESTER: alethe
 (set-logic QF_NIA)
 (declare-fun x () Int)
 (assert (< x 0))

diff --git a/test/regress/cli/regress0/nl/tpp-fail-pf-012921.smt2 b/test/regress/cli/regress0/nl/tpp-fail-pf-012921.smt2
@@ -1,3 +1,5 @@
+;; introduces div_by_zero Skolem
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun x () Real)

diff --git a/test/regress/cli/regress0/rels/addr_book_0.cvc.smt2 b/test/regress/cli/regress0/rels/addr_book_0.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 (declare-sort Atom 0)

diff --git a/test/regress/cli/regress0/rels/atom_univ2.cvc.smt2 b/test/regress/cli/regress0/rels/atom_univ2.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-option :sets-ext true)
 (set-logic ALL)

diff --git a/test/regress/cli/regress0/rels/iden_0.cvc.smt2 b/test/regress/cli/regress0/rels/iden_0.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 (declare-sort Atom 0)

diff --git a/test/regress/cli/regress0/rels/iden_1.cvc.smt2 b/test/regress/cli/regress0/rels/iden_1.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-option :sets-ext true)
 (set-logic ALL)

diff --git a/test/regress/cli/regress0/rels/join-eq-u.cvc.smt2 b/test/regress/cli/regress0/rels/join-eq-u.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/joinImg_0.cvc.smt2 b/test/regress/cli/regress0/rels/joinImg_0.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 (set-option :sets-ext true)

diff --git a/test/regress/cli/regress0/rels/rel_1tup_0.cvc.smt2 b/test/regress/cli/regress0/rels/rel_1tup_0.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/rel_complex_0.cvc.smt2 b/test/regress/cli/regress0/rels/rel_complex_0.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/rel_complex_1.cvc.smt2 b/test/regress/cli/regress0/rels/rel_complex_1.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/rel_conflict_0.cvc.smt2 b/test/regress/cli/regress0/rels/rel_conflict_0.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/rel_join_0.cvc.smt2 b/test/regress/cli/regress0/rels/rel_join_0.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/rel_join_1.cvc.smt2 b/test/regress/cli/regress0/rels/rel_join_1.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/rel_join_2.cvc.smt2 b/test/regress/cli/regress0/rels/rel_join_2.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/rel_join_3.cvc.smt2 b/test/regress/cli/regress0/rels/rel_join_3.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/rel_join_4.cvc.smt2 b/test/regress/cli/regress0/rels/rel_join_4.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/rel_join_5.cvc.smt2 b/test/regress/cli/regress0/rels/rel_join_5.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/rel_join_6.cvc.smt2 b/test/regress/cli/regress0/rels/rel_join_6.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/rel_join_7.cvc.smt2 b/test/regress/cli/regress0/rels/rel_join_7.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/rel_product_0.cvc.smt2 b/test/regress/cli/regress0/rels/rel_product_0.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/rel_product_1.cvc.smt2 b/test/regress/cli/regress0/rels/rel_product_1.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/rel_symbolic_1.cvc.smt2 b/test/regress/cli/regress0/rels/rel_symbolic_1.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/rel_tc_11.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tc_11.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/rel_tc_3.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tc_3.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/rel_tc_7.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tc_7.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/rel_tc_8.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tc_8.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/rel_tp_join_0.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tp_join_0.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/rel_tp_join_1.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tp_join_1.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/rel_tp_join_2.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tp_join_2.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/rel_tp_join_3.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tp_join_3.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/rel_tp_join_eq_0.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tp_join_eq_0.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)
 

diff --git a/test/regress/cli/regress0/rels/rel_tp_join_int_0.cvc.smt2 b/test/regress/cli/regress0/rels/rel_tp_join_int_0.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; Logic not supported in Alethe
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-logic ALL)