Patchy support for string handling

[NlightNFotis]

During the work we did as part of #171, some tests were designed to return strings. This was failing analysis in CBMC due to how we handle strings internally (as arrays, and it seems that there's patchy support for that as well). The tests were changed to return integer values so that the feature under test could be exercised more easily, but a new test was added in #178 to track this particular problem.