Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

SMTChecker: Cross-contract function calls cause the BMC model to crash. #15605

Open
Subway2023 opened this issue Dec 2, 2024 · 0 comments
Open
Labels

Comments

@Subway2023
Copy link

Environment

  • Compiler version: 0.8.28
  • Target EVM version (as per compiler settings): Non
  • Framework/IDE (e.g. Truffle or Remix): None
  • EVM execution environment / backend / blockchain client: None
  • Operating system: Ubuntu

Steps to Reproduce

contract Combined {
    C1 internal c1;
    constructor() {
        c1 = new C1();
    }
    function invokeAndCheck() public {
        c1.set();
        assert(c1.n() <= 1);
    }
}
contract C1 {
    uint public n;
    function set() external {
        n = 1;
    }
}
solc-0828 b.sol --model-checker-ext-calls trusted --model-checker-timeout 0 --model-checker-engine bmc --model-checker-bmc-loop-iterations 10 --model-checker-solvers z3
Internal compiler error:
./libsolidity/formal/SMTEncoder.cpp(2513): Throw in function solidity::smtutil::Expression solidity::frontend::SMTEncoder::currentValue(const solidity::frontend::VariableDeclaration&) const
Dynamic exception type: boost::wrapexcept<solidity::langutil::InternalCompilerError>
std::exception::what: Solidity assertion failed
[solidity::util::tag_comment*] = Solidity assertion failed

If I comment out assert(c1.n() <= 1), the BMC model can be called normally. Even without commenting it out, the CHC model can be called normally.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant