spec: Handle non-deterministic check results in array-ext workaround

If we fall back to the array-ext work around, it's possible Z3 will
return unknown on subsequent checks (or even unsat, though hopefully
not).  Deal with this.
spec: Don't try to continue when array-ext workaround fails

Things *don't* end well, so don't try.  Hopefully this will become
less important when Z3 issue #125 is addressed.
spec: Record testgen errors in the model file
profile: Add up and report testgen errors
profile: Show histograms of # tests per model path
Z3 debugging helpers
symtypes: Add and use SListBase._get_unchecked

This way callers don't have to reach into the internal representation
of SList to do this.