Fixing regression test setup

model-checking · Jun 28, 2023 · c15a591 · c15a591
1 parent 1ebba9e
commit c15a591
Show file tree

Hide file tree

Showing 3 changed files with 0 additions and 3 deletions.
diff --git a/tests/expected/function-contract/arbitrary_ensures_fail.rs b/tests/expected/function-contract/arbitrary_ensures_fail.rs
@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-verify-fail
 
 #[kani::ensures(result == x)]
 fn max(x: u32, y: u32) -> u32 {

diff --git a/tests/expected/function-contract/arbitrary_requires_fail.rs b/tests/expected/function-contract/arbitrary_requires_fail.rs
@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-verify-fail
 
 fn div(dividend: u32, divisor: u32) -> u32 {
     dividend / divisor

diff --git a/tests/expected/function-contract/simple_ensures_fail.rs b/tests/expected/function-contract/simple_ensures_fail.rs
@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-verify-fail
 
 #[kani::ensures(result == x)]
 fn max(x: u32, y: u32) -> u32 {