blob: c30f95550811ab3bc5977cae00d8fd5808f63541 (
plain)
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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
|
% EXPECT: unsat
DATATYPE DT1 =
DT1_a |
DT1_b |
DT1_c |
DT1_d |
DT1_e |
DT1_f |
DT1_g |
DT1_h |
DT1_i |
DT1_j |
DT1_k |
DT1_l |
DT1_m |
DT1_n |
DT1_o |
DT1_p |
DT1_q |
DT1_r |
DT1_s |
DT1_t |
DT1_u |
DT1_v |
DT1_w |
DT1_x |
DT1_y |
DT1_z
END;
DATATYPE DT2 =
DT2_a |
DT2_b |
DT2_c |
DT2_d
END;
DATATYPE DT3 =
DT3_a |
DT3_b
END;
var1 : DT3;
var2 : DT3;
var3 : DT1;
var4 : DT3;
var5 : DT3;
var6 : DT3;
var7 : DT3;
var8 : DT3;
var9 : DT3;
var10 : DT3;
var11 : DT2;
var12 : DT3;
var13 : DT3;
var14 : DT3;
var16 : DT3;
var17 : DT3;
var18 : DT3;
var20 : DT3;
var21 : DT3;
CHECKSAT
(
(((NOT(var13 = DT3_a)) AND (NOT(var10 = DT3_b))) AND (NOT((((((var7 = DT3_b) AND (var4 = DT3_b)) AND (var1 = DT3_a)) OR ((((var5 = DT3_a) AND (var17 = DT3_b)) OR ((var21 = DT3_b) AND ((var3 = DT1_f) OR (var3 = DT1_g)))) <=> (DT3_b = DT3_b))) OR (((var14 = DT3_a) AND (var2 = DT3_a)) AND (((((var8 = DT3_a) AND (var18 = DT3_b)) OR ((var6 = DT3_a) AND (var11 /= DT2_a))) OR (var20 = DT3_b)) OR (var9 = DT3_b)))) OR ((NOT(((((var7 = DT3_b) AND (var4 = DT3_b)) AND (var1 = DT3_a)) OR ((((var5 = DT3_a) AND (var17 = DT3_b)) OR ((var21 = DT3_b) AND ((var3 = DT1_f) OR (var3 = DT1_g)))) <=> (DT3_b = DT3_b))) OR (((var14 = DT3_a) AND (var2 = DT3_a)) AND (((((var8 = DT3_a) AND (var18 = DT3_b)) OR ((var6 = DT3_a) AND (var11 /= DT2_a))) OR (var20 = DT3_b)) OR (var9 = DT3_b))))) AND ((var14 = DT3_b) AND (TRUE))))))
AND
(NOT((var12 = DT3_a) OR ((var12 = DT3_b) AND ((var16 = DT3_b) OR (TRUE)))))
);
|
