[SMTChecker] Option `--model-checker-contract` does not work as expected

[blishko]

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 (uint) {
        uint ret = d.dec(0);
        return ret;
    }
}

We would like to check that SMTChecker detects the underflow in D.dec when C.f is called. However, with default settings, it will much more likely detect the underflow when D.dec is called directly.

We should have an option to restrict the analysis to consider only contract C as the entry point. There exists an option, --model-checker-contract , that should allow us to restrict the analysis, but currently it does not work as expected. At the moment, SMTChecker analyzes all contracts in the source unit specified with this option, disregarding the actual contract specified.

In my opinion, the option should restrict the possible entry point to the contracts specified, but we still need to analyze other contracts if their functions are called from the analyzed contract and we are in the trusted mode.

If we manage to resolve this issue, we should add the test above to SMTChecker's test suite for trusted external calls.