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 PeSCo 1.7-svn b8d6131600+ 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
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:44:04 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
Run set 2ls.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized] cbmc.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized] cbmc-path.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized] cpa-seq.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized] depthk.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized] divine-explicit.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized] divine-smt.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized] esbmc-kind.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized] pesco.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized] smack.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized] symbiotic.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized] uautomizer.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized] ukojak.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized] utaipan.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized] veriabs.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized] verifuzz.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized]
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 -w error-witness.graphml --witness witness.graphml --full-output --full-output --full-output
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J)
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i error (134) .084 24 .76 out of memory 200     14000   1800    error (42) 880     1600   12000    timeout 960   6200 7100 unknown 900    1600 13000   unknown 8.0  430 98   unknown 7.9  430 85   true .11  26 .94 unknown 100 2800 1000 disqualified 4.1  120 45   false(unreach-call) 1.3   110 17    timeout 900   1700 11000 timeout 900   5400 11000 timeout 900   1900 12000 out of memory 66   15000 830 false(unreach-call) 5.0 1300 52
array-examples/sorting_bubblesort_false-unreach-call2_ground.i error (134) .088 24 .88 out of memory 25     15000   360    error (42) 880     14000   12000    timeout 960   4200 8300 unknown 900    770 11000   unknown 8.2  430 99   unknown 8.1  430 99   timeout 900     2800 11000    timeout 960 4500 7000 disqualified 3.6  91 43   probably out of memory (killed (signal 9, verification)) 290     15000 4000    timeout 900   1600 12000 timeout 900   6200 9600 timeout 900   1300 13000 out of memory 430   15000 4900 error (1) 64   1200 970
array-examples/sorting_bubblesort_false-unreach-call_ground.i error (134) .084 24 .74 out of memory 25     15000   270    error (42) 880     14000   12000    timeout 960   4400 6600 unknown 900    770 10000   unknown 8.1  430 93   unknown 8.1  430 120   timeout 900     2800 11000    timeout 960 4700 7200 disqualified 3.6  90 44   probably out of memory (killed (signal 9, verification)) 290     15000 4000    timeout 900   1500 12000 timeout 900   5000 9600 timeout 900   1200 11000 out of memory 440   15000 6100 error (1) 64   1200 910
array-examples/sorting_selectionsort_false-unreach-call2_ground.i error (134) .078 24 .77 out of memory 72     12000   890    error (42) 870     990   12000    timeout 960   4500 10000 unknown 900    1300 9600   unknown 8.2  430 120   unknown 8.2  430 98   timeout 900     9100 9400    timeout 960 6700 8600 disqualified 880    500 10000   probably out of memory (killed (signal 9, verification)) 350     15000 5200    timeout 900   1300 11000 timeout 900   3800 8600 timeout 900   1400 13000 out of memory 90   15000 1100 false(unreach-call) 25   3500 280
array-examples/sorting_selectionsort_false-unreach-call_ground.i error (134) .089 24 .66 out of memory 71     12000   800    error (42) 870     2500   12000    timeout 960   4200 9500 unknown 900    1600 9800   unknown 8.2  430 98   unknown 8.3  430 100   timeout 900     8900 9900    timeout 960 8300 9700 disqualified 350    830 3800   probably out of memory (killed (signal 9, verification)) 350     15000 5200    timeout 900   2000 12000 timeout 900   4900 8300 timeout 900   1400 12000 out of memory 87   15000 1100 false(unreach-call) 10   2900 110
array-examples/standard_allDiff2_false-unreach-call_ground.i error (134) .080 24 1.0  out of memory 490     10000   4200    out of memory 150     15000   1700    timeout 960   4300 7600 unknown 900    1500 10000   unknown 8.2  430 97   unknown 8.2  430 99   timeout 900     3300 7000    timeout 920 12000 10000 disqualified 17    130 220   false(unreach-call) .17  16 1.8  timeout 900   5400 9200 timeout 900   1200 6500 timeout 900   5300 9400 out of memory 180   15000 2300 error (1) 54   620 630
array-examples/standard_copy1_false-unreach-call_ground.i error (134) .090 24 .89 out of memory 86     15000   1100    error (42) 880     2900   13000    timeout 960   3400 9600 unknown 160    60 2100   timeout 900    1000 11000   timeout 900    2500 9600   timeout 900     11000 9500    timeout 970 5600 8900 disqualified 3.6  91 43   false(unreach-call) 6.6   410 87    timeout 900   830 9000 timeout 900   5100 9000 timeout 900   1000 11000 false(unreach-call) 4.6 190 33 false(unreach-call) 4.8 1400 50
array-examples/standard_copy2_false-unreach-call_ground.i error (134) .077 24 .86 out of memory 97     15000   1300    error (42) 880     3800   9700    timeout 960   3900 9500 unknown 170    65 2100   timeout 900    740 9200   timeout 900    2500 8000   timeout 900     11000 9100    timeout 960 6000 8000 disqualified 3.7  120 45   false(unreach-call) 8.7   520 120    timeout 900   760 8500 timeout 900   5100 9300 timeout 900   940 9700 false(unreach-call) 4.7 190 36 false(unreach-call) 5.3 2100 60
array-examples/standard_copy3_false-unreach-call_ground.i error (134) .087 24 .86 out of memory 110     15000   1600    error (42) 880     4900   11000    timeout 960   5000 11000 unknown 210    75 2900   timeout 900    550 7900   timeout 900    2500 9300   timeout 900     11000 8900    timeout 960 5800 8200 disqualified 3.7  95 48   false(unreach-call) 9.7   590 140    timeout 900   910 13000 timeout 900   5200 8600 timeout 900   810 10000 false(unreach-call) 4.7 190 36 false(unreach-call) 5.7 2700 77
array-examples/standard_copy4_false-unreach-call_ground.i error (134) .090 24 .88 out of memory 120     15000   1600    error (42) 880     5800   11000    timeout 960   3000 11000 unknown 230    82 3100   timeout 900    570 8500   timeout 900    2500 9000   timeout 900     11000 9200    timeout 900 8800 12000 disqualified 3.9  120 51   false(unreach-call) 11     650 150    timeout 900   920 9700 timeout 900   5000 8200 timeout 900   1000 10000 false(unreach-call) 4.6 190 34 false(unreach-call) 6.3 3300 79
array-examples/standard_copy5_false-unreach-call_ground.i error (134) .083 24 .70 out of memory 94     15000   1400    error (42) 880     6800   12000    timeout 970   4800 10000 unknown 250    84 3400   timeout 900    590 8700   timeout 900    2500 8300   timeout 900     11000 9900    timeout 960 5300 8800 disqualified 3.9  110 49   false(unreach-call) 12     730 170    timeout 900   920 9000 timeout 900   5300 7800 timeout 900   950 11000 false(unreach-call) 4.8 190 35 false(unreach-call) 6.9 4000 77
array-examples/standard_copy6_false-unreach-call_ground.i error (134) .091 24 .66 out of memory 100     15000   1500    error (42) 880     7800   12000    timeout 970   4700 8700 unknown 280    90 3200   timeout 900    610 8900   timeout 900    2500 8600   timeout 900     11000 10000    timeout 960 5700 8800 disqualified 4.2  100 48   false(unreach-call) 13     820 150    timeout 900   950 12000 timeout 900   4900 8400 timeout 900   1800 12000 false(unreach-call) 4.8 190 41 false(unreach-call) 7.5 4600 89
array-examples/standard_copy7_false-unreach-call_ground.i error (134) .085 24 .77 out of memory 110     15000   1600    error (42) 880     8700   12000    timeout 960   4500 9800 unknown 280    130 3900   timeout 900    620 8500   timeout 900    2500 8900   timeout 900     11000 9900    timeout 960 6900 8800 disqualified 4.1  130 48   false(unreach-call) 13     910 180    timeout 900   890 11000 timeout 900   5000 8300 timeout 900   980 12000 false(unreach-call) 4.8 190 38 false(unreach-call) 8.0 5300 100
array-examples/standard_copy8_false-unreach-call_ground.i error (134) .087 24 .74 out of memory 120     15000   1600    error (42) 880     9600   12000    timeout 960   3900 9100 unknown 310    140 4000   timeout 900    640 9800   timeout 900    2500 8400   timeout 900     11000 10000    timeout 960 4500 11000 disqualified 4.3  120 49   false(unreach-call) 15     1000 190    timeout 900   970 13000 timeout 900   5000 8000 timeout 900   1100 10000 false(unreach-call) 4.9 200 40 false(unreach-call) 8.4 5900 94
array-examples/standard_copy9_false-unreach-call_ground.i error (134) .084 24 .88 out of memory 97     15000   1300    error (42) 880     11000   9700    timeout 960   4400 9500 unknown 330    110 4500   timeout 900    660 9100   timeout 900    2500 8300   timeout 900     10000 11000    timeout 960 5200 8800 disqualified 4.4  120 66   false(unreach-call) 16     1100 210    timeout 900   930 11000 timeout 900   5300 9200 timeout 900   1400 8300 false(unreach-call) 5.1 200 39 false(unreach-call) 9.1 6500 110
array-examples/standard_copyInitSum2_false-unreach-call_ground.i error (134) .081 23 .75 out of memory 64     15000   800    error (42) 880     2900   12000    timeout 960   3300 9300 unknown 120    59 1600   out of memory (unknown error) 170    15000 1600   out of memory (unknown error) 170    15000 1500   timeout 900     6800 11000    timeout 960 3900 7500 disqualified 3.3  85 43   false(unreach-call) 2.1   250 31    timeout 900   1300 10000 timeout 900   5300 7700 timeout 900   940 12000 false(unreach-call) 16   200 100 false(unreach-call) 4.5 1400 47
array-examples/standard_init1_false-unreach-call_ground.i error (134) .081 24 .74 out of memory 100     15000   1600    error (42) 880     1400   15000    timeout 960   3500 11000 unknown 87    51 1100   out of memory (unknown error) 170    15000 1500   out of memory (unknown error) 170    15000 1700   timeout 900     6500 8500    timeout 960 6800 8400 disqualified 3.1  78 39   false(unreach-call) .77  100 11    timeout 900   920 13000 timeout 900   4600 8000 timeout 900   810 11000 false(unreach-call) 15   200 100 false(unreach-call) 15   1200 180
array-examples/standard_init2_false-unreach-call_ground.i error (134) .088 24 .70 out of memory 52     15000   800    error (42) 880     2000   15000    timeout 960   2700 9200 unknown 110    59 1400   out of memory (unknown error) 170    15000 1700   out of memory (unknown error) 160    15000 1600   timeout 900     6700 11000    timeout 960 6600 8200 disqualified 3.1  82 38   false(unreach-call) 1.4   190 24    timeout 900   880 9800 timeout 900   5800 8800 timeout 900   770 10000 false(unreach-call) 15   200 110 false(unreach-call) 15   1300 220
array-examples/standard_init3_false-unreach-call_ground.i error (134) .080 24 .90 out of memory 57     15000   780    error (42) 880     2600   14000    timeout 970   3700 10000 unknown 120    61 1500   out of memory (unknown error) 170    15000 1700   out of memory (unknown error) 170    15000 1800   timeout 900     6700 9700    timeout 960 5900 8800 disqualified 3.2  84 38   false(unreach-call) 2.0   280 31    timeout 900   860 12000 timeout 900   5200 9300 timeout 900   910 11000 false(unreach-call) 16   200 110 false(unreach-call) 15   1400 230
array-examples/standard_init4_false-unreach-call_ground.i error (134) .089 24 .91 out of memory 61     15000   900    error (42) 880     3200   12000    timeout 960   3300 12000 unknown 150    81 2400   out of memory (unknown error) 170    15000 1600   out of memory (unknown error) 170    15000 1700   timeout 900     6600 9400    timeout 960 5200 9400 disqualified 3.2  83 38   false(unreach-call) 2.6   370 38    timeout 900   890 13000 timeout 900   5200 8200 timeout 900   840 11000 false(unreach-call) 16   200 120 false(unreach-call) 15   1500 200
array-examples/standard_init5_false-unreach-call_ground.i error (134) .12  24 .58 out of memory 66     15000   920    error (42) 880     3800   11000    timeout 970   4200 9800 unknown 170    76 2100   out of memory (unknown error) 170    15000 1500   out of memory (unknown error) 170    15000 1800   timeout 900     6400 10000    timeout 970 5300 7800 disqualified 3.2  82 39   false(unreach-call) 3.2   460 46    timeout 900   890 10000 timeout 900   5700 8300 timeout 900   750 9600 false(unreach-call) 16   200 110 false(unreach-call) 16   1600 200
array-examples/standard_init6_false-unreach-call_ground.i error (134) .086 24 .70 out of memory 70     15000   1000    error (42) 880     4400   12000    timeout 960   2700 7800 unknown 190    98 2400   out of memory (unknown error) 170    15000 1700   out of memory (unknown error) 160    15000 1800   timeout 900     6600 11000    timeout 960 5000 8800 disqualified 3.2  84 42   false(unreach-call) 3.8   540 51    timeout 900   880 9700 timeout 900   6300 11000 timeout 900   720 9100 false(unreach-call) 17   200 110 false(unreach-call) 16   1700 200
array-examples/standard_init7_false-unreach-call_ground.i error (134) .083 24 .85 out of memory 75     15000   980    error (42) 880     5000   12000    timeout 960   3200 9200 unknown 210    85 2700   out of memory (unknown error) 170    15000 1700   out of memory (unknown error) 170    15000 1600   timeout 900     6500 10000    timeout 960 5200 7900 disqualified 3.3  87 41   false(unreach-call) 4.5   630 66    timeout 900   810 11000 timeout 900   5300 8700 timeout 900   910 10000 false(unreach-call) 17   200 130 false(unreach-call) 17   1700 240
array-examples/standard_init8_false-unreach-call_ground.i error (134) .11  24 .69 out of memory 54     15000   720    error (42) 880     5600   11000    timeout 970   4400 9300 unknown 240    110 3400   out of memory (unknown error) 170    15000 1600   out of memory (unknown error) 170    15000 1800   timeout 900     6700 8800    timeout 970 5100 8600 disqualified 3.3  85 45   false(unreach-call) 5.1   720 70    timeout 900   880 9000 timeout 900   5400 7500 timeout 900   770 9600 false(unreach-call) 17   200 120 false(unreach-call) 17   1800 220
array-examples/standard_init9_false-unreach-call_ground.i error (134) .085 24 .86 out of memory 57     15000   900    error (42) 880     6200   14000    timeout 960   3700 10000 unknown 260    98 3400   out of memory (unknown error) 160    15000 1700   out of memory (unknown error) 170    15000 1800   timeout 900     6700 10000    timeout 970 7000 7800 disqualified 3.4  110 37   false(unreach-call) 5.6   810 90    timeout 900   900 9300 timeout 900   5000 8100 timeout 900   930 11000 false(unreach-call) 17   200 120 false(unreach-call) 17   1900 210
array-examples/standard_minInArray_false-unreach-call_ground.i error (134) .088 24 .72 error (42) 880     1100   4000    error (42) 870     960   12000    timeout 960   4300 9300 unknown 110    64 1300   unknown 8.2  430 95   unknown 8.1  430 130   timeout 900     8500 10000    timeout 960 4800 9000 disqualified 3.2  83 37   false(unreach-call) .99  100 12    timeout 900   1700 11000 timeout 900   5500 11000 timeout 900   1200 12000 false(unreach-call) 4.5 190 39 false(unreach-call) 14   1000 210
array-examples/standard_partition_false-unreach-call_ground.i error (134) .082 24 .76 out of memory 170     14000   2000    error (42) 880     3300   14000    timeout 960   4300 10000 unknown 300    120 3700   unknown 8.6  430 120   timeout 900    1400 7600   timeout 900     4400 11000    timeout 960 4300 7600 disqualified 4.1  93 50   timeout (verification) 900     2800 7700    timeout 900   1300 11000 timeout 900   5200 8800 timeout 900   900 8100 out of memory 58   15000 610 false(unreach-call) 36   2800 540
array-examples/standard_running_false-unreach-call.i error (134) .12  23 .65 out of memory 82     15000   1200    out of memory 300     15000   4500    timeout 970   4600 8500 unknown 260    130 3500   unknown 8.2  430 100   unknown 8.3  430 94   out of memory 390     15000 5300    timeout 960 4800 10000 disqualified 3.0  85 37   false(unreach-call) 1.9   180 29    timeout 900   1300 13000 timeout 900   6700 8800 timeout 900   1100 12000 out of memory 57   15000 680 error (1) 890   2300 12000
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i error (134) .094 24 .67 true 130     4200   1600    true 130     2900   1700    true 93   1300 1100 unknown 900    2700 9000   true 21    430 220   true 21    430 240   true .10  26 1.1  true 11 1200 80 disqualified 3.4  100 51   true .97  95 15    true 9.4 370 83 timeout 900   2100 9800 true 8.7 350 81 true 21   500 190 error (1) 880   1300 11000
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i error (134) .087 24 .70 error (42) 880     9800   12000    error (42) 880     1300   14000    timeout 970   5500 11000 unknown 900    1200 12000   unknown 8.1  430 99   unknown 8.1  430 110   true .14  26 .99 unknown 100 2000 1300 disqualified 880    210 14000   true 1.1   86 16    timeout 900   5500 10000 timeout 900   5300 9400 timeout 900   2000 12000 out of memory 65   15000 740 error (1) 890   1300 12000
array-examples/relax_true-unreach-call.i error (134) .18  26 1.3  out of memory 280     13000   3400    out of memory 200     15000   2500    timeout 970   6800 8400 unknown 900    170 13000   unknown 8.5  450 120   unknown 1.6  200 21   timeout 900     340 13000    timeout 960 5100 10000 disqualified 880    340 9800   timeout (verification) 900     750 11000    timeout 900   730 11000 timeout 900   690 13000 timeout 900   930 12000 out of memory 540   15000 4600 timeout 900   180 13000
array-examples/sanfoundry_02_true-unreach-call_ground.i error (134) .088 23 .68 error (42) 880     2100   4300    error (42) 880     1300   13000    timeout 960   4400 10000 unknown 200    100 2400   unknown 48    430 610   unknown 48    430 690   timeout 900     12000 9700    timeout 960 4100 9000 disqualified 2.7  80 30   true 1.7   95 24    timeout 900   1700 14000 timeout 900   5700 8000 timeout 900   1300 12000 true 11   190 120 error (1) 880   620 12000
array-examples/sanfoundry_10_true-unreach-call_ground.i error (134) .093 24 .68 error (42) 880     13000   11000    error (42) 880     13000   11000    timeout 910   1000 10000 unknown 320    83 4500   unknown 8.2  430 110   unknown 8.4  430 120   true .13  26 1.2  out of memory 840 15000 11000 disqualified 5.7  94 73   true 1.4   68 21    timeout 900   1800 11000 timeout 900   1600 8800 timeout 900   1200 12000 true 16   200 110 error (1) 880   8500 12000
array-examples/sanfoundry_24_true-unreach-call_true-termination.i error (134) .089 24 .69 error (42) 880     2700   10000    error (42) 880     1800   12000    true 14   630 110 unknown .79 67 9.3 unknown 8.3  430 120   unknown 8.6  430 130   true .088 26 1.1  true 18 1400 130 disqualified 880    350 11000   timeout (verification) 900     1200 10000    true 9.5 380 75 true 9.3 370 74 true 8.9 360 67 true 16   190 90 error (1) 880   1100 11000
array-examples/sanfoundry_27_true-unreach-call_ground.i error (134) .081 24 .99 error (42) 880     1100   4300    error (42) 880     980   12000    timeout 960   4200 12000 unknown 93    69 1200   unknown 8.1  430 110   unknown 8.3  430 110   timeout 900     8600 10000    timeout 960 5200 9100 disqualified 3.0  83 41   true 1.1   62 14    timeout 900   1600 14000 timeout 900   4900 9400 timeout 900   1200 11000 true 5.0 190 46 error (1) 890   670 10000
array-examples/sanfoundry_43_true-unreach-call_ground.i error (134) .083 24 .69 out of memory 95     15000   1600    out of memory 84     15000   1100    true 93   1100 1100 unknown .80 66 9.3 out of memory (unknown error) 170    15000 1800   out of memory (unknown error) 170    15000 1800   true .089 26 .86 true 13 1000 93 disqualified 2.0  73 25   true .14  16 1.4  true 7.9 360 59 true 7.5 370 69 true 7.7 370 59 true 4.5 190 40 error (1) 880   1300 11000
array-examples/sorting_bubblesort_true-unreach-call_ground.i error (134) .084 24 .74 out of memory 24     15000   320    error (42) 880     15000   13000    timeout 960   4200 7000 unknown 900    780 9800   unknown 8.4  430 97   unknown 8.1  430 110   timeout 900     2800 10000    timeout 960 4500 7700 disqualified 22    140 310   probably out of memory (killed (signal 9, verification)) 290     15000 3700    timeout 900   1700 9800 timeout 900   5200 8500 timeout 900   1700 11000 out of memory 390   15000 5000 error (1) 54   780 840
array-examples/sorting_selectionsort_true-unreach-call_ground.i error (134) .088 24 .81 out of memory 72     12000   820    error (42) 870     2500   12000    timeout 960   4200 9400 unknown 900    1600 8600   unknown 8.1  430 93   unknown 8.2  430 110   timeout 900     9100 10000    timeout 960 6800 9700 disqualified 880    780 9600   probably out of memory (killed (signal 9, verification)) 350     15000 4900    timeout 900   1300 13000 timeout 900   3500 8800 timeout 900   1300 12000 out of memory 90   15000 1000 error (1) 60   2900 770
array-examples/standard_compareModified_true-unreach-call_ground.i error (134) .079 23 .68 out of memory 120     15000   1500    error (42) 880     1700   12000    timeout 970   4100 7800 unknown 150    72 1800   unknown 8.2  430 100   unknown 8.2  430 110   timeout 900     6700 9800    timeout 900 7300 12000 disqualified 2.5  81 34   true 2.1   100 23    timeout 900   710 10000 timeout 900   5800 10000 timeout 900   850 12000 true 4.7 190 37 error (1) 890   1800 11000
array-examples/standard_compare_true-unreach-call_ground.i error (134) .080 23 .90 error (42) 880     1100   4600    error (42) 880     1300   11000    timeout 970   4500 9700 unknown 65    56 880   unknown 8.0  430 99   unknown 8.1  430 96   timeout 900     9300 9000    timeout 900 1800 11000 disqualified 2.7  84 36   true 1.3   63 17    timeout 900   880 11000 timeout 900   5000 10000 timeout 900   940 11000 true 4.3 190 34 error (1) 880   1800 11000
array-examples/standard_copy1_true-unreach-call_ground.i error (134) .080 24 .97 out of memory 59     15000   880    error (42) 880     2300   12000    timeout 960   4700 13000 unknown 160    59 2100   unknown 890    1500 11000   timeout 900    2300 8500   timeout 900     11000 9700    timeout 960 4900 11000 disqualified 3.2  82 38   true 2.9   230 38    timeout 900   930 10000 timeout 900   5200 8200 timeout 900   1000 9800 true 4.6 180 38 error (1) 890   1300 11000
array-examples/standard_copy2_true-unreach-call_ground.i error (134) .089 24 .73 out of memory 71     15000   990    error (42) 880     3200   14000    timeout 970   4600 9500 unknown 170    66 2400   timeout 900    1000 9200   timeout 900    2300 8500   timeout 900     11000 9700    timeout 960 5300 8800 disqualified 3.3  85 39   true 3.3   250 41    timeout 900   850 9800 timeout 900   5300 8900 timeout 900   820 11000 true 4.8 190 35 error (1) 880   2000 11000
array-examples/standard_copy3_true-unreach-call_ground.i error (134) .077 24 .92 out of memory 82     15000   1200    error (42) 870     4200   13000    timeout 960   4200 10000 unknown 190    84 2500   timeout 900    770 9400   timeout 900    2300 8400   timeout 900     11000 11000    timeout 970 5800 8100 disqualified 3.5  89 47   true 3.9   280 45    timeout 900   740 11000 timeout 900   5200 8100 timeout 900   820 10000 true 4.6 190 36 error (1) 890   2700 11000
array-examples/standard_copy4_true-unreach-call_ground.i error (134) .082 24 .70 out of memory 95     15000   1300    error (42) 880     5300   12000    timeout 960   4100 10000 unknown 210    84 3100   timeout 900    610 9800   timeout 900    2300 7800   timeout 900     12000 12000    timeout 900 7800 14000 disqualified 3.7  93 47   true 4.3   300 55    timeout 900   750 8500 timeout 900   4700 8000 timeout 900   840 10000 true 4.7 190 40 error (1) 890   3300 12000
array-examples/standard_copy5_true-unreach-call_ground.i error (134) .099 24 .65 out of memory 110     15000   1400    error (42) 880     6200   12000    timeout 970   4900 8800 unknown 260    98 3300   timeout 900    630 9000   timeout 900    2300 9100   timeout 900     11000 11000    timeout 960 6000 9900 disqualified 3.8  95 54   true 4.9   330 67    timeout 900   760 10000 timeout 900   5300 10000 timeout 900   990 11000 true 4.9 200 39 error (1) 890   3900 14000
array-examples/standard_copy6_true-unreach-call_ground.i error (134) .079 24 .77 out of memory 87     15000   1200    error (42) 880     7200   12000    timeout 960   3800 11000 unknown 280    99 3500   timeout 900    650 8200   timeout 900    2300 9200   timeout 900     12000 11000    timeout 970 7300 9200 disqualified 4.0  100 50   true 5.3   350 75    timeout 900   920 9900 timeout 900   5200 8600 timeout 900   990 9100 true 4.9 190 36 error (1) 890   4500 13000
array-examples/standard_copy7_true-unreach-call_ground.i error (134) .098 23 .73 out of memory 96     15000   1200    error (42) 880     8100   14000    timeout 960   4700 9200 unknown 300    100 4100   timeout 900    670 9000   timeout 900    2300 8700   timeout 900     12000 10000    timeout 960 6000 9400 disqualified 4.2  100 53   true 5.8   380 79    timeout 900   890 9900 timeout 900   5200 7900 timeout 900   1100 11000 true 4.9 200 36 error (1) 880   5200 12000
array-examples/standard_copy8_true-unreach-call_ground.i error (134) .088 24 .76 out of memory 110     15000   1700    error (42) 880     9100   12000    timeout 960   4300 9100 unknown 350    110 4600   timeout 900    700 10000   timeout 900    2300 8100   timeout 900     12000 9400    timeout 960 7200 9200 disqualified 4.4  100 58   true 6.4   400 94    timeout 900   940 10000 timeout 900   5300 8500 timeout 900   1000 8000 true 5.1 200 43 error (1) 890   5800 11000
array-examples/standard_copy9_true-unreach-call_ground.i error (134) .084 24 .99 out of memory 110     15000   1600    error (42) 880     10000   11000    timeout 970   4300 9500 unknown 360    120 5300   timeout 900    720 9900   timeout 900    2200 7900   timeout 900     11000 10000    timeout 960 6200 10000 disqualified 4.6  110 58   true 7.0   430 95    timeout 900   790 9200 timeout 900   4400 8900 timeout 900   1100 9000 true 5.0 200 39 error (1) 890   6400 9600
array-examples/standard_copyInitSum2_true-unreach-call_ground.i error (134) .098 24 .84 out of memory 64     15000   940    error (42) 880     2900   14000    timeout 960   2700 7000 unknown 130    73 1700   out of memory (unknown error) 170    15000 1600   out of memory (unknown error) 160    15000 1500   timeout 900     6800 11000    timeout 970 5900 8500 disqualified 3.2  87 39   true 1.8   99 26    timeout 900   910 8800 timeout 900   5300 11000 timeout 900   730 9200 true 17   200 120 error (1) 880   1400 10000
array-examples/standard_copyInitSum3_true-unreach-call_ground.i error (134) .11  24 .62 out of memory 68     15000   920    error (42) 880     3500   12000    timeout 960   3400 9700 unknown 170    91 2300   out of memory (unknown error) 160    15000 1600   out of memory (unknown error) 170    15000 1600   timeout 900     6800 10000    timeout 960 4400 8600 disqualified 3.9  92 50   true 2.2   120 31    timeout 900   960 13000 timeout 900   6100 9400 timeout 900   930 9000 true 4.6 190 38 error (1) 880   1500 13000
array-examples/standard_copyInitSum_true-unreach-call_ground.i error (134) .088 24 .73 out of memory 64     15000   820    error (42) 880     2900   10000    timeout 960   3900 9900 unknown 130    70 1700   out of memory (unknown error) 170    15000 1600   out of memory (unknown error) 170    15000 1500   timeout 900     6700 8500    timeout 970 3800 8400 disqualified 3.0  83 35   true 1.8   140 26    timeout 900   920 11000 timeout 900   5100 9400 timeout 900   780 11000 true 32   200 330 error (1) 880   1400 9400
array-examples/standard_copyInit_true-unreach-call_ground.i error (134) .082 24 .76 out of memory 59     15000   870    error (42) 880     2300   11000    timeout 960   2600 8900 unknown 100    54 1400   out of memory (unknown error) 170    15000 1700   out of memory (unknown error) 170    15000 1500   timeout 900     6500 9600    timeout 970 7700 7700 disqualified 2.8  84 33   true 1.3   81 20    timeout 900   740 9900 timeout 900   5100 7500 timeout 900   760 9800 true 16   200 110 error (1) 890   1400 11000
array-examples/standard_find_true-unreach-call_ground.i error (134) .087 24 .69 out of memory 100     15000   1400    error (42) 880     1400   12000    timeout 970   4600 11000 unknown 230    110 3800   unknown 360    950 4000   timeout 900    2300 8000   timeout 900     11000 11000    timeout 900 7400 13000 disqualified 3.5  89 41   error(unknown, verification-finished) 350     2400 4800    timeout 900   930 9500 timeout 900   5000 9700 timeout 900   1300 13000 true 17   200 110 error (1) 890   750 12000
array-examples/standard_init1_true-unreach-call_ground.i error (134) .090 24 .71 out of memory 100     15000   1400    error (42) 870     1400   11000    timeout 960   2800 8300 unknown 87    51 1100   out of memory (unknown error) 170    15000 1600   out of memory (unknown error) 170    15000 1600   timeout 900     6600 11000    timeout 960 6700 8400 disqualified 2.6  79 37   true .92  63 14    timeout 900   910 10000 timeout 900   5200 6700 timeout 900   930 11000 true 16   200 100 error (1) 890   750 11000
array-examples/standard_init2_true-unreach-call_ground.i error (134) .086 24 .91 out of memory 52     15000   630    error (42) 870     2000   12000    timeout 960   2800 8900 unknown 110    60 1700   out of memory (unknown error) 170    15000 1900   out of memory (unknown error) 160    15000 1600   timeout 900     6600 13000    timeout 970 7700 8400 disqualified 2.7  77 29   true 1.2   79 17    timeout 900   730 9600 timeout 900   5200 8100 timeout 900   960 13000 true 15   200 130 error (1) 890   800 12000
array-examples/standard_init3_true-unreach-call_ground.i error (134) .081 24 .67 out of memory 57     15000   920    error (42) 880     2600   13000    timeout 960   3300 8600 unknown 120    60 1400   out of memory (unknown error) 170    15000 1600   out of memory (unknown error) 170    15000 1500   timeout 900     6400 9500    timeout 960 7500 8200 disqualified 2.7  80 40   true 1.5   96 20    timeout 900   760 13000 timeout 900   5200 10000 timeout 900   710 12000 true 17   200 110 error (1) 880   830 10000
array-examples/standard_init4_true-unreach-call_ground.i error (134) .085 24 .70 out of memory 61     15000   850    error (42) 880     3200   14000    timeout 970   4500 10000 unknown 150    81 2100   out of memory (unknown error) 170    15000 1700   out of memory (unknown error) 170    15000 1500   timeout 900     6500 12000    timeout 960 5500 8500 disqualified 2.9  84 36   true 1.8   110 25    timeout 900   880 9700 timeout 900   4500 8200 timeout 900   700 11000 true 16   200 120 error (1) 880   890 12000
array-examples/standard_init5_true-unreach-call_ground.i error (134) .11  24 .61 out of memory 66     15000   960    error (42) 880     3800   11000    timeout 970   4200 11000 unknown 170    77 2300   out of memory (unknown error) 170    15000 1700   out of memory (unknown error) 160    15000 1600   timeout 900     6600 10000    timeout 960 4900 8000 disqualified 2.9  85 39   true 2.0   130 28    timeout 900   730 9100 timeout 900   6200 8400 timeout 900   870 11000 true 16   200 110 error (1) 890   950 13000
array-examples/standard_init6_true-unreach-call_ground.i error (134) .085 23 1.2  out of memory 70     15000   950    error (42) 880     4400   12000    timeout 960   3100 9200 unknown 190    98 2900   out of memory (unknown error) 170    15000 1700   out of memory (unknown error) 160    15000 1500   timeout 900     6400 10000    timeout 960 5200 7800 disqualified 3.0  88 37   true 2.3   140 33    timeout 900   840 9000 timeout 900   5100 7700 timeout 900   870 8800 true 16   200 110 error (1) 880   1000 10000
array-examples/standard_init7_true-unreach-call_ground.i error (134) .082 24 .68 out of memory 75     15000   1100    error (42) 880     5000   11000    timeout 970   4400 10000 unknown 210    85 2500   out of memory (unknown error) 160    15000 1700   out of memory (unknown error) 160    15000 1600   timeout 900     6500 11000    timeout 970 7300 9400 disqualified 3.0  86 42   true 2.5   160 38    timeout 900   820 8500 timeout 900   5000 8000 timeout 900   870 9100 true 17   200 110 error (1) 880   1100 9900
array-examples/standard_init8_true-unreach-call_ground.i error (134) .13  24 .72 out of memory 54     15000   790    error (42) 880     5600   13000    timeout 960   2700 7800 unknown 240    110 3100   out of memory (unknown error) 170    15000 1600   out of memory (unknown error) 160    15000 1700   timeout 900     6600 11000    timeout 970 6900 9200 disqualified 3.1  91 38   true 2.8   180 39    timeout 900   880 8300 timeout 900   5300 8500 timeout 900   770 8100 true 17   200 130 error (1) 890   1100 10000
array-examples/standard_init9_true-unreach-call_ground.i error (134) .084 24 .82 out of memory 57     15000   860    error (42) 880     6200   11000    timeout 960   3400 9400 unknown 260    98 3100   out of memory (unknown error) 170    15000 1600   out of memory (unknown error) 170    15000 1600   timeout 900     6500 9400    timeout 960 7100 8400 disqualified 3.2  91 38   true 3.0   190 45    timeout 900   770 8700 timeout 900   3700 9400 timeout 900   920 10000 true 17   200 130 error (1) 880   1200 11000
array-examples/standard_maxInArray_true-unreach-call_ground.i error (134) .090 24 .62 error (42) 880     1100   4800    error (42) 880     980   14000    timeout 970   5000 7600 unknown 93    70 1200   unknown 8.4  430 97   unknown 8.0  430 120   timeout 900     8600 10000    timeout 960 4700 7200 disqualified 3.0  83 36   true 1.0   64 13    timeout 900   1800 13000 timeout 900   6400 8600 timeout 900   1300 12000 true 5.2 190 43 error (1) 880   650 13000
array-examples/standard_minInArray_true-unreach-call_ground.i error (134) .078 23 .89 error (42) 880     1100   4700    error (42) 880     980   12000    timeout 960   4500 8000 unknown 120    66 1400   unknown 8.3  430 95   unknown 8.2  430 97   timeout 900     8700 10000    timeout 970 6100 9900 disqualified 3.0  83 37   true 1.1   64 14    timeout 900   1700 11000 timeout 900   6100 8100 timeout 900   1200 12000 true 5.5 190 47 error (1) 880   650 11000
array-examples/standard_palindrome_true-unreach-call_ground.i error (134) .080 24 .85 out of memory 150     13000   1900    error (42) 880     3700   12000    timeout 960   4200 9200 unknown 140    57 2200   unknown 180    680 2300   unknown 180    680 2000   timeout 900     12000 10000    timeout 970 7400 10000 disqualified 2.5  77 28   true .68  39 9.0  timeout 900   890 11000 timeout 900   4800 8300 timeout 900   910 10000 true 20   190 160 error (1) 880   750 11000
array-examples/standard_partial_init_true-unreach-call_ground.i error (134) .082 24 .91 error (42) 880     7000   13000    error (42) 880     1700   14000    timeout 970   4500 12000 unknown 300    110 3800   unknown 8.1  430 96   unknown 8.2  430 100   timeout 900     4200 11000    timeout 960 4800 7600 disqualified 140    110 1900   true 2.0   120 29    timeout 900   940 11000 timeout 900   5300 7300 timeout 900   1000 10000 true 16   200 120 error (1) 890   1900 10000
array-examples/standard_partition_original_true-unreach-call_ground.i error (134) .081 24 .86 out of memory 140     14000   1700    error (42) 870     2000   13000    timeout 970   4100 11000 unknown 300    86 4500   unknown 8.3  430 110   unknown 8.2  430 120   out of memory 430     15000 5600    timeout 960 5400 9100 disqualified 68    100 910   true 1.3   84 21    timeout 900   930 11000 timeout 900   5300 8600 timeout 900   1000 11000 true 17   200 100 error (1) 890   2100 13000
array-examples/standard_partition_true-unreach-call_ground.i error (134) .089 24 .81 out of memory 160     14000   1900    error (42) 880     3000   12000    timeout 960   4400 12000 unknown 150    71 1800   unknown 8.1  430 93   unknown 8.2  430 90   timeout 900     4200 12000    timeout 960 4000 9200 disqualified 24    93 340   true .58  47 9.0  timeout 900   1300 11000 timeout 900   5400 7900 timeout 900   1000 12000 true 16   200 120 error (1) 890   2800 11000
array-examples/standard_password_true-unreach-call_ground.i error (134) .091 24 .71 error (42) 880     1100   4000    error (42) 880     1300   13000    timeout 960   4600 9600 unknown 65    56 760   unknown 8.2  430 100   unknown 8.1  430 96   timeout 900     9100 10000    timeout 900 2300 12000 disqualified 2.7  85 32   true 1.3   63 18    timeout 900   910 12000 timeout 900   4900 8400 timeout 900   930 10000 true 4.6 190 36 error (1) 880   1200 12000
array-examples/standard_reverse_true-unreach-call_ground.i error (134) .077 23 .80 out of memory 150     13000   2000    error (42) 880     4100   12000    timeout 970   4800 8000 unknown 140    84 1800   unknown 450    950 5500   unknown 450    950 5500   timeout 900     10000 12000    unknown 100 1500 1300 disqualified 2.7  82 36   true 1.2   64 17    timeout 900   920 12000 timeout 900   4600 7900 timeout 900   1000 12000 true 17   200 120 error (1) 880   1300 13000
array-examples/standard_running_true-unreach-call.i error (134) .088 23 .68 out of memory 82     15000   1200    out of memory 310     15000   4100    timeout 960   4600 8100 unknown 900    1700 10000   unknown 8.1  430 120   unknown 8.1  430 100   out of memory 390     15000 4600    timeout 970 3900 8200 disqualified 2.7  80 34   true 1.1   45 16    timeout 900   1600 13000 timeout 900   5300 8700 timeout 900   1400 13000 true 16   200 100 error (1) 880   2000 12000
array-examples/standard_sentinel_true-unreach-call_true-termination.i error (134) .12  24 .65 error (42) 880     2500   12000    error (42) 880     2600   11000    timeout 960   4100 11000 unknown 55    44 810   unknown 48    430 660   true 8.8  370 110   timeout 900     330 12000    true 15 1200 98 disqualified 2.7  75 28   timeout (verification) 900     2600 4100    true 13   500 110 true 15   640 120 true 14   570 130 true 29   510 220 error (1) 860   5200 11000
array-examples/standard_seq_init_true-unreach-call_ground.i error (134) .081 23 .78 out of memory 150     13000   2200    error (42) 880     3800   12000    timeout 960   2500 8500 unknown 120    56 1600   out of memory (unknown error) 170    15000 1700   out of memory (unknown error) 170    15000 1700   timeout 900     7600 13000    timeout 900 7600 11000 disqualified 2.8  82 36   true 1.1   64 18    timeout 900   670 13000 timeout 900   5100 7800 timeout 900   980 13000 true 4.5 190 38 error (1) 880   800 11000
array-examples/standard_strcmp_true-unreach-call_ground.i error (134) .080 23 .80 error (42) 880     2600   6400    error (42) 880     1200   12000    timeout 960   4400 8600 unknown 56    55 800   unknown 89    430 1400   unknown 88    430 1200   timeout 900     8400 10000    timeout 970 7000 8400 disqualified 2.7  82 37   true 1.3   79 22    timeout 900   1100 11000 timeout 900   5600 8500 timeout 900   4300 5400 true 4.4 200 38 error (1) 880   1800 11000
array-examples/standard_strcpy_original_true-unreach-call.i error (134) .084 24 .69 out of memory 64     15000   800    error (42) 880     2100   14000    timeout 970   4300 8600 unknown 120    63 1600   unknown 450    950 5300   timeout 900    2200 8500   timeout 900     12000 9700    timeout 960 6900 7500 disqualified 7.6  100 100   error(unknown, verification-finished) 170     2300 2300    timeout 900   760 11000 timeout 900   3700 11000 timeout 900   910 12000 true 16   200 120 error (1) 890   2000 12000
array-examples/standard_strcpy_true-unreach-call_ground.i error (134) .085 24 .75 out of memory 64     15000   950    error (42) 880     2200   12000    timeout 960   4100 9500 unknown 190    140 2600   unknown 450    950 4900   timeout 900    2300 8100   timeout 900     12000 11000    timeout 970 6400 9200 disqualified 5.7  98 76   error(unknown, verification-finished) 160     2400 1900    timeout 900   900 11000 timeout 900   4000 11000 timeout 900   1000 11000 true 16   200 100 error (1) 890   1400 13000
array-examples/standard_two_index_01_true-unreach-call.i out of memory 300     15000 2000    out of memory 71     15000   930    error (42) 870     840   13000    timeout 970   9200 6100 unknown 120    59 1800   unknown 23    520 270   timeout 900    1300 7900   timeout 900     12000 11000    timeout 960 9900 10000 disqualified 880    870 9100   true .40  34 5.2  timeout 900   910 9600 timeout 900   5300 8200 timeout 900   940 12000 true 16   200 110 error (1) 880   220 11000
array-examples/standard_two_index_02_true-unreach-call.i error (134) .084 24 .67 out of memory 160     13000   2100    error (42) 880     4300   13000    timeout 970   4100 12000 unknown 180    66 2800   unknown 670    1200 8000   timeout 900    2300 7800   timeout 900     11000 11000    timeout 960 5800 9100 disqualified 2.7  81 34   true 2.4   190 29    timeout 900   860 10000 timeout 900   4300 7900 timeout 900   990 10000 true 17   200 110 error (1) 890   2000 11000
array-examples/standard_two_index_03_true-unreach-call.i out of memory 250     15000 2200    out of memory 97     13000   1500    error (42) 880     960   12000    timeout 960   9900 8900 unknown 140    63 2200   unknown 18    490 200   timeout 900    1300 7800   timeout 900     12000 9100    timeout 960 7600 8200 disqualified 900    4400 13000   true .33  31 4.9  timeout 900   730 11000 timeout 900   5300 7900 timeout 900   890 11000 true 17   200 110 error (1) 880   220 11000
array-examples/standard_two_index_04_true-unreach-call.i error (134) .087 24 .66 out of memory 150     13000   2600    error (42) 880     4600   12000    timeout 970   4600 8700 unknown 160    64 2500   unknown 560    1100 6400   timeout 900    2300 8600   timeout 900     11000 9900    timeout 960 6500 9800 disqualified 2.6  82 37   true 2.1   180 24    timeout 900   740 12000 timeout 900   5100 9600 timeout 900   1100 10000 true 16   200 110 error (1) 890   2000 12000
array-examples/standard_two_index_05_true-unreach-call.i error (134) .081 24 .80 out of memory 160     13000   2100    error (42) 880     4700   12000    timeout 960   2800 9500 unknown 150    68 2200   unknown 540    1100 6300   timeout 900    2300 8400   timeout 900     12000 12000    timeout 960 7700 9400 disqualified 2.5  81 37   true 1.9   180 27    timeout 900   750 8600 timeout 900   3800 7700 timeout 900   1100 11000 true 16   200 110 error (1) 890   2000 12000
array-examples/standard_two_index_06_true-unreach-call.i out of memory 230     15000 1600    out of memory 97     13000   1500    error (42) 880     970   13000    timeout 960   9700 10000 unknown 160    65 1900   unknown 17    480 210   timeout 900    1300 8300   timeout 900     12000 9800    timeout 970 8000 9200 disqualified 890    1100 11000   true .32  29 3.5  timeout 900   730 12000 timeout 900   5200 10000 timeout 900   980 11000 true 16   200 120 error (1) 880   220 11000
array-examples/standard_two_index_07_true-unreach-call.i error (134) .082 23 .84 out of memory 160     13000   2000    error (42) 880     4300   12000    timeout 970   3900 7200 unknown 160    71 1900   unknown 510    1000 5600   timeout 900    2300 9200   timeout 900     12000 9900    timeout 960 5400 8400 disqualified 2.5  81 39   true 1.9   180 24    timeout 900   910 9000 timeout 900   5100 7600 timeout 900   1100 13000 true 16   200 110 error (1) 890   2000 11000
array-examples/standard_two_index_08_true-unreach-call.i error (134) .087 24 1.0  out of memory 160     13000   2100    error (42) 880     4300   11000    timeout 970   4000 10000 unknown 160    67 2000   unknown 500    1000 6200   timeout 900    2300 8200   timeout 900     12000 10000    timeout 960 4900 8500 disqualified 2.5  81 32   true 1.9   180 25    timeout 900   930 9800 timeout 900   5200 8400 timeout 900   1100 12000 true 17   200 110 error (1) 890   2000 11000
array-examples/standard_two_index_09_true-unreach-call.i error (134) .11  24 .73 out of memory 160     13000   2500    error (42) 880     4700   11000    timeout 970   3600 9000 unknown 170    70 2200   unknown 500    1000 5500   timeout 900    2300 8100   timeout 900     12000 9800    timeout 970 7900 8700 disqualified 2.4  74 29   true 1.9   180 23    timeout 900   920 9700 timeout 900   5200 8000 timeout 900   1100 12000 true 17   200 130 error (1) 890   2000 13000
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i error (134) .081 24 .77 error (42) 880     1800   8800    error (42) 880     790   11000    timeout 960   6100 7400 unknown 60    51 920   unknown 8.2  430 93   unknown 8.1  430 100   timeout 900     1000 11000    timeout 940 5900 7100 disqualified 880    380 11000   true .14  15 1.5  timeout 900   1200 11000 timeout 900   970 7300 timeout 900   960 13000 true 15   200 110 error (1) 880   620 12000
array-examples/standard_vector_difference_true-unreach-call_ground.i error (134) .086 24 .69 out of memory 120     15000   1700    error (42) 880     2000   11000    timeout 960   4100 11000 unknown 130    73 1700   unknown 540    950 6200   unknown 540    950 7300   timeout 900     5400 13000    timeout 960 6100 7700 disqualified 2.9  86 39   true 1.5   67 20    timeout 900   680 12000 timeout 900   3400 7900 timeout 900   750 11000 true 4.5 190 41 error (1) 890   1800 12000
array-examples/standard_sentinel_true-unreach-call.i.v+cfa-reducer.c error (134) .094 24 .74 error (42) 880     2500   13000    error (42) 880     2700   11000    timeout 960   4300 10000 unknown 55    44 700   unknown 48    430 670   true 9.2  370 130   timeout 900     330 12000    timeout 960 5100 12000 disqualified 2.7  75 33   timeout (verification) 900     2600 4200    true 15   650 140 true 17   650 130 true 15   660 120 timeout 900   3400 11000 error (1) 870   3900 13000
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i error (134) .10  24 .84 out of memory 52     15000   630    error (42) 870     1800   12000    timeout 970   4000 9700 unknown 1.2  67 13   out of memory (unknown error) 170    15000 1600   out of memory (unknown error) 160    15000 1500   timeout 900     7400 9900    timeout 960 5400 8900 disqualified 3.1  82 38   false(unreach-call) .79  110 12    timeout 900   1000 10000 timeout 900   5000 8600 timeout 900   1100 9400 out of memory 480   15000 5300 false(unreach-call) 4.2 820 47
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i out of memory 35     15000 510    out of memory 290     15000   3100    out of memory 23     8000   230    timeout 960   3700 7700 unknown 1.2  67 15   out of memory (unknown error) 170    15000 1800   out of memory (unknown error) 170    15000 1600   timeout 900     6400 10000    timeout 960 6900 7100 disqualified 3.2  82 38   false(unreach-call) .78  110 9.8  timeout 900   1500 10000 timeout 900   5100 7800 timeout 900   4900 9200 out of memory 600   15000 6100 false(unreach-call) 5.6 490 49
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i error (134) .086 24 .83 out of memory 68     15000   980    out of memory 190     15000   3100    timeout 970   4700 12000 unknown 230    66 3100   unknown 8.2  430 97   timeout 900    12000 7000   timeout 900     4900 11000    timeout 900 6500 12000 disqualified 4.4  110 53   false(unreach-call) 1.7   200 22    timeout 900   1100 9300 timeout 900   5100 9500 timeout 900   1200 10000 false(unreach-call) 16   200 110 false(unreach-call) 5.6 2400 67
array-industry-pattern/array_range_init_false-unreach-call.i true 42     15000 480    out of memory 380     15000   4900    out of memory 280     15000   3700    timeout 960   3800 10000 unknown 210    55 2900   false(unreach-call) 400    3700 4300   false(unreach-call) 400    3700 4600   timeout 900     5200 10000    timeout 960 6200 7900 disqualified 3.1  85 38   false(unreach-call) 1.0   120 14    timeout 900   1200 8800 timeout 900   5300 7100 timeout 900   4100 9100 false(unreach-call) 15   200 120 false(unreach-call) 3.8 150 43
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i error (134) .090 24 .82 out of memory 68     15000   880    out of memory 190     15000   2900    timeout 970   4000 9500 unknown 180    81 2500   unknown 8.2  430 98   timeout 900    13000 7100   timeout 900     4900 10000    timeout 900 6800 11000 disqualified 4.5  120 58   timeout (verification) 900     2600 10000    timeout 900   1100 11000 timeout 900   5000 7500 timeout 900   1200 8900 false(unreach-call) 17   200 120 error (1) 890   2400 13000
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i error (134) .087 24 .76 out of memory 66     14000   880    error (42) 880     1800   13000    timeout 970   5700 9100 unknown 900    1300 11000   unknown 8.1  430 120   unknown 8.2  430 91   timeout 900     3400 10000    timeout 910 7900 12000 disqualified 5.9  110 76   false(unreach-call) 1.7   320 23    timeout 900   1700 14000 timeout 900   5300 9600 timeout 900   1500 13000 out of memory 71   15000 900 error (1) 24   9200 330
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i error (134) .081 24 .76 out of memory 89     15000   1400    error (42) 880     1900   12000    timeout 970   4800 9800 unknown 170    58 2200   unknown 8.3  430 95   timeout 900    4200 5200   timeout 900     4000 9700    timeout 960 4800 9100 disqualified 2.7  84 40   timeout (verification) 900     2600 13000    timeout 900   770 11000 timeout 900   5300 7500 timeout 900   910 11000 true 16   200 120 error (1) 880   1400 13000
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i error (134) .080 24 .80 out of memory 100     15000   1400    error (42) 880     2700   14000    timeout 970   4200 8400 unknown 900    340 11000   out of memory (unknown error) 270    15000 2700   out of memory (unknown error) 270    15000 3100   timeout 900     4400 10000    timeout 910 7900 11000 disqualified 880    260 12000   timeout (verification) 900     3100 9600    timeout 900   890 10000 timeout 900   3800 8300 timeout 900   820 12000 out of memory 470   15000 5400 error (1) 890   1600 14000
array-industry-pattern/array_of_struct_break_true-unreach-call.i true 36     13000 480    out of memory 210     15000   2600    out of memory 760     15000   9100    timeout 970   6800 7300 unknown 740    1400 8000   unknown 8.2  430 91   timeout 900    6200 9100   out of memory 570     15000 4600    timeout 960 6900 8100 disqualified 2.7  84 30   true .95  69 14    timeout 900   1400 12000 timeout 900   5200 11000 timeout 900   4900 9800 true 16   200 110 error (1) 880   360 12000
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i error (134) 240     7000 1800    out of memory 310     15000   4200    error (134) 2.6   400   30    timeout 970   4800 8400 unknown .81 65 8.7 unknown 8.3  440 99   timeout 900    4700 8600   timeout 900     5300 10000    timeout 910 5300 6800 disqualified 8.6  100 120   timeout (verification) 900     3200 14000    timeout 900   1200 9300 timeout 900   5200 6600 timeout 900   4000 6200 true 17   200 120 error (1) 890   410 11000
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i error (134) .18  24 1.2  out of memory 180     15000   2100    error (42) 880     2000   12000    timeout 960   4800 7200 unknown 400    590 4500   out of memory (unknown error) 120    15000 1300   out of memory (unknown error) 120    15000 1200   timeout 900     13000 10000    timeout 970 7600 8600 disqualified 3.0  83 35   true 1.2   100 17    true 15   500 120 timeout 900   5300 7600 true 18   650 140 true 41   1200 450 error (1) 890   750 11000
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i error (134) 160     7000 1100    out of memory 310     15000   4000    error (134) 2.5   400   29    timeout 960   4000 8800 unknown .83 67 8.4 unknown 8.3  440 110   timeout 900    4600 9100   timeout 900     4900 10000    timeout 930 5700 6900 disqualified 2.9  80 37   timeout (verification) 900     4000 12000    timeout 900   1000 8700 timeout 900   5400 8800 timeout 900   4000 6200 true 16   200 110 error (1) 880   410 13000
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i out of memory 36     15000 440    out of memory 410     15000   5000    error (134) 5.3   500   51    timeout 960   4000 8900 unknown 900    1500 9200   out of memory (unknown error) 170    15000 1900   out of memory (unknown error) 170    15000 1800   timeout 900     3000 14000    timeout 960 6300 10000 disqualified 880    440 9300   timeout (verification) 900     2800 9400    timeout 900   1700 11000 timeout 900   2700 8800 timeout 900   5200 8100 true 18   200 130 error (1) 890   510 11000
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i out of memory 28     15000 450    out of memory 89     15000   1200    out of memory 22     9200   320    timeout 960   3900 10000 unknown 900    2200 12000   unknown 8.3  440 97   unknown 8.5  440 110   timeout 900     1700 13000    timeout 900 6900 13000 disqualified 5.9  97 84   true 1.4   110 16    timeout 900   1300 8100 timeout 900   5400 10000 timeout 900   5000 6500 true 17   200 130 error (1) 890   510 13000
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i timeout 900     11000 7900    error (42) 870     13000   12000    error (42) 880     10000   10000    timeout 960   3700 7900 unknown 900    1900 9600   out of memory (unknown error) 130    15000 1300   out of memory (unknown error) 130    15000 1200   timeout 900     9100 11000    timeout 900 5600 8600 disqualified 2.7  84 34   true 1.1   82 16    timeout 900   1200 9700 timeout 900   5200 7400 timeout 900   4700 6800 true 15   200 120 error (1) 880   220 13000
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i error (134) 260     6900 1900    out of memory 320     15000   4100    error (134) 6.7   400   69    timeout 970   4900 7300 unknown 900    2200 8700   unknown 8.3  440 120   timeout 900    9400 8100   timeout 900     4300 9000    timeout 960 5700 7000 disqualified 19    120 250   timeout (verification) 900     4200 12000    timeout 900   1300 9800 timeout 900   5400 8800 timeout 900   4400 6500 true 17   200 120 error (1) 880   410 12000
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i timeout 900     12000 4500    out of memory 510     13000   6400    error (42) 870     4500   10000    timeout 960   5500 7700 unknown 900    83 11000   unknown 8.3  430 120   unknown 1.5  200 25   timeout 900     150 11000    timeout 960 6000 9500 disqualified 880    380 12000   timeout (verification) 900     1100 10000    timeout 900   1000 8600 timeout 900   1000 7800 timeout 900   920 7300 true 16   200 110 timeout 900   150 12000
reducercommutativity/rangesum05_false-unreach-call_true-termination.i error (134) .087 24 .71 false(unreach-call) .13  9.3 .89 false(unreach-call) .16  8.9 1.2  exception 380   2300 2800 false(unreach-call) 6.0  69 61   unknown 8.2  430 100   false(unreach-call) 8.8  430 110   false(unreach-call) .88  58 13    false(unreach-call) 16 1200 120 disqualified 2.8  84 36   false(unreach-call) .46  62 5.5  false(unreach-call) 14   550 110 false(unreach-call) 14   510 120 false(unreach-call) 22   740 180 false(unreach-call) 67   610 700 false(unreach-call) 3.5 150 35
reducercommutativity/rangesum10_false-unreach-call_true-termination.i error (134) .090 24 .62 false(unreach-call) .15  9.5 1.5  false(unreach-call) .15  9.4 1.5  exception 460   2500 2600 false(unreach-call) 14    79 200   unknown 8.1  430 110   false(unreach-call) 9.0  440 110   false(unreach-call) .88  58 11    false(unreach-call) 16 1300 110 disqualified 3.0  84 37   false(unreach-call) .61  61 6.6  false(unreach-call) 32   550 370 false(unreach-call) 20   560 170 false(unreach-call) 26   750 220 false(unreach-call) 230   910 2200 false(unreach-call) 3.6 150 37
reducercommutativity/rangesum20_false-unreach-call.i error (134) .087 24 .74 false(unreach-call) .53  14   7.8  false(unreach-call) .53  15   7.0  timeout 900   3500 6400 false(unreach-call) 46    94 490   unknown 8.1  430 100   false(unreach-call) 20    490 230   false(unreach-call) 1.4   57 18    false(unreach-call) 18 1300 120 disqualified 3.7  120 50   false(unreach-call) 1.5   62 21    timeout 900   1100 9500 false(unreach-call) 46   970 490 unknown 29   860 250 false(unreach-call) 210   1400 2200 false(unreach-call) 3.5 150 34
reducercommutativity/rangesum40_false-unreach-call.i error (134) .085 24 .73 false(unreach-call) .89  24   13    false(unreach-call) 4.2   38   54    timeout 900   5100 6900 unknown 680    270 8000   unknown 8.2  430 88   false(unreach-call) 130    510 1600   false(unreach-call) 9.3   59 110    false(unreach-call) 29 1500 230 disqualified 5.0  140 72   false(unreach-call) 8.4   69 82    timeout 900   1000 11000 timeout 900   1300 9500 unknown 63   920 680 false(unreach-call) 240   1500 3000 false(unreach-call) 3.6 150 36
reducercommutativity/rangesum60_false-unreach-call.i error (134) .088 24 .69 false(unreach-call) 5.2   49   67    false(unreach-call) 1.7   42   26    timeout 910   5800 6700 unknown 900    360 11000   unknown 8.4  430 110   false(unreach-call) 190    530 2100   false(unreach-call) 180     170 2200    false(unreach-call) 68 1800 670 disqualified 7.4  220 110   false(unreach-call) 66     89 800    timeout 900   770 10000 timeout 900   3300 11000 unknown 59   1900 560 false(unreach-call) 250   1500 2800 false(unreach-call) 3.6 150 34
reducercommutativity/rangesum_false-unreach-call_true-termination.i error (134) .085 24 .94 false(unreach-call) .39  37   5.3  out of memory 350     15000   5600    exception 32   1400 220 false(unreach-call) 4.5  68 54   unknown 8.1  430 100   unknown 1.6  200 23   false(unreach-call) 1.1   58 17    false(unreach-call) 40 1400 400 disqualified 3.7  88 48   false(unreach-call) .76  21 10    false(unreach-call) 12   540 96 timeout 900   1100 10000 false(unreach-call) 27   980 220 false(unreach-call) 91   620 950 false(unreach-call) 3.9 150 40
reducercommutativity/avg05_true-unreach-call_true-termination.i error (134) .091 24 .72 error (42) 880     220   13000    error (42) 880     230   13000    timeout 900   2200 7500 unknown 46    84 610   unknown 8.1  430 120   true 8.8  370 120   true 43     70 570    timeout 900 3600 7600 disqualified 2.1  72 26   true .17  18 1.7  timeout 900   760 13000 true 69   760 680 timeout 900   810 13000 true 4.7 190 30 timeout 900   150 10000
reducercommutativity/avg10_true-unreach-call_true-termination.i error (134) .098 23 .67 error (42) 880     320   13000    error (42) 880     310   13000    timeout 900   3700 10000 unknown 520    200 8200   unknown 8.2  430 94   true 8.5  370 140   true 520     200 7300    timeout 900 3600 8300 disqualified 2.1  76 29   true .17  17 1.8  timeout 900   1600 11000 timeout 900   1400 12000 timeout 900   1900 12000 true 4.6 190 36 timeout 900   150 9900
reducercommutativity/avg20_true-unreach-call.i error (134) .082 24 .84 error (42) 880     470   13000    error (42) 880     410   13000    timeout 900   3800 6300 unknown 900    310 12000   unknown 8.2  430 100   true 8.6  370 110   timeout 900     280 11000    timeout 900 4300 8000 disqualified 2.4  90 34   true .17  18 1.8  timeout 900   5400 7900 timeout 900   4800 8800 timeout 900   5300 6200 true 5.0 190 36 timeout 900   160 14000
reducercommutativity/avg40_true-unreach-call.i error (134) .085 24 .70 error (42) 880     550   11000    error (42) 880     560   12000    timeout 900   6100 6700 unknown 260    270 3000   unknown 8.2  430 110   true 8.8  380 100   timeout 900     360 11000    timeout 900 6000 7600 disqualified 3.3  140 43   true .18  18 2.8  timeout 900   1000 12000 timeout 900   3600 8300 timeout 900   5200 11000 true 4.8 190 38 timeout 900   150 13000
reducercommutativity/avg60_true-unreach-call.i error (134) .079 23 1.0  error (42) 880     650   11000    error (42) 880     670   11000    timeout 900   5100 7300 unknown 900    510 12000   unknown 8.4  430 100   true 8.9  380 120   timeout 900     420 11000    timeout 900 5400 9700 disqualified 5.0  220 70   true .20  17 1.9  timeout 900   890 12000 timeout 900   4000 13000 timeout 900   1600 11000 true 4.7 190 41 timeout 900   150 11000
reducercommutativity/avg_true-unreach-call_true-termination.i error (134) .080 24 .70 error (42) 870     360   13000    error (42) 880     310   11000    exception 26   1200 210 unknown 900    130 12000   unknown 8.1  430 110   unknown 1.6  200 18   timeout 900     150 12000    timeout 930 4100 9200 disqualified 880    180 11000   timeout (verification) 900     3800 12000    timeout 900   590 13000 timeout 900   640 12000 timeout 900   700 13000 true 3.1 150 26 error (1) 3.5 150 41
reducercommutativity/max05_true-unreach-call_true-termination.i error (134) .11  24 .66 true 2.1   12   27    true 410     5300   5900    true 220   1500 1700 unknown 2.6  67 39   unknown 8.2  430 97   true 400    410 3900   true .71  28 10    true 240 2300 1900 disqualified 2.1  73 30   true 2.8   23 36    timeout 900   2000 12000 true 440   2600 4800 timeout 900   1300 12000 true 5.5 190 44 timeout 900   200 13000
reducercommutativity/max10_true-unreach-call_true-termination.i error (134) .088 24 .75 true 230     49   3500    out of memory 110     15000   1300    timeout 900   2100 6700 unknown 21    68 300   unknown 8.2  430 92   timeout 900    400 7400   true 17     42 220    timeout 900 2900 7200 disqualified 2.4  81 38   true 180     64 2900    timeout 900   2900 8300 timeout 900   5800 10000 timeout 900   1500 13000 true 5.5 190 49 timeout 900   150 13000
reducercommutativity/max20_true-unreach-call.i error (134) .085 24 .82 error (42) 880     210   11000    out of memory 110     15000   1300    timeout 900   2300 7900 unknown 900    140 11000   unknown 8.3  430 120   timeout 900    400 7700   timeout 900     130 13000    timeout 900 2900 6500 disqualified 3.5  110 39   timeout (verification) 900     140 11000    timeout 900   1600 11000 timeout 900   11000 6800 timeout 900   2600 12000 true 5.2 190 40 timeout 900   150 10000
reducercommutativity/max40_true-unreach-call.i error (134) .10  24 .66 error (42) 880     450   12000    out of memory 110     15000   1300    timeout 900   2700 8100 unknown 48    130 690   unknown 8.2  430 100   timeout 900    400 8200   timeout 900     200 13000    timeout 900 2900 11000 disqualified 12    200 100   timeout (verification) 900     200 13000    timeout 900   1400 8400 timeout 900   6500 11000 timeout 900   2200 11000 true 5.3 190 40 timeout 900   150 12000
reducercommutativity/max60_true-unreach-call.i error (134) .11  24 .69 error (42) 880     580   10000    out of memory 110     15000   1500    timeout 900   3000 7600 unknown 160    220 2200   unknown 8.4  430 110   timeout 900    400 8300   timeout 900     240 13000    timeout 900 3400 7900 disqualified 38    340 270   timeout (verification) 900     210 12000    timeout 900   1100 11000 timeout 900   6800 8500 timeout 900   2800 11000 true 5.5 190 47 timeout 900   150 12000
reducercommutativity/max_true-unreach-call_true-termination.i error (134) .086 24 .65 error (42) 880     250   10000    out of memory 410     15000   5300    timeout 960   5400 7300 unknown 900    110 12000   unknown 8.2  430 100   unknown 1.6  200 19   timeout 900     120 11000    timeout 960 4600 6800 disqualified 880    380 11000   error(unknown, verification-finished) 810     3300 9700    timeout 900   4600 7600 timeout 900   3200 7700 timeout 900   4700 6500 true 7.3 150 79 error (1) 880   150 12000
reducercommutativity/sep05_true-unreach-call_true-termination.i error (134) .087 24 .71 true .17  9.9 2.3  error (42) 880     4800   8000    true 290   2500 2800 unknown 2.0  68 26   unknown 8.4  430 120   true 60    390 590   true .19  28 2.2  true 16 1100 120 disqualified 2.1  72 25   true .17  17 1.9  timeout 900   2200 13000 timeout 900   4700 8600 timeout 900   1400 9900 true 160   1300 1500 timeout 900   150 11000
reducercommutativity/sep10_true-unreach-call.i error (134) .087 23 .70 true .38  15   5.9  out of memory 110     15000   1500    exception 80   2500 820 unknown 4.3  67 62   unknown 8.3  430 110   timeout 900    430 6900   true .20  28 2.7  true 31 1400 350 disqualified 3.0  81 39   true .21  16 1.8  timeout 900   5600 9300 timeout 900   4800 8300 timeout 900   5400 9200 true 170   1500 1600 timeout 900   150 11000
reducercommutativity/sep20_true-unreach-call.i error (134) .10  24 .69 true 4.9   35   79    out of memory 110     15000   1200    timeout 910   4800 8900 unknown 12    67 160   unknown 8.4  430 100   timeout 900    400 7100   true .24  28 2.3  true 240 1900 1800 disqualified 880    110 12000   true .22  17 2.0  timeout 900   4200 7800 timeout 900   12000 9000 timeout 900   4300 9500 true 170   1600 1700 timeout 900   150 12000
reducercommutativity/sep40_true-unreach-call.i error (134) .10  24 .83 true 37     85   460    out of memory 110     15000   1400    timeout 910   3500 9100 unknown 41    87 550   unknown 8.3  430 100   timeout 900    400 7300   true .26  28 3.2  timeout 900 2800 8200 disqualified 880    170 12000   true .19  18 1.8  timeout 900   1200 10000 timeout 900   13000 8300 timeout 900   2000 10000 true 210   1400 2200 timeout 900   150 13000
reducercommutativity/sep60_true-unreach-call.i error (134) .11  24 .69 true 170     160   2200    out of memory 110     15000   1300    timeout 920   4400 11000 unknown 98    180 1400   unknown 8.2  430 93   timeout 900    410 7600   true .33  29 4.4  timeout 900 3600 6600 disqualified 880    270 13000   true .18  18 2.0  timeout 900   1100 11000 timeout 910   13000 9700 timeout 900   2200 10000 true 300   1400 3600 timeout 900   150 13000
reducercommutativity/sep_true-unreach-call_true-termination.i error (134) .11  24 .78 error (42) 880     810   7000    out of memory 570     15000   8900    timeout 940   5000 9600 unknown 900    88 12000   unknown 8.1  430 110   unknown 1.6  200 20   timeout 900     120 10000    timeout 910 3200 8800 disqualified 880    180 11000   error(unknown, verification-finished) 800     3100 9200    timeout 900   2100 11000 timeout 900   830 12000 timeout 900   1500 10000 timeout 900   15000 9200 error (1) 3.5 150 32
reducercommutativity/sum05_true-unreach-call_true-termination.i error (134) .088 24 .80 true 34     21   430    true 45     23   700    timeout 900   1600 12000 unknown 2.0  66 24   unknown 8.2  430 100   true 8.4  370 110   true .17  27 2.0  timeout 900 2200 10000 disqualified 2.1  73 23   true .17  17 1.9  timeout 900   4700 6900 true 700   800 10000 timeout 900   4100 6600 true 4.7 190 39 timeout 900   150 12000
reducercommutativity/sum10_true-unreach-call_true-termination.i error (134) .081 24 .83 error (42) 880     250   11000    error (42) 870     250   12000    timeout 900   3600 6600 unknown 4.0  67 51   unknown 8.3  430 130   true 8.5  370 97   true .17  27 2.3  timeout 900 4300 6400 disqualified 2.1  76 26   true .19  17 1.6  timeout 900   1200 11000 timeout 900   4900 6800 timeout 900   1200 13000 true 4.7 190 34 timeout 900   160 11000
reducercommutativity/sum20_true-unreach-call.i error (134) .088 23 .73 error (42) 870     410   13000    error (42) 880     430   11000    timeout 900   4700 6800 unknown 10    69 130   unknown 8.1  430 96   true 8.6  370 98   true .19  27 2.9  timeout 900 4200 6600 disqualified 2.3  90 33   true .17  17 2.2  timeout 900   5300 7600 timeout 900   5400 6300 timeout 900   5400 6900 true 4.7 190 37 timeout 900   150 12000
reducercommutativity/sum40_true-unreach-call.i error (134) .082 24 .90 error (42) 880     560   14000    error (42) 870     550   11000    timeout 910   5600 8200 unknown 36    75 460   unknown 8.5  430 100   true 8.6  370 100   true .23  27 3.2  timeout 900 6800 7500 disqualified 2.8  140 35   true .18  17 2.0  timeout 900   1100 11000 timeout 900   6100 6100 timeout 900   3500 12000 true 4.7 190 34 timeout 900   150 12000
reducercommutativity/sum60_true-unreach-call.i error (134) .082 24 .77 error (42) 880     620   11000    error (42) 880     600   9800    timeout 910   6300 7700 unknown 900    800 11000   unknown 8.2  430 110   true 8.4  380 110   true .30  27 3.2  timeout 910 5300 6700 disqualified 4.8  220 61   true .20  17 2.2  timeout 900   1100 9400 timeout 900   3600 12000 timeout 900   1600 12000 true 4.7 190 37 timeout 900   150 12000
reducercommutativity/sum_true-unreach-call_true-termination.i error (134) .088 23 .85 error (42) 880     360   10000    error (42) 880     1000   13000    timeout 970   4500 9500 unknown 890    120 9800   unknown 7.9  430 100   unknown 1.6  200 19   timeout 900     160 13000    timeout 970 4500 9100 disqualified 880    380 10000   error(unknown, verification-finished) 890     3400 9300    timeout 900   770 12000 timeout 900   4800 7800 timeout 900   14000 6000 true 2.9 150 29 error (1) 3.4 150 32
array-tiling/mlceu_false-unreach-call.i out of memory 790     15000 3900    out of memory 520     13000   6700    error (42) 870     4400   9700    timeout 960   5600 9300 unknown 900    84 14000   unknown 8.1  430 86   unknown 1.6  200 21   timeout 900     140 11000    timeout 960 5900 7000 disqualified 880    270 7800   timeout (verification) 900     1300 9400    timeout 900   1500 11000 timeout 900   840 6700 timeout 900   1400 11000 false(unreach-call) 16   190 110 error (1) 3.4 150 34
array-tiling/skippedu_false-unreach-call.i false(unreach-call) .30  27 3.2  false(unreach-call) .088 9.7 .96 false(unreach-call) .11  9.5 1.1  false(unreach-call) 6.4 320 60 false(unreach-call) .38 35 4.9 unknown 8.4  430 100   unknown 1.5  200 18   false(unreach-call) .10  26 1.2  false(unreach-call) 16 1200 110 disqualified 3.2  82 37   timeout (verification) 900     420 15000    false(unreach-call) 9.8 410 83 false(unreach-call) 9.1 370 67 false(unreach-call) 11   500 97 false(unreach-call) 24   200 210 error (1) 3.5 150 33
array-tiling/mbpr2_true-unreach-call.i out of memory 490     15000 2700    out of memory 99     13000   1200    out of memory 800     15000   11000    timeout 970   6000 7500 unknown 900    100 10000   unknown 8.4  430 99   unknown 1.6  200 22   timeout 900     150 10000    timeout 960 5100 7500 disqualified 880    390 11000   timeout (verification) 900     380 11000    timeout 900   920 11000 timeout 900   960 7800 timeout 900   790 12000 true 17   200 140 timeout 900   150 11000
array-tiling/mbpr3_true-unreach-call.i out of memory 340     15000 2900    out of memory 210     13000   2900    out of memory 630     15000   7200    timeout 960   6700 7200 unknown 900    280 10000   unknown 8.3  430 110   unknown 1.6  200 23   timeout 900     160 9900    timeout 970 7100 9000 disqualified 880    410 8100   timeout (verification) 900     280 13000    timeout 900   930 13000 timeout 900   1400 8600 timeout 900   990 11000 true 20   200 140 timeout 900   150 13000
array-tiling/mbpr4_true-unreach-call.i out of memory 310     15000 3000    error (134) 430     14000   5400    out of memory 500     15000   6800    timeout 920   7500 9100 unknown 900    86 11000   unknown 8.1  430 110   unknown 1.6  200 19   timeout 900     170 11000    timeout (exception) 910 7200 9800 disqualified 880    500 9000   timeout (verification) 900     350 11000    timeout 900   900 11000 timeout 900   1000 6800 timeout 900   850 12000 true 29   200 270 timeout 900   150 10000
array-tiling/mbpr5_true-unreach-call.i timeout 900     12000 5300    error (134) 780     14000   9900    out of memory 450     15000   5500    timeout 930   7200 9500 unknown 900    320 12000   unknown 8.2  430 100   unknown 1.6  200 20   timeout 900     170 11000    timeout 930 7500 8700 disqualified 880    510 9200   timeout (verification) 900     270 12000    timeout 900   1200 10000 timeout 900   1000 9000 timeout 900   1600 10000 true 40   210 390 timeout 900   150 14000
array-tiling/nr2_true-unreach-call.i out of memory 390     15000 2000    error (42) 880     12000   11000    out of memory 300     15000   4400    timeout 970   6700 10000 unknown 900    680 12000   unknown 8.2  430 100   unknown 1.5  200 18   timeout 900     140 12000    timeout 960 4400 9700 disqualified 880    330 14000   timeout (verification) 900     410 12000    timeout 900   1100 15000 timeout 900   930 7900 timeout 900   1100 9400 out of memory 320   15000 3200 timeout 900   150 11000
array-tiling/nr3_true-unreach-call.i out of memory 770     15000 2800    out of memory 91     13000   970    out of memory 400     15000   5200    timeout 960   6200 7800 unknown 900    660 9800   unknown 8.1  430 110   unknown 1.6  200 20   timeout 900     140 13000    timeout 970 6500 8800 disqualified 880    360 10000   timeout (verification) 900     320 11000    timeout 900   1000 13000 timeout 900   1000 9000 timeout 900   1600 12000 out of memory 360   15000 3100 timeout 900   150 10000
array-tiling/nr4_true-unreach-call.i out of memory 350     15000 2000    out of memory 120     14000   1800    out of memory 510     15000   7500    timeout 970   6600 8500 unknown 900    630 12000   unknown 8.1  430 110   unknown 1.6  200 20   timeout 900     140 12000    timeout 960 5200 8200 disqualified 880    380 12000   timeout (verification) 900     390 12000    timeout 900   2100 12000 timeout 900   940 10000 timeout 900   1900 10000 out of memory 220   15000 2600 timeout 900   150 11000
array-tiling/nr5_true-unreach-call.i out of memory 390     15000 2100    error (134) 150     14000   1800    out of memory 690     15000   11000    timeout 960   6100 11000 unknown 900    590 13000   unknown 8.3  430 99   unknown 1.6  200 19   timeout 900     130 12000    timeout 960 5100 8100 disqualified 880    410 9300   timeout (verification) 900     290 11000    timeout 900   2200 14000 timeout 900   980 7400 timeout 900   2100 11000 out of memory 260   15000 3400 timeout 900   150 12000
array-tiling/pnr2_true-unreach-call.i out of memory 780     15000 3200    out of memory 120     13000   1300    out of memory 550     15000   6500    timeout 960   3700 9700 unknown 900    220 11000   unknown 8.3  430 86   unknown 1.6  200 21   timeout 900     240 9200    timeout 970 3300 8300 disqualified 880    210 11000   timeout (verification) 900     400 11000    timeout 900   1300 11000 timeout 900   990 7000 timeout 900   5400 8000 true 17   200 120 error (1) 3.5 150 37
array-tiling/pnr3_true-unreach-call.i out of memory 590     15000 3000    out of memory 210     13000   3000    out of memory 220     15000   3000    timeout 960   6900 7100 unknown 900    210 8900   unknown 8.2  430 110   unknown 1.6  200 18   timeout 900     280 11000    timeout 960 6500 7600 disqualified 880    220 11000   timeout (verification) 900     310 12000    timeout 900   1500 12000 timeout 900   1300 10000 timeout 900   1000 13000 true 22   200 220 timeout 900   150 13000
array-tiling/pnr4_true-unreach-call.i out of memory 660     15000 3600    out of memory 350     13000   3600    out of memory 190     15000   2900    timeout 960   3500 10000 unknown 890    280 14000   unknown 8.1  430 97   unknown 1.6  200 21   timeout 900     270 9800    timeout 970 3100 8200 disqualified 880    260 10000   timeout (verification) 900     380 14000    timeout 900   1100 10000 timeout 900   2400 11000 timeout 900   1200 11000 true 86   200 1200 timeout 900   200 12000
array-tiling/pnr5_true-unreach-call.i out of memory 490     15000 2100    out of memory 520     13000   5600    out of memory 210     15000   2500    timeout 960   6600 9300 unknown 900    430 10000   unknown 8.3  430 99   unknown 1.6  200 19   timeout 900     260 12000    timeout 960 6100 8900 disqualified 880    250 11000   timeout (verification) 900     280 14000    timeout 900   5000 13000 timeout 900   3900 10000 timeout 900   1600 12000 true 140   200 1900 timeout 900   150 12000
array-tiling/poly1_true-unreach-call.i timeout 900     10000 5700    out of memory 74     14000   960    error (42) 880     4200   12000    timeout 960   5300 6100 unknown 10    38 170   unknown 8.2  430 93   unknown 1.5  200 17   unknown .076 26 .80 timeout 900 1700 11000 disqualified 880    180 11000   timeout (verification) 900     580 11000    timeout 900   750 11000 timeout 900   1100 10000 timeout 900   610 10000 true 3.0 150 27 error (1) 3.6 150 39
array-tiling/poly2_true-unreach-call.i timeout 900     8600 4500    out of memory 100     14000   1200    error (42) 880     8600   14000    timeout 970   5100 6600 unknown 13    39 190   unknown 8.1  430 120   unknown 1.5  200 20   unknown .099 26 .81 timeout 950 5400 7300 disqualified 880    700 12000   timeout (verification) 900     500 12000    timeout 900   630 13000 timeout 900   980 11000 timeout 900   710 14000 true 3.1 150 30 error (1) 3.4 150 34
array-tiling/pr2_true-unreach-call.i out of memory 610     15000 2700    out of memory 120     13000   1300    out of memory 260     15000   3200    timeout 960   3800 6800 unknown 900    130 12000   unknown 8.3  430 110   unknown 1.6  200 22   timeout 900     180 13000    timeout 960 4000 6800 disqualified 880    380 11000   timeout (verification) 900     1500 12000    timeout 900   1600 12000 timeout 900   920 8500 timeout 900   2100 10000 true 17   200 120 timeout 900   150 10000
array-tiling/pr3_true-unreach-call.i out of memory 370     15000 2000    out of memory 220     13000   2400    out of memory 150     15000   2100    timeout 960   3800 6400 unknown 900    190 13000   unknown 8.1  430 110   unknown 1.6  200 22   timeout 900     200 11000    timeout 960 4100 7000 disqualified 880    370 10000   timeout (verification) 900     1400 13000    timeout 900   1100 11000 timeout 900   930 8300 timeout 900   950 10000 true 20   200 180 timeout 900   150 9100
array-tiling/pr4_true-unreach-call.i out of memory 400     15000 2200    out of memory 350     13000   4500    out of memory 150     15000   2200    timeout 960   3800 7000 unknown 900    120 13000   unknown 8.3  430 110   unknown 1.6  200 20   timeout 900     200 11000    timeout 960 3800 7800 disqualified 880    390 11000   timeout (verification) 900     1700 10000    timeout 900   990 12000 timeout 900   900 11000 timeout 900   910 9200 true 27   200 290 timeout 900   150 12000
array-tiling/pr5_true-unreach-call.i out of memory 310     15000 2400    out of memory 520     13000   6400    out of memory 210     15000   2600    timeout 960   3300 8900 unknown 900    160 13000   unknown 8.3  430 110   unknown 1.5  200 20   timeout 900     230 13000    timeout 960 3500 8500 disqualified 880    400 10000   timeout (verification) 900     1400 10000    timeout 900   1100 9100 timeout 900   870 9500 timeout 900   1100 12000 true 32   200 290 timeout 900   150 11000
array-tiling/revcpyswp2_true-unreach-call.i timeout 900     11000 4800    out of memory 210     14000   2300    error (42) 870     2000   12000    timeout 960   3400 6400 unknown 900    100 11000   unknown 8.3  430 100   unknown 1.6  200 18   timeout 900     190 12000    timeout 960 3400 8100 disqualified 880    290 14000   timeout (verification) 900     140 13000    timeout 900   940 12000 timeout 900   1000 8200 timeout 900   830 10000 out of memory 570   15000 4900 error (1) 3.4 150 35
array-tiling/rew_true-unreach-call.i out of memory 770     15000 3700    error (42) 880     9300   12000    out of memory 490     15000   6400    timeout 960   4100 7200 unknown 900    98 13000   unknown 8.2  430 97   unknown 1.6  200 22   timeout 900     170 11000    timeout 970 4100 7400 disqualified 880    390 11000   timeout (verification) 900     920 11000    timeout 900   1500 12000 timeout 900   990 7300 timeout 900   1100 12000 true 17   200 140 timeout 900   150 12000
array-tiling/rewnif_true-unreach-call.i out of memory 680     15000 5500    error (42) 880     9300   13000    out of memory 510     15000   7000    timeout 960   4200 7700 unknown 900    98 10000   unknown 8.1  430 120   unknown 1.6  200 25   timeout 900     160 11000    timeout 960 5300 6900 disqualified 880    400 12000   timeout (verification) 900     920 12000    timeout 900   1200 10000 timeout 900   900 6300 timeout 900   950 11000 true 26   200 250 timeout 900   150 13000
array-tiling/rewnifrev2_true-unreach-call.i out of memory 710     15000 4400    out of memory 170     13000   2200    error (42) 880     1600   9600    timeout 960   4100 9500 unknown 900    220 11000   unknown 8.2  430 110   unknown 1.6  200 23   timeout 900     330 13000    timeout 970 3400 8700 disqualified 880    310 10000   timeout (verification) 900     570 12000    timeout 900   2400 12000 timeout 900   800 7100 timeout 900   2400 11000 true 42   200 460 error (1) 3.8 150 36
array-tiling/rewnifrev_true-unreach-call.i out of memory 730     15000 3200    out of memory 220     12000   2500    error (42) 880     1200   13000    timeout 960   3900 7200 unknown 900    210 14000   unknown 8.2  430 94   unknown 1.5  200 19   timeout 900     340 11000    timeout 960 4100 7700 disqualified 880    320 11000   timeout (verification) 900     600 13000    timeout 900   1100 9300 timeout 900   980 6900 timeout 900   980 8900 out of memory 260   15000 2700 error (1) 3.6 150 33
array-tiling/rewrev_true-unreach-call.i out of memory 640     15000 2900    out of memory 220     12000   2400    error (42) 880     1300   10000    timeout 960   4100 7100 unknown 900    150 11000   unknown 8.0  430 100   unknown 1.6  200 19   timeout 900     240 13000    timeout 960 5000 7700 disqualified 880    280 12000   timeout (verification) 900     660 11000    timeout 900   1200 11000 timeout 900   1100 8300 timeout 900   1400 11000 true 27   200 250 error (1) 3.7 150 38
array-tiling/skipped_true-unreach-call.i out of memory 900     15000 5000    out of memory 100     14000   1500    out of memory 580     15000   8500    timeout 960   3700 10000 unknown 900    390 11000   unknown 8.2  430 110   unknown 1.6  200 23   timeout 900     250 12000    timeout 970 4300 9400 disqualified 880    230 13000   timeout (verification) 900     420 13000    timeout 900   2600 11000 timeout 900   1000 8300 timeout 900   2700 11000 true 21   200 170 timeout 900   150 11000
array-tiling/tcpy_true-unreach-call.i timeout 900     10000 3800    error (42) 880     11000   5500    error (42) 880     2500   10000    timeout 960   3700 9700 unknown 900    130 14000   unknown 8.3  430 110   unknown 1.6  200 19   timeout 900     170 10000    timeout 960 3000 7700 disqualified 880    240 14000   timeout (verification) 900     690 12000    timeout 900   1300 11000 timeout 900   900 8200 timeout 900   2400 8000 true 21   200 150 timeout 900   150 9700
array-programs/copysome1_false-unreach-call.i error (134) .083 24 .86 out of memory 160     15000   2100    error (42) 880     5400   12000    timeout 970   4600 11000 unknown 220    120 3100   timeout 900    440 9800   timeout 900    3300 7800   timeout 900     11000 9400    timeout 970 6200 9600 disqualified 880    820 13000   false(unreach-call) 25     1200 240    timeout 900   1500 12000 timeout 900   4100 8000 timeout 900   3700 11000 false(unreach-call) 17   200 110 false(unreach-call) 300   2800 4000
array-programs/copysome2_false-unreach-call.i error (134) .083 24 .81 out of memory 150     15000   2100    error (42) 880     8600   12000    timeout 960   4100 10000 unknown 350    95 4600   timeout 900    430 8100   timeout 900    3300 8600   timeout 900     11000 11000    timeout 900 9100 11000 disqualified 890    860 13000   false(unreach-call) 42     1500 370    timeout 900   1600 8400 timeout 900   5000 9400 timeout 900   1700 13000 false(unreach-call) 18   200 120 false(unreach-call) 440   4200 5900
array-programs/copysome1_true-unreach-call.i error (134) .093 24 .79 out of memory 160     15000   2000    error (42) 880     5400   11000    timeout 960   5000 9300 unknown 230    67 2700   timeout 900    440 8900   timeout 900    3300 8100   timeout 900     11000 9500    timeout 970 6500 8300 disqualified 880    790 11000   true 17     770 130    timeout 900   1600 9800 timeout 900   5100 8400 timeout 900   4100 13000 true 16   200 110 error (1) 880   2800 11000
array-programs/copysome2_true-unreach-call.i error (134) .081 24 .76 out of memory 150     15000   2200    error (42) 880     8600   12000    timeout 970   5100 9200 unknown 280    84 3800   timeout 900    430 9400   timeout 900    3300 10000   timeout 900     11000 9400    timeout 900 8200 12000 disqualified 890    820 11000   true 31     1100 220    timeout 900   1600 7800 timeout 900   5100 7700 timeout 900   1900 11000 true 17   200 130 error (1) 890   4200 11000
array-crafted/bAnd1_true-unreach-call.i error (134) .095 24 .64 true .59  29   7.3  true .62  31   7.8  timeout 900   6500 8100 unknown 240    240 3000   unknown 8.3  430 110   true 8.8  380 110   true .68  29 9.8  timeout 900 5100 8000 disqualified 880    1700 7400   true .18  18 2.0  timeout 900   980 11000 timeout 900   3700 10000 timeout 900   1500 14000 true 4.7 190 34 timeout 900   150 10000
array-crafted/bAnd2_true-unreach-call.i error (134) .079 23 .79 true 9.0   1200   120    true 8.7   1200   120    timeout 910   5900 11000 unknown 220    180 2600   unknown 10    450 110   true 26    600 280   true 17     290 220    timeout 910 6500 8200 disqualified 66    15000 590   true 23     180 200    timeout 900   1000 11000 timeout 900   5700 10000 timeout 900   1400 11000 true 4.6 190 36 timeout 900   150 10000
array-crafted/bAnd3_true-unreach-call.i error (134) .086 24 .72 out of memory 71     15000   1100    out of memory 62     15000   910    timeout 960   5400 9900 unknown 210    170 3100   unknown 33    680 370   timeout 900    1300 8100   timeout 900     11000 10000    timeout 970 6600 8500 disqualified 880    490 13000   timeout (verification) 900     1700 6700    timeout 900   1000 10000 timeout 900   5300 9100 timeout 900   1400 13000 true 4.8 190 40 timeout 900   150 13000
array-crafted/bAnd4_true-unreach-call.i error (134) .082 24 .89 out of memory 53     15000   660    out of memory 50     15000   660    timeout 960   4000 8900 unknown 280    220 3500   timeout 900    2300 10000   timeout 900    2300 9200   timeout 900     11000 12000    timeout 960 4700 8400 disqualified 3.9  100 48   out of memory (killed (signal 9, verification)) 560     15000 3300    timeout 900   850 9400 timeout 900   6200 8300 timeout 900   1300 11000 true 4.6 190 38 error (1) 880   940 12000
array-crafted/bAnd5_true-unreach-call.i error (134) .084 23 .70 error (42) 880     8500   4100    error (42) 870     1500   11000    timeout 960   4600 7200 unknown 900    86 11000   unknown 8.2  430 100   unknown 1.6  200 21   timeout 900     170 13000    timeout 970 4600 8100 disqualified 880    400 8700   error(unknown, verification-finished) 860     3400 10000    timeout 900   950 11000 timeout 900   830 11000 timeout 900   1200 12000 true 2.9 150 31 error (1) 880   150 11000
array-crafted/bor1_true-unreach-call.i error (134) .088 24 .63 true .62  29   8.1  true .61  31   8.6  timeout 910   7600 8100 unknown 170    97 2500   unknown 8.4  430 97   true 8.8  380 100   true .46  28 5.7  timeout 900 5900 7600 disqualified 880    1000 8900   true .17  18 2.7  timeout 900   1000 10000 timeout 900   4500 9300 timeout 900   1700 11000 true 4.8 190 39 timeout 900   150 13000
array-crafted/bor2_true-unreach-call.i error (134) .086 23 .65 true 8.9   1200   120    true 8.7   1200   100    timeout 910   5900 9700 unknown 190    98 3100   unknown 9.8  450 130   true 25    600 280   true 16     280 200    timeout 910 6300 8500 disqualified 65    15000 610   true 10     110 120    timeout 900   850 9700 timeout 900   5200 11000 timeout 900   1300 11000 true 5.1 190 37 timeout 900   150 12000
array-crafted/bor3_true-unreach-call.i error (134) .089 24 .52 out of memory 71     15000   990    out of memory 62     15000   1000    timeout 970   4800 10000 unknown 180    100 2300   unknown 33    680 370   timeout 900    1300 7900   timeout 900     11000 10000    timeout 960 6200 8300 disqualified 880    340 9500   true 520     1300 5000    timeout 900   1100 8700 timeout 900   5400 7500 timeout 900   1400 12000 true 4.7 200 35 timeout 900   150 10000
array-crafted/bor4_true-unreach-call.i error (134) .10  24 .79 out of memory 53     15000   800    out of memory 50     15000   630    timeout 960   4300 10000 unknown 230    100 3300   timeout 900    2300 10000   timeout 900    2300 9400   timeout 900     11000 10000    timeout 960 7300 8700 disqualified 62    120 870   out of memory (killed (signal 9, verification)) 180     15000 1500    timeout 900   1100 9500 timeout 900   5300 8100 timeout 900   1400 11000 true 4.8 200 36 error (1) 880   940 12000
array-crafted/bor5_true-unreach-call.i error (134) .082 24 .83 error (42) 880     8500   3500    error (42) 870     1500   10000    timeout 960   4700 7600 unknown 900    85 11000   unknown 8.3  430 110   unknown 1.6  200 23   timeout 900     160 11000    timeout 960 5400 7500