From c15a591b3f584db776419340ee3fe616cc5c0b43 Mon Sep 17 00:00:00 2001
From: Justus Adam <justbldr@amazon.com>
Date: Wed, 28 Jun 2023 15:08:34 -0700
Subject: [PATCH] Fixing regression test setup

---
 tests/expected/function-contract/arbitrary_ensures_fail.rs  | 1 -
 tests/expected/function-contract/arbitrary_requires_fail.rs | 1 -
 tests/expected/function-contract/simple_ensures_fail.rs     | 1 -
 3 files changed, 3 deletions(-)

diff --git a/tests/expected/function-contract/arbitrary_ensures_fail.rs b/tests/expected/function-contract/arbitrary_ensures_fail.rs
index 1788538b9254..4ebbe16b5c02 100644
--- 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
index 9491788fc564..526753673f57 100644
--- 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
index 0ee61c78bc7a..b1e2132b6cbc 100644
--- 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 {