[YICES] Fwd: RE: Question about Yices

[Bruno Dutertre]

Hyondeuk Kim wrote:
> 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,
> 
> ----

I don't understand the problem. The example you sent is a propositional problem in dimacs
format. Are you sure this is the right file?

Bruno