Add SMTChecker to nightly build

[elenadimitrova]

SMT Checker is an experimental verification tool we can enable directly in contracts via pragma experimental SMTChecker statement.

Similarly to how we run mythril in the nightly build we need to compile our contracts with the Solidity SMTChecker pragma enabled. We have an experimental branch where this is tested. Below are the steps and changes done so far:

1. Build custom solc with Z3 support
   Note that installing Z3 for me wasn't exactly straight forward, so leaving notes here in case anyone faces the same problems:

• brew install z3

• Use instructions from https://github.com/Z3Prover/z3

python scripts/mk_make.py
cd build
make
sudo make install

• Clone solc repo and follow build from source instructions
  Note that to compile as a release you need an empty prerelease.txt file, see Latest v0.4.25 version is marked as a nightly ethereum/solidity#5463 (comment)

• Install the newly built solc via make install

2. Switch the truffle compiler to use this 👆

compilers: {
    solc: {
      version: "native",
    }
  }

3. Script the addition of SMTChecker experimental pragma in CI
4. Run solc contracts/PatriciaTree/Data.sol --allow-paths lib/dappsys/*.sol as an example, which results in Segmentation fault: 11 potentially meaning a bad solc build.

Note the ongoing work to better integrate the SMTChecker capabilities in the dev experience, e.g. ethereum/solc-js#316

Related materials
Presentation by Chris Reitwiessner from EF
DevCon4 talk by EF's Leonardo Alt on using SMTChecker