[YICES-HELP] Re: Strange `sat' in API Lite

[Evgeni Kornikhin]

Oh, sorry-sorry-sorry, I miss a bracket:
>>         yicesl_read(ctx, "(assert (and a b)");
and Yices says it is satisfiable.


2009/5/27 Bruno Dutertre <bruno at csl.sri.com>:
> Evgeni Kornikhin wrote:
>>
>> Sorry, the right code is
>>
>>                int ctx = yicesl_mk_context();
>>                yicesl_read(ctx, "(define a::bool)");
>>                yicesl_read(ctx, "(define b::bool)");
>>                yicesl_read(ctx, "(assert (and a b))");
>>                yicesl_read(ctx, "(assert (and a (not b)))");
>>                yicesl_read(ctx, "(check)");
>>                return yicesl_inconsistent(ctx);
>>
>>
>>> Hello! I use the latest version of Yices for Windows. And yices.exe
>>> returns `unsat' for the following simple code:
>>> (define a::bool)
>>> (define b::bool)
>>> (assert (and a b))
>>> (assert (and a (not b)))
>>> (check)
>>>
>>> but yicesl_inconsistent(ctx) returns 0 (i.e. it thinks this code is
>>> satisfiable??)
>>>
>>>               int ctx = yicesl_mk_context();
>>>               yicesl_read(ctx, "(define a::bool)");
>>>               yicesl_read(ctx, "(define b::bool)");
>>>               yicesl_read(ctx, "(assert (or (and a b) (and a (not
>>> b))))");
>>>               yicesl_read(ctx, "(check)");
>>>               return yicesl_inconsistent(ctx);
>>>
>>> is this behavior of Yices correct ?
>>>
>>>
>>>
>>> Evgeni
>>>
>>
>
> Evgeni,
>
> I can't reproduce this behavior. yicesl_inconsistent(ctx) returns 1 when
> I run this code.
>
> Bruno
>
>
>