This is necessary because what was there was invalid:
sorts<->types are not a bijection, since several Leon types compile to
the same sort (BV32) <-> (CharType, Int32Type).

By providing the expected type, we can reconstruct the correct model.
If the model uses expressions, we can no longer make sure we get the
right thing, and will guess using sorts.