Skip to content

Commit a5eb24d

Browse files
authored
Merge pull request #16270 from ParKing666/patch-3
Update smtchecker.rst: fix int128 range = [-2^127,2^127-1], was ^128
2 parents ee72983 + 74ea280 commit a5eb24d

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

docs/smtchecker.rst

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -263,7 +263,7 @@ A common type of properties in smart contracts are properties that involve the
263263
state of the contract. Multiple transactions might be needed to make an assertion
264264
fail for such a property.
265265

266-
As an example, consider a 2D grid where both axis have coordinates in the range (-2^128, 2^128 - 1).
266+
As an example, consider a 2D grid where both axis have coordinates in the range (-2^127, 2^127 - 1).
267267
Let us place a robot at position (0, 0). The robot can only move diagonally, one step at a time,
268268
and cannot move outside the grid. The robot's state machine can be represented by the smart contract
269269
below.

0 commit comments

Comments
 (0)