summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bv/div_mod.cvc
blob: 3f31bdd70d31794ff61aaf0d53443fe003e3cc25 (plain) 
1
2
3
4
5
6
7
8
9
10

% EXPECT: entailed

x : BITVECTOR(4);

QUERY
( BVUDIV(x, 0bin0000) = 0bin1111 ) AND
( BVUREM(x, 0bin0000) = x ) AND
( BVSDIV(x, 0bin0000) = 0bin1111 OR BVSDIV(x, 0bin0000) = 0bin0001 ) AND
( BVSREM(x, 0bin0000) = x ) AND
( BVSMOD(x, 0bin0000) = x );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback