New model parser for SMTv2 outputs, with stronger type checking

This branch implements a new implementation of the interpretation of SMT models. It directly constructs Why3 terms instead of intermediate values in an ad-hoc datatype.

As a side effect, we expect that the obtained counterexample is always well-typed, which currently poorly ensured.