Martin Blicha
Martin Blicha
Instead of using Z3 as a library, we use Z3 as an external solver, the same way as we already use Eldarica and cvc5. After discussion with @ekpyron, we decided...
Input ``` contract C { function abiEncodeSlice(bytes4 sel, uint[] calldata data) external pure { bytes memory b1 = abi.encodeWithSelector(sel, data); bytes memory b2 = abi.encodeWithSelector(sel, data[0:]); assert(b1.length == b2.length); bytes...
In the [inner loop of IMC](https://github.com/ftsrg/theta/blob/cb77d7e6bb0e51ea00d2a1dc483fdf510dd8e8b4/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedChecker.kt#L224-L247) Theta uses the same solver both for checking reachability and for checking fixedpoint. Because of this, everything is popped from the solver in preparation...
Consider the following two contracts: ``` contract D { function dec(uint v) public pure returns (uint) { --v; return v; } } contract C { function f() public pure returns...
Previously, when a contract was selected for analysis, the analysis was incorrect. There were two issues. First, the contracts in the same file were considered as entry points even though...
Value of loop condition can change between iterations of the loop. Therefore, BMC should be in the "inside loop" state when analyzing loop conditions. Previously, when visiting loop condition of...
As described in the note in [the documentation](https://docs.soliditylang.org/en/latest/smtchecker.html#smtchecker-and-formal-verification), since version 0.8.5, the model checker got its own command-line/JSON options, and `pragma experimental SMTChecker` has been deprecated. It should be removed...
The module known as SMTChecker has evolved from a simple BMC-like approach to a proper model checker. It would be good to reflect the current status in the module's name....
CHC analysis does not work correctly if a contract calls another contract that is defined in a different file and external calls are trusted (`--model-checker-ext-calls=trusted` and only the first contract...
Model checker's CLI option to select contracts to be analyzed (`--model-checker-contracts`) rejects some valid values, for example if the path contains `:`.