From 5bfa17e5b640c416cedd65906ed4bf8c49681c22 Mon Sep 17 00:00:00 2001
From: Kamil Chmielewski <45183584+ChmielewskiKamil@users.noreply.github.com>
Date: Sat, 21 Jan 2023 15:37:28 +0100
Subject: [PATCH] docs: fix value boundary

Using `val = val % token.balanceOf(address(this))` constrains the value to be from zero up to the `token.balanceOf(address(this))` (not included). It misses the maximal value of `token.balanceOf(address(this))`.
---
 program-analysis/echidna/property-creation.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/program-analysis/echidna/property-creation.md b/program-analysis/echidna/property-creation.md
index ee5f406c..18072936 100644
--- a/program-analysis/echidna/property-creation.md
+++ b/program-analysis/echidna/property-creation.md
@@ -162,7 +162,7 @@ We want Echidna to spend most of the execution exploring the contract to test. S
 ```solidity
   function depositShares_never_reverts(uint256 val) public {
     if(token.balanceOf(address(this)) > 0) {
-      val = val % token.balanceOf(address(this));
+      val = val % (token.balanceOf(address(this)) + 1);
       try c.depositShares(val) { /* not reverted */ } catch { assert(false); }
       assert(c.getShares(address(this)) > 0);
     } else {