Feature: SMTChecker support (a.k.a support all possible outputs)

[sambacha]

Component

Forge

Describe the feature you would like

As of 0.8.4, solidity is depreciating the experimental pragma for SMT Checker as it runs on all files if enabled

pragma experimental SMTChecker;

The new way to configure this is through the JSON config file

"settings.modelChecker.targets": ["underflow", "overflow"]

You have to define which engine it should run as well, see https://docs.soliditylang.org/en/v0.8.11/smtchecker.html#smtchecker-engines

"settings.modelChecker.solvers": ["smtlib2","z3"]

settings.modelChecker.targets=<targets>

And what targets to check

: --model-checker-targets assert,overflow

These options are not configurable currently for forge

Additional benefits would be when using the yul optimizer you would have access to the ReasoningBasedSimplifier

Additional context

Additionally custom natspec parsing would help in tests

/// @custom:smtchecker

maybe can be expanded to slither other tools, etc

[sambacha]

Bump to @gakonst now that revm is the default

[sambacha]

There are multiple issues covering compiled output already. utilizing the solc binary directly and feeding the compiled output is satisfactory for the use case described here