Adding check files for verification integration tests

[mario-bucev]

This PR extends the verification test suite to optionally validate the VCs results.
For each .scala file, a corresponding .check file dictates the expected output.
The latter is a CSV with the following columns:

• Position of the VC, of the form <line>:<column>
• Function name of the VC
• The kind of VC (e.g. precondition, assert and so on)
• The status (e.g. valid, invalid, unknown)

Note that VCs are allowed to be undistinguishable (i.e. all 5 properties are equal), for instance BigIntMonoidLaws.check has 3 times the entry 10:9;append;precondition;valid because there are 3 corresponding VCs.

To opt-in for .check files test for benchmarks that are expected to fail, the function VerificationComponentTestSuite#testNegAllWithCheckFiles may be used.
It is currently only used by VerificationSuite to test verification/invalid. For now, a warning is issued for benchmarks missing a corresponding .check file.

To quickly generate .check files, a utility check-files-util module is provided.
It essentially runs Stainless and writes the results.
The utility must be passed a folder or individual files (which must resides in frontends/benchmarks).
It accepts the following options:

• --ignore=<comma-separated-without-spaces-files> to ignore specific files
• --parallelism=<n> sets the number of threads for Stainless
  Options can be passed to Stainless by adding a separation --.

For instances, the following command (in SBT shell):

check-files-util/run verification/invalid \
  --parallelism=2 \
  --ignore=verification/invalid/BadConcRope.scala,verification/invalid/BadOpaque.scala \
  -- \
  --solvers=smt-cvc5 \
  --strict-arithmetic=true

will:

• Generate .check files for the verification/invalid benchmarks except BadConcRope.scala and BadOpaque.scala as indicated by the --ignore options (note that the files are concatenated with commas without any space!)
• Set to 2 the number of threads for Stainless to run
• Use smt-cvc5 as solver
• Generate VCs for overflows (strict-arithmetic option)

Note that the primary motivation for this is to fix missing positions in VCs (which are probably the second most annoying things after timed-out VCs).
If a benchmark has VCs with missing positions, the utility will issue a warning but it won't be able to know from which file the VC comes (since the position is also responsible to contain the filename).