hacky fix to parse string constants as integer sorts

This is required to let Z3 know that all strings are different when
calling SMT. The parser only knows about ints and bools, because we do
not want type annotations in the .star files just yet. In particular,
this prevents the parser from using a third sort "string".

Before this fix, the examples involving strings did not pass correctly
because the parser interpreted them as integers (to get well-typed
expressions), but the prover only acts on strings of sort String.

Now strings are of sort Integer, in accordance with the parser.