summaryrefslogtreecommitdiff
path: root/test/regress/regress0/cvc3.userdoc.02.cvc
blob: b6329e9531181257a0b8a5dd42ecbb1c6ccbe54a (plain) 
1
2
3
4
5
6
7

x : BITVECTOR(5);
y : BITVECTOR(4);
yy : BITVECTOR(3);

% EXPECT: valid
QUERY
 BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11))[8:4] = BVPLUS(5, x, ~(y[3:2])) ;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback