Tool 2LS 0.7.2-sv-comp19 CBMC CBMC Path 5.10 () CPAchecker 1.7-svn 29852 DepthK 3.1 DIVINE ESBMC version 6.0.0 64-bit x86_64 linux Map2Check v7.2-Flock : Tue Nov 27 22:00:00 -04 2018 PeSCo 1.7-svn b8d6131600+ Pinaka 0.1 skink 2.0 SMACK 1.9.3 symbiotic 6.0.3-77d4af47 ULTIMATE Automizer 0.1.23-635dfa2a ULTIMATE Kojak 0.1.23-635dfa2a ULTIMATE Taipan 0.1.23-635dfa2a VeriAbs 1.3.10 VeriFuzz 1.0.0 VerifierIntegerAssignmentPrograms 1.1.12(Date 28/11/2018)
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-04 22:44:17 CET 2018-12-04 22:48:40 CET 2018-12-04 22:45:10 CET 2018-12-05 05:46:16 CET 2018-12-05 09:36:33 CET 2018-12-10 10:00:20 CET 2018-12-06 11:06:04 CET 2018-12-06 11:03:31 CET 2018-12-06 12:20:21 CET 2018-12-06 12:44:04 CET 2018-12-06 20:14:43 CET 2018-12-07 12:00:55 CET 2018-12-07 19:13:55 CET 2018-12-07 21:42:05 CET 2018-12-08 07:42:40 CET 2018-12-08 11:04:44 CET 2018-12-08 14:19:36 CET 2018-12-10 16:50:17 CET 2018-12-09 02:47:33 CET 2018-12-09 18:49:43 CET
Run set 2ls.sv-comp19_prop-reachsafety.ReachSafety-Arrays cbmc.sv-comp19_prop-reachsafety.ReachSafety-Arrays cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Arrays cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Arrays depthk.sv-comp19_prop-reachsafety.ReachSafety-Arrays divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-Arrays divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Arrays esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Arrays map2check.sv-comp19_prop-reachsafety.ReachSafety-Arrays pesco.sv-comp19_prop-reachsafety.ReachSafety-Arrays pinaka.sv-comp19_prop-reachsafety.ReachSafety-Arrays skink.sv-comp19_prop-reachsafety.ReachSafety-Arrays smack.sv-comp19_prop-reachsafety.ReachSafety-Arrays symbiotic.sv-comp19_prop-reachsafety.ReachSafety-Arrays uautomizer.sv-comp19_prop-reachsafety.ReachSafety-Arrays ukojak.sv-comp19_prop-reachsafety.ReachSafety-Arrays utaipan.sv-comp19_prop-reachsafety.ReachSafety-Arrays veriabs.sv-comp19_prop-reachsafety.ReachSafety-Arrays verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Arrays viap.sv-comp19_prop-reachsafety.ReachSafety-Arrays
Options --graphml-witness witness.graphml --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp19 -heap 10000M -benchmark -timelimit 900s --no-symbolic -s kinduction -svcomp19-pesco -heap 10000M -stack 2048k -benchmark -timelimit 900s --graphml-witness witness.graphml -w error-witness.graphml --witness witness.graphml --full-output --full-output --full-output
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i error (134) .084 24 .76 0 out of memory 200     14000   1800    0 error (42) 880     1600   12000    0 timeout 960   6200 7100 0 unknown 900    1600 13000   0 unknown 8.0 430 98 0 unknown 7.9 430 85 0 true .11  26 .94 -32 unknown .89 40 13   0 unknown 100 2800 1000 0 out of memory 310    15000 3800   0 false(unreach-call) 6.2 320 49 1 disqualified 4.1 120 45 0 false(unreach-call) 1.3  110 17   1 timeout 900   1700 11000 0 timeout 900   5400 11000 0 timeout 900   1900 12000 0 out of memory 66   15000 830 0 false(unreach-call) 5.0 1300 52 1 unknown 42   130 550 0
array-examples/sorting_bubblesort_false-unreach-call2_ground.i error (134) .088 24 .88 0 out of memory 25     15000   360    0 error (42) 880     14000   12000    0 timeout 960   4200 8300 0 unknown 900    770 11000   0 unknown 8.2 430 99 0 unknown 8.1 430 99 0 timeout 900     2800 11000    0 unknown 900    79 13000   0 timeout 960 4500 7000 0 out of memory 420    15000 5200   0 unknown 73   1600 900 0 disqualified 3.6 91 43 0 probably out of memory (killed (signal 9, verification)) 290    15000 4000   0 timeout 900   1600 12000 0 timeout 900   6200 9600 0 timeout 900   1300 13000 0 out of memory 430   15000 4900 0 error (1) 64   1200 970 0 unknown 330   470 3700 0
array-examples/sorting_bubblesort_false-unreach-call_ground.i error (134) .084 24 .74 0 out of memory 25     15000   270    0 error (42) 880     14000   12000    0 timeout 960   4400 6600 0 unknown 900    770 10000   0 unknown 8.1 430 93 0 unknown 8.1 430 120 0 timeout 900     2800 11000    0 timeout 900    79 9900   0 timeout 960 4700 7200 0 out of memory 420    15000 5700   0 unknown 73   1500 790 0 disqualified 3.6 90 44 0 probably out of memory (killed (signal 9, verification)) 290    15000 4000   0 timeout 900   1500 12000 0 timeout 900   5000 9600 0 timeout 900   1200 11000 0 out of memory 440   15000 6100 0 error (1) 64   1200 910 0 unknown 330   450 3400 0
array-examples/sorting_selectionsort_false-unreach-call2_ground.i error (134) .078 24 .77 0 out of memory 72     12000   890    0 error (42) 870     990   12000    0 timeout 960   4500 10000 0 unknown 900    1300 9600   0 unknown 8.2 430 120 0 unknown 8.2 430 98 0 timeout 900     9100 9400    0 timeout 900    81 11000   0 timeout 960 6700 8600 0 out of memory 630    15000 8300   0 unknown 170   1500 1800 0 disqualified 880   500 10000 0 probably out of memory (killed (signal 9, verification)) 350    15000 5200   0 timeout 900   1300 11000 0 timeout 900   3800 8600 0 timeout 900   1400 13000 0 out of memory 90   15000 1100 0 false(unreach-call) 25   3500 280 1 unknown 580   390 6500 0
array-examples/sorting_selectionsort_false-unreach-call_ground.i error (134) .089 24 .66 0 out of memory 71     12000   800    0 error (42) 870     2500   12000    0 timeout 960   4200 9500 0 unknown 900    1600 9800   0 unknown 8.2 430 98 0 unknown 8.3 430 100 0 timeout 900     8900 9900    0 timeout 900    77 9400   0 timeout 960 8300 9700 0 timeout 900    14000 9100   0 unknown 190   1500 1700 0 disqualified 350   830 3800 0 probably out of memory (killed (signal 9, verification)) 350    15000 5200   0 timeout 900   2000 12000 0 timeout 900   4900 8300 0 timeout 900   1400 12000 0 out of memory 87   15000 1100 0 false(unreach-call) 10   2900 110 1 unknown 890   440 11000 0
array-examples/standard_allDiff2_false-unreach-call_ground.i error (134) .080 24 1.0  0 out of memory 490     10000   4200    0 out of memory 150     15000   1700    0 timeout 960   4300 7600 0 unknown 900    1500 10000   0 unknown 8.2 430 97 0 unknown 8.2 430 99 0 timeout 900     3300 7000    0 timeout 900    75 6800   0 timeout 920 12000 10000 0 out of memory 290    15000 4200   0 false(unreach-call) 6.0 300 55 1 disqualified 17   130 220 0 false(unreach-call) .17 16 1.8 1 timeout 900   5400 9200 0 timeout 900   1200 6500 0 timeout 900   5300 9400 0 out of memory 180   15000 2300 0 error (1) 54   620 630 0 unknown 420   400 4700 0
array-examples/standard_copy1_false-unreach-call_ground.i error (134) .090 24 .89 0 out of memory 86     15000   1100    0 error (42) 880     2900   13000    0 timeout 960   3400 9600 0 unknown 160    60 2100   0 timeout 900   1000 11000 0 timeout 900   2500 9600 0 timeout 900     11000 9500    0 false(unreach-call) 6.6  480 81   1 timeout 970 5600 8900 0 false(unreach-call) 480    7400 6200   0 unknown 91   1900 1200 0 disqualified 3.6 91 43 0 false(unreach-call) 6.6  410 87   1 timeout 900   830 9000 0 timeout 900   5100 9000 0 timeout 900   1000 11000 0 false(unreach-call) 4.6 190 33 1 false(unreach-call) 4.8 1400 50 1 false(unreach-call) 7.4 130 100 1
array-examples/standard_copy2_false-unreach-call_ground.i error (134) .077 24 .86 0 out of memory 97     15000   1300    0 error (42) 880     3800   9700    0 timeout 960   3900 9500 0 unknown 170    65 2100   0 timeout 900   740 9200 0 timeout 900   2500 8000 0 timeout 900     11000 9100    0 false(unreach-call) 6.3  480 79   1 timeout 960 6000 8000 0 false(unreach-call) 670    10000 7800   0 unknown 9.5 290 89 0 disqualified 3.7 120 45 0 false(unreach-call) 8.7  520 120   1 timeout 900   760 8500 0 timeout 900   5100 9300 0 timeout 900   940 9700 0 false(unreach-call) 4.7 190 36 1 false(unreach-call) 5.3 2100 60 1 false(unreach-call) 8.6 130 120 1
array-examples/standard_copy3_false-unreach-call_ground.i error (134) .087 24 .86 0 out of memory 110     15000   1600    0 error (42) 880     4900   11000    0 timeout 960   5000 11000 0 unknown 210    75 2900   0 timeout 900   550 7900 0 timeout 900   2500 9300 0 timeout 900     11000 8900    0 false(unreach-call) 6.4  480 78   1 timeout 960 5800 8200 0 false(unreach-call) 890    13000 11000   0 unknown 9.3 300 86 0 disqualified 3.7 95 48 0 false(unreach-call) 9.7  590 140   1 timeout 900   910 13000 0 timeout 900   5200 8600 0 timeout 900   810 10000 0 false(unreach-call) 4.7 190 36 1 false(unreach-call) 5.7 2700 77 1 false(unreach-call) 9.7 130 140 1
array-examples/standard_copy4_false-unreach-call_ground.i error (134) .090 24 .88 0 out of memory 120     15000   1600    0 error (42) 880     5800   11000    0 timeout 960   3000 11000 0 unknown 230    82 3100   0 timeout 900   570 8500 0 timeout 900   2500 9000 0 timeout 900     11000 9200    0 false(unreach-call) 6.4  480 87   1 timeout 900 8800 12000 0 timeout 900    12000 10000   0 unknown 9.3 300 95 0 disqualified 3.9 120 51 0 false(unreach-call) 11    650 150   1 timeout 900   920 9700 0 timeout 900   5000 8200 0 timeout 900   1000 10000 0 false(unreach-call) 4.6 190 34 1 false(unreach-call) 6.3 3300 79 1 false(unreach-call) 11   130 160 1
array-examples/standard_copy5_false-unreach-call_ground.i error (134) .083 24 .70 0 out of memory 94     15000   1400    0 error (42) 880     6800   12000    0 timeout 970   4800 10000 0 unknown 250    84 3400   0 timeout 900   590 8700 0 timeout 900   2500 8300 0 timeout 900     11000 9900    0 false(unreach-call) 6.5  480 90   0 timeout 960 5300 8800 0 timeout 900    14000 12000   0 unknown 9.6 290 100 0 disqualified 3.9 110 49 0 false(unreach-call) 12    730 170   1 timeout 900   920 9000 0 timeout 900   5300 7800 0 timeout 900   950 11000 0 false(unreach-call) 4.8 190 35 1 false(unreach-call) 6.9 4000 77 1 false(unreach-call) 12   140 160 1
array-examples/standard_copy6_false-unreach-call_ground.i error (134) .091 24 .66 0 out of memory 100     15000   1500    0 error (42) 880     7800   12000    0 timeout 970   4700 8700 0 unknown 280    90 3200   0 timeout 900   610 8900 0 timeout 900   2500 8600 0 timeout 900     11000 10000    0 false(unreach-call) 7.0  480 99   0 timeout 960 5700 8800 0 out of memory 890    15000 12000   0 unknown 9.2 300 90 0 disqualified 4.2 100 48 0 false(unreach-call) 13    820 150   1 timeout 900   950 12000 0 timeout 900   4900 8400 0 timeout 900   1800 12000 0 false(unreach-call) 4.8 190 41 1 false(unreach-call) 7.5 4600 89 1 false(unreach-call) 13   150 210 1
array-examples/standard_copy7_false-unreach-call_ground.i error (134) .085 24 .77 0 out of memory 110     15000   1600    0 error (42) 880     8700   12000    0 timeout 960   4500 9800 0 unknown 280    130 3900   0 timeout 900   620 8500 0 timeout 900   2500 8900 0 timeout 900     11000 9900    0 false(unreach-call) 6.8  480 84   0 timeout 960 6900 8800 0 out of memory 400    15000 5800   0 unknown 9.1 290 87 0 disqualified 4.1 130 48 0 false(unreach-call) 13    910 180   1 timeout 900   890 11000 0 timeout 900   5000 8300 0 timeout 900   980 12000 0 false(unreach-call) 4.8 190 38 1 false(unreach-call) 8.0 5300 100 1 false(unreach-call) 14   160 210 1
array-examples/standard_copy8_false-unreach-call_ground.i error (134) .087 24 .74 0 out of memory 120     15000   1600    0 error (42) 880     9600   12000    0 timeout 960   3900 9100 0 unknown 310    140 4000   0 timeout 900   640 9800 0 timeout 900   2500 8400 0 timeout 900     11000 10000    0 false(unreach-call) 6.7  520 87   1 timeout 960 4500 11000 0 out of memory 450    15000 5900   0 unknown 8.9 290 81 0 disqualified 4.3 120 49 0 false(unreach-call) 15    1000 190   1 timeout 900   970 13000 0 timeout 900   5000 8000 0 timeout 900   1100 10000 0 false(unreach-call) 4.9 200 40 1 false(unreach-call) 8.4 5900 94 1 false(unreach-call) 15   170 200 1
array-examples/standard_copy9_false-unreach-call_ground.i error (134) .084 24 .88 0 out of memory 97     15000   1300    0 error (42) 880     11000   9700    0 timeout 960   4400 9500 0 unknown 330    110 4500   0 timeout 900   660 9100 0 timeout 900   2500 8300 0 timeout 900     10000 11000    0 false(unreach-call) 6.7  480 96   1 timeout 960 5200 8800 0 out of memory 480    15000 5800   0 unknown 9.5 300 88 0 disqualified 4.4 120 66 0 false(unreach-call) 16    1100 210   1 timeout 900   930 11000 0 timeout 900   5300 9200 0 timeout 900   1400 8300 0 false(unreach-call) 5.1 200 39 1 false(unreach-call) 9.1 6500 110 1 false(unreach-call) 16   180 220 1
array-examples/standard_copyInitSum2_false-unreach-call_ground.i error (134) .081 23 .75 0 out of memory 64     15000   800    0 error (42) 880     2900   12000    0 timeout 960   3300 9300 0 unknown 120    59 1600   0 out of memory (unknown error) 170   15000 1600 0 out of memory (unknown error) 170   15000 1500 0 timeout 900     6800 11000    0 false(unreach-call) .50 85 4.9 1 timeout 960 3900 7500 0 false(unreach-call) 570    7600 6700   0 unknown 8.8 300 80 0 disqualified 3.3 85 43 0 false(unreach-call) 2.1  250 31   1 timeout 900   1300 10000 0 timeout 900   5300 7700 0 timeout 900   940 12000 0 false(unreach-call) 16   200 100 1 false(unreach-call) 4.5 1400 47 1 false(unreach-call) 8.1 130 120 1
array-examples/standard_init1_false-unreach-call_ground.i error (134) .081 24 .74 0 out of memory 100     15000   1600    0 error (42) 880     1400   15000    0 timeout 960   3500 11000 0 unknown 87    51 1100   0 out of memory (unknown error) 170   15000 1500 0 out of memory (unknown error) 170   15000 1700 0 timeout 900     6500 8500    0 false(unreach-call) .46 84 5.6 1 timeout 960 6800 8400 0 false(unreach-call) 190    3200 2800   1 unknown 77   1400 820 0 disqualified 3.1 78 39 0 false(unreach-call) .77 100 11   1 timeout 900   920 13000 0 timeout 900   4600 8000 0 timeout 900   810 11000 0 false(unreach-call) 15   200 100 1 false(unreach-call) 15   1200 180 1 false(unreach-call) 6.0 130 81 1
array-examples/standard_init2_false-unreach-call_ground.i error (134) .088 24 .70 0 out of memory 52     15000   800    0 error (42) 880     2000   15000    0 timeout 960   2700 9200 0 unknown 110    59 1400   0 out of memory (unknown error) 170   15000 1700 0 out of memory (unknown error) 160   15000 1600 0 timeout 900     6700 11000    0 false(unreach-call) .44 83 5.7 1 timeout 960 6600 8200 0 false(unreach-call) 370    5300 5300   0 unknown 61   1600 730 0 disqualified 3.1 82 38 0 false(unreach-call) 1.4  190 24   1 timeout 900   880 9800 0 timeout 900   5800 8800 0 timeout 900   770 10000 0 false(unreach-call) 15   200 110 1 false(unreach-call) 15   1300 220 1 false(unreach-call) 6.9 130 88 1
array-examples/standard_init3_false-unreach-call_ground.i error (134) .080 24 .90 0 out of memory 57     15000   780    0 error (42) 880     2600   14000    0 timeout 970   3700 10000 0 unknown 120    61 1500   0 out of memory (unknown error) 170   15000 1700 0 out of memory (unknown error) 170   15000 1800 0 timeout 900     6700 9700    0 false(unreach-call) .45 84 5.3 1 timeout 960 5900 8800 0 false(unreach-call) 570    7500 8900   0 unknown 55   1600 590 0 disqualified 3.2 84 38 0 false(unreach-call) 2.0  280 31   1 timeout 900   860 12000 0 timeout 900   5200 9300 0 timeout 900   910 11000 0 false(unreach-call) 16   200 110 1 false(unreach-call) 15   1400 230 1 false(unreach-call) 7.9 130 99 1
array-examples/standard_init4_false-unreach-call_ground.i error (134) .089 24 .91 0 out of memory 61     15000   900    0 error (42) 880     3200   12000    0 timeout 960   3300 12000 0 unknown 150    81 2400   0 out of memory (unknown error) 170   15000 1600 0 out of memory (unknown error) 170   15000 1700 0 timeout 900     6600 9400    0 false(unreach-call) .48 84 6.3 1 timeout 960 5200 9400 0 false(unreach-call) 760    9700 9700   0 unknown 57   1800 540 0 disqualified 3.2 83 38 0 false(unreach-call) 2.6  370 38   1 timeout 900   890 13000 0 timeout 900   5200 8200 0 timeout 900   840 11000 0 false(unreach-call) 16   200 120 1 false(unreach-call) 15   1500 200 1 false(unreach-call) 8.8 130 140 1
array-examples/standard_init5_false-unreach-call_ground.i error (134) .12  24 .58 0 out of memory 66     15000   920    0 error (42) 880     3800   11000    0 timeout 970   4200 9800 0 unknown 170    76 2100   0 out of memory (unknown error) 170   15000 1500 0 out of memory (unknown error) 170   15000 1800 0 timeout 900     6400 10000    0 false(unreach-call) .49 84 5.0 1 timeout 970 5300 7800 0 timeout 900    8800 13000   0 unknown 58   1600 650 0 disqualified 3.2 82 39 0 false(unreach-call) 3.2  460 46   1 timeout 900   890 10000 0 timeout 900   5700 8300 0 timeout 900   750 9600 0 false(unreach-call) 16   200 110 1 false(unreach-call) 16   1600 200 1 false(unreach-call) 9.8 140 130 1
array-examples/standard_init6_false-unreach-call_ground.i error (134) .086 24 .70 0 out of memory 70     15000   1000    0 error (42) 880     4400   12000    0 timeout 960   2700 7800 0 unknown 190    98 2400   0 out of memory (unknown error) 170   15000 1700 0 out of memory (unknown error) 160   15000 1800 0 timeout 900     6600 11000    0 false(unreach-call) .51 84 5.9 1 timeout 960 5000 8800 0 timeout 900    9200 12000   0 unknown 60   1500 620 0 disqualified 3.2 84 42 0 false(unreach-call) 3.8  540 51   1 timeout 900   880 9700 0 timeout 900   6300 11000 0 timeout 900   720 9100 0 false(unreach-call) 17   200 110 1 false(unreach-call) 16   1700 200 1 false(unreach-call) 11   160 130 1
array-examples/standard_init7_false-unreach-call_ground.i error (134) .083 24 .85 0 out of memory 75     15000   980    0 error (42) 880     5000   12000    0 timeout 960   3200 9200 0 unknown 210    85 2700   0 out of memory (unknown error) 170   15000 1700 0 out of memory (unknown error) 170   15000 1600 0 timeout 900     6500 10000    0 false(unreach-call) .54 84 6.3 1 timeout 960 5200 7900 0 timeout 900    9600 11000   0 unknown 62   1600 630 0 disqualified 3.3 87 41 0 false(unreach-call) 4.5  630 66   1 timeout 900   810 11000 0 timeout 900   5300 8700 0 timeout 900   910 10000 0 false(unreach-call) 17   200 130 1 false(unreach-call) 17   1700 240 1 false(unreach-call) 12   170 160 1
array-examples/standard_init8_false-unreach-call_ground.i error (134) .11  24 .69 0 out of memory 54     15000   720    0 error (42) 880     5600   11000    0 timeout 970   4400 9300 0 unknown 240    110 3400   0 out of memory (unknown error) 170   15000 1600 0 out of memory (unknown error) 170   15000 1800 0 timeout 900     6700 8800    0 false(unreach-call) .56 84 7.3 1 timeout 970 5100 8600 0 timeout 900    10000 12000   0 unknown 63   1900 680 0 disqualified 3.3 85 45 0 false(unreach-call) 5.1  720 70   1 timeout 900   880 9000 0 timeout 900   5400 7500 0 timeout 900   770 9600 0 false(unreach-call) 17   200 120 1 false(unreach-call) 17   1800 220 1 false(unreach-call) 13   180 190 1
array-examples/standard_init9_false-unreach-call_ground.i error (134) .085 24 .86 0 out of memory 57     15000   900    0 error (42) 880     6200   14000    0 timeout 960   3700 10000 0 unknown 260    98 3400   0 out of memory (unknown error) 160   15000 1700 0 out of memory (unknown error) 170   15000 1800 0 timeout 900     6700 10000    0 false(unreach-call) .58 85 8.4 1 timeout 970 7000 7800 0 timeout 900    10000 12000   0 unknown 64   1600 690 0 disqualified 3.4 110 37 0 false(unreach-call) 5.6  810 90   1 timeout 900   900 9300 0 timeout 900   5000 8100 0 timeout 900   930 11000 0 false(unreach-call) 17   200 120 1 false(unreach-call) 17   1900 210 1 false(unreach-call) 14   190 190 1
array-examples/standard_minInArray_false-unreach-call_ground.i error (134) .088 24 .72 0 error (42) 880     1100   4000    0 error (42) 870     960   12000    0 timeout 960   4300 9300 0 unknown 110    64 1300   0 unknown 8.2 430 95 0 unknown 8.1 430 130 0 timeout 900     8500 10000    0 false(unreach-call) .47 83 4.9 1 timeout 960 4800 9000 0 timeout 900    13000 11000   0 unknown 80   1300 1000 0 disqualified 3.2 83 37 0 false(unreach-call) .99 100 12   1 timeout 900   1700 11000 0 timeout 900   5500 11000 0 timeout 900   1200 12000 0 false(unreach-call) 4.5 190 39 1 false(unreach-call) 14   1000 210 1 false(unreach-call) 6.6 130 100 1
array-examples/standard_partition_false-unreach-call_ground.i error (134) .082 24 .76 0 out of memory 170     14000   2000    0 error (42) 880     3300   14000    0 timeout 960   4300 10000 0 unknown 300    120 3700   0 unknown 8.6 430 120 0 timeout 900   1400 7600 0 timeout 900     4400 11000    0 false(unreach-call) 3.3  230 47   1 timeout 960 4300 7600 0 out of memory 310    15000 4400   0 unknown 63   1600 660 0 disqualified 4.1 93 50 0 timeout (verification) 900    2800 7700   0 timeout 900   1300 11000 0 timeout 900   5200 8800 0 timeout 900   900 8100 0 out of memory 58   15000 610 0 false(unreach-call) 36   2800 540 1 unknown 290   530 3900 0
array-examples/standard_running_false-unreach-call.i error (134) .12  23 .65 0 out of memory 82     15000   1200    0 out of memory 300     15000   4500    0 timeout 970   4600 8500 0 unknown 260    130 3500   0 unknown 8.2 430 100 0 unknown 8.3 430 94 0 out of memory 390     15000 5300    0 timeout 900    76 8400   0 timeout 960 4800 10000 0 out of memory 350    15000 4300   0 unknown 59   1200 680 0 disqualified 3.0 85 37 0 false(unreach-call) 1.9  180 29   1 timeout 900   1300 13000 0 timeout 900   6700 8800 0 timeout 900   1100 12000 0 out of memory 57   15000 680 0 error (1) 890   2300 12000 0 unknown 280   760 3200 0
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i error (134) .094 24 .67 0 true 130     4200   1600    2 true 130     2900   1700    2 true 93   1300 1100 2 unknown 900    2700 9000   0 true 21   430 220 2 true 21   430 240 2 true .10  26 1.1  2 timeout 900    83 9300   0 true 11 1200 80 2 true 130    2900 1500   2 true 4.4 240 43 2 disqualified 3.4 100 51 0 true .97 95 15   2 true 9.4 370 83 2 timeout 900   2100 9800 0 true 8.7 350 81 2 true 21   500 190 2 error (1) 880   1300 11000 0 unknown 75   130 1100 0
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i error (134) .087 24 .70 0 error (42) 880     9800   12000    0 error (42) 880     1300   14000    0 timeout 970   5500 11000 0 unknown 900    1200 12000   0 unknown 8.1 430 99 0 unknown 8.1 430 110 0 true .14  26 .99 2 timeout 900    76 11000   0 unknown 100 2000 1300 0 out of memory 280    15000 3600   0 unknown 69   1500 890 0 disqualified 880   210 14000 0 true 1.1  86 16   2 timeout 900   5500 10000 0 timeout 900   5300 9400 0 timeout 900   2000 12000 0 out of memory 65   15000 740 0 error (1) 890   1300 12000 0 unknown 42   130 570 0
array-examples/relax_true-unreach-call.i error (134) .18  26 1.3  0 out of memory 280     13000   3400    0 out of memory 200     15000   2500    0 timeout 970   6800 8400 0 unknown 900    170 13000   0 unknown 8.5 450 120 0 unknown 1.6 200 21 0 timeout 900     340 13000    0 true 40    4200 410   2 timeout 960 5100 10000 0 timeout 900    1100 5800   0 unknown 15   350 150 0 disqualified 880   340 9800 0 timeout (verification) 900    750 11000   0 timeout 900   730 11000 0 timeout 900   690 13000 0 timeout 900   930 12000 0 out of memory 540   15000 4600 0 timeout 900   180 13000 0 unknown 41   130 580 0
array-examples/sanfoundry_02_true-unreach-call_ground.i error (134) .088 23 .68 0 error (42) 880     2100   4300    0 error (42) 880     1300   13000    0 timeout 960   4400 10000 0 unknown 200    100 2400   0 unknown 48   430 610 0 unknown 48   430 690 0 timeout 900     12000 9700    0 timeout 900    75 9400   0 timeout 960 4100 9000 0 out of memory 790    15000 8100   0 unknown 67   1600 720 0 disqualified 2.7 80 30 0 true 1.7  95 24   2 timeout 900   1700 14000 0 timeout 900   5700 8000 0 timeout 900   1300 12000 0 true 11   190 120 2 error (1) 880   620 12000 0 true 20   240 230 2
array-examples/sanfoundry_10_true-unreach-call_ground.i error (134) .093 24 .68 0 error (42) 880     13000   11000    0 error (42) 880     13000   11000    0 timeout 910   1000 10000 0 unknown 320    83 4500   0 unknown 8.2 430 110 0 unknown 8.4 430 120 0 true .13  26 1.2  2 timeout 900    220 8800   0 out of memory 840 15000 11000 0 out of memory 430    15000 6700   0 unknown 240   1500 2700 0 disqualified 5.7 94 73 0 true 1.4  68 21   2 timeout 900   1800 11000 0 timeout 900   1600 8800 0 timeout 900   1200 12000 0 true 16   200 110 2 error (1) 880   8500 12000 0 true 19   240 210 2
array-examples/sanfoundry_24_true-unreach-call_true-termination.i error (134) .089 24 .69 0 error (42) 880     2700   10000    0 error (42) 880     1800   12000    0 true 14   630 110 2 unknown .79 67 9.3 0 unknown 8.3 430 120 0 unknown 8.6 430 130 0 true .088 26 1.1  2 timeout 900    1300 7800   0 true 18 1400 130 2 out of memory 42    15000 480   0 true 4.3 230 40 2 disqualified 880   350 11000 0 timeout (verification) 900    1200 10000   0 true 9.5 380 75 2 true 9.3 370 74 2 true 8.9 360 67 2 true 16   190 90 2 error (1) 880   1100 11000 0 true 14   130 170 2
array-examples/sanfoundry_27_true-unreach-call_ground.i error (134) .081 24 .99 0 error (42) 880     1100   4300    0 error (42) 880     980   12000    0 timeout 960   4200 12000 0 unknown 93    69 1200   0 unknown 8.1 430 110 0 unknown 8.3 430 110 0 timeout 900     8600 10000    0 timeout 900    75 8900   0 timeout 960 5200 9100 0 out of memory 580    15000 7300   0 unknown 100   1300 1100 0 disqualified 3.0 83 41 0 true 1.1  62 14   2 timeout 900   1600 14000 0 timeout 900   4900 9400 0 timeout 900   1200 11000 0 true 5.0 190 46 2 error (1) 890   670 10000 0 true 30   240 370 2
array-examples/sanfoundry_43_true-unreach-call_ground.i error (134) .083 24 .69 0 out of memory 95     15000   1600    0 out of memory 84     15000   1100    0 true 93   1100 1100 2 unknown .80 66 9.3 0 out of memory (unknown error) 170   15000 1800 0 out of memory (unknown error) 170   15000 1800 0 true .089 26 .86 2 unknown .78 39 8.9 0 true 13 1000 93 2 true 96    1900 1400   2 true 4.6 270 50 2 disqualified 2.0 73 25 0 true .14 16 1.4 2 true 7.9 360 59 2 true 7.5 370 69 2 true 7.7 370 59 2 true 4.5 190 40 2 error (1) 880   1300 11000 0 true 21   130 270 2
array-examples/sorting_bubblesort_true-unreach-call_ground.i error (134) .084 24 .74 0 out of memory 24     15000   320    0 error (42) 880     15000   13000    0 timeout 960   4200 7000 0 unknown 900    780 9800   0 unknown 8.4 430 97 0 unknown 8.1 430 110 0 timeout 900     2800 10000    0 timeout 900    76 9600   0 timeout 960 4500 7700 0 out of memory 420    15000 6400   0 unknown 73   1400 800 0 disqualified 22   140 310 0 probably out of memory (killed (signal 9, verification)) 290    15000 3700   0 timeout 900   1700 9800 0 timeout 900   5200 8500 0 timeout 900   1700 11000 0 out of memory 390   15000 5000 0 error (1) 54   780 840 0 true 12   250 130 2
array-examples/sorting_selectionsort_true-unreach-call_ground.i error (134) .088 24 .81 0 out of memory 72     12000   820    0 error (42) 870     2500   12000    0 timeout 960   4200 9400 0 unknown 900    1600 8600   0 unknown 8.1 430 93 0 unknown 8.2 430 110 0 timeout 900     9100 10000    0 timeout 900    78 9700   0 timeout 960 6800 9700 0 timeout 900    13000 8900   0 timeout 900   3000 6800 0 disqualified 880   780 9600 0 probably out of memory (killed (signal 9, verification)) 350    15000 4900   0 timeout 900   1300 13000 0 timeout 900   3500 8800 0 timeout 900   1300 12000 0 out of memory 90   15000 1000 0 error (1) 60   2900 770 0 unknown 470   440 5300 0
array-examples/standard_compareModified_true-unreach-call_ground.i error (134) .079 23 .68 0 out of memory 120     15000   1500    0 error (42) 880     1700   12000    0 timeout 970   4100 7800 0 unknown 150    72 1800   0 unknown 8.2 430 100 0 unknown 8.2 430 110 0 timeout 900     6700 9800    0 true 2.0  83 28   2 timeout 900 7300 12000 0 out of memory 320    15000 4100   0 unknown 66   1600 740 0 disqualified 2.5 81 34 0 true 2.1  100 23   2 timeout 900   710 10000 0 timeout 900   5800 10000 0 timeout 900   850 12000 0 true 4.7 190 37 2 error (1) 890   1800 11000 0 true 21   340 240 2
array-examples/standard_compare_true-unreach-call_ground.i error (134) .080 23 .90 0 error (42) 880     1100   4600    0 error (42) 880     1300   11000    0 timeout 970   4500 9700 0 unknown 65    56 880   0 unknown 8.0 430 99 0 unknown 8.1 430 96 0 timeout 900     9300 9000    0 timeout 900    76 8500   0 timeout 900 1800 11000 0 out of memory 330    15000 4100   0 unknown 90   1700 960 0 disqualified 2.7 84 36 0 true 1.3  63 17   2 timeout 900   880 11000 0 timeout 900   5000 10000 0 timeout 900   940 11000 0 true 4.3 190 34 2 error (1) 880   1800 11000 0 true 24   240 300 2
array-examples/standard_copy1_true-unreach-call_ground.i error (134) .080 24 .97 0 out of memory 59     15000   880    0 error (42) 880     2300   12000    0 timeout 960   4700 13000 0 unknown 160    59 2100   0 unknown 890   1500 11000 0 timeout 900   2300 8500 0 timeout 900     11000 9700    0 timeout 900    5000 13000   0 timeout 960 4900 11000 0 true 110    2400 1300   2 unknown 9.4 290 96 0 disqualified 3.2 82 38 0 true 2.9  230 38   2 timeout 900   930 10000 0 timeout 900   5200 8200 0 timeout 900   1000 9800 0 true 4.6 180 38 2 error (1) 890   1300 11000 0 true 40   270 540 2
array-examples/standard_copy2_true-unreach-call_ground.i error (134) .089 24 .73 0 out of memory 71     15000   990    0 error (42) 880     3200   14000    0 timeout 970   4600 9500 0 unknown 170    66 2400   0 timeout 900   1000 9200 0 timeout 900   2300 8500 0 timeout 900     11000 9700    0 timeout 900    4900 12000   0 timeout 960 5300 8800 0 true 160    3200 1800   2 unknown 9.4 290 94 0 disqualified 3.3 85 39 0 true 3.3  250 41   2 timeout 900   850 9800 0 timeout 900   5300 8900 0 timeout 900   820 11000 0 true 4.8 190 35 2 error (1) 880   2000 11000 0 true 49   250 500 2
array-examples/standard_copy3_true-unreach-call_ground.i error (134) .077 24 .92 0 out of memory 82     15000   1200    0 error (42) 870     4200   13000    0 timeout 960   4200 10000 0 unknown 190    84 2500   0 timeout 900   770 9400 0 timeout 900   2300 8400 0 timeout 900     11000 11000    0 timeout 900    4900 12000   0 timeout 970 5800 8100 0 true 200    3900 2400   2 unknown 9.4 290 86 0 disqualified 3.5 89 47 0 true 3.9  280 45   2 timeout 900   740 11000 0 timeout 900   5200 8100 0 timeout 900   820 10000 0 true 4.6 190 36 2 error (1) 890   2700 11000 0 true 65   340 830 2
array-examples/standard_copy4_true-unreach-call_ground.i error (134) .082 24 .70 0 out of memory 95     15000   1300    0 error (42) 880     5300   12000    0 timeout 960   4100 10000 0 unknown 210    84 3100   0 timeout 900   610 9800 0 timeout 900   2300 7800 0 timeout 900     12000 12000    0 timeout 900    4900 11000   0 timeout 900 7800 14000 0 true 250    4700 3100   2 unknown 9.3 290 87 0 disqualified 3.7 93 47 0 true 4.3  300 55   2 timeout 900   750 8500 0 timeout 900   4700 8000 0 timeout 900   840 10000 0 true 4.7 190 40 2 error (1) 890   3300 12000 0 true 120   550 1600 2
array-examples/standard_copy5_true-unreach-call_ground.i error (134) .099 24 .65 0 out of memory 110     15000   1400    0 error (42) 880     6200   12000    0 timeout 970   4900 8800 0 unknown 260    98 3300   0 timeout 900   630 9000 0 timeout 900   2300 9100 0 timeout 900     11000 11000    0 timeout 900    4800 12000   0 timeout 960 6000 9900 0 true 290    5500 3900   2 unknown 8.7 280 75 0 disqualified 3.8 95 54 0 true 4.9  330 67   2 timeout 900   760 10000 0 timeout 900   5300 10000 0 timeout 900   990 11000 0 true 4.9 200 39 2 error (1) 890   3900 14000 0 true 130   430 1400 2
array-examples/standard_copy6_true-unreach-call_ground.i error (134) .079 24 .77 0 out of memory 87     15000   1200    0 error (42) 880     7200   12000    0 timeout 960   3800 11000 0 unknown 280    99 3500   0 timeout 900   650 8200 0 timeout 900   2300 9200 0 timeout 900     12000 11000    0 timeout 900    4800 13000   0 timeout 970 7300 9200 0 true 340    6700 3900   2 unknown 9.3 290 91 0 disqualified 4.0 100 50 0 true 5.3  350 75   2 timeout 900   920 9900 0 timeout 900   5200 8600 0 timeout 900   990 9100 0 true 4.9 190 36 2 error (1) 890   4500 13000 0 true 140   480 1300 2
array-examples/standard_copy7_true-unreach-call_ground.i error (134) .098 23 .73 0 out of memory 96     15000   1200    0 error (42) 880     8100   14000    0 timeout 960   4700 9200 0 unknown 300    100 4100   0 timeout 900   670 9000 0 timeout 900   2300 8700 0 timeout 900     12000 10000    0 timeout 900    4800 11000   0 timeout 960 6000 9400 0 true 380    7100 4800   2 unknown 9.1 300 85 0 disqualified 4.2 100 53 0 true 5.8  380 79   2 timeout 900   890 9900 0 timeout 900   5200 7900 0 timeout 900   1100 11000 0 true 4.9 200 36 2 error (1) 880   5200 12000 0 true 140   490 1600 2
array-examples/standard_copy8_true-unreach-call_ground.i error (134) .088 24 .76 0 out of memory 110     15000   1700    0 error (42) 880     9100   12000    0 timeout 960   4300 9100 0 unknown 350    110 4600   0 timeout 900   700 10000 0 timeout 900   2300 8100 0 timeout 900     12000 9400    0 timeout 900    4700 11000   0 timeout 960 7200 9200 0 true 430    7800 4900   2 unknown 9.6 310 99 0 disqualified 4.4 100 58 0 true 6.4  400 94   2 timeout 900   940 10000 0 timeout 900   5300 8500 0 timeout 900   1000 8000 0 true 5.1 200 43 2 error (1) 890   5800 11000 0 true 150   420 1900 2
array-examples/standard_copy9_true-unreach-call_ground.i error (134) .084 24 .99 0 out of memory 110     15000   1600    0 error (42) 880     10000   11000    0 timeout 970   4300 9500 0 unknown 360    120 5300   0 timeout 900   720 9900 0 timeout 900   2200 7900 0 timeout 900     11000 10000    0 timeout 900    4700 13000   0 timeout 960 6200 10000 0 true 480    8600 5700   2 unknown 9.4 290 97 0 disqualified 4.6 110 58 0 true 7.0  430 95   2 timeout 900   790 9200 0 timeout 900   4400 8900 0 timeout 900   1100 9000 0 true 5.0 200 39 2 error (1) 890   6400 9600 0 true 160   430 1900 2
array-examples/standard_copyInitSum2_true-unreach-call_ground.i error (134) .098 24 .84 0 out of memory 64     15000   940    0 error (42) 880     2900   14000    0 timeout 960   2700 7000 0 unknown 130    73 1700   0 out of memory (unknown error) 170   15000 1600 0 out of memory (unknown error) 160   15000 1500 0 timeout 900     6800 11000    0 timeout 900    77 7800   0 timeout 970 5900 8500 0 true 150    3000 1800   2 unknown 9.6 300 86 0 disqualified 3.2 87 39 0 true 1.8  99 26   2 timeout 900   910 8800 0 timeout 900   5300 11000 0 timeout 900   730 9200 0 true 17   200 120 2 error (1) 880   1400 10000 0 true 81   650 830 2
array-examples/standard_copyInitSum3_true-unreach-call_ground.i error (134) .11  24 .62 0 out of memory 68     15000   920    0 error (42) 880     3500   12000    0 timeout 960   3400 9700 0 unknown 170    91 2300   0 out of memory (unknown error) 160   15000 1600 0 out of memory (unknown error) 170   15000 1600 0 timeout 900     6800 10000    0 timeout 900    77 9900   0 timeout 960 4400 8600 0 true 190    3400 2600   2 unknown 9.9 300 88 0 disqualified 3.9 92 50 0 true 2.2  120 31   2 timeout 900   960 13000 0 timeout 900   6100 9400 0 timeout 900   930 9000 0 true 4.6 190 38 2 error (1) 880   1500 13000 0 true 84   430 980 2
array-examples/standard_copyInitSum_true-unreach-call_ground.i error (134) .088 24 .73 0 out of memory 64     15000   820    0 error (42) 880     2900   10000    0 timeout 960   3900 9900 0 unknown 130    70 1700   0 out of memory (unknown error) 170   15000 1600 0 out of memory (unknown error) 170   15000 1500 0 timeout 900     6700 8500    0 timeout 900    160 8900   0 timeout 970 3800 8400 0 true 150    3000 1800   2 unknown 9.6 290 88 0 disqualified 3.0 83 35 0 true 1.8  140 26   2 timeout 900   920 11000 0 timeout 900   5100 9400 0 timeout 900   780 11000 0 true 32   200 330 2 error (1) 880   1400 9400 0 true 38   350 430 2
array-examples/standard_copyInit_true-unreach-call_ground.i error (134) .082 24 .76 0 out of memory 59     15000   870    0 error (42) 880     2300   11000    0 timeout 960   2600 8900 0 unknown 100    54 1400   0 out of memory (unknown error) 170   15000 1700 0 out of memory (unknown error) 170   15000 1500 0 timeout 900     6500 9600    0 timeout 900    77 9800   0 timeout 970 7700 7700 0 true 110    2300 1200   2 unknown 9.2 290 83 0 disqualified 2.8 84 33 0 true 1.3  81 20   2 timeout 900   740 9900 0 timeout 900   5100 7500 0 timeout 900   760 9800 0 true 16   200 110 2 error (1) 890   1400 11000 0 true 40   310 480 2
array-examples/standard_find_true-unreach-call_ground.i error (134) .087 24 .69 0 out of memory 100     15000   1400    0 error (42) 880     1400   12000    0 timeout 970   4600 11000 0 unknown 230    110 3800   0 unknown 360   950 4000 0 timeout 900   2300 8000 0 timeout 900     11000 11000    0 timeout 900    5200 11000   0 timeout 900 7400 13000 0 out of memory 650    15000 7800   0 unknown 59   1700 640 0 disqualified 3.5 89 41 0 error(unknown, verification-finished) 350    2400 4800   0 timeout 900   930 9500 0 timeout 900   5000 9700 0 timeout 900   1300 13000 0 true 17   200 110 2 error (1) 890   750 12000 0 true 26   270 320 2
array-examples/standard_init1_true-unreach-call_ground.i error (134) .090 24 .71 0 out of memory 100     15000   1400    0 error (42) 870     1400   11000    0 timeout 960   2800 8300 0 unknown 87    51 1100   0 out of memory (unknown error) 170   15000 1600 0 out of memory (unknown error) 170   15000 1600 0 timeout 900     6600 11000    0 timeout 900    76 9500   0 timeout 960 6700 8400 0 true 66    1500 840   2 unknown 78   1500 870 0 disqualified 2.6 79 37 0 true .92 63 14   2 timeout 900   910 10000 0 timeout 900   5200 6700 0 timeout 900   930 11000 0 true 16   200 100 2 error (1) 890   750 11000 0 true 23   260 300 2
array-examples/standard_init2_true-unreach-call_ground.i error (134) .086 24 .91 0 out of memory 52     15000   630    0 error (42) 870     2000   12000    0 timeout 960   2800 8900 0 unknown 110    60 1700   0 out of memory (unknown error) 170   15000 1900 0 out of memory (unknown error) 160   15000 1600 0 timeout 900     6600 13000    0 timeout 900    76 9000   0 timeout 970 7700 8400 0 true 110    2000 1400   2 unknown 60   1400 660 0 disqualified 2.7 77 29 0 true 1.2  79 17   2 timeout 900   730 9600 0 timeout 900   5200 8100 0 timeout 900   960 13000 0 true 15   200 130 2 error (1) 890   800 12000 0 true 23   260 350 2
array-examples/standard_init3_true-unreach-call_ground.i error (134) .081 24 .67 0 out of memory 57     15000   920    0 error (42) 880     2600   13000    0 timeout 960   3300 8600 0 unknown 120    60 1400   0 out of memory (unknown error) 170   15000 1600 0 out of memory (unknown error) 170   15000 1500 0 timeout 900     6400 9500    0 timeout 900    76 9600   0 timeout 960 7500 8200 0 true 150    2800 1800   2 unknown 55   1500 580 0 disqualified 2.7 80 40 0 true 1.5  96 20   2 timeout 900   760 13000 0 timeout 900   5200 10000 0 timeout 900   710 12000 0 true 17   200 110 2 error (1) 880   830 10000 0 true 24   250 330 2
array-examples/standard_init4_true-unreach-call_ground.i error (134) .085 24 .70 0 out of memory 61     15000   850    0 error (42) 880     3200   14000    0 timeout 970   4500 10000 0 unknown 150    81 2100   0 out of memory (unknown error) 170   15000 1700 0 out of memory (unknown error) 170   15000 1500 0 timeout 900     6500 12000    0 timeout 900    76 9200   0 timeout 960 5500 8500 0 true 190    3000 2800   2 unknown 56   1500 590 0 disqualified 2.9 84 36 0 true 1.8  110 25   2 timeout 900   880 9700 0 timeout 900   4500 8200 0 timeout 900   700 11000 0 true 16   200 120 2 error (1) 880   890 12000 0 true 24   250 350 2
array-examples/standard_init5_true-unreach-call_ground.i error (134) .11  24 .61 0 out of memory 66     15000   960    0 error (42) 880     3800   11000    0 timeout 970   4200 11000 0 unknown 170    77 2300   0 out of memory (unknown error) 170   15000 1700 0 out of memory (unknown error) 160   15000 1600 0 timeout 900     6600 10000    0 timeout 900    76 8700   0 timeout 960 4900 8000 0 true 230    3500 2600   2 unknown 59   1500 650 0 disqualified 2.9 85 39 0 true 2.0  130 28   2 timeout 900   730 9100 0 timeout 900   6200 8400 0 timeout 900   870 11000 0 true 16   200 110 2 error (1) 890   950 13000 0 true 33   330 430 2
array-examples/standard_init6_true-unreach-call_ground.i error (134) .085 23 1.2  0 out of memory 70     15000   950    0 error (42) 880     4400   12000    0 timeout 960   3100 9200 0 unknown 190    98 2900   0 out of memory (unknown error) 170   15000 1700 0 out of memory (unknown error) 160   15000 1500 0 timeout 900     6400 10000    0 timeout 900    77 9500   0 timeout 960 5200 7800 0 true 270    4000 3300   2 unknown 60   1700 750 0 disqualified 3.0 88 37 0 true 2.3  140 33   2 timeout 900   840 9000 0 timeout 900   5100 7700 0 timeout 900   870 8800 0 true 16   200 110 2 error (1) 880   1000 10000 0 true 26   260 360 2
array-examples/standard_init7_true-unreach-call_ground.i error (134) .082 24 .68 0 out of memory 75     15000   1100    0 error (42) 880     5000   11000    0 timeout 970   4400 10000 0 unknown 210    85 2500   0 out of memory (unknown error) 160   15000 1700 0 out of memory (unknown error) 160   15000 1600 0 timeout 900     6500 11000    0 timeout 900    77 9500   0 timeout 970 7300 9400 0 true 310    4500 3800   2 unknown 63   1500 600 0 disqualified 3.0 86 42 0 true 2.5  160 38   2 timeout 900   820 8500 0 timeout 900   5000 8000 0 timeout 900   870 9100 0 true 17   200 110 2 error (1) 880   1100 9900 0 true 27   260 370 2
array-examples/standard_init8_true-unreach-call_ground.i error (134) .13  24 .72 0 out of memory 54     15000   790    0 error (42) 880     5600   13000    0 timeout 960   2700 7800 0 unknown 240    110 3100   0 out of memory (unknown error) 170   15000 1600 0 out of memory (unknown error) 160   15000 1700 0 timeout 900     6600 11000    0 timeout 900    77 8400   0 timeout 970 6900 9200 0 true 350    5000 4000   2 unknown 63   1600 650 0 disqualified 3.1 91 38 0 true 2.8  180 39   2 timeout 900   880 8300 0 timeout 900   5300 8500 0 timeout 900   770 8100 0 true 17   200 130 2 error (1) 890   1100 10000 0 true 27   250 360 2
array-examples/standard_init9_true-unreach-call_ground.i error (134) .084 24 .82 0 out of memory 57     15000   860    0 error (42) 880     6200   11000    0 timeout 960   3400 9400 0 unknown 260    98 3100   0 out of memory (unknown error) 170   15000 1600 0 out of memory (unknown error) 170   15000 1600 0 timeout 900     6500 9400    0 timeout 900    77 8100   0 timeout 960 7100 8400 0 true 390    5800 4500   2 unknown 65   1600 660 0 disqualified 3.2 91 38 0 true 3.0  190 45   2 timeout 900   770 8700 0 timeout 900   3700 9400 0 timeout 900   920 10000 0 true 17   200 130 2 error (1) 880   1200 11000 0 true 28   260 400 2
array-examples/standard_maxInArray_true-unreach-call_ground.i error (134) .090 24 .62 0 error (42) 880     1100   4800    0 error (42) 880     980   14000    0 timeout 970   5000 7600 0 unknown 93    70 1200   0 unknown 8.4 430 97 0 unknown 8.0 430 120 0 timeout 900     8600 10000    0 timeout 900    75 8400   0 timeout 960 4700 7200 0 timeout 900    13000 11000   0 unknown 81   1500 910 0 disqualified 3.0 83 36 0 true 1.0  64 13   2 timeout 900   1800 13000 0 timeout 900   6400 8600 0 timeout 900   1300 12000 0 true 5.2 190 43 2 error (1) 880   650 13000 0 true 30   250 340 2
array-examples/standard_minInArray_true-unreach-call_ground.i error (134) .078 23 .89 0 error (42) 880     1100   4700    0 error (42) 880     980   12000    0 timeout 960   4500 8000 0 unknown 120    66 1400   0 unknown 8.3 430 95 0 unknown 8.2 430 97 0 timeout 900     8700 10000    0 true 1.3  83 16   2 timeout 970 6100 9900 0 timeout 900    13000 11000   0 unknown 81   1300 830 0 disqualified 3.0 83 37 0 true 1.1  64 14   2 timeout 900   1700 11000 0 timeout 900   6100 8100 0 timeout 900   1200 12000 0 true 5.5 190 47 2 error (1) 880   650 11000 0 true 28   240 370 2
array-examples/standard_palindrome_true-unreach-call_ground.i error (134) .080 24 .85 0 out of memory 150     13000   1900    0 error (42) 880     3700   12000    0 timeout 960   4200 9200 0 unknown 140    57 2200   0 unknown 180   680 2300 0 unknown 180   680 2000 0 timeout 900     12000 10000    0 timeout 900    76 7100   0 timeout 970 7400 10000 0 true 40    920 520   2 unknown 93   1600 1000 0 disqualified 2.5 77 28 0 true .68 39 9.0 2 timeout 900   890 11000 0 timeout 900   4800 8300 0 timeout 900   910 10000 0 true 20   190 160 2 error (1) 880   750 11000 0 true 17   130 210 2
array-examples/standard_partial_init_true-unreach-call_ground.i error (134) .082 24 .91 0 error (42) 880     7000   13000    0 error (42) 880     1700   14000    0 timeout 970   4500 12000 0 unknown 300    110 3800   0 unknown 8.1 430 96 0 unknown 8.2 430 100 0 timeout 900     4200 11000    0 timeout 900    77 8600   0 timeout 960 4800 7600 0 out of memory 260    15000 3100   0 unknown 78   1600 930 0 disqualified 140   110 1900 0 true 2.0  120 29   2 timeout 900   940 11000 0 timeout 900   5300 7300 0 timeout 900   1000 10000 0 true 16   200 120 2 error (1) 890   1900 10000 0 true 50   610 530 2
array-examples/standard_partition_original_true-unreach-call_ground.i error (134) .081 24 .86 0 out of memory 140     14000   1700    0 error (42) 870     2000   13000    0 timeout 970   4100 11000 0 unknown 300    86 4500   0 unknown 8.3 430 110 0 unknown 8.2 430 120 0 out of memory 430     15000 5600    0 true 1.7  83 26   2 timeout 960 5400 9100 0 out of memory 310    15000 3800   0 unknown 73   1500 730 0 disqualified 68   100 910 0 true 1.3  84 21   2 timeout 900   930 11000 0 timeout 900   5300 8600 0 timeout 900   1000 11000 0 true 17   200 100 2 error (1) 890   2100 13000 0 true 490   530 5700 2
array-examples/standard_partition_true-unreach-call_ground.i error (134) .089 24 .81 0 out of memory 160     14000   1900    0 error (42) 880     3000   12000    0 timeout 960   4400 12000 0 unknown 150    71 1800   0 unknown 8.1 430 93 0 unknown 8.2 430 90 0 timeout 900     4200 12000    0 timeout 900    76 9200   0 timeout 960 4000 9200 0 out of memory 310    15000 4100   0 unknown 120   1900 1200 0 disqualified 24   93 340 0 true .58 47 9.0 2 timeout 900   1300 11000 0 timeout 900   5400 7900 0 timeout 900   1000 12000 0 true 16   200 120 2 error (1) 890   2800 11000 0 true 200   440 2800 2
array-examples/standard_password_true-unreach-call_ground.i error (134) .091 24 .71 0 error (42) 880     1100   4000    0 error (42) 880     1300   13000    0 timeout 960   4600 9600 0 unknown 65    56 760   0 unknown 8.2 430 100 0 unknown 8.1 430 96 0 timeout 900     9100 10000    0 timeout 900    76 8000   0 timeout 900 2300 12000 0 out of memory 350    15000 4700   0 unknown 90   1700 1300 0 disqualified 2.7 85 32 0 true 1.3  63 18   2 timeout 900   910 12000 0 timeout 900   4900 8400 0 timeout 900   930 10000 0 true 4.6 190 36 2 error (1) 880   1200 12000 0 true 24   240 340 2
array-examples/standard_reverse_true-unreach-call_ground.i error (134) .077 23 .80 0 out of memory 150     13000   2000    0 error (42) 880     4100   12000    0 timeout 970   4800 8000 0 unknown 140    84 1800   0 unknown 450   950 5500 0 unknown 450   950 5500 0 timeout 900     10000 12000    0 timeout 900    76 9000   0 unknown 100 1500 1300 0 true 76    1800 1000   2 unknown 94   1600 1100 0 disqualified 2.7 82 36 0 true 1.2  64 17   2 timeout 900   920 12000 0 timeout 900   4600 7900 0 timeout 900   1000 12000 0 true 17   200 120 2 error (1) 880   1300 13000 0 true 79   610 810 2
array-examples/standard_running_true-unreach-call.i error (134) .088 23 .68 0 out of memory 82     15000   1200    0 out of memory 310     15000   4100    0 timeout 960   4600 8100 0 unknown 900    1700 10000   0 unknown 8.1 430 120 0 unknown 8.1 430 100 0 out of memory 390     15000 4600    0 timeout 900    76 8900   0 timeout 970 3900 8200 0 out of memory 330    15000 4800   0 unknown 74   1700 880 0 disqualified 2.7 80 34 0 true 1.1  45 16   2 timeout 900   1600 13000 0 timeout 900   5300 8700 0 timeout 900   1400 13000 0 true 16   200 100 2 error (1) 880   2000 12000 0 true 230   1100 2200 2
array-examples/standard_sentinel_true-unreach-call_true-termination.i error (134) .12  24 .65 0 error (42) 880     2500   12000    0 error (42) 880     2600   11000    0 timeout 960   4100 11000 0 unknown 55    44 810   0 unknown 48   430 660 0 true 8.8 370 110 2 timeout 900     330 12000    0 timeout 900    3600 11000   0 true 15 1200 98 2 timeout 900    930 4400   0 true 29   1000 290 2 disqualified 2.7 75 28 0 timeout (verification) 900    2600 4100   0 true 13   500 110 2 true 15   640 120 2 true 14   570 130 2 true 29   510 220 2 error (1) 860   5200 11000 0 true 14   140 180 2
array-examples/standard_seq_init_true-unreach-call_ground.i error (134) .081 23 .78 0 out of memory 150     13000   2200    0 error (42) 880     3800   12000    0 timeout 960   2500 8500 0 unknown 120    56 1600   0 out of memory (unknown error) 170   15000 1700 0 out of memory (unknown error) 170   15000 1700 0 timeout 900     7600 13000    0 timeout 900    76 8800   0 timeout 900 7600 11000 0 true 74    1600 840   2 unknown 85   1600 960 0 disqualified 2.8 82 36 0 true 1.1  64 18   2 timeout 900   670 13000 0 timeout 900   5100 7800 0 timeout 900   980 13000 0 true 4.5 190 38 2 error (1) 880   800 11000 0 true 22   240 270 2
array-examples/standard_strcmp_true-unreach-call_ground.i error (134) .080 23 .80 0 error (42) 880     2600   6400    0 error (42) 880     1200   12000    0 timeout 960   4400 8600 0 unknown 56    55 800   0 unknown 89   430 1400 0 unknown 88   430 1200 0 timeout 900     8400 10000    0 true 1.6  83 20   2 timeout 970 7000 8400 0 out of memory 41    15000 500   0 unknown 360   1600 3200 0 disqualified 2.7 82 37 0 true 1.3  79 22   2 timeout 900   1100 11000 0 timeout 900   5600 8500 0 timeout 900   4300 5400 0 true 4.4 200 38 2 error (1) 880   1800 11000 0 true 130   660 1300 2
array-examples/standard_strcpy_original_true-unreach-call.i error (134) .084 24 .69 0 out of memory 64     15000   800    0 error (42) 880     2100   14000    0 timeout 970   4300 8600 0 unknown 120    63 1600   0 unknown 450   950 5300 0 timeout 900   2200 8500 0 timeout 900     12000 9700    0 timeout 900    5100 11000   0 timeout 960 6900 7500 0 out of memory 500    15000 6400   0 unknown 82   1600 980 0 disqualified 7.6 100 100 0 error(unknown, verification-finished) 170    2300 2300   0 timeout 900   760 11000 0 timeout 900   3700 11000 0 timeout 900   910 12000 0 true 16   200 120 2 error (1) 890   2000 12000 0 true 37   280 450 2
array-examples/standard_strcpy_true-unreach-call_ground.i error (134) .085 24 .75 0 out of memory 64     15000   950    0 error (42) 880     2200   12000    0 timeout 960   4100 9500 0 unknown 190    140 2600   0 unknown 450   950 4900 0 timeout 900   2300 8100 0 timeout 900     12000 11000    0 timeout 900    4900 11000   0 timeout 970 6400 9200 0 out of memory 480    15000 5100   0 unknown 65   1600 640 0 disqualified 5.7 98 76 0 error(unknown, verification-finished) 160    2400 1900   0 timeout 900   900 11000 0 timeout 900   4000 11000 0 timeout 900   1000 11000 0 true 16   200 100 2 error (1) 890   1400 13000 0 true 32   240 410 2
array-examples/standard_two_index_01_true-unreach-call.i out of memory 300     15000 2000    0 out of memory 71     15000   930    0 error (42) 870     840   13000    0 timeout 970   9200 6100 0 unknown 120    59 1800   0 unknown 23   520 270 0 timeout 900   1300 7900 0 timeout 900     12000 11000    0 timeout 900    4500 11000   0 timeout 960 9900 10000 0 true 14    290 180   2 unknown 9.0 290 81 0 disqualified 880   870 9100 0 true .40 34 5.2 2 timeout 900   910 9600 0 timeout 900   5300 8200 0 timeout 900   940 12000 0 true 16   200 110 2 error (1) 880   220 11000 0 true 16   240 170 2
array-examples/standard_two_index_02_true-unreach-call.i error (134) .084 24 .67 0 out of memory 160     13000   2100    0 error (42) 880     4300   13000    0 timeout 970   4100 12000 0 unknown 180    66 2800   0 unknown 670   1200 8000 0 timeout 900   2300 7800 0 timeout 900     11000 11000    0 timeout 900    5000 13000   0 timeout 960 5800 9100 0 true 97    2000 1200   2 unknown 83   1500 1200 0 disqualified 2.7 81 34 0 true 2.4  190 29   2 timeout 900   860 10000 0 timeout 900   4300 7900 0 timeout 900   990 10000 0 true 17   200 110 2 error (1) 890   2000 11000 0 true 34   130 390 2
array-examples/standard_two_index_03_true-unreach-call.i out of memory 250     15000 2200    0 out of memory 97     13000   1500    0 error (42) 880     960   12000    0 timeout 960   9900 8900 0 unknown 140    63 2200   0 unknown 18   490 200 0 timeout 900   1300 7800 0 timeout 900     12000 9100    0 timeout 900    4600 10000   0 timeout 960 7600 8200 0 true 7.9  180 96   2 unknown 83   1800 940 0 disqualified 900   4400 13000 0 true .33 31 4.9 2 timeout 900   730 11000 0 timeout 900   5300 7900 0 timeout 900   890 11000 0 true 17   200 110 2 error (1) 880   220 11000 0 true 61   400 780 2
array-examples/standard_two_index_04_true-unreach-call.i error (134) .087 24 .66 0 out of memory 150     13000   2600    0 error (42) 880     4600   12000    0 timeout 970   4600 8700 0 unknown 160    64 2500   0 unknown 560   1100 6400 0 timeout 900   2300 8600 0 timeout 900     11000 9900    0 timeout 900    5100 11000   0 timeout 960 6500 9800 0 true 71    1600 970   2 unknown 83   1600 910 0 disqualified 2.6 82 37 0 true 2.1  180 24   2 timeout 900   740 12000 0 timeout 900   5100 9600 0 timeout 900   1100 10000 0 true 16   200 110 2 error (1) 890   2000 12000 0 true 32   130 410 2
array-examples/standard_two_index_05_true-unreach-call.i error (134) .081 24 .80 0 out of memory 160     13000   2100    0 error (42) 880     4700   12000    0 timeout 960   2800 9500 0 unknown 150    68 2200   0 unknown 540   1100 6300 0 timeout 900   2300 8400 0 timeout 900     12000 12000    0 timeout 900    5100 11000   0 timeout 960 7700 9400 0 true 65    1500 790   2 unknown 84   1700 910 0 disqualified 2.5 81 37 0 true 1.9  180 27   2 timeout 900   750 8600 0 timeout 900   3800 7700 0 timeout 900   1100 11000 0 true 16   200 110 2 error (1) 890   2000 12000 0 true 31   130 440 2
array-examples/standard_two_index_06_true-unreach-call.i out of memory 230     15000 1600    0 out of memory 97     13000   1500    0 error (42) 880     970   13000    0 timeout 960   9700 10000 0 unknown 160    65 1900   0 unknown 17   480 210 0 timeout 900   1300 8300 0 timeout 900     12000 9800    0 timeout 900    4700 12000   0 timeout 970 8000 9200 0 true 6.3  150 87   2 unknown 84   1600 860 0 disqualified 890   1100 11000 0 true .32 29 3.5 2 timeout 900   730 12000 0 timeout 900   5200 10000 0 timeout 900   980 11000 0 true 16   200 120 2 error (1) 880   220 11000 0 true 8.5 130 100 2
array-examples/standard_two_index_07_true-unreach-call.i error (134) .082 23 .84 0 out of memory 160     13000   2000    0 error (42) 880     4300   12000    0 timeout 970   3900 7200 0 unknown 160    71 1900   0 unknown 510   1000 5600 0 timeout 900   2300 9200 0 timeout 900     12000 9900    0 timeout 900    5100 12000   0 timeout 960 5400 8400 0 true 60    1400 730   2 unknown 84   1600 1100 0 disqualified 2.5 81 39 0 true 1.9  180 24   2 timeout 900   910 9000 0 timeout 900   5100 7600 0 timeout 900   1100 13000 0 true 16   200 110 2 error (1) 890   2000 11000 0 true 83   630 960 2
array-examples/standard_two_index_08_true-unreach-call.i error (134) .087 24 1.0  0 out of memory 160     13000   2100    0 error (42) 880     4300   11000    0 timeout 970   4000 10000 0 unknown 160    67 2000   0 unknown 500   1000 6200 0 timeout 900   2300 8200 0 timeout 900     12000 10000    0 timeout 900    5200 12000   0 timeout 960 4900 8500 0 true 58    1400 790   2 unknown 83   1500 1100 0 disqualified 2.5 81 32 0 true 1.9  180 25   2 timeout 900   930 9800 0 timeout 900   5200 8400 0 timeout 900   1100 12000 0 true 17   200 110 2 error (1) 890   2000 11000 0 true 31   130 440 2
array-examples/standard_two_index_09_true-unreach-call.i error (134) .11  24 .73 0 out of memory 160     13000   2500    0 error (42) 880     4700   11000    0 timeout 970   3600 9000 0 unknown 170    70 2200   0 unknown 500   1000 5500 0 timeout 900   2300 8100 0 timeout 900     12000 9800    0 timeout 900    5200 11000   0 timeout 970 7900 8700 0 true 57    1400 680   2 unknown 84   1700 990 0 disqualified 2.4 74 29 0 true 1.9  180 23   2 timeout 900   920 9700 0 timeout 900   5200 8000 0 timeout 900   1100 12000 0 true 17   200 130 2 error (1) 890   2000 13000 0 true 83   700 950 2
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i error (134) .081 24 .77 0 error (42) 880     1800   8800    0 error (42) 880     790   11000    0 timeout 960   6100 7400 0 unknown 60    51 920   0 unknown 8.2 430 93 0 unknown 8.1 430 100 0 timeout 900     1000 11000    0 timeout 900    75 5900   0 timeout 940 5900 7100 0 out of memory 380    15000 5900   0 unknown 170   1300 1400 0 disqualified 880   380 11000 0 true .14 15 1.5 2 timeout 900   1200 11000 0 timeout 900   970 7300 0 timeout 900   960 13000 0 true 15   200 110 2 error (1) 880   620 12000 0 true 130   340 1700 2
array-examples/standard_vector_difference_true-unreach-call_ground.i error (134) .086 24 .69 0 out of memory 120     15000   1700    0 error (42) 880     2000   11000    0 timeout 960   4100 11000 0 unknown 130    73 1700   0 unknown 540   950 6200 0 unknown 540   950 7300 0 timeout 900     5400 13000    0 timeout 900    76 8400   0 timeout 960 6100 7700 0 out of memory 130    15000 1200   0 unknown 100   1900 1200 0 disqualified 2.9 86 39 0 true 1.5  67 20   2 timeout 900   680 12000 0 timeout 900   3400 7900 0 timeout 900   750 11000 0 true 4.5 190 41 2 error (1) 890   1800 12000 0 true 56   260 810 2
array-examples/standard_sentinel_true-unreach-call.i.v+cfa-reducer.c error (134) .094 24 .74 0 error (42) 880     2500   13000    0 error (42) 880     2700   11000    0 timeout 960   4300 10000 0 unknown 55    44 700   0 unknown 48   430 670 0 true 9.2 370 130 2 timeout 900     330 12000    0 timeout 900    3400 10000   0 timeout 960 5100 12000 0 timeout 900    940 3900   0 true 30   970 300 2 disqualified 2.7 75 33 0 timeout (verification) 900    2600 4200   0 true 15   650 140 2 true 17   650 130 2 true 15   660 120 2 timeout 900   3400 11000 0 error (1) 870   3900 13000 0 unknown 18   130 220 0
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i error (134) .10  24 .84 0 out of memory 52     15000   630    0 error (42) 870     1800   12000    0 timeout 970   4000 9700 0 unknown 1.2  67 13   0 out of memory (unknown error) 170   15000 1600 0 out of memory (unknown error) 160   15000 1500 0 timeout 900     7400 9900    0 false(unreach-call) .44 84 5.2 1 timeout 960 5400 8900 0 false(unreach-call) 190    2800 2600   1 unknown 84   1500 1000 0 disqualified 3.1 82 38 0 false(unreach-call) .79 110 12   1 timeout 900   1000 10000 0 timeout 900   5000 8600 0 timeout 900   1100 9400 0 out of memory 480   15000 5300 0 false(unreach-call) 4.2 820 47 1 false(unreach-call) 6.6 130 92 1
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i out of memory 35     15000 510    0 out of memory 290     15000   3100    0 out of memory 23     8000   230    0 timeout 960   3700 7700 0 unknown 1.2  67 15   0 out of memory (unknown error) 170   15000 1800 0 out of memory (unknown error) 170   15000 1600 0 timeout 900     6400 10000    0 false(unreach-call) .45 84 5.0 1 timeout 960 6900 7100 0 false(unreach-call) 180    2300 2600   1 unknown 14   730 130 0 disqualified 3.2 82 38 0 false(unreach-call) .78 110 9.8 1 timeout 900   1500 10000 0 timeout 900   5100 7800 0 timeout 900   4900 9200 0 out of memory 600   15000 6100 0 false(unreach-call) 5.6 490 49 1 unknown 60   280 690 0
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i error (134) .086 24 .83 0 out of memory 68     15000   980    0 out of memory 190     15000   3100    0 timeout 970   4700 12000 0 unknown 230    66 3100   0 unknown 8.2 430 97 0 timeout 900   12000 7000 0 timeout 900     4900 11000    0 false(unreach-call) 3.1  240 40   1 timeout 900 6500 12000 0 out of memory 310    15000 4300   0 unknown 150   1500 1400 0 disqualified 4.4 110 53 0 false(unreach-call) 1.7  200 22   1 timeout 900   1100 9300 0 timeout 900   5100 9500 0 timeout 900   1200 10000 0 false(unreach-call) 16   200 110 1 false(unreach-call) 5.6 2400 67 1 false(unreach-call) 9.5 130 140 1
array-industry-pattern/array_range_init_false-unreach-call.i true 42     15000 480    -32 out of memory 380     15000   4900    0 out of memory 280     15000   3700    0 timeout 960   3800 10000 0 unknown 210    55 2900   0 false(unreach-call) 400   3700 4300 1 false(unreach-call) 400   3700 4600 1 timeout 900     5200 10000    0 false(unreach-call) .48 83 5.7 1 timeout 960 6200 7900 0 false(unreach-call) 210    2900 2800   1 unknown 41   780 440 0 disqualified 3.1 85 38 0 false(unreach-call) 1.0  120 14   1 timeout 900   1200 8800 0 timeout 900   5300 7100 0 timeout 900   4100 9100 0 false(unreach-call) 15   200 120 1 false(unreach-call) 3.8 150 43 1 false(unreach-call) 6.9 130 91 1
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i error (134) .090 24 .82 0 out of memory 68     15000   880    0 out of memory 190     15000   2900    0 timeout 970   4000 9500 0 unknown 180    81 2500   0 unknown 8.2 430 98 0 timeout 900   13000 7100 0 timeout 900     4900 10000    0 timeout 900    5000 6100   0 timeout 900 6800 11000 0 out of memory 310    15000 3700   0 unknown 420   1500 3600 0 disqualified 4.5 120 58 0 timeout (verification) 900    2600 10000   0 timeout 900   1100 11000 0 timeout 900   5000 7500 0 timeout 900   1200 8900 0 false(unreach-call) 17   200 120 0 error (1) 890   2400 13000 0 false(unreach-call) 9.5 130 130 0
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i error (134) .087 24 .76 0 out of memory 66     14000   880    0 error (42) 880     1800   13000    0 timeout 970   5700 9100 0 unknown 900    1300 11000   0 unknown 8.1 430 120 0 unknown 8.2 430 91 0 timeout 900     3400 10000    0 false(unreach-call) .53 84 6.8 1 timeout 910 7900 12000 0 out of memory 720    15000 4600   0 unknown 89   1500 960 0 disqualified 5.9 110 76 0 false(unreach-call) 1.7  320 23   1 timeout 900   1700 14000 0 timeout 900   5300 9600 0 timeout 900   1500 13000 0 out of memory 71   15000 900 0 error (1) 24   9200 330 0 out of memory 55   15000 670 0
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i error (134) .081 24 .76 0 out of memory 89     15000   1400    0 error (42) 880     1900   12000    0 timeout 970   4800 9800 0 unknown 170    58 2200   0 unknown 8.3 430 95 0 timeout 900   4200 5200 0 timeout 900     4000 9700    0 timeout 900    5000 11000   0 timeout 960 4800 9100 0 out of memory 320    15000 4800   0 unknown 580   1800 5200 0 disqualified 2.7 84 40 0 timeout (verification) 900    2600 13000   0 timeout 900   770 11000 0 timeout 900   5300 7500 0 timeout 900   910 11000 0 true 16   200 120 2 error (1) 880   1400 13000 0 true 25   130 290 2
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i error (134) .080 24 .80 0 out of memory 100     15000   1400    0 error (42) 880     2700   14000    0 timeout 970   4200 8400 0 unknown 900    340 11000   0 out of memory (unknown error) 270   15000 2700 0 out of memory (unknown error) 270   15000 3100 0 timeout 900     4400 10000    0 unknown 1.1  43 16   0 timeout 910 7900 11000 0 out of memory 440    15000 5300   0 unknown 73   1500 710 0 disqualified 880   260 12000 0 timeout (verification) 900    3100 9600   0 timeout 900   890 10000 0 timeout 900   3800 8300 0 timeout 900   820 12000 0 out of memory 470   15000 5400 0 error (1) 890   1600 14000 0 true 62   240 680 2
array-industry-pattern/array_of_struct_break_true-unreach-call.i true 36     13000 480    2 out of memory 210     15000   2600    0 out of memory 760     15000   9100    0 timeout 970   6800 7300 0 unknown 740    1400 8000   0 unknown 8.2 430 91 0 timeout 900   6200 9100 0 out of memory 570     15000 4600    0 timeout 900    210 8800   0 timeout 960 6900 8100 0 out of memory 43    15000 320   0 unknown 14   730 120 0 disqualified 2.7 84 30 0 true .95 69 14   2 timeout 900   1400 12000 0 timeout 900   5200 11000 0 timeout 900   4900 9800 0 true 16   200 110 2 error (1) 880   360 12000 0 unknown 59   150 750 0
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i error (134) 240     7000 1800    0 out of memory 310     15000   4200    0 error (134) 2.6   400   30    0 timeout 970   4800 8400 0 unknown .81 65 8.7 0 unknown 8.3 440 99 0 timeout 900   4700 8600 0 timeout 900     5300 10000    0 timeout 900    4800 6300   0 timeout 910 5300 6800 0 timeout 900    5800 9200   0 unknown 14   690 140 0 disqualified 8.6 100 120 0 timeout (verification) 900    3200 14000   0 timeout 900   1200 9300 0 timeout 900   5200 6600 0 timeout 900   4000 6200 0 true 17   200 120 2 error (1) 890   410 11000 0 error (1) 2.4 130 33 0
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i error (134) .18  24 1.2  0 out of memory 180     15000   2100    0 error (42) 880     2000   12000    0 timeout 960   4800 7200 0 unknown 400    590 4500   0 out of memory (unknown error) 120   15000 1300 0 out of memory (unknown error) 120   15000 1200 0 timeout 900     13000 10000    0 true 9.8  4700 100   2 timeout 970 7600 8600 0 timeout 900    450 9700   0 unknown 11   290 110 0 disqualified 3.0 83 35 0 true 1.2  100 17   2 true 15   500 120 2 timeout 900   5300 7600 0 true 18   650 140 2 true 41   1200 450 2 error (1) 890   750 11000 0 unknown 2.4 130 34 0
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i error (134) 160     7000 1100    0 out of memory 310     15000   4000    0 error (134) 2.5   400   29    0 timeout 960   4000 8800 0 unknown .83 67 8.4 0 unknown 8.3 440 110 0 timeout 900   4600 9100 0 timeout 900     4900 10000    0 timeout 900    4900 7900   0 timeout 930 5700 6900 0 timeout 900    5800 13000   0 unknown 14   690 150 0 disqualified 2.9 80 37 0 timeout (verification) 900    4000 12000   0 timeout 900   1000 8700 0 timeout 900   5400 8800 0 timeout 900   4000 6200 0 true 16   200 110 2 error (1) 880   410 13000 0 error (1) 2.5 130 31 0
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i out of memory 36     15000 440    0 out of memory 410     15000   5000    0 error (134) 5.3   500   51    0 timeout 960   4000 8900 0 unknown 900    1500 9200   0 out of memory (unknown error) 170   15000 1900 0 out of memory (unknown error) 170   15000 1800 0 timeout 900     3000 14000    0 unknown 1.1  43 15   0 timeout 960 6300 10000 0 out of memory 110    15000 1000   0 unknown 14   690 130 0 disqualified 880   440 9300 0 timeout (verification) 900    2800 9400   0 timeout 900   1700 11000 0 timeout 900   2700 8800 0 timeout 900   5200 8100 0 true 18   200 130 2 error (1) 890   510 11000 0 unknown 2.4 130 31 0
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i out of memory 28     15000 450    0 out of memory 89     15000   1200    0 out of memory 22     9200   320    0 timeout 960   3900 10000 0 unknown 900    2200 12000   0 unknown 8.3 440 97 0 unknown 8.5 440 110 0 timeout 900     1700 13000    0 timeout 900    210 11000   0 timeout 900 6900 13000 0 out of memory 42    15000 460   0 unknown 15   1200 120 0 disqualified 5.9 97 84 0 true 1.4  110 16   2 timeout 900   1300 8100 0 timeout 900   5400 10000 0 timeout 900   5000 6500 0 true 17   200 130 2 error (1) 890   510 13000 0 unknown 62   200 740 0
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i timeout 900     11000 7900    0 error (42) 870     13000   12000    0 error (42) 880     10000   10000    0 timeout 960   3700 7900 0 unknown 900    1900 9600   0 out of memory (unknown error) 130   15000 1300 0 out of memory (unknown error) 130   15000 1200 0 timeout 900     9100 11000    0 timeout 900    79 8200   0 timeout 900 5600 8600 0 timeout 900    920 11000   0 unknown 14   760 120 0 disqualified 2.7 84 34 0 true 1.1  82 16   2 timeout 900   1200 9700 0 timeout 900   5200 7400 0 timeout 900   4700 6800 0 true 15   200 120 2 error (1) 880   220 13000 0 true 8.3 130 120 2
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i error (134) 260     6900 1900    0 out of memory 320     15000   4100    0 error (134) 6.7   400   69    0 timeout 970   4900 7300 0 unknown 900    2200 8700   0 unknown 8.3 440 120 0 timeout 900   9400 8100 0 timeout 900     4300 9000    0 timeout 900    4900 6700   0 timeout 960 5700 7000 0 timeout 900    11000 8800   0 unknown 14   680 130 0 disqualified 19   120 250 0 timeout (verification) 900    4200 12000   0 timeout 900   1300 9800 0 timeout 900   5400 8800 0 timeout 900   4400 6500 0 true 17   200 120 2 error (1) 880   410 12000 0 error (1) 2.5 130 33 0
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i timeout 900     12000 4500    0 out of memory 510     13000   6400    0 error (42) 870     4500   10000    0 timeout 960   5500 7700 0 unknown 900    83 11000   0 unknown 8.3 430 120 0 unknown 1.5 200 25 0 timeout 900     150 11000    0 true 9.3  75 120   2 timeout 960 6000 9500 0 timeout 900    8700 4000   0 unknown 9.2 300 87 0 disqualified 880   380 12000 0 timeout (verification) 900    1100 10000   0 timeout 900   1000 8600 0 timeout 900   1000 7800 0 timeout 900   920 7300 0 true 16   200 110 2 timeout 900   150 12000 0 true 7.5 240 86 2
reducercommutativity/rangesum05_false-unreach-call_true-termination.i error (134) .087 24 .71 0 false(unreach-call) .13  9.3 .89 1 false(unreach-call) .16  8.9 1.2  1 exception 380   2300 2800 0 false(unreach-call) 6.0  69 61   1 unknown 8.2 430 100 0 false(unreach-call) 8.8 430 110 1 false(unreach-call) .88  58 13    1 unknown .83 40 13   0 false(unreach-call) 16 1200 120 1 false(unreach-call) .41 58 4.3 1 false(unreach-call) 6.3 370 56 1 disqualified 2.8 84 36 0 false(unreach-call) .46 62 5.5 1 false(unreach-call) 14   550 110 1 false(unreach-call) 14   510 120 1 false(unreach-call) 22   740 180 1 false(unreach-call) 67   610 700 1 false(unreach-call) 3.5 150 35 1 false(unreach-call) 5.1 130 77 1
reducercommutativity/rangesum10_false-unreach-call_true-termination.i error (134) .090 24 .62 0 false(unreach-call) .15  9.5 1.5  1 false(unreach-call) .15  9.4 1.5  1 exception 460   2500 2600 0 false(unreach-call) 14    79 200   1 unknown 8.1 430 110 0 false(unreach-call) 9.0 440 110 1 false(unreach-call) .88  58 11    1 unknown .80 39 11   0 false(unreach-call) 16 1300 110 1 false(unreach-call) .43 58 5.1 1 false(unreach-call) 7.2 410 59 1 disqualified 3.0 84 37 0 false(unreach-call) .61 61 6.6 1 false(unreach-call) 32   550 370 1 false(unreach-call) 20   560 170 1 false(unreach-call) 26   750 220 1 false(unreach-call) 230   910 2200 1 false(unreach-call) 3.6 150 37 1 false(unreach-call) 5.1 130 76 1
reducercommutativity/rangesum20_false-unreach-call.i error (134) .087 24 .74 0 false(unreach-call) .53  14   7.8  0 false(unreach-call) .53  15   7.0  0 timeout 900   3500 6400 0 false(unreach-call) 46    94 490   1 unknown 8.1 430 100 0 false(unreach-call) 20   490 230 1 false(unreach-call) 1.4   57 18    1 unknown .82 40 9.3 0 false(unreach-call) 18 1300 120 1 false(unreach-call) .57 60 5.0 1 false(unreach-call) 7.6 430 72 1 disqualified 3.7 120 50 0 false(unreach-call) 1.5  62 21   1 timeout 900   1100 9500 0 false(unreach-call) 46   970 490 1 unknown 29   860 250 0 false(unreach-call) 210   1400 2200 1 false(unreach-call) 3.5 150 34 1 false(unreach-call) 5.1 130 65 1
reducercommutativity/rangesum40_false-unreach-call.i error (134) .085 24 .73 0 false(unreach-call) .89  24   13    0 false(unreach-call) 4.2   38   54    0 timeout 900   5100 6900 0 unknown 680    270 8000   0 unknown 8.2 430 88 0 false(unreach-call) 130   510 1600 1 false(unreach-call) 9.3   59 110    1 unknown .83 40 7.9 0 false(unreach-call) 29 1500 230 1 false(unreach-call) .75 72 8.7 1 unknown 87   2000 900 0 disqualified 5.0 140 72 0 false(unreach-call) 8.4  69 82   1 timeout 900   1000 11000 0 timeout 900   1300 9500 0 unknown 63   920 680 0 false(unreach-call) 240   1500 3000 0 false(unreach-call) 3.6 150 36 1 false(unreach-call) 5.2 130 68 1
reducercommutativity/rangesum60_false-unreach-call.i error (134) .088 24 .69 0 false(unreach-call) 5.2   49   67    0 false(unreach-call) 1.7   42   26    0 timeout 910   5800 6700 0 unknown 900    360 11000   0 unknown 8.4 430 110 0 false(unreach-call) 190   530 2100 1 false(unreach-call) 180     170 2200    1 unknown .82 39 12   0 false(unreach-call) 68 1800 670 1 false(unreach-call) 1.0  91 11   1 unknown 87   1700 1100 0 disqualified 7.4 220 110 0 false(unreach-call) 66    89 800   1 timeout 900   770 10000 0 timeout 900   3300 11000 0 unknown 59   1900 560 0 false(unreach-call) 250   1500 2800 0 false(unreach-call) 3.6 150 34 1 false(unreach-call) 5.2 130 74 1
reducercommutativity/rangesum_false-unreach-call_true-termination.i error (134) .085 24 .94 0 false(unreach-call) .39  37   5.3  1 out of memory 350     15000   5600    0 exception 32   1400 220 0 false(unreach-call) 4.5  68 54   1 unknown 8.1 430 100 0 unknown 1.6 200 23 0 false(unreach-call) 1.1   58 17    1 unknown .85 40 9.6 0 false(unreach-call) 40 1400 400 1 timeout 900    7500 5400   0 unknown 12   320 120 0 disqualified 3.7 88 48 0 false(unreach-call) .76 21 10   1 false(unreach-call) 12   540 96 1 timeout 900   1100 10000 0 false(unreach-call) 27   980 220 1 false(unreach-call) 91   620 950 1 false(unreach-call) 3.9 150 40 0 unknown 190   400 2500 0
reducercommutativity/avg05_true-unreach-call_true-termination.i error (134) .091 24 .72 0 error (42) 880     220   13000    0 error (42) 880     230   13000    0 timeout 900   2200 7500 0 unknown 46    84 610   0 unknown 8.1 430 120 0 true 8.8 370 120 2 true 43     70 570    2 unknown .77 39 11   0 timeout 900 3600 7600 0 true .37 59 3.5 2 true 17   640 160 2 disqualified 2.1 72 26 0 true .17 18 1.7 2 timeout 900   760 13000 0 true 69   760 680 2 timeout 900   810 13000 0 true 4.7 190 30 2 timeout 900   150 10000 0 true 28   240 340 2
reducercommutativity/avg10_true-unreach-call_true-termination.i error (134) .098 23 .67 0 error (42) 880     320   13000    0 error (42) 880     310   13000    0 timeout 900   3700 10000 0 unknown 520    200 8200   0 unknown 8.2 430 94 0 true 8.5 370 140 2 true 520     200 7300    2 unknown .78 39 11   0 timeout 900 3600 8300 0 true .39 62 3.5 2 true 18   650 200 2 disqualified 2.1 76 29 0 true .17 17 1.8 2 timeout 900   1600 11000 0 timeout 900   1400 12000 0 timeout 900   1900 12000 0 true 4.6 190 36 2 timeout 900   150 9900 0 true 21   230 250 2
reducercommutativity/avg20_true-unreach-call.i error (134) .082 24 .84 0 error (42) 880     470   13000    0 error (42) 880     410   13000    0 timeout 900   3800 6300 0 unknown 900    310 12000   0 unknown 8.2 430 100 0 true 8.6 370 110 2 timeout 900     280 11000    0 unknown .79 39 10   0 timeout 900 4300 8000 0 true .50 87 5.0 2 true 20   540 210 2 disqualified 2.4 90 34 0 true .17 18 1.8 2 timeout 900   5400 7900 0 timeout 900   4800 8800 0 timeout 900   5300 6200 0 true 5.0 190 36 2 timeout 900   160 14000 0 true 16   220 220 2
reducercommutativity/avg40_true-unreach-call.i error (134) .085 24 .70 0 error (42) 880     550   11000    0 error (42) 880     560   12000    0 timeout 900   6100 6700 0 unknown 260    270 3000   0 unknown 8.2 430 110 0 true 8.8 380 100 2 timeout 900     360 11000    0 unknown .80 39 9.8 0 timeout 900 6000 7600 0 true .94 230 12   2 unknown 220   2500 2400 0 disqualified 3.3 140 43 0 true .18 18 2.8 2 timeout 900   1000 12000 0 timeout 900   3600 8300 0 timeout 900   5200 11000 0 true 4.8 190 38 2 timeout 900   150 13000 0 true 24   240 330 2
reducercommutativity/avg60_true-unreach-call.i error (134) .079 23 1.0  0 error (42) 880     650   11000    0 error (42) 880     670   11000    0 timeout 900   5100 7300 0 unknown 900    510 12000   0 unknown 8.4 430 100 0 true 8.9 380 120 2 timeout 900     420 11000    0 unknown .81 40 10   0 timeout 900 5400 9700 0 true 1.4  490 17   2 unknown 92   1600 950 0 disqualified 5.0 220 70 0 true .20 17 1.9 2 timeout 900   890 12000 0 timeout 900   4000 13000 0 timeout 900   1600 11000 0 true 4.7 190 41 2 timeout 900   150 11000 0 true 32   240 330 2
reducercommutativity/avg_true-unreach-call_true-termination.i error (134) .080 24 .70 0 error (42) 870     360   13000    0 error (42) 880     310   11000    0 exception 26   1200 210 0 unknown 900    130 12000   0 unknown 8.1 430 110 0 unknown 1.6 200 18 0 timeout 900     150 12000    0 unknown .79 40 11   0 timeout 930 4100 9200 0 timeout 900    9800 5500   0 unknown 11   320 93 0 disqualified 880   180 11000 0 timeout (verification) 900    3800 12000   0 timeout 900   590 13000 0 timeout 900   640 12000 0 timeout 900   700 13000 0 true 3.1 150 26 2 error (1) 3.5 150 41 0 true 11   240 160 2
reducercommutativity/max05_true-unreach-call_true-termination.i error (134) .11  24 .66 0 true 2.1   12   27    2 true 410     5300   5900    2 true 220   1500 1700 2 unknown 2.6  67 39   0 unknown 8.2 430 97 0 true 400   410 3900 2 true .71  28 10    2 unknown .78 39 11   0 true 240 2300 1900 2 true 2.3  380 28   2 true 17   420 240 2 disqualified 2.1 73 30 0 true 2.8  23 36   2 timeout 900   2000 12000 0 true 440   2600 4800 2 timeout 900   1300 12000 0 true 5.5 190 44 2 timeout 900   200 13000 0 true 12   230 150 2
reducercommutativity/max10_true-unreach-call_true-termination.i error (134) .088 24 .75 0 true 230     49   3500    2 out of memory 110     15000   1300    0 timeout 900   2100 6700 0 unknown 21    68 300   0 unknown 8.2 430 92 0 timeout 900   400 7400 0 true 17     42 220    2 unknown .80 39 8.3 0 timeout 900 2900 7200 0 out of memory 61    15000 800   0 true 19   400 210 2 disqualified 2.4 81 38 0 true 180    64 2900   2 timeout 900   2900 8300 0 timeout 900   5800 10000 0 timeout 900   1500 13000 0 true 5.5 190 49 2 timeout 900   150 13000 0 true 19   330 210 2
reducercommutativity/max20_true-unreach-call.i error (134) .085 24 .82 0 error (42) 880     210   11000    0 out of memory 110     15000   1300    0 timeout 900   2300 7900 0 unknown 900    140 11000   0 unknown 8.3 430 120 0 timeout 900   400 7700 0 timeout 900     130 13000    0 unknown .78 39 13   0 timeout 900 2900 6500 0 out of memory 86    15000 1300   0 true 23   530 190 2 disqualified 3.5 110 39 0 timeout (verification) 900    140 11000   0 timeout 900   1600 11000 0 timeout 900   11000 6800 0 timeout 900   2600 12000 0 true 5.2 190 40 2 timeout 900   150 10000 0 true 11   230 140 2
reducercommutativity/max40_true-unreach-call.i error (134) .10  24 .66 0 error (42) 880     450   12000    0 out of memory 110     15000   1300    0 timeout 900   2700 8100 0 unknown 48    130 690   0 unknown 8.2 430 100 0 timeout 900   400 8200 0 timeout 900     200 13000    0 unknown .77 40 9.5 0 timeout 900 2900 11000 0 out of memory 120    15000 1600   0 unknown 62   1500 670 0 disqualified 12   200 100 0 timeout (verification) 900    200 13000   0 timeout 900   1400 8400 0 timeout 900   6500 11000 0 timeout 900   2200 11000 0 true 5.3 190 40 2 timeout 900   150 12000 0 true 23   240 260 2
reducercommutativity/max60_true-unreach-call.i error (134) .11  24 .69 0 error (42) 880     580   10000    0 out of memory 110     15000   1500    0 timeout 900   3000 7600 0 unknown 160    220 2200   0 unknown 8.4 430 110 0 timeout 900   400 8300 0 timeout 900     240 13000    0 unknown .80 39 10   0 timeout 900 3400 7900 0 out of memory 160    15000 2400   0 unknown 64   1500 680 0 disqualified 38   340 270 0 timeout (verification) 900    210 12000   0 timeout 900   1100 11000 0 timeout 900   6800 8500 0 timeout 900   2800 11000 0 true 5.5 190 47 2 timeout 900   150 12000 0 true 24   240 280 2
reducercommutativity/max_true-unreach-call_true-termination.i error (134) .086 24 .65 0 error (42) 880     250   10000    0 out of memory 410     15000   5300    0 timeout 960   5400 7300 0 unknown 900    110 12000   0 unknown 8.2 430 100 0 unknown 1.6 200 19 0 timeout 900     120 11000    0 unknown .79 40 9.4 0 timeout 960 4600 6800 0 timeout 900    900 7500   0 unknown 10   310 110 0 disqualified 880   380 11000 0 error(unknown, verification-finished) 810    3300 9700   0 timeout 900   4600 7600 0 timeout 900   3200 7700 0 timeout 900   4700 6500 0 true 7.3 150 79 2 error (1) 880   150 12000 0 true 17   310 210 2
reducercommutativity/sep05_true-unreach-call_true-termination.i error (134) .087 24 .71 0 true .17  9.9 2.3  2 error (42) 880     4800   8000    0 true 290   2500 2800 2 unknown 2.0  68 26   0 unknown 8.4 430 120 0 true 60   390 590 2 true .19  28 2.2  2 unknown .78 39 8.9 0 true 16 1100 120 2 true 1.6  410 21   2 true 12   460 130 2 disqualified 2.1 72 25 0 true .17 17 1.9 2 timeout 900   2200 13000 0 timeout 900   4700 8600 0 timeout 900   1400 9900 0 true 160   1300 1500 2 timeout 900   150 11000 0 true 14   230 170 2
reducercommutativity/sep10_true-unreach-call.i error (134) .087 23 .70 0 true .38  15   5.9  2 out of memory 110     15000   1500    0 exception 80   2500 820 0 unknown 4.3  67 62   0 unknown 8.3 430 110 0 timeout 900   430 6900 0 true .20  28 2.7  2 unknown .80 39 10   0 true 31 1400 350 2 out of memory 40    15000 520   0 true 22   510 240 2 disqualified 3.0 81 39 0 true .21 16 1.8 2 timeout 900   5600 9300 0 timeout 900   4800 8300 0 timeout 900   5400 9200 0 true 170   1500 1600 2 timeout 900   150 11000 0 true 56   250 570 2
reducercommutativity/sep20_true-unreach-call.i error (134) .10  24 .69 0 true 4.9   35   79    2 out of memory 110     15000   1200    0 timeout 910   4800 8900 0 unknown 12    67 160   0 unknown 8.4 430 100 0 timeout 900   400 7100 0 true .24  28 2.3  2 unknown .78 39 9.5 0 true 240 1900 1800 2 out of memory 47    15000 710   0 true 52   760 500 2 disqualified 880   110 12000 0 true .22 17 2.0 2 timeout 900   4200 7800 0 timeout 900   12000 9000 0 timeout 900   4300 9500 0 true 170   1600 1700 2 timeout 900   150 12000 0 true 11   230 140 2
reducercommutativity/sep40_true-unreach-call.i error (134) .10  24 .83 0 true 37     85   460    2 out of memory 110     15000   1400    0 timeout 910   3500 9100 0 unknown 41    87 550   0 unknown 8.3 430 100 0 timeout 900   400 7300 0 true .26  28 3.2  2 unknown .79 39 9.7 0 timeout 900 2800 8200 0 out of memory 68    15000 850   0 unknown 68   1600 860 0 disqualified 880   170 12000 0 true .19 18 1.8 2 timeout 900   1200 10000 0 timeout 900   13000 8300 0 timeout 900   2000 10000 0 true 210   1400 2200 2 timeout 900   150 13000 0 true 11   230 150 2
reducercommutativity/sep60_true-unreach-call.i error (134) .11  24 .69 0 true 170     160   2200    2 out of memory 110     15000   1300    0 timeout 920   4400 11000 0 unknown 98    180 1400   0 unknown 8.2 430 93 0 timeout 900   410 7600 0 true .33  29 4.4  2 unknown .80 40 9.2 0 timeout 900 3600 6600 0 out of memory 100    15000 1300   0 unknown 66   1600 790 0 disqualified 880   270 13000 0 true .18 18 2.0 2 timeout 900   1100 11000 0 timeout 910   13000 9700 0 timeout 900   2200 10000 0 true 300   1400 3600 2 timeout 900   150 13000 0 true 35   240 410 2
reducercommutativity/sep_true-unreach-call_true-termination.i error (134) .11  24 .78 0 error (42) 880     810   7000    0 out of memory 570     15000   8900    0 timeout 940   5000 9600 0 unknown 900    88 12000   0 unknown 8.1 430 110 0 unknown 1.6 200 20 0 timeout 900     120 10000    0 unknown .80 40 9.8 0 timeout 910 3200 8800 0 timeout 900    2900 5100   0 unknown 10   310 94 0 disqualified 880   180 11000 0 error(unknown, verification-finished) 800    3100 9200   0 timeout 900   2100 11000 0 timeout 900   830 12000 0 timeout 900   1500 10000 0 timeout 900   15000 9200 0 error (1) 3.5 150 32 0 true 17   280 200 2
reducercommutativity/sum05_true-unreach-call_true-termination.i error (134) .088 24 .80 0 true 34     21   430    2 true 45     23   700    2 timeout 900   1600 12000 0 unknown 2.0  66 24   0 unknown 8.2 430 100 0 true 8.4 370 110 2 true .17  27 2.0  2 unknown .77 39 9.7 0 timeout 900 2200 10000 0 true .36 58 3.6 2 true 17   620 210 2 disqualified 2.1 73 23 0 true .17 17 1.9 2 timeout 900   4700 6900 0 true 700   800 10000 2 timeout 900   4100 6600 0 true 4.7 190 39 2 timeout 900   150 12000 0 true 24   240 300 2
reducercommutativity/sum10_true-unreach-call_true-termination.i error (134) .081 24 .83 0 error (42) 880     250   11000    0 error (42) 870     250   12000    0 timeout 900   3600 6600 0 unknown 4.0  67 51   0 unknown 8.3 430 130 0 true 8.5 370 97 2 true .17  27 2.3  2 unknown .78 39 9.1 0 timeout 900 4300 6400 0 true .41 58 4.4 2 true 17   390 190 2 disqualified 2.1 76 26 0 true .19 17 1.6 2 timeout 900   1200 11000 0 timeout 900   4900 6800 0 timeout 900   1200 13000 0 true 4.7 190 34 2 timeout 900   160 11000 0 true 40   250 380 2
reducercommutativity/sum20_true-unreach-call.i error (134) .088 23 .73 0 error (42) 870     410   13000    0 error (42) 880     430   11000    0 timeout 900   4700 6800 0 unknown 10    69 130   0 unknown 8.1 430 96 0 true 8.6 370 98 2 true .19  27 2.9  2 unknown .78 39 11