summaryrefslogtreecommitdiff
path: root/test/regress/regress0/cvc-rerror-print.cvc
blob: e134b56667cac782036eb6920a880f26a9e8f488 (plain)
1
2
3
4
5
6
7
% EXPECT: entailed
% EXPECT: Cannot get model unless immediately preceded by SAT/NOT_ENTAILED or UNKNOWN response.
OPTION "logic" "ALL";
OPTION "produce-models" true;
x : INT;
QUERY x = x;
COUNTEREXAMPLE;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback