SMT2 strings tests

[allredj]

Adds tests for SMT2 string operations. This PR is limited to tests for constant strings. More tests will come later. The main objective is to check support for these operations on external solvers, but that suite will also become useful once string support is added to CBMC SMT2 backend.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[tautschnig]

Seems ok except as noted below.

[tautschnig]

Should that be smt2_solver instead? Not that it would support the theory, but the above doesn't exist at all...

[allredj]

Yep, fixed.

[tautschnig]

That would mean that Makefile, CMakeLists.txt, *.desc are also ignore, which doesn't seem right.

[allredj]

I don't understand. I need to discard the ignore that is introduced here:
https://github.com/diffblue/cbmc/blob/develop/.gitignore#L59
and which is useful on the regression tests where cbmc is run with the --smt2 option.

[tautschnig]

Oops, I wasn't aware of that interaction.

[kroening]

I don't think that cbmc still writes the file on disk when run with --smt2?

[allredj]

@kroening some of the regression tests use --outfile, e.g. https://github.com/diffblue/cbmc/blob/develop/regression/cbmc/Malloc22/test.desc#L3

[allredj]

🚫
This PR failed Diffblue compatibility checks (cbmc commit: 817ce97).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99315203
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

• the cbmc commit has disappeared in the mean time (e.g. in a force-push)
• the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 361050f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99324952