From f719b565968568335d9be03ef27c5d05bb8fd0b7 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
Date: Wed, 4 May 2022 13:23:06 -0400
Subject: [PATCH] Small adjustments (part 2) (#1158)

---
 README.md | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index c6f4ff800cb8..2d37d1912223 100644
--- a/README.md
+++ b/README.md
@@ -25,13 +25,16 @@ 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, meets_specification};
+use my_crate::{function_under_test, meets_specification, precondition};
 
 #[kani::proof]
 fn check_my_property() {
    // Create a nondeterministic input
    let input = kani::any();
 
+   // Constrain it according to the function's precondition
+   kani::assume(precondition(input));
+
    // Call the function under verification
    let output = function_under_test(input);