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

% EXPECT: sat

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

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