summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bug595.cvc
blob: c11cfb6e4538555ac9d18c90f3e34bf546130f4b (plain) 
1
2
3
4
5
6
7

% EXPECT: sat

f : INT -> [# i:INT, b:INT #];
a : INT;
ASSERT f(a) /= (# i := 0, b := 0 #);

CHECKSAT;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback