[YICES-HELP] set-arith-only! prevents set-evidence! from working
(in some cases)?
johannes at albapasser.de
Sat Sep 1 07:39:52 PDT 2007
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))
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.
More information about the YICES-HELP