Check why MultEven is invalid with z3.
Testing MultEven with the z3-translation currently yields "unsatisfiable".
The generated counterexample is interesting, because it does not actually satisfy all assertions.
It ignores that x * y == res
and just uses x = 2, y = -2, res = -1
as a model.