[YICES] Fwd: RE: Question about Yices

[Hyondeuk Kim]

I sent you wrong file. I am sending you again.
Sorry for the inconvenience.

----
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 17:21:57 -0600 (MDT)
>From: Hyondeuk Kim <Hyondeuk.Kim at Colorado.EDU>  
>Subject: RE: [YICES] Fwd: RE: Question about Yices  
>To: Leonardo de Moura <leonardo at microsoft.com>, Bruno Dutertre <bruno at csl.sri.com>, Hyondeuk Kim <Hyondeuk.Kim at Colorado.EDU>
>Cc: yices at csl.sri.com
>
>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
>>
>________________
>sanity.qlock.5.induction.smt.cnf (49k bytes)
-------------- next part --------------
A non-text attachment was scrubbed...
Name: sanity.qlock.5.induction.smt
Type: application/octet-stream
Size: 31145 bytes
Desc: not available
Url : http://lists.csl.sri.com/pipermail/yices/attachments/20070618/889ccf4e/sanity.qlock.5.induction.obj