Attempt at model checking with the SMT checker from the solidity compiler. It does not seem to be usable for us just yet. This PR is meant as documentation for future attempts to use the SMT checker.
Observations
Both the BMC and the CHC engines are not able to deal with the relatively simple invariant from Collateral.sol. This appears to be a know restriction when calling external functions without implementation. Because we depend quite heavily on an IERC20 interface for our money flows, this is quite unfortunate.
On Debian it won't recognize the installed z3 library. For it to work it currently requires:
cd /usr/lib/x86_64-linux-gnu/
sudo ln -s libz3.so.4 libz3.so.4.8
Attempt at model checking with the SMT checker from the solidity compiler. It does not seem to be usable for us just yet. This PR is meant as documentation for future attempts to use the SMT checker.
Observations
Both the BMC and the CHC engines are not able to deal with the relatively simple invariant from
Collateral.sol. This appears to be a know restriction when calling external functions without implementation. Because we depend quite heavily on an IERC20 interface for our money flows, this is quite unfortunate.On Debian it won't recognize the installed z3 library. For it to work it currently requires: