From c90f44733d2308838d6db60cdd3ce76ed99bf187 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
Date: Fri, 20 Jan 2023 17:17:53 -0500
Subject: [PATCH] Rename `kani::any_value_where` to `kani::any_where` (#2139)

---
 library/kani/src/lib.rs   | 4 ++--
 tests/kani/Assume/main.rs | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index 8a3b69949603..9c4bd6ca30c9 100644
--- a/library/kani/src/lib.rs
+++ b/library/kani/src/lib.rs
@@ -120,7 +120,7 @@ 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);
 /// ```
 ///
@@ -128,7 +128,7 @@ pub fn any<T: Arbitrary>() -> T {
 /// 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
diff --git a/tests/kani/Assume/main.rs b/tests/kani/Assume/main.rs
index e58fd62a4c5c..d4ca44a920e3 100644
--- a/tests/kani/Assume/main.rs
+++ b/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);
 }