[YICES] Fwd: RE: Question about Yices

[Leonardo de Moura]

Hi Hyondeuk,

I'm completely lost. You sent us a satisfiable CNF file. Yices is producing the correct answer.

Leo


-----Original Message-----
From: Hyondeuk Kim [mailto:Hyondeuk.Kim at Colorado.EDU]
Sent: Monday, June 18, 2007 4:22 PM
To: Leonardo de Moura; Bruno Dutertre; Hyondeuk Kim
Cc: yices at csl.sri.com
Subject: RE: [YICES] Fwd: RE: Question about Yices

Hello Leonardo and Bruno,

Actually, I was trying partial example of qlock. I am sending you the example. It seems that Yices is giving wrong result to this example. The result is supposed to be unsat, but yices gives sat result with real solution.

thanks,

----
Hyondeuk Kim, Ph.D. Candidate
Department of Electrical & Computer Engineering
University of Colorado at Boulder
Email: Hyondeuk.Kim at colorado.edu

---- Original message ----
>Date: Mon, 18 Jun 2007 13:59:02 -0700
>From: Leonardo de Moura <leonardo at microsoft.com>
>Subject: RE: [YICES] Fwd: RE: Question about Yices
>To: Bruno Dutertre <bruno at csl.sri.com>, Hyondeuk Kim <Hyondeuk.Kim at Colorado.EDU>
>Cc: "yices at csl.sri.com" <yices at csl.sri.com>
>
>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
>