Using SMTChecker formal verification module in Solidity compiler with Remix & Dapptools

The SMTChecker is a formal verification module inside the Solidity compiler. Historically it has been complicated to run the SMTChecker on your own contracts, since you had to compile the compiler with an SMT/Horn solver, usually z3. We have been working on different solutions to this, and nowadays it is quite easy to run it.