[YICES] Fwd: RE: Question about Yices

Hyondeuk Kim Hyondeuk.Kim at Colorado.EDU
Mon Jun 18 16:21:57 PDT 2007

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.


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.
>-----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?
-------------- next part --------------
A non-text attachment was scrubbed...
Name: sanity.qlock.5.induction.smt.cnf
Type: application/octet-stream
Size: 36609 bytes
Desc: not available
Url : http://lists.csl.sri.com/pipermail/yices/attachments/20070618/e3ded7d0/sanity.qlock.5.induction.smt.obj

More information about the YICES mailing list