[YICES] Fwd: RE: Question about Yices
bruno at csl.sri.com
Mon Jun 18 16:50:30 PDT 2007
Hyondeuk Kim wrote:
> I sent you wrong file. I am sending you again.
> Sorry for the inconvenience.
The file you sent is not in a valid SMT-LIB format. The
:extrapreds ((x_40 Int))
:extrapreds ((x_41 Int))
:extrapreds ((x_42 Int))
mean that x_40, x_41, x_42, etc. are predicates with integer
arguments. That should not occur in the QF_IDL logic.
Then when you write
(= (- x_42 x_41) 1)
Yices gets confused. Because Yices assumes all input in SMT-LIB
are type correct, it does not do any typechecking.
The correct behavior in this case would be to report an error.
Try to use yices -tc to see the error message.
The correct declarations should be:
:extrafuns ((x_40 Int))
:extrafuns ((x_41 Int))
If you do that, yices will answer unsat.
More information about the YICES