SMTChecker: Unable to determine the return value of the function about solidity HOT 5 CLOSED

contract SomeOtherContract {
    function f() public returns (int){
        return 2;
    }
}
contract ExampleContract {
    SomeOtherContract public otherContract;
    function f() public{
        otherContract = new SomeOtherContract();
        assert(otherContract.f()==2);
    }
}

If the called function is located in another contract, the SMTChecker correctly determines the return value.

from solidity.

The difference is not in whether or not the function is in the same or other contract, the difference is that in the second example, the function returns a constant value, while in the first one it returns x+1. BMC engine does not keep context around so it does not know that x never changes. CHC engine is more powerful and should work as expected on this example. @Subway2023, can you confirm this?

from solidity.

contract SomeOtherContract {
    function f() public returns (int){
        return 2;
    }
}
contract ExampleContract {
    SomeOtherContract public otherContract;
    function f() public{
        otherContract = new SomeOtherContract();
        assert(otherContract.f()==2);
    }
}

If the called function is located in another contract, the SMTChecker correctly determines the return value.

solc SomeOtherContract.sol --model-checker-engine all

from solidity.

This is because it is an external call, which in general cannot be trusted even though it is a contract in the same source.
If you want to trust external call to known contracts you can add the option --model-checker-ext-calls trusted.
With this option CHC engine verifies that the assertion cannot be violated.

from solidity.

The current behaviour matches the expected behaviour, so I am closing this issue.

from solidity.