What
To ease the maintenance cost of the built-in model checker (SMTChecker), we are considering deprecating and eventually removing the BMC engine of the model checker.
Why
The BMC engine has demonstrated the capabilities of SMT-based model-checking techniques for automatically proving certain properties of smart contracts, or detecting possible violations of these properties.
However, the BMC approach has considerable limitations. Since it analyzes functions in isolation, it does not take the overall behavior of the contract over multiple transactions into account when analyzing each function. Due to this and other approximations, BMC is prone to reporting false positives.
To overcome these limitations, we have introduced a verification approach based on constrained Horn clauses, implemented in the CHC engine of the model checker.
CHC engine is more powerful and more precise than the BMC engine. The downside is that it requires more resources.
Our current belief is that the cost of maintaining the BMC engine outweighs its benefits, and we would like to eventually remove it from the model checker.
Conclusion
If you are using the BMC engine, please share your use case and your experience with us.
Unless serious objections arise, we plan to move ahead with deprecation and eventual removal of the engine.