more disabling

HanielB · Feb 25, 2024 · 40f15cf · 40f15cf
1 parent a37c892
commit 40f15cf
Show file tree

Hide file tree

Showing 9 changed files with 18 additions and 0 deletions.
diff --git a/test/regress/cli/regress0/unconstrained/bvmul2.smt2 b/test/regress/cli/regress0/unconstrained/bvmul2.smt2
@@ -1,4 +1,6 @@
 ; COMMAND-LINE: --unconstrained-simp
+;; introduces fresh Skolem in a trusted step
+; DISABLE-TESTER: alethe
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/cli/regress0/unconstrained/bvsle3.smt2 b/test/regress/cli/regress0/unconstrained/bvsle3.smt2
@@ -1,4 +1,6 @@
 ; COMMAND-LINE: --unconstrained-simp
+;; introduces fresh Skolem in a trusted step
+; DISABLE-TESTER: alethe
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/cli/regress0/unconstrained/bvsle5.smt2 b/test/regress/cli/regress0/unconstrained/bvsle5.smt2
@@ -1,4 +1,6 @@
 ; COMMAND-LINE: --unconstrained-simp
+;; introduces fresh Skolem in a trusted step
+; DISABLE-TESTER: alethe
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/cli/regress0/unconstrained/bvslt3.smt2 b/test/regress/cli/regress0/unconstrained/bvslt3.smt2
@@ -1,4 +1,6 @@
 ; COMMAND-LINE: --unconstrained-simp
+;; introduces fresh Skolem in a trusted step
+; DISABLE-TESTER: alethe
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/cli/regress0/unconstrained/bvslt5.smt2 b/test/regress/cli/regress0/unconstrained/bvslt5.smt2
@@ -1,4 +1,6 @@
 ; COMMAND-LINE: --unconstrained-simp
+;; introduces fresh Skolem in a trusted step
+; DISABLE-TESTER: alethe
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/cli/regress0/unconstrained/bvule3.smt2 b/test/regress/cli/regress0/unconstrained/bvule3.smt2
@@ -1,4 +1,6 @@
 ; COMMAND-LINE: --unconstrained-simp
+;; introduces fresh Skolem in a trusted step
+; DISABLE-TESTER: alethe
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/cli/regress0/unconstrained/bvule5.smt2 b/test/regress/cli/regress0/unconstrained/bvule5.smt2
@@ -1,4 +1,6 @@
 ; COMMAND-LINE: --unconstrained-simp
+;; introduces fresh Skolem in a trusted step
+; DISABLE-TESTER: alethe
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/cli/regress0/unconstrained/bvult3.smt2 b/test/regress/cli/regress0/unconstrained/bvult3.smt2
@@ -1,4 +1,6 @@
 ; COMMAND-LINE: --unconstrained-simp
+;; introduces fresh Skolem in a trusted step
+; DISABLE-TESTER: alethe
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")

diff --git a/test/regress/cli/regress0/unconstrained/bvult5.smt2 b/test/regress/cli/regress0/unconstrained/bvult5.smt2
@@ -1,4 +1,6 @@
 ; COMMAND-LINE: --unconstrained-simp
+;; introduces fresh Skolem in a trusted step
+; DISABLE-TESTER: alethe
 (set-logic QF_AUFBVLIA)
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")