summaryrefslogtreecommitdiff
path: root/test/regress/regress0/cvc-rerror-print.cvc
blob: 728db28d87cdebdbf1fe93228466e3d6cf104bfa (plain)
1
2
3
4
5
6
7
% EXPECT: entailed
% EXPECT: Cannot get model unless after a SAT 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