path: root/test/regress/regress0/push-pop/bug233.cvc

% Tests the invariants for multiple queries.
% COMMAND-LINE: --incremental

a, b: BOOLEAN;

% EXPECT: entailed
QUERY (a AND b) OR NOT (a AND b);

% EXPECT: not_entailed
QUERY (a OR b);