[YICES] Fwd: RE: Question about Yices
Leonardo de Moura
leonardo at microsoft.com
Mon Jun 18 13:59:02 PDT 2007
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.
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?
More information about the YICES