[YICES-HELP] set-arith-only! prevents set-evidence! from working
(in some cases)?
johannes at albapasser.de
Wed Sep 5 00:04:14 PDT 2007
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.
More information about the YICES-HELP