[SMTChecker] Option --model-checker-contract in combination with trusted external calls causes unsound CHC analysis

[blishko]

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 is selected for analysis (with --model-checker-contracts).

File A.sol

contract A { function a() pure public { } }

File B.sol

import "A.sol";
contract B { function b(A a) pure public { a.a(); assert(false); } }

Command-line arguments: --model-checker-engine chc B.sol --model-checker-ext-calls trusted --model-checker-contracts B.sol:B Expected outcome: Reported assertion violation in B.b Incorrect actual outcome: CHC engine reports the assertion as safe.

NOTE: The analysis works as expected if the two contracts live in the same file.

[blishko]

This has the same underlying cause as the incorrect behaviour reported in #14275. However, the problem reported here is much more serious.