summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bv/core/equality-02.cvc
blob: e8f51d61ad5f349297b9816705cf4a238e5468a7 (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

x0, x1, x2, x3 : BITVECTOR(32);
y0, y1, y2, y3 : BITVECTOR(32);

ASSERT (x0 = x1);
ASSERT (x1 = x2);
ASSERT (x2 = x3);

ASSERT (y0 = y1);
ASSERT (y1 = y2);
ASSERT (y2 = y3);

ASSERT (x0 = y0);

QUERY (x3 = y3);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback