more disabling

HanielB · Feb 25, 2024 · 5fc9b01 · 5fc9b01
1 parent 118179b
commit 5fc9b01
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 1 deletion.
diff --git a/test/regress/cli/regress0/arrays/incorrect10.smtv1.smt2 b/test/regress/cli/regress0/arrays/incorrect10.smtv1.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; introduces arrays Skolem
+; DISABLE-TESTER: alethe
 (set-option :incremental false)
 (set-info :status unsat)
 (set-logic QF_AUF)

diff --git a/test/regress/cli/regress0/bv/ackermann3.smt2 b/test/regress/cli/regress0/bv/ackermann3.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --ackermann
 ; EXPECT: unsat
+;; introduces fresh Skolem in a trusted step
+; DISABLE-TESTER: alethe
 (set-logic QF_ABV)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/cli/regress0/bv/ackermann6.smt2 b/test/regress/cli/regress0/bv/ackermann6.smt2
@@ -1,5 +1,7 @@
 ; COMMAND-LINE: --ackermann
 ; EXPECT: unsat
+;; introduces fresh Skolem in a trusted step
+; DISABLE-TESTER: alethe
 (set-logic QF_UFBV)
 
 (declare-sort S 0)
@@ -28,4 +30,3 @@
 
 (check-sat)
 (exit)
-
diff --git a/test/regress/cli/regress0/bv/bvproof3.smt2 b/test/regress/cli/regress0/bv/bvproof3.smt2
@@ -1,4 +1,6 @@
 ; COMMAND-LINE: --bitblast=eager
+;; eager bit-blasting not supported by Alethe
+; DISABLE-TESTER: alethe
 (set-logic QF_BV)
 (set-info :status unsat)
 (declare-const x (_ BitVec 1))