SMTChecker

Setup

Compiler Setup

1. solc-select installation - the link includes a number of ways to download and install, but the easiest is probably pip3 install solc-select
2. Run solc --version
   1. If you see Version: 0.8.0 you can skip the next step
3. solc-select install 0.8.0 && solc-select use 0.8.0
   1. Run solc --version you should see Version: 0.8.0

Download files

1. Download this file

tutorial1.sol

1. run solc tutorial1.sol
   1. You should see… Compiler run successful, no output requested.

Instructions

1. Uncomment line 3 in tutorial1.sol
2. run solc tutorial.sol
   1. The model checker should return a Warning that the Overflow property could not be verified. It also includes a counterexample and the line number where it found the overflow.
3. Add one or more require statements to prevent the code from overflowing.
   1. Hint: type(uint).max returns the max value for a uint