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

[Evgeni Kornikhin]

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