[YICES] Fwd: RE: Question about Yices

Bruno Dutertre 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.
> 

Hyondeuk,

The file you sent is not in a valid SMT-LIB format. The
declarations

: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.

Bruno



More information about the YICES mailing list