From 40f15cf91afb22118423208a769f443f9bc8d1c6 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Sun, 25 Feb 2024 17:50:32 -0300 Subject: [PATCH] more disabling --- test/regress/cli/regress0/unconstrained/bvmul2.smt2 | 2 ++ test/regress/cli/regress0/unconstrained/bvsle3.smt2 | 2 ++ test/regress/cli/regress0/unconstrained/bvsle5.smt2 | 2 ++ test/regress/cli/regress0/unconstrained/bvslt3.smt2 | 2 ++ test/regress/cli/regress0/unconstrained/bvslt5.smt2 | 2 ++ test/regress/cli/regress0/unconstrained/bvule3.smt2 | 2 ++ test/regress/cli/regress0/unconstrained/bvule5.smt2 | 2 ++ test/regress/cli/regress0/unconstrained/bvult3.smt2 | 2 ++ test/regress/cli/regress0/unconstrained/bvult5.smt2 | 2 ++ 9 files changed, 18 insertions(+) diff --git a/test/regress/cli/regress0/unconstrained/bvmul2.smt2 b/test/regress/cli/regress0/unconstrained/bvmul2.smt2 index 62fc5f123f1..57bba761521 100644 --- 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 index 0194ee3f795..2c84ad51c2e 100644 --- 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 index c292cc1a373..208b164c163 100644 --- 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 index ad8cd5216ea..78a0b5abc43 100644 --- 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 index 25d7b4a1ea2..9bb0fd350d6 100644 --- 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 index dfd5a45c301..4237f01d4c5 100644 --- 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 index 4a7ba96553b..c686d44a88d 100644 --- 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 index 40666a5df7a..91e609db8d9 100644 --- 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 index 9823aaf679f..57d5db671e6 100644 --- 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")