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

[Bruno Dutertre]

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