From af32ddd057c1c6dcc9ae3e20c0e0c5bb5b91b66e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 2 Aug 2024 14:05:44 +0000 Subject: [PATCH] Remove unnecessary check --- tests/kani/Cast/cast_abstract_args_to_concrete.rs | 3 --- 1 file changed, 3 deletions(-) diff --git a/tests/kani/Cast/cast_abstract_args_to_concrete.rs b/tests/kani/Cast/cast_abstract_args_to_concrete.rs index 51067e0e0a73..6694f799493a 100644 --- a/tests/kani/Cast/cast_abstract_args_to_concrete.rs +++ b/tests/kani/Cast/cast_abstract_args_to_concrete.rs @@ -1,9 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// https://github.com/model-checking/kani/issues/555 -// kani-flags: --no-undefined-function-checks - // This regression test is in response to issue #135. // The type of the second parameter to powi is a `CInteger`, but // the type of `2` here is a `u32`. This test ensures that