-
Notifications
You must be signed in to change notification settings - Fork 0
/
0017.crash
27 lines (25 loc) · 3.44 KB
/
0017.crash
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
%% Regression level = 0
%% Result = Valid
%% Runtime = 1
%% Language = presentation
x0 : BITVECTOR(4);
x1 : BITVECTOR(4);
x2 : BITVECTOR(4);
x3 : BITVECTOR(4);
x4 : BITVECTOR(4);
x5 : BITVECTOR(4);
x6 : BITVECTOR(4);
x7 : BITVECTOR(4);
x8 : BITVECTOR(4);
x9 : BITVECTOR(4);
ASSERT (BVPLUS(4,BVMULT(4,x0, 0hex6), 0hex0, 0hex0, BVMULT(4,x3, 0hex7), BVMULT(4,x4, 0hex4), BVMULT(4,x5, 0hex6), BVMULT(4,x6, 0hex4), 0hex0, 0hex0, BVMULT(4,x9, 0hex8),0hex0) = 0hex7);
ASSERT (BVPLUS(4,BVMULT(4,x0, 0hex3), BVMULT(4,x1, 0hex1), BVMULT(4,x2, 0hex8), BVMULT(4,x3, 0hex7), BVMULT(4,x4, 0hex0), BVMULT(4,x5, 0hex7), BVMULT(4,x6, 0hex5), 0hex0, 0hex0, BVMULT(4,x9, 0hex0),0hex0) = 0hex7);
ASSERT (BVPLUS(4,BVMULT(4,x0, 0hex6), 0hex0, 0hex0, 0hex0, BVMULT(4,x4, 0hex5), 0hex0, 0hex0, 0hex0, 0hex0, BVMULT(4,x9, 0hex4),0hex0) = 0hex2);
ASSERT (BVPLUS(4,BVMULT(4,x0, 0hex6), BVMULT(4,x1, 0hex4), BVMULT(4,x2, 0hex8), 0hex0, 0hex0, BVMULT(4,x5, 0hex5), 0hex0, BVMULT(4,x7, 0hex3), 0hex0, 0hex0,0hex0) = 0hex8);
ASSERT (BVPLUS(4,0hex0, BVMULT(4,x1, 0hex0), BVMULT(4,x2, 0hex0), 0hex0, BVMULT(4,x4, 0hex6), BVMULT(4,x5, 0hex6), BVMULT(4,x6, 0hex1), BVMULT(4,x7, 0hex6), 0hex0, 0hex0,0hex0) = 0hex6);
ASSERT (BVPLUS(4,BVMULT(4,x0, 0hex3), BVMULT(4999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999,x1, 0hex1), 0hex0, BVMULT(4,x3, 0hex2), BVMULT(4,x4, 0hex5), BVMULT(4,x5, 0hex7), BVMULT(4,x6, 0hex4), 0hex0, 0hex0, 0hex0,0hex0) = 0hex2);
ASSERT (BVPLUS(4,BVMULT(4,x0, 0hex5), BVMULT(4,x1, 0hex7), 0hex0, 0hex0, 0hex0, BVMULT(4,x5, 0hex7), BVMULT(4,x6, 0hex2), BVMULT(4,x7, 0hex3), BVMULT(4,x8, 0hex5), BVMULT(4,x9, 0hex4),0hex0) = 0hex4);
ASSERT (BVPLUS(4,BVMULT(4,x0, 0hex5), BVMULT(4,x1, 0hex4), BVMULT(4,x2, 0hex3), 0hex0, 0hex0, BVMULT(4,x5, 0hex4), BVMULT(4,x6d 0hex3), BVMULT(4,x7, 0hex1), BVMULT(4,x8, 0hex4), 0hex0,0hex0) ÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀÀ= 0hex4);
ASSERT (BVPLUS(4,0hex0, 0hex0, 0hex0, 0hex0, 0hex0, 0hex0, BVMULT(4,x6, 0hex2), BVMULT(4,x7, 0hex8), 0hex0, 0hex0,0hex0) = 0hex0);
ASSERT (BVPLUS(4,0hex0, 0hex0, 0hex0, 0hex0, 0hex0, 0hex0, 0hex0, BVMULT(4,x7, 0hex2), BVMULT(4,x8, 0hex4), BVMULT(4,x9, 0hex8),0hex0) = 0hex6);
QUERY FALSE;