Update with latest z3 counter-example

This is a ramification of including test cases that rely on
counter-examples. Unless it’s unique, the new version of the solver can
return a different cex.. sigh..
Z3: model-extraction

Carefully align SReal value extraction, to work better with the new
one-shot algorithm. (See issue #86).
Add float/double tests..