From 4e43f694bc85c93cd761f5306d9b895c8059bb0f Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Wed, 4 May 2022 06:38:52 -0700
Subject: [PATCH] Small adjustments to our doc / help (#1153)

* Remove redundant check from README.md

In the example, we were calling is_valid after `kani::any()` which is
redundant since the type has to implement the Arbitrary type.

* Also adjust Kani help
---
 README.md               | 5 +----
 kani-driver/src/args.rs | 2 +-
 2 files changed, 2 insertions(+), 5 deletions(-)

diff --git a/README.md b/README.md
index 22cfe369f7cce..68111e7eb4d73 100644
--- a/README.md
+++ b/README.md
@@ -25,16 +25,13 @@ See [the installation guide](https://model-checking.github.io/kani/install-guide
 Similar to testing, you write a harness, but with Kani you can check all possible values using `kani::any()`:
 
 ```rust
-use my_crate::{function_under_test, is_valid, meets_specification};
+use my_crate::{function_under_test, meets_specification};
 
 #[kani::proof]
 fn check_my_property() {
    // Create a nondeterministic input
    let input = kani::any();
 
-   // Constrain it to represent valid values
-   kani::assume(is_valid(input));
-
    // Call the function under verification
    let output = function_under_test(input);
 
diff --git a/kani-driver/src/args.rs b/kani-driver/src/args.rs
index bf655f825a60f..f82ca7426e5ed 100644
--- a/kani-driver/src/args.rs
+++ b/kani-driver/src/args.rs
@@ -13,7 +13,7 @@ const DEFAULT_OBJECT_BITS: u32 = 16;
 #[derive(Debug, StructOpt)]
 #[structopt(
     name = "kani",
-    about = "Verify a single Rust file. For more information, see https://github.com/model-checking/kani",
+    about = "Verify a single Rust crate. For more information, see https://github.com/model-checking/kani",
     setting = structopt::clap::AppSettings::AllArgsOverrideSelf
 )]
 pub struct StandaloneArgs {