[YICES] Fwd: RE: Question about Yices

[Leonardo de Moura]

Hi Bruno,

Hyondeuk claims that yices produces a non integer model for one of the qlock benchmarks. I tried several of the satisfiable qlock benchmarks with yices, but I was not able to reproduce the problem.

Cheers,
Leo.



-----Original Message-----
From: yices-bounces+leonardo=microsoft.com at csl.sri.com [mailto:yices-bounces+leonardo=microsoft.com at csl.sri.com] On Behalf Of Bruno Dutertre
Sent: Monday, June 18, 2007 12:05 PM
To: Hyondeuk Kim
Cc: yices at csl.sri.com
Subject: Re: [YICES] Fwd: RE: Question about Yices

Hyondeuk Kim wrote:
> Hello Yices,
>
> Could you give more detailed explanation for below question?
>
> thanks,

What question?

Thanks

Bruno