Rename kani::any_value_where to kani::any_where (#2139)

library/kani/src/lib.rs

@@ -120,15 +120,15 @@ pub fn any<T: Arbitrary>() -> T {
 /// under all possible `NonZeroU8` input values between 0 and 12.
 ///
 /// ```rust
-/// let inputA = kani::any_value_where::<std::num::NonZeroU8>(|x| *x < 12, "explanation");
+/// let inputA = kani::any_where::<std::num::NonZeroU8>(|x| *x < 12, "explanation");
 /// fn_under_verification(inputA);
 /// ```
 ///
 /// Note: This is a safe construct and can only be used with types that implement the `Arbitrary`
 /// trait. The Arbitrary trait is used to build a symbolic value that represents all possible
 /// valid values for type `T`.
 #[inline(always)]
-pub fn any_value_where<T: Arbitrary, F: FnOnce(&T) -> bool>(f: F, _msg: &'static str) -> T {
+pub fn any_where<T: Arbitrary, F: FnOnce(&T) -> bool>(f: F, _msg: &'static str) -> T {
     let result = T::any();
     assume(f(&result));
     result

tests/kani/Assume/main.rs

@@ -9,7 +9,7 @@ fn main() {
 }
 
 #[kani::proof]
-fn verify_any_value_where() {
-    let i: i32 = kani::any_value_where(|x| *x < 10, "Only single digit values are legal");
+fn verify_any_where() {
+    let i: i32 = kani::any_where(|x| *x < 10, "Only single digit values are legal");
     assert!(i < 20);
 }