[YICES] Fwd: RE: Question about Yices

Leonardo de Moura leonardo at microsoft.com
Mon Jun 18 13:59:02 PDT 2007

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.


-----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?



More information about the YICES mailing list