Further fixup for using output of get-value.

Rather than the previously used get-model command, which spammed Z3
internal gunk.