[YICES-HELP] logic definiton in yices v1

[André Scholz]

Hello,

why does

prompt> yices -smt test.smt

answer "sat" on the following file. More specific, why can i specify a variable 
to be Real, when i am using the logic of linear "integer" arithmetic? I can 
even omit the :logic line without Yices complaining. Does Yices infer which 
logic is needed for the given input?

The file "test.smt" contains:

(benchmark Test

:logic QF_LIA
:extrafuns ( (v_1 Real) )
:formula
(and
    (< 0 v_1)
    (< v_1 1)
)
)

Kind regards,
André

P.S.: I am not a member of this list. Please add me to the CC. Thank you.