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

[Evgeni Kornikhin]

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
>