Generate Z3 error messages with counter examples

[joom]

We can get-model from Z3, which we can then use to generate error messages for the Z3 rule that include counter examples.