path: root/test/regress/regress0/cvc-rerror-print.cvc

% EXPECT: valid
% EXPECT: Cannot get model unless immediately preceded by SAT/INVALID or UNKNOWN response.
OPTION "logic" "ALL";
OPTION "produce-models" true;
x : INT;
QUERY x = x;
COUNTEREXAMPLE;