Fixed model construction and tests.

The construction of numeric models did wrongly assume 0 could be used as a
default value.  This lead to buggy array models when one array contained 0 at a
position where the other array was unconstrained, but the arrays had to differ.
This update fixes this problem by delaying the creation of the default value for
numeric sorts until all values induced by the partial models of the other theory
solvers are aggregated.  We then choose a fresh value.

Fixed the tests related to the model evaluation.  Made model evaluation
independent of an assumption on the index of true and false.  Fixed output of
function symbols in the get-model call.  They are now quoted if needed.