Better error message for mismatching sorts in substitutions

[rindPHI]

When substituting expressions in the Z3 API, the error message in case of a sort mismatch was confusing:

import z3

# x * y
expr = z3.Int('x') * z3.Int('y')

# (x * y)[z / x]
subst_expr = z3.substitute(expr, (z3.Int('x'), z3.Int('z')))

# Wrong type:
try:
    subst_expr = z3.substitute(expr, (z3.String('x'), z3.Int('z')))
except z3.z3types.Z3Exception as exc:
    print(exc)  # -> "Z3 invalid substitution, expression pairs expected."

In the above example, expression pairs were passed, only with the wrong type. This issue confused me a lot in my beginner times with Z3, and currently, it's confusing my students ;)

This pull request leads to the, in my opinion more meaningful, error message 'Z3 invalid substitution, mismatching "from" and "to" sorts.' in that case.

[NikolajBjorner]

thanks!