[YICES] Fwd: RE: Question about Yices
Leonardo de Moura
leonardo at microsoft.com
Mon Jun 18 16:29:36 PDT 2007
I'm completely lost. You sent us a satisfiable CNF file. Yices is producing the correct answer.
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.
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>
>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