Ticket #5: gzip_hello_edited.report

File gzip_hello_edited.report, 12.1 KB (added by Vladimír Štill, 6 months ago)

Valid report with stdin stripped

Line 
1states per second: 2195.05
2state count: 799
3mips: 0.512332
4
5version: 4.1.6+43d9a505081f
6architecture: Intel(R) Core(TM) i5-4690 CPU @ 3.50GHz
7memory used: 598684
8physical memory used: 517368
9user time: 4.429853
10system time: 0.170765
11wall time: 3.547207
12
13fragment memory:
14  total: { items: 2439, used: 56737929, held: 59569704 }
15  1: { items: 9, used: 9, held: 12264 }
16  2: { items: 2, used: 4, held: 8176 }
17  3: { items: 2, used: 6, held: 4088 }
18  4: { items: 9, used: 36, held: 20440 }
19  6: { items: 1, used: 6, held: 4088 }
20  7: { items: 1, used: 7, held: 4088 }
21  8: { items: 12, used: 96, held: 20440 }
22  10: { items: 1, used: 10, held: 8160 }
23  12: { items: 1, used: 12, held: 20400 }
24  16: { items: 9, used: 144, held: 20400 }
25  20: { items: 3, used: 60, held: 20400 }
26  24: { items: 27, used: 648, held: 20400 }
27  25: { items: 1, used: 25, held: 16256 }
28  28: { items: 0, used: 0, held: 16256 }
29  29: { items: 1, used: 29, held: 4064 }
30  32: { items: 15, used: 480, held: 20320 }
31  33: { items: 1, used: 33, held: 12240 }
32  36: { items: 0, used: 0, held: 16320 }
33  40: { items: 9, used: 360, held: 12240 }
34  41: { items: 1, used: 41, held: 20400 }
35  44: { items: 1, used: 44, held: 8160 }
36  48: { items: 216, used: 10368, held: 20400 }
37  49: { items: 2, used: 98, held: 8176 }
38  50: { items: 1, used: 50, held: 8176 }
39  52: { items: 0, used: 0, held: 16352 }
40  56: { items: 5, used: 280, held: 20440 }
41  57: { items: 0, used: 0, held: 8064 }
42  58: { items: 1, used: 58, held: 8064 }
43  60: { items: 1, used: 60, held: 8064 }
44  64: { items: 6, used: 384, held: 12096 }
45  65: { items: 1, used: 65, held: 8064 }
46  66: { items: 1, used: 66, held: 12096 }
47  67: { items: 21, used: 1407, held: 20160 }
48  68: { items: 426, used: 28968, held: 81504 }
49  69: { items: 2, used: 138, held: 20160 }
50  70: { items: 1, used: 70, held: 16128 }
51  72: { items: 0, used: 0, held: 4032 }
52  73: { items: 2, used: 146, held: 12240 }
53  74: { items: 1, used: 74, held: 8160 }
54  76: { items: 0, used: 0, held: 4080 }
55  77: { items: 1, used: 77, held: 4080 }
56  78: { items: 0, used: 0, held: 16320 }
57  80: { items: 112, used: 8960, held: 20400 }
58  81: { items: 1, used: 81, held: 12144 }
59  82: { items: 1, used: 82, held: 4048 }
60  83: { items: 0, used: 0, held: 4048 }
61  84: { items: 0, used: 0, held: 4048 }
62  85: { items: 1, used: 85, held: 4048 }
63  87: { items: 1, used: 87, held: 8096 }
64  88: { items: 2, used: 176, held: 12144 }
65  89: { items: 1, used: 89, held: 4032 }
66  90: { items: 1, used: 90, held: 12096 }
67  93: { items: 0, used: 0, held: 4032 }
68  96: { items: 6, used: 576, held: 8064 }
69  97: { items: 1, used: 97, held: 20280 }
70  98: { items: 1, used: 98, held: 12168 }
71  101: { items: 6, used: 606, held: 16224 }
72  104: { items: 2, used: 208, held: 12168 }
73  105: { items: 1, used: 105, held: 4032 }
74  107: { items: 0, used: 0, held: 4032 }
75  108: { items: 2, used: 216, held: 12096 }
76  109: { items: 1, used: 109, held: 4032 }
77  110: { items: 1, used: 110, held: 4032 }
78  112: { items: 1, used: 112, held: 4032 }
79  114: { items: 0, used: 0, held: 8160 }
80  116: { items: 1, used: 116, held: 8160 }
81  117: { items: 1, used: 117, held: 4080 }
82  119: { items: 0, used: 0, held: 4080 }
83  120: { items: 2, used: 240, held: 4080 }
84  123: { items: 0, used: 0, held: 15872 }
85  124: { items: 0, used: 0, held: 3968 }
86  125: { items: 1, used: 125, held: 7936 }
87  128: { items: 111, used: 14208, held: 19840 }
88  129: { items: 1, used: 129, held: 4080 }
89  130: { items: 1, used: 130, held: 12240 }
90  131: { items: 1, used: 131, held: 8160 }
91  133: { items: 1, used: 133, held: 4080 }
92  137: { items: 1, used: 137, held: 8064 }
93  141: { items: 1, used: 141, held: 8064 }
94  144: { items: 2, used: 288, held: 4032 }
95  146: { items: 0, used: 0, held: 3952 }
96  147: { items: 0, used: 0, held: 3952 }
97  150: { items: 0, used: 0, held: 3952 }
98  152: { items: 0, used: 0, held: 7904 }
99  154: { items: 0, used: 0, held: 16000 }
100  156: { items: 1, used: 156, held: 4000 }
101  158: { items: 1, used: 158, held: 4000 }
102  161: { items: 0, used: 0, held: 4032 }
103  167: { items: 0, used: 0, held: 4032 }
104  170: { items: 0, used: 0, held: 4048 }
105  173: { items: 1, used: 173, held: 4048 }
106  184: { items: 1, used: 184, held: 4048 }
107  186: { items: 1, used: 186, held: 4032 }
108  194: { items: 1, used: 194, held: 4000 }
109  197: { items: 0, used: 0, held: 4000 }
110  201: { items: 1, used: 201, held: 3952 }
111  206: { items: 0, used: 0, held: 3952 }
112  211: { items: 1, used: 211, held: 3888 }
113  231: { items: 1, used: 231, held: 3944 }
114  243: { items: 1, used: 243, held: 3968 }
115  246: { items: 0, used: 0, held: 3968 }
116  259: { items: 1, used: 259, held: 3960 }
117  269: { items: 6, used: 1614, held: 20400 }
118  274: { items: 0, used: 0, held: 3920 }
119  276: { items: 1, used: 276, held: 3920 }
120  286: { items: 0, used: 0, held: 8064 }
121  294: { items: 0, used: 0, held: 3848 }
122  314: { items: 0, used: 0, held: 3840 }
123  329: { items: 0, used: 0, held: 4032 }
124  341: { items: 2, used: 682, held: 7568 }
125  342: { items: 1, used: 342, held: 3784 }
126  348: { items: 0, used: 0, held: 3872 }
127  350: { items: 0, used: 0, held: 3872 }
128  351: { items: 0, used: 0, held: 3872 }
129  357: { items: 0, used: 0, held: 3960 }
130  367: { items: 1, used: 367, held: 4048 }
131  404: { items: 1, used: 404, held: 4080 }
132  420: { items: 1, used: 420, held: 3816 }
133  469: { items: 1, used: 469, held: 3776 }
134  498: { items: 1, used: 498, held: 4032 }
135  512: { items: 1, used: 512, held: 3584 }
136  522: { items: 1, used: 522, held: 3696 }
137  528: { items: 23, used: 12144, held: 14784 }
138  587: { items: 1, used: 587, held: 17760 }
139  602: { items: 1, used: 602, held: 3648 }
140  607: { items: 1, used: 607, held: 3648 }
141  612: { items: 1, used: 612, held: 3696 }
142  653: { items: 3, used: 1959, held: 11808 }
143  703: { items: 1, used: 703, held: 3520 }
144  791: { items: 1, used: 791, held: 3960 }
145  879: { items: 1, used: 879, held: 3520 }
146  996: { items: 1, used: 996, held: 4000 }
147  1024: { items: 1, used: 1024, held: 3072 }
148  1075: { items: 6, used: 6450, held: 9720 }
149  1084: { items: 1, used: 1084, held: 3264 }
150  1105: { items: 1, used: 1105, held: 3336 }
151  1115: { items: 1, used: 1115, held: 3360 }
152  1152: { items: 288, used: 331776, held: 859392 }
153  1264: { items: 1, used: 1264, held: 3792 }
154  1738: { items: 6, used: 10428, held: 29648 }
155  1791: { items: 1, used: 1791, held: 7168 }
156  1920: { items: 1, used: 1920, held: 7680 }
157  1955: { items: 1, used: 1955, held: 3920 }
158  1996: { items: 1, used: 1996, held: 4000 }
159  2062: { items: 581, used: 1198022, held: 1632624 }
160  2064: { items: 121, used: 249744, held: 321984 }
161  2880: { items: 1, used: 2880, held: 2880 }
162  3920: { items: 182, used: 713440, held: 1364160 }
163  354652: { items: 121, used: 42912892, held: 42913376 }
164  3680304: { items: 1, used: 3680304, held: 3680304 }
165  7518416: { items: 1, used: 7518416, held: 7518416 }
166snapshot memory:
167  total: { items: 799, used: 846480, held: 1725072 }
168  288: { items: 1, used: 288, held: 4032 }
169  372: { items: 1, used: 372, held: 3760 }
170  480: { items: 5, used: 2400, held: 11520 }
171  492: { items: 20, used: 9840, held: 15872 }
172  516: { items: 1, used: 516, held: 3640 }
173  600: { items: 1, used: 600, held: 3600 }
174  672: { items: 126, used: 84672, held: 211008 }
175  684: { items: 5, used: 3420, held: 13760 }
176  696: { items: 1, used: 696, held: 3480 }
177  720: { items: 1, used: 720, held: 3600 }
178  744: { items: 290, used: 215760, held: 342240 }
179  756: { items: 18, used: 13608, held: 31160 }
180  768: { items: 2, used: 1536, held: 7680 }
181  780: { items: 2, used: 1560, held: 7840 }
182  792: { items: 2, used: 1584, held: 7920 }
183  804: { items: 2, used: 1608, held: 8080 }
184  816: { items: 2, used: 1632, held: 8160 }
185  828: { items: 2, used: 1656, held: 6656 }
186  840: { items: 2, used: 1680, held: 3360 }
187  852: { items: 4, used: 3408, held: 10272 }
188  864: { items: 2, used: 1728, held: 6912 }
189  876: { items: 2, used: 1752, held: 7040 }
190  888: { items: 2, used: 1776, held: 7104 }
191  900: { items: 2, used: 1800, held: 7232 }
192  912: { items: 2, used: 1824, held: 3648 }
193  924: { items: 2, used: 1848, held: 7424 }
194  936: { items: 2, used: 1872, held: 7488 }
195  948: { items: 3, used: 2844, held: 7616 }
196  960: { items: 2, used: 1920, held: 7680 }
197  972: { items: 2, used: 1944, held: 7808 }
198  984: { items: 2, used: 1968, held: 7872 }
199  996: { items: 2, used: 1992, held: 8000 }
200  1008: { items: 2, used: 2016, held: 8064 }
201  1020: { items: 2, used: 2040, held: 6144 }
202  1032: { items: 2, used: 2064, held: 6192 }
203  1044: { items: 3, used: 3132, held: 9432 }
204  1056: { items: 2, used: 2112, held: 6336 }
205  1068: { items: 2, used: 2136, held: 6432 }
206  1080: { items: 2, used: 2160, held: 6480 }
207  1092: { items: 2, used: 2184, held: 6576 }
208  1104: { items: 2, used: 2208, held: 6624 }
209  1116: { items: 2, used: 2232, held: 6720 }
210  1128: { items: 2, used: 2256, held: 6768 }
211  1140: { items: 3, used: 3420, held: 10296 }
212  1152: { items: 2, used: 2304, held: 6912 }
213  1164: { items: 2, used: 2328, held: 7008 }
214  1176: { items: 2, used: 2352, held: 3528 }
215  1188: { items: 2, used: 2376, held: 7152 }
216  1200: { items: 2, used: 2400, held: 7200 }
217  1212: { items: 2, used: 2424, held: 7296 }
218  1224: { items: 2, used: 2448, held: 7344 }
219  1236: { items: 4, used: 4944, held: 11160 }
220  1248: { items: 2, used: 2496, held: 7488 }
221  1260: { items: 2, used: 2520, held: 7584 }
222  1272: { items: 2, used: 2544, held: 7632 }
223  1284: { items: 2, used: 2568, held: 7728 }
224  1296: { items: 2, used: 2592, held: 3888 }
225  1308: { items: 2, used: 2616, held: 7872 }
226  1320: { items: 2, used: 2640, held: 7920 }
227  1332: { items: 3, used: 3996, held: 12024 }
228  1344: { items: 2, used: 2688, held: 8064 }
229  1356: { items: 2, used: 2712, held: 8160 }
230  1368: { items: 2, used: 2736, held: 5472 }
231  1380: { items: 2, used: 2760, held: 5536 }
232  1392: { items: 2, used: 2784, held: 5568 }
233  1404: { items: 2, used: 2808, held: 5632 }
234  1416: { items: 2, used: 2832, held: 5664 }
235  1428: { items: 3, used: 4284, held: 8592 }
236  1440: { items: 2, used: 2880, held: 2880 }
237  1452: { items: 2, used: 2904, held: 5824 }
238  1464: { items: 2, used: 2928, held: 5856 }
239  1476: { items: 2, used: 2952, held: 5920 }
240  1488: { items: 2, used: 2976, held: 5952 }
241  1500: { items: 2, used: 3000, held: 6016 }
242  1512: { items: 2, used: 3024, held: 6048 }
243  1524: { items: 3, used: 4572, held: 9168 }
244  1536: { items: 2, used: 3072, held: 6144 }
245  1548: { items: 2, used: 3096, held: 6208 }
246  1560: { items: 2, used: 3120, held: 6240 }
247  1572: { items: 2, used: 3144, held: 6304 }
248  1584: { items: 2, used: 3168, held: 6336 }
249  1596: { items: 2, used: 3192, held: 6400 }
250  1608: { items: 2, used: 3216, held: 3216 }
251  1620: { items: 4, used: 6480, held: 9744 }
252  1632: { items: 2, used: 3264, held: 6528 }
253  1644: { items: 2, used: 3288, held: 6592 }
254  1656: { items: 2, used: 3312, held: 6624 }
255  1668: { items: 2, used: 3336, held: 6688 }
256  1680: { items: 4, used: 6720, held: 10080 }
257  1692: { items: 3, used: 5076, held: 6784 }
258  1704: { items: 4, used: 6816, held: 10224 }
259  1716: { items: 4, used: 6864, held: 6880 }
260  1728: { items: 4, used: 6912, held: 10368 }
261  1740: { items: 3, used: 5220, held: 10464 }
262  1752: { items: 4, used: 7008, held: 10512 }
263  1764: { items: 4, used: 7056, held: 10608 }
264  1776: { items: 4, used: 7104, held: 23088 }
265  1788: { items: 3, used: 5364, held: 10752 }
266  1800: { items: 4, used: 7200, held: 10800 }
267  1812: { items: 5, used: 9060, held: 10896 }
268  1824: { items: 4, used: 7296, held: 14592 }
269  1836: { items: 3, used: 5508, held: 7360 }
270  1848: { items: 4, used: 7392, held: 11088 }
271  1860: { items: 4, used: 7440, held: 11184 }
272  1872: { items: 4, used: 7488, held: 7488 }
273  1884: { items: 3, used: 5652, held: 7552 }
274  1896: { items: 4, used: 7584, held: 11376 }
275  1908: { items: 4, used: 7632, held: 11472 }
276  1920: { items: 4, used: 7680, held: 11520 }
277  1932: { items: 3, used: 5796, held: 7744 }
278  1944: { items: 3, used: 5832, held: 11664 }
279  1956: { items: 10, used: 19560, held: 47040 }
280  1968: { items: 3, used: 5904, held: 11808 }
281  1980: { items: 3, used: 5940, held: 11904 }
282  1992: { items: 3, used: 5976, held: 7968 }
283  2004: { items: 35, used: 70140, held: 144576 }
284  2016: { items: 25, used: 50400, held: 80640 }
285input file: ./gzip
286input options:
287  arg.0: "-f"
288  arg.1: "-d"
289  arg.2: "-"
290  sys.0: nofail:malloc
291  divine.bcname: ./gzip
292smt solver: stp
293property type: safety
294timers:
295  lart: 0.775
296  loader: 1.39
297  boot: 0.126
298  search: 0.364
299  ce: 0.034
300error found: no