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

[Johannes Waldmann]

for the following program,


(define-type foo (record bar :: nat))

(define a :: foo)
(define b :: foo)

(define gt :: (-> foo foo bool)
        (lambda (x :: foo y :: foo)  (> (select x foo) (select y foo))))

(assert (gt a b))

(check)


yices correctly finds a model,
and it is output after "-e" on the command line
resp. (set-evidence! true)  in the source.

now, if I switch on (set-arith-only! true) in the source,
yices still says "sat", but it will not print the model
(via either of the above methods).

I am not sure whether "arith-only" is applicable here
but if I change the assertion to (gt a a) yices says "unsat",
so the engine seems to be working fine.

I am asking because I have a larger program
where arith-only gives a noticeable speedup
but it is not much use if I don't see the model afterwards.


Best regards, Johannes Waldmann.