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

[Bruno Dutertre]

Johannes Waldmann wrote:
> 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.
> 
> 
> 

Hi Johannes,

A model is generated but nothing is displayed because there are no
arithmetic variables in your specifications.

In any case, you should not use (set-arith-only! true) on this
example. As the name indicates that's reserved for specifications that
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.

Bruno