[YICES-HELP] set-arith-only! prevents set-evidence! from working (in some cases)?

[Johannes Waldmann]

Bruno Dutertre wrote:

> contain only arithmetic. Records are not part of the arithmetic
> fragment. It's a lucky coincidence that you get the right
> answer in two cases.

Thanks for the response.

I respectfully suggest that yices checks whether set-arith-only!
is applicable, and if not, complains loudly and rejects the input.
Even a segfault would be better than writing "(un)sat"
that may or may not be correct.

Best regards, Johannes Waldmann.