Tool 2LS 0.6.0 CBMC 5.8 CPAchecker 1.6.1-svn 26725 CPAchecker 1.6.1-svn 26758M CPAchecker 1.6.1-svn 26773 DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 ESBMC ESBMC version 4.6.0 64-bit x86_64 linux CPAchecker Map2Check Map2Check 7.1 : Wed Nov 22 22:30:11 -04 2017 skink symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 ULTIMATE Automizer 0.1.23-3204b741 ULTIMATE Kojak 0.1.23-3204b741 ULTIMATE Taipan 0.1.23-3204b741 VeriAbs VerifierIntegerAssignmentPrograms File not exits
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-11-30 11:20:26 CET 2017-11-30 16:01:31 CET 2017-12-01 08:49:27 CET 2017-12-01 12:59:33 CET 2017-12-05 07:52:24 CET 2017-12-01 19:46:39 CET 2017-12-01 22:03:39 CET 2017-12-01 22:41:19 CET 2017-12-02 01:06:24 CET 2017-12-02 02:33:02 CET 2017-12-02 17:23:13 CET 2017-12-02 18:04:04 CET 2017-12-03 03:42:11 CET
Run set 2ls.sv-comp18.ReachSafety-Arrays cbmc.sv-comp18.ReachSafety-Arrays cpa-bam-bnb.sv-comp18.ReachSafety-Arrays cpa-bam-slicing.sv-comp18.ReachSafety-Arrays cpa-seq.sv-comp18.ReachSafety-Arrays depthk.sv-comp18.ReachSafety-Arrays esbmc-incr.sv-comp18.ReachSafety-Arrays esbmc-kind.sv-comp18.ReachSafety-Arrays interpchecker.sv-comp18.ReachSafety-Arrays map2check.sv-comp18.ReachSafety-Arrays skink.sv-comp18.ReachSafety-Arrays symbiotic.sv-comp18.ReachSafety-Arrays uautomizer.sv-comp18.ReachSafety-Arrays ukojak.sv-comp18.ReachSafety-Arrays utaipan.sv-comp18.ReachSafety-Arrays veriabs.sv-comp18.ReachSafety-Arrays viap.sv-comp18.ReachSafety-Arrays
Options --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp18-bam-bnb -disable-java-assertions -heap 10000m -ldv-bam-svcomp -disable-java-assertions -heap 10000m -svcomp18 -heap 10000M -benchmark -timelimit 900s -s incr -s kinduction -sv-comp18-interpcpachecker -heap 10000M -disable-java-assertions --witness witness.graphml --full-output --full-output --full-output
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i error (134) .093 22 .78 0 error (6) 160    14000 1700   0 error 2.6 270 21 0 error 2.5 260 25 0 timeout 900   9100 7500 0 timeout 900   750 11000 0 timeout 900     3800 8400    0 timeout 900     3900 8500    0 timeout 900   5100 11000 0 out of memory 61     15000 720    0 false(unreach-call) 6.0 330 56 1 false(unreach-call) 1.6  200 17   1 timeout 900   4700 12000 0 timeout 900   5100 11000 0 timeout 900   4100 12000 0 timeout 900   9100 10000 0 unknown 46   120 620 0
array-examples/sorting_bubblesort_false-unreach-call2_ground.i out of memory 31     15000 440    0 out of memory 23    15000 370   0 error 2.5 270 25 0 error 2.5 260 22 0 timeout 900   6600 9000 0 unknown 46   160 530 0 timeout 900     2800 10000    0 timeout 900     2800 12000    0 timeout 900   5000 11000 0 unknown 890     11 12000    0 unknown 34   690 390 0 timeout (timeout) 900    4000 9800   0 timeout 900   5200 12000 0 timeout 900   4900 10000 0 timeout 900   2900 14000 0 unknown 780   10000 11000 0 unknown 230   370 2300 0
array-examples/sorting_bubblesort_false-unreach-call_ground.i out of memory 33     15000 490    0 out of memory 23    15000 300   0 error 2.6 270 23 0 error 2.5 270 23 0 timeout 900   6800 10000 0 unknown 46   160 650 0 timeout 900     2800 10000    0 timeout 900     2800 12000    0 timeout 910   5000 12000 0 unknown 890     11 14000    0 unknown 34   700 390 0 timeout (timeout) 900    4100 12000   0 timeout 900   5100 12000 0 timeout 900   4900 14000 0 timeout 900   2800 12000 0 unknown 780   10000 11000 0 unknown 230   330 2200 0
array-examples/sorting_selectionsort_false-unreach-call2_ground.i out of memory 33     15000 470    0 error (134) 62    13000 780   0 error 2.8 290 26 0 error 2.6 260 22 0 timeout 900   6000 7800 0 unknown 890   340 12000 0 timeout 900     7400 9800    0 timeout 900     7500 12000    0 timeout 900   4800 10000 0 unknown 890     12 12000    0 unknown 110   860 1200 0 timeout (timeout) 900    100 8500   0 timeout 900   5000 14000 0 timeout 900   5100 14000 0 timeout 900   2000 11000 0 unknown 690   9400 7500 0 unknown 470   420 5600 0
array-examples/sorting_selectionsort_false-unreach-call_ground.i out of memory 33     15000 470    0 error (134) 77    13000 1000   0 error 2.8 290 28 0 error 2.5 260 21 0 timeout 900   6900 9200 0 unknown 890   360 9100 0 timeout 900     7400 12000    0 timeout 900     7300 10000    0 timeout 900   4900 12000 0 unknown 890     11 13000    0 unknown 110   810 1200 0 timeout (timeout) 900    100 9900   0 timeout 900   5100 11000 0 timeout 900   5000 14000 0 timeout 900   2600 12000 0 unknown 690   9600 7800 0 unknown 260   280 3700 0
array-examples/standard_allDiff2_false-unreach-call_ground.i out of memory 290     15000 2000    0 error (6) 420    10000 2500   0 error 2.5 270 23 0 error 2.5 270 21 0 timeout 900   8400 8500 0 unknown 900   1400 9700 0 timeout 900     3000 7000    0 timeout 900     3000 6800    0 timeout 910   4600 11000 0 unknown 890     11 11000    0 false(unreach-call) 5.8 320 53 1 false(unreach-call) 1.1  140 15   1 timeout 900   5400 11000 0 timeout 900   5300 12000 0 timeout 900   5500 12000 0 timeout 900   8100 9900 0 unknown 530   420 5300 0
array-examples/standard_copy1_false-unreach-call_ground.i out of memory 31     15000 360    0 out of memory 100    15000 1300   0 error 2.5 270 24 0 error 2.5 270 19 0 timeout 900   7600 11000 0 timeout 900   2400 13000 0 timeout 900     9300 10000    0 timeout 900     9500 12000    0 timeout 900   4500 11000 0 unknown 890     130 12000    0 unknown 43   710 460 0 false(unreach-call) 3.4  300 45   1 timeout 900   4500 10000 0 timeout 900   4900 14000 0 timeout 900   1700 12000 0 false(unreach-call) 380   2500 5400 0 false(unreach-call) 15   540 190 1
array-examples/standard_copy2_false-unreach-call_ground.i out of memory 31     15000 400    0 out of memory 120    15000 1900   0 error 2.5 260 20 0 error 2.5 270 22 0 timeout 900   6200 9300 0 timeout 900   1400 12000 0 timeout 900     9400 9300    0 timeout 900     9300 10000    0 timeout 900   4400 10000 0 unknown 890     130 12000    0 unknown 5.7 320 52 0 false(unreach-call) 4.2  350 59   1 timeout 900   4900 10000 0 timeout 900   4900 12000 0 timeout 900   1000 10000 0 false(unreach-call) 500   3500 7400 0 false(unreach-call) 18   710 240 1
array-examples/standard_copy3_false-unreach-call_ground.i out of memory 31     15000 430    0 out of memory 130    15000 1800   0 error 2.6 270 23 0 error 2.6 270 26 0 timeout 900   6900 9600 0 timeout 900   2400 11000 0 timeout 900     9500 10000    0 timeout 900     9300 8400    0 timeout 900   4400 11000 0 unknown 900     140 11000    0 unknown 5.9 320 50 0 false(unreach-call) 4.5  370 66   1 timeout 900   5100 10000 0 timeout 900   4700 11000 0 timeout 900   1100 11000 0 false(unreach-call) 620   4500 9300 0 false(unreach-call) 21   880 270 1
array-examples/standard_copy4_false-unreach-call_ground.i out of memory 31     15000 460    0 error (134) 95    15000 1300   0 error 2.6 270 24 0 error 2.5 270 21 0 timeout 900   8000 9700 0 timeout 900   2400 11000 0 timeout 900     9300 8800    0 timeout 900     9500 12000    0 timeout 900   4400 11000 0 unknown 890     130 11000    0 unknown 6.0 320 54 0 false(unreach-call) 5.0  400 69   1 timeout 900   5200 9400 0 timeout 900   4700 12000 0 timeout 900   1400 12000 0 false(unreach-call) 700   5400 10000 1 false(unreach-call) 23   1000 320 1
array-examples/standard_copy5_false-unreach-call_ground.i out of memory 31     15000 390    0 out of memory 100    15000 1200   0 error 2.6 270 23 0 error 2.7 270 24 0 timeout 900   8100 9600 0 timeout 900   2500 12000 0 timeout 900     9500 10000    0 timeout 900     9300 11000    0 timeout 900   4300 12000 0 unknown 890     140 12000    0 unknown 5.7 320 50 0 false(unreach-call) 5.3  430 59   1 timeout 900   5200 11000 0 timeout 900   5500 11000 0 timeout 900   1500 12000 0 false(unreach-call) 700   6300 10000 1 false(unreach-call) 26   1200 310 1
array-examples/standard_copy6_false-unreach-call_ground.i out of memory 31     15000 380    0 out of memory 110    15000 1500   0 error 2.5 270 23 0 error 2.6 270 24 0 timeout 900   8400 8800 0 timeout 900   2200 13000 0 timeout 900     9400 9900    0 timeout 900     9400 9700    0 timeout 900   4200 11000 0 unknown 900     130 11000    0 unknown 6.1 320 52 0 false(unreach-call) 5.8  470 67   1 timeout 900   5300 9800 0 timeout 900   4900 11000 0 timeout 900   1600 9400 0 false(unreach-call) 700   7200 8700 1 false(unreach-call) 28   1400 410 1
array-examples/standard_copy7_false-unreach-call_ground.i out of memory 31     15000 420    0 out of memory 120    15000 1900   0 error 2.5 270 23 0 error 2.6 260 23 0 timeout 900   8100 9500 0 timeout 900   2200 13000 0 timeout 900     9600 8700    0 timeout 900     9600 9400    0 timeout 900   4300 12000 0 unknown 900     130 12000    0 unknown 5.5 300 46 0 false(unreach-call) 6.1  500 71   1 timeout 900   5200 11000 0 timeout 900   4700 13000 0 timeout 900   1700 7700 0 false(unreach-call) 700   8200 10000 1 false(unreach-call) 31   1600 490 1
array-examples/standard_copy8_false-unreach-call_ground.i out of memory 31     15000 390    0 error (134) 65    14000 970   0 error 2.6 270 25 0 error 2.6 260 25 0 timeout 900   9000 10000 0 timeout 900   2200 11000 0 timeout 900     9900 9700    0 timeout 900     9600 11000    0 timeout 900   4200 11000 0 unknown 900     130 13000    0 unknown 5.8 320 46 0 false(unreach-call) 6.5  530 82   1 timeout 900   5300 9900 0 timeout 900   4800 11000 0 timeout 900   1800 11000 0 false(unreach-call) 700   9100 8000 1 false(unreach-call) 34   1800 440 1
array-examples/standard_copy9_false-unreach-call_ground.i out of memory 31     15000 490    0 error (134) 70    15000 910   0 error 2.6 270 21 0 error 2.5 260 26 0 timeout 900   8900 10000 0 timeout 900   2500 11000 0 timeout 900     9200 9500    0 timeout 900     9300 9800    0 timeout 900   4300 13000 0 unknown 900     130 12000    0 unknown 5.5 300 49 0 false(unreach-call) 7.0  560 88   1 timeout 900   5200 10000 0 timeout 900   4900 11000 0 timeout 900   2000 10000 0 false(unreach-call) 700   10000 9900 1 false(unreach-call) 36   2000 550 1
array-examples/standard_copyInitSum2_false-unreach-call_ground.i out of memory 33     15000 440    0 out of memory 72    15000 980   0 error 2.5 270 25 0 error 2.7 270 26 0 timeout 900   4100 8700 0 unknown 890   220 9100 0 timeout 900     6200 12000    0 timeout 900     6100 11000    0 timeout 900   4200 11000 0 out of memory 33     15000 380    0 unknown 6.1 320 54 0 false(unreach-call) .80 71 11   1 timeout 900   4500 11000 0 timeout 900   4800 14000 0 timeout 900   880 10000 0 false(unreach-call) 390   2500 5600 0 false(unreach-call) 17   1100 260 1
array-examples/standard_init1_false-unreach-call_ground.i true 32     12000 400    -32 out of memory 100    15000 1500   0 error 2.4 270 22 0 error 2.5 260 21 0 timeout 900   4600 10000 0 timeout 900   700 11000 0 timeout 900     5900 9600    0 timeout 900     5800 10000    0 timeout 900   4500 13000 0 out of memory 26     15000 380    0 unknown 40   720 460 0 false(unreach-call) .42 39 5.7 1 timeout 900   2100 10000 0 timeout 900   4800 11000 0 timeout 900   1100 11000 0 false(unreach-call) 140   1000 1800 0 false(unreach-call) 12   480 160 1
array-examples/standard_init2_false-unreach-call_ground.i out of memory 31     15000 410    0 out of memory 61    15000 790   0 error 2.7 290 23 0 error 2.6 270 25 0 timeout 900   2900 8900 0 timeout 900   710 13000 0 timeout 900     5900 10000    0 timeout 900     6000 10000    0 timeout 900   4400 13000 0 out of memory 29     15000 390    0 unknown 26   690 270 0 false(unreach-call) .64 68 8.5 1 timeout 900   2200 11000 0 timeout 900   4800 12000 0 timeout 900   760 13000 0 false(unreach-call) 270   1500 3500 0 false(unreach-call) 14   790 210 1
array-examples/standard_init3_false-unreach-call_ground.i out of memory 31     15000 400    0 out of memory 64    15000 840   0 error 2.6 260 24 0 error 2.5 270 23 0 timeout 900   4300 11000 0 timeout 900   730 12000 0 timeout 900     5900 10000    0 timeout 900     5900 10000    0 timeout 900   4200 11000 0 out of memory 30     15000 370    0 unknown 22   720 200 0 false(unreach-call) .88 95 12   1 timeout 900   4200 11000 0 timeout 900   4800 12000 0 timeout 900   780 10000 0 false(unreach-call) 390   2000 5500 0 false(unreach-call) 17   1100 210 1
array-examples/standard_init4_false-unreach-call_ground.i out of memory 31     15000 390    0 out of memory 67    15000 1100   0 error 2.6 270 25 0 error 2.5 270 23 0 timeout 900   4400 10000 0 timeout 900   700 12000 0 timeout 900     6000 9000    0 timeout 900     6000 10000    0 timeout 900   4000 12000 0 out of memory 32     15000 440    0 unknown 22   690 220 0 false(unreach-call) 1.1  120 15   1 timeout 900   4900 9200 0 timeout 900   4800 12000 0 timeout 900   730 12000 0 false(unreach-call) 500   2500 6500 0 false(unreach-call) 20   1400 290 0
array-examples/standard_init5_false-unreach-call_ground.i out of memory 31     15000 460    0 out of memory 71    15000 1000   0 error 2.7 290 26 0 error 2.4 270 22 0 timeout 900   4200 8900 0 unknown 890   210 9200 0 timeout 900     5900 9700    0 timeout 900     6100 9600    0 timeout 900   4000 13000 0 out of memory 34     15000 470    0 unknown 22   680 190 0 false(unreach-call) 1.3  150 18   1 timeout 900   5500 9200 0 timeout 900   4800 11000 0 timeout 900   720 11000 0 false(unreach-call) 620   3000 9600 0 false(unreach-call) 23   1800 290 0
array-examples/standard_init6_false-unreach-call_ground.i out of memory 31     15000 410    0 out of memory 74    15000 980   0 error 2.7 290 23 0 error 2.6 260 25 0 timeout 900   4100 11000 0 unknown 890   240 8400 0 timeout 900     6100 11000    0 timeout 900     6100 9900    0 timeout 900   3900 12000 0 out of memory 36     15000 490    0 unknown 24   690 240 0 false(unreach-call) 1.5  180 23   1 timeout 900   5700 9400 0 timeout 900   4800 11000 0 timeout 900   770 12000 0 false(unreach-call) 710   3500 9700 1 false(unreach-call) 26   2100 350 0
array-examples/standard_init7_false-unreach-call_ground.i out of memory 31     15000 470    0 out of memory 52    15000 790   0 error 2.7 270 22 0 error 2.7 270 21 0 timeout 900   4100 8300 0 unknown 900   270 8300 0 timeout 900     6000 11000    0 timeout 900     6100 10000    0 timeout 900   4000 11000 0 out of memory 38     15000 470    0 unknown 24   690 270 0 false(unreach-call) 1.8  200 24   1 timeout 900   5700 12000 0 timeout 900   4800 12000 0 timeout 900   840 11000 0 false(unreach-call) 710   3900 11000 1 false(unreach-call) 28   2400 400 0
array-examples/standard_init8_false-unreach-call_ground.i out of memory 31     15000 470    0 out of memory 54    15000 660   0 error 2.7 270 21 0 error 2.5 270 22 0 timeout 900   4300 9200 0 unknown 890   290 8700 0 timeout 900     6100 9100    0 timeout 900     6100 12000    0 timeout 900   3900 13000 0 out of memory 40     15000 600    0 unknown 25   700 240 0 false(unreach-call) 2.0  230 28   1 timeout 900   5100 8500 0 timeout 900   4800 12000 0 timeout 900   920 10000 0 false(unreach-call) 710   4400 8400 1 false(unreach-call) 31   2700 380 0
array-examples/standard_init9_false-unreach-call_ground.i out of memory 33     15000 480    0 out of memory 56    15000 680   0 error 2.7 270 23 0 error 2.5 270 22 0 timeout 900   4300 11000 0 unknown 900   320 10000 0 timeout 900     6000 11000    0 timeout 900     6100 9700    0 timeout 900   4000 12000 0 out of memory 42     15000 640    0 unknown 26   690 240 0 false(unreach-call) 2.2  260 31   1 timeout 900   5600 8900 0 timeout 900   4800 11000 0 timeout 900   930 11000 0 false(unreach-call) 710   4800 8800 1 false(unreach-call) 34   3100 420 0
array-examples/standard_minInArray_false-unreach-call_ground.i out of memory 320     15000 2200    0 error (42) 870    1400 3800   0 error 2.5 270 22 0 error 2.6 270 24 0 timeout 900   4100 11000 0 unknown 98   110 1400 0 timeout 900     7100 11000    0 timeout 900     7100 9800    0 timeout 900   5100 13000 0 out of memory 28     15000 410    0 unknown 42   710 510 0 out of memory 100    15000 1200   0 timeout 900   5200 11000 0 timeout 900   4800 11000 0 timeout 900   2900 15000 0 false(unreach-call) 4.4 510 35 1 false(unreach-call) 12   580 160 1
array-examples/standard_partition_false-unreach-call_ground.i out of memory 31     15000 380    0 error (134) 65    14000 710   0 error 2.4 270 23 0 error 2.5 270 21 0 timeout 900   6000 8300 0 timeout 900   2300 12000 0 timeout 900     4200 10000    0 timeout 900     4300 11000    0 timeout 900   4200 14000 0 true 6.7   15 83    -32 unknown 26   680 240 0 timeout (timeout) 900    12000 9400   0 timeout 900   4500 11000 0 timeout 900   4900 9300 0 timeout 900   2800 12000 0 timeout 900   8100 11000 0 unknown 29   110 430 0
array-examples/standard_running_false-unreach-call.i out of memory 31     15000 370    0 out of memory 88    15000 1300   0 error 3.0 290 26 0 error 2.5 270 21 0 timeout 900   4700 9200 0 unknown 890   340 9300 0 out of memory 430     15000 5600    0 out of memory 430     15000 5600    0 timeout 900   4100 12000 0 out of memory 36     15000 450    0 unknown 24   700 240 0 timeout (timeout) 900    11000 13000   0 timeout 900   6300 10000 0 timeout 900   4800 12000 0 timeout 900   6300 11000 0 timeout 900   9200 10000 0 unknown 530   1200 5200 0
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i error (134) .11  22 .62 0 error (42) 870    1500 4900   0 error 2.5 260 24 0 error 2.6 260 26 0 true 93   2300 980 2 unknown 890   970 7800 0 timeout 900     9200 10000    0 timeout 900     9100 10000    0 timeout 900   5000 10000 0 true 23     11 340    2 true 4.1 270 36 2 true .15 11 1.8 2 true 6.2 290 49 2 timeout 900   5200 13000 0 true 6.2 300 48 2 unknown 650   8700 6600 0 unknown 70   160 1000 0
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i error (134) .078 22 .71 0 error (134) 26    13000 420   0 error 2.6 270 23 0 error 2.6 270 22 0 timeout 900   8700 9100 0 unknown 900   260 8100 0 timeout 900     3500 7700    0 timeout 900     3600 11000    0 timeout 900   5100 13000 0 true 30     12 470    2 unknown 31   690 310 0 timeout (timeout) 900    1300 10000   0 timeout 900   2000 11000 0 timeout 900   4900 12000 0 timeout 900   2500 11000 0 timeout 900   9200 9200 0 unknown 46   120 680 0
array-examples/relax_true-unreach-call.i error (134) .18  26 1.6  0 error (6) 690    14000 3800   0 error 8.1 440 61 0 unknown 5.7 310 48 0 timeout 900   5500 8000 0 unknown 890   190 7100 0 timeout 900     350 10000    0 timeout 900     360 13000    0 timeout 900   5300 11000 0 unknown .038 11 .48 0 unknown 8.1 410 67 0 unknown 370    180 1900   0 timeout 900   740 11000 0 timeout 900   590 13000 0 timeout 900   5100 10000 0 timeout 900   9100 9300 0 unknown 11   92 170 0
array-examples/sanfoundry_02_true-unreach-call_ground.i out of memory 180     15000 1400    0 error (42) 870    2600 4400   0 error 2.6 270 25 0 error 2.6 260 25 0 timeout 900   4300 9800 0 unknown 320   180 4200 0 timeout 900     10000 12000    0 timeout 900     10000 10000    0 timeout 900   5100 10000 0 true 20     11 270    2 unknown 31   700 320 0 out of memory 460    15000 3900   0 timeout 900   5300 13000 0 timeout 900   4900 11000 0 timeout 900   3300 13000 0 true 8.9 220 90 2 true 360   1100 3600 2
array-examples/sanfoundry_10_true-unreach-call_ground.i out of memory 34     15000 390    0 error (134) 28    13000 400   0 timeout 900   4100 8100 0 timeout 900   4100 11000 0 timeout 900   9100 9100 0 unknown 890   180 11000 0 timeout 900     360 12000    0 timeout 900     520 10000    0 timeout 900   4600 11000 0 true 9.5   11 110    2 unknown 160   720 1700 0 timeout (timeout) 900    830 11000   0 timeout 900   980 13000 0 timeout 900   5300 11000 0 timeout 900   1100 11000 0 true 16   220 110 2 unknown 340   730 4000 0
array-examples/sanfoundry_24_true-unreach-call_true-termination.i true 17     5700 190    2 error (42) 870    4200 9100   0 error 2.7 290 25 0 error 2.5 260 21 0 true 6.1 480 65 2 timeout 900   3900 11000 0 timeout 900     1000 12000    0 true .10  26 .80 2 timeout 900   4300 13000 0 unknown 900     330 11000    0 true 4.5 270 44 2 timeout (timeout) 900    5400 8400   0 true 6.3 290 49 2 true 5.8 330 48 2 true 6.5 300 59 2 true 15   210 94 2 true 15   130 180 2
array-examples/sanfoundry_27_true-unreach-call_ground.i out of memory 270     15000 2100    0 error (42) 870    1400 4100   0 error 2.5 270 26 0 error 2.5 270 22 0 timeout 900   4600 9200 0 unknown 120   120 1500 0 timeout 900     7000 10000    0 timeout 900     7000 9800    0 timeout 900   5100 11000 0 true 10     11 170    2 unknown 60   720 640 0 out of memory 100    15000 990   0 timeout 900   2800 8900 0 timeout 900   4700 11000 0 timeout 900   3000 10000 0 true 3.9 220 28 2 true 120   840 1100 2
array-examples/sanfoundry_43_true-unreach-call_ground.i error (134) .074 22 .82 0 out of memory 93    15000 1200   0 true 2.8 280 29 2 true 2.7 270 25 2 true 93   2300 1000 2 unknown 52   100 720 0 timeout 900     9700 12000    0 true .10  26 .87 2 true 2.5 270 23 2 true 6.4   12 81    2 true 4.4 290 41 2 true .15 11 1.3 2 true 4.2 250 34 2 true 4.3 250 35 2 true 4.5 250 35 2 true 3.3 220 26 2 unknown 13   93 160 0
array-examples/sorting_bubblesort_true-unreach-call_ground.i out of memory 31     15000 370    0 out of memory 20    15000 250   0 error 3.0 290 25 0 error 2.6 260 23 0 timeout 900   6400 9100 0 unknown 46   160 510 0 timeout 900     2800 9900    0 timeout 900     2800 10000    0 timeout 900   5000 11000 0 unknown 890     11 14000    0 unknown 34   720 410 0 timeout (timeout) 900    3900 9800   0 timeout 900   5000 11000 0 timeout 900   5200 11000 0 timeout 900   5300 11000 0 unknown 780   10000 9800 0 unknown 230   320 1900 0
array-examples/sorting_selectionsort_true-unreach-call_ground.i out of memory 33     15000 520    0 error (134) 74    13000 820   0 error 2.5 270 20 0 error 2.5 270 24 0 timeout 900   6000 9400 0 unknown 890   300 7800 0 timeout 900     7300 11000    0 timeout 900     7300 8600    0 timeout 900   4800 11000 0 unknown 900     12 13000    0 timeout 900   1700 8800 0 timeout (timeout) 900    100 8100   0 timeout 900   5100 15000 0 timeout 900   5100 12000 0 timeout 900   2500 14000 0 unknown 690   9200 9000 0 unknown 260   250 3600 0
array-examples/standard_compareModified_true-unreach-call_ground.i out of memory 32     15000 450    0 error (6) 120    15000 1800   0 error 2.5 270 21 0 error 2.5 270 21 0 timeout 900   6000 8700 0 unknown 890   190 9500 0 timeout 900     5800 11000    0 timeout 900     5700 9500    0 timeout 900   4600 14000 0 true 18     12 260    2 unknown 26   680 240 0 timeout (timeout) 900    10000 10000   0 timeout 900   2600 11000 0 timeout 900   4900 12000 0 timeout 900   2700 9500 0 true 3.6 220 24 2 true 120   550 1300 2
array-examples/standard_compare_true-unreach-call_ground.i out of memory 150     15000 1300    0 error (42) 870    1500 3800   0 error 2.9 290 24 0 error 2.5 260 23 0 timeout 900   3900 10000 0 unknown 110   170 1300 0 timeout 900     7500 10000    0 timeout 900     7500 10000    0 timeout 900   5000 9900 0 true 11     12 150    2 unknown 45   710 470 0 timeout (timeout) 900    11000 11000   0 timeout 900   5200 12000 0 timeout 900   4800 13000 0 timeout 900   3900 15000 0 true 3.5 220 20 2 true 120   900 1400 2
array-examples/standard_copy1_true-unreach-call_ground.i out of memory 33     15000 440    0 out of memory 68    15000 1100   0 error 2.5 270 23 0 error 2.5 260 23 0 timeout 900   6600 9800 0 unknown 890   240 9600 0 timeout 900     10000 10000    0 timeout 900     10000 11000    0 timeout 900   4500 13000 0 unknown 900     120 11000    0 unknown 5.8 320 48 0 true 2.2  130 29   2 timeout 900   4400 11000 0 timeout 900   4700 11000 0 timeout 900   1000 11000 0 true 3.6 220 23 2 true 33   140 430 2
array-examples/standard_copy2_true-unreach-call_ground.i out of memory 34     15000 430    0 out of memory 81    15000 1000   0 error 2.6 270 23 0 error 2.5 260 25 0 timeout 900   6900 8900 0 timeout 900   2200 12000 0 timeout 900     10000 11000    0 timeout 900     10000 9100    0 timeout 900   4500 12000 0 unknown 890     120 11000    0 unknown 5.8 320 56 0 true 2.5  150 32   2 timeout 900   5100 13000 0 timeout 900   4900 12000 0 timeout 900   940 10000 0 true 3.6 230 23 2 true 36   140 460 2
array-examples/standard_copy3_true-unreach-call_ground.i out of memory 33     15000 430    0 out of memory 92    15000 1100   0 error 2.7 270 20 0 error 2.5 260 24 0 timeout 900   6600 10000 0 timeout 900   2200 12000 0 timeout 900     10000 9900    0 timeout 900     10000 11000    0 timeout 900   4300 12000 0 unknown 900     120 11000    0 unknown 5.6 320 53 0 true 2.9  160 34   2 timeout 900   5100 11000 0 timeout 900   4700 12000 0 timeout 900   1000 12000 0 true 3.8 220 24 2 true 38   140 610 2
array-examples/standard_copy4_true-unreach-call_ground.i out of memory 33     15000 470    0 out of memory 100    15000 1300   0 error 2.6 270 23 0 error 2.6 260 23 0 timeout 900   7700 9700 0 timeout 900   1400 12000 0 timeout 900     10000 9900    0 timeout 900     10000 10000    0 timeout 900   4300 11000 0 unknown 890     130 14000    0 unknown 5.8 320 47 0 true 3.2  170 38   2 timeout 900   5200 11000 0 timeout 900   4700 12000 0 timeout 900   1100 9200 0 true 3.5 220 28 2 true 41   140 600 2
array-examples/standard_copy5_true-unreach-call_ground.i out of memory 33     15000 440    0 error (134) 82    15000 1100   0 error 2.6 270 23 0 error 2.6 270 24 0 timeout 900   8400 8500 0 timeout 900   2200 11000 0 timeout 900     10000 12000    0 timeout 900     10000 11000    0 timeout 900   4300 11000 0 unknown 900     130 14000    0 unknown 5.6 320 53 0 true 3.5  180 45   2 timeout 900   5100 12000 0 timeout 900   4900 13000 0 timeout 900   1300 11000 0 true 3.6 220 29 2 true 44   140 570 2
array-examples/standard_copy6_true-unreach-call_ground.i out of memory 33     15000 480    0 out of memory 91    15000 1200   0 error 2.5 270 25 0 error 2.6 270 23 0 timeout 900   8800 9300 0 timeout 900   1400 11000 0 timeout 900     10000 10000    0 timeout 900     10000 9800    0 timeout 900   4200 12000 0 unknown 900     130 12000    0 unknown 6.4 400 50 0 true 3.9  190 49   2 timeout 900   5300 10000 0 timeout 900   4700 11000 0 timeout 900   1500 11000 0 true 3.5 220 26 2 true 46   140 620 2
array-examples/standard_copy7_true-unreach-call_ground.i out of memory 33     15000 450    0 out of memory 99    15000 1200   0 error 2.5 270 21 0 error 2.5 270 22 0 timeout 900   8700 11000 0 timeout 900   2200 11000 0 timeout 900     10000 12000    0 timeout 900     10000 9700    0 timeout 900   4100 12000 0 unknown 900     130 11000    0 unknown 5.7 320 51 0 true 4.1  200 50   2 timeout 900   5200 9700 0 timeout 900   4800 13000 0 timeout 900   1500 9300 0 true 3.9 220 26 2 true 50   140 730 2
array-examples/standard_copy8_true-unreach-call_ground.i out of memory 33     15000 520    0 error (134) 82    15000 1300   0 error 2.6 270 22 0 error 2.6 270 24 0 timeout 900   8200 8900 0 timeout 900   2200 12000 0 timeout 900     10000 9800    0 timeout 900     10000 11000    0 timeout 900   4100 12000 0 unknown 900     130 10000    0 unknown 5.3 310 45 0 true 4.6  210 71   2 timeout 900   5400 12000 0 timeout 900   4700 13000 0 timeout 900   1900 7700 0 true 3.7 230 24 2 true 53   170 760 2
array-examples/standard_copy9_true-unreach-call_ground.i out of memory 33     15000 390    0 error (134) 62    14000 730   0 error 2.6 270 22 0 error 2.5 270 23 0 timeout 900   9000 10000 0 timeout 900   2400 13000 0 timeout 900     10000 9900    0 timeout 900     10000 11000    0 timeout 900   4200 12000 0 unknown 890     130 13000    0 unknown 5.7 320 52 0 true 5.1  220 61   2 timeout 900   5300 10000 0 timeout 900   4700 11000 0 timeout 900   2100 11000 0 true 3.7 230 25 2 true 55   150 710 2
array-examples/standard_copyInitSum2_true-unreach-call_ground.i out of memory 32     15000 500    0 out of memory 72    15000 900   0 error 2.5 270 25 0 error 2.5 270 23 0 timeout 900   4100 8900 0 unknown 890   160 10000 0 timeout 900     6000 9700    0 timeout 900     6100 10000    0 timeout 900   4200 12000 0 true 15     12 210    2 unknown 5.8 310 53 0 true 1.4  51 18   2 timeout 900   5000 10000 0 timeout 900   4800 12000 0 timeout 900   780 11000 0 true 16   220 120 2 true 25   130 360 2
array-examples/standard_copyInitSum3_true-unreach-call_ground.i out of memory 32     15000 420    0 out of memory 75    15000 1100   0 error 2.5 270 21 0 error 2.5 270 21 0 timeout 900   4100 8700 0 unknown 900   210 9800 0 timeout 900     6100 10000    0 timeout 900     6000 10000    0 timeout 900   4000 13000 0 true 18     12 260    2 unknown 6.0 320 58 0 true 1.8  59 27   2 timeout 900   4800 11000 0 timeout 900   4800 11000 0 timeout 900   780 12000 0 true 3.4 220 24 2 true 30   170 390 2
array-examples/standard_copyInitSum_true-unreach-call_ground.i out of memory 32     15000 460    0 out of memory 72    15000 1000   0 error 2.6 270 24 0 error 2.6 270 21 0 timeout 900   4000 8600 0 unknown 890   190 8600 0 timeout 900     6000 9600    0 timeout 900     6000 10000    0 timeout 900   4200 13000 0 true 16     46 210    2 unknown 5.9 310 56 0 true 1.5  82 20   2 timeout 900   5100 12000 0 timeout 900   4800 12000 0 timeout 900   1000 11000 0 true 31   220 310 2 true 26   130 370 2
array-examples/standard_copyInit_true-unreach-call_ground.i out of memory 32     15000 390    0 out of memory 69    15000 900   0 error 2.5 270 21 0 error 2.6 270 25 0 timeout 900   4700 10000 0 unknown 890   220 10000 0 timeout 900     6000 9500    0 timeout 900     5900 9800    0 timeout 900   4300 11000 0 true 12     12 180    2 unknown 5.5 310 51 0 true 1.1  41 16   2 timeout 900   3300 9900 0 timeout 900   5000 11000 0 timeout 900   910 11000 0 true 16   220 99 2 true 22   130 300 2
array-examples/standard_find_true-unreach-call_ground.i true 40     15000 500    2 out of memory 100    15000 1300   0 error 2.6 270 25 0 error 2.6 270 24 0 timeout 900   6500 9000 0 timeout 900   2300 13000 0 timeout 900     10000 9800    0 timeout 900     10000 9600    0 timeout 900   4600 12000 0 unknown 890     130 11000    0 unknown 24   710 250 0 unknown 530    2400 8300   0 timeout 900   5000 12000 0 timeout 900   5000 12000 0 timeout 900   1300 12000 0 true 16   220 100 2 true 25   180 340 2
array-examples/standard_init1_true-unreach-call_ground.i true 32     12000 390    2 out of memory 100    15000 1400   0 error 2.5 260 22 0 error 2.5 260 25 0 timeout 900   2800 9300 0 timeout 900   730 13000 0 timeout 900     5800 11000    0 timeout 900     5900 11000    0 timeout 900   4500 11000 0 true 9.1   11 120    2 unknown 39   720 400 0 true .80 32 10   2 timeout 900   2200 10000 0 timeout 900   4800 13000 0 timeout 900   890 11000 0 true 15   220 92 2 true 20   130 330 2
array-examples/standard_init2_true-unreach-call_ground.i out of memory 31     15000 380    0 out of memory 61    15000 860   0 error 2.4 270 21 0 error 2.5 270 22 0 timeout 900   4300 11000 0 timeout 900   770 10000 0 timeout 900     5900 9600    0 timeout 900     5900 9900    0 timeout 900   4400 10000 0 true 11     11 180    2 unknown 26   690 250 0 true .97 39 14   2 timeout 900   2900 10000 0 timeout 900   4700 12000 0 timeout 900   790 12000 0 true 15   220 120 2 true 22   130 360 2
array-examples/standard_init3_true-unreach-call_ground.i out of memory 31     15000 410    0 out of memory 64    15000 880   0 error 2.5 270 22 0 error 2.6 260 27 0 timeout 900   4300 10000 0 timeout 900   730 10000 0 timeout 900     6000 12000    0 timeout 900     5900 9300    0 timeout 900   4200 13000 0 true 13     11 170    2 unknown 21   710 190 0 true 1.2  47 17   2 timeout 900   4400 9700 0 timeout 900   5200 12000 0 timeout 900   890 10000 0 true 16   220 100 2 true 25   140 380 2
array-examples/standard_init4_true-unreach-call_ground.i out of memory 31     15000 470    0 out of memory 67    15000 910   0 error 2.5 270 25 0 error 2.6 270 23 0 timeout 900   4200 9400 0 timeout 900   770 10000 0 timeout 900     6000 10000    0 timeout 900     5900 11000    0 timeout 900   4000 12000 0 true 15     11 210    2 unknown 21   670 200 0 true 1.4  54 21   2 timeout 900   5100 8100 0 timeout 900   5200 14000 0 timeout 900   770 11000 0 true 16   220 100 2 true 28   140 370 2
array-examples/standard_init5_true-unreach-call_ground.i out of memory 31     15000 400    0 out of memory 71    15000 1000   0 error 2.6 270 23 0 error 2.5 260 23 0 timeout 900   4100 9200 0 unknown 890   220 9700 0 timeout 900     6000 11000    0 timeout 900     6000 9700    0 timeout 900   4000 13000 0 true 17     11 220    2 unknown 23   680 230 0 true 1.6  61 23   2 timeout 900   5500 8700 0 timeout 900   4800 12000 0 timeout 900   850 10000 0 true 16   220 100 2 true 30   140 390 2
array-examples/standard_init6_true-unreach-call_ground.i out of memory 31     15000 400    0 out of memory 74    15000 990   0 error 2.8 290 23 0 error 2.5 260 25 0 timeout 900   4200 9300 0 unknown 900   240 9600 0 timeout 900     6000 8600    0 timeout 900     6000 10000    0 timeout 900   3900 11000 0 true 19     11 250    2 unknown 23   680 230 0 true 1.8  68 27   2 timeout 900   5700 8300 0 timeout 900   4800 12000 0 timeout 900   790 13000 0 true 15   220 120 2 true 33   140 490 2
array-examples/standard_init7_true-unreach-call_ground.i out of memory 31     15000 490    0 out of memory 52    15000 700   0 error 2.7 290 24 0 error 2.6 270 26 0 timeout 900   4300 9200 0 unknown 890   270 9800 0 timeout 900     6000 10000    0 timeout 900     6000 11000    0 timeout 900   4000 11000 0 true 21     11 310    2 unknown 25   700 250 0 true 2.0  75 27   2 timeout 900   5800 11000 0 timeout 900   4800 11000 0 timeout 900   800 10000 0 true 16   210 130 2 true 35   150 490 2
array-examples/standard_init8_true-unreach-call_ground.i out of memory 31     15000 440    0 out of memory 54    15000 730   0 error 2.6 270 21 0 error 2.7 270 24 0 timeout 900   4400 9100 0 unknown 890   290 10000 0 timeout 900     6000 10000    0 timeout 900     6000 13000    0 timeout 900   3900 11000 0 true 22     12 340    2 unknown 24   680 230 0 true 2.2  83 30   2 timeout 900   5100 8100 0 timeout 900   4800 13000 0 timeout 900   910 9800 0 true 17   220 110 2 true 38   140 520 2
array-examples/standard_init9_true-unreach-call_ground.i out of memory 31     15000 450    0 out of memory 56    15000 730   0 error 2.6 260 22 0 error 2.6 270 24 0 timeout 900   4000 9300 0 unknown 900   320 9000 0 timeout 900     6000 10000    0 timeout 900     6000 11000    0 timeout 900   3900 12000 0 true 25     11 260    2 unknown 25   690 280 0 true 2.4  90 38   2 timeout 900   5600 8000 0 timeout 900   4800 13000 0 timeout 900   910 13000 0 true 16   210 130 2 true 40   170 520 2
array-examples/standard_maxInArray_true-unreach-call_ground.i out of memory 260     15000 1900    0 error (42) 870    1400 4900   0 error 2.4 270 22 0 error 2.5 270 21 0 timeout 900   4500 8500 0 unknown 120   120 1600 0 timeout 900     7100 10000    0 timeout 900     7100 9800    0 timeout 900   5100 11000 0 true 10     11 130    2 unknown 41   740 410 0 out of memory 100    15000 940   0 timeout 900   2600 11000 0 timeout 900   4800 12000 0 timeout 910   4300 9700 0 true 4.2 220 27 2 true 130   1200 1500 2
array-examples/standard_minInArray_true-unreach-call_ground.i out of memory 310     15000 2100    0 error (42) 870    1400 3900   0 error 2.6 270 25 0 error 2.4 260 21 0 timeout 900   5200 8000 0 unknown 100   120 1500 0 timeout 900     7200 12000    0 timeout 900     7200 9700    0 timeout 900   5100 13000 0 true 11     11 120    2 unknown 42   730 440 0 out of memory 100    15000 1000   0 timeout 900   2700 8800 0 timeout 900   4800 11000 0 timeout 900   4400 9200 0 true 4.2 220 26 2 true 130   1400 1600 2
array-examples/standard_palindrome_true-unreach-call_ground.i out of memory 34     15000 420    0 out of memory 100    15000 1300   0 error 2.5 270 23 0 error 2.4 260 21 0 timeout 900   5600 11000 0 unknown 890   160 10000 0 timeout 900     10000 12000    0 timeout 900     10000 11000    0 timeout 900   4700 11000 0 true 5.5   11 89    2 unknown 45   710 530 0 true .69 45 8.6 2 timeout 900   1400 10000 0 timeout 900   4800 11000 0 timeout 900   850 9900 0 true 19   220 160 2 true 18   130 250 2
array-examples/standard_partial_init_true-unreach-call_ground.i out of memory 31     15000 400    0 error (134) 90    13000 870   0 error 2.8 300 24 0 error 2.6 270 23 0 timeout 900   4700 8000 0 timeout 900   2200 13000 0 timeout 900     4200 12000    0 timeout 900     4200 11000    0 timeout 900   4800 12000 0 true 20     13 250    2 unknown 34   720 410 0 timeout (timeout) 900    3800 8200   0 timeout 900   2900 11000 0 timeout 900   4800 14000 0 timeout 900   2100 9400 0 true 15   210 100 2 unknown 220   740 2300 0
array-examples/standard_partition_original_true-unreach-call_ground.i out of memory 29     15000 370    0 error (134) 74    14000 880   0 error 2.6 270 21 0 error 2.6 270 24 0 timeout 900   4900 10000 0 timeout 900   2500 12000 0 out of memory 480     15000 6600    0 out of memory 470     15000 5200    0 timeout 900   4600 13000 0 true 12     13 140    2 unknown 33   690 300 0 out of memory 16    15000 180   0 timeout 910   14000 3500 0 timeout 900   5200 11000 0 timeout 910   15000 3400 0 true 16   220 120 2 unknown 24   120 350 0
array-examples/standard_partition_true-unreach-call_ground.i out of memory 31     15000 400    0 error (134) 66    14000 810   0 error 2.8 290 24 0 error 2.5 270 23 0 timeout 900   6400 8700 0 unknown 890   270 9600 0 timeout 900     4200 12000    0 timeout 900     4300 12000    0 timeout 910   4200 11000 0 true 8.3   12 110    2 unknown 69   710 830 0 timeout (timeout) 900    12000 8700   0 timeout 900   650 13000 0 timeout 900   4700 12000 0 error (7) 32   720 310 0 true 16   220 120 2 unknown 31   120 410 0
array-examples/standard_password_true-unreach-call_ground.i out of memory 150     15000 1400    0 error (42) 870    1500 3500   0 error 2.5 270 21 0 error 2.5 260 21 0 timeout 900   3800 9600 0 unknown 120   180 1400 0 timeout 900     7500 11000    0 timeout 900     7500 9500    0 timeout 900   5000 11000 0 true 10     12 160    2 unknown 46   700 520 0 timeout (timeout) 900    10000 10000   0 timeout 900   5200 13000 0 timeout 900   4800 11000 0 timeout 900   3500 13000 0 true 3.3 220 22 2 true 120   1200 1500 2
array-examples/standard_reverse_true-unreach-call_ground.i out of memory 33     15000 510    0 out of memory 110    15000 1500   0 error 2.4 260 22 0 error 2.5 270 22 0 timeout 900   7200 8800 0 unknown 900   180 8600 0 timeout 900     8700 9700    0 timeout 900     8600 11000    0 timeout 900   4500 10000 0 true 10     12 140    2 unknown 46   730 430 0 true 1.1  75 13   2 timeout 900   1800 11000 0 timeout 900   4800 9400 0 timeout 900   980 10000 0 true 16   220 100 2 true 20   120 280 2
array-examples/standard_running_true-unreach-call.i out of memory 31     15000 510    0 out of memory 88    15000 1100   0 error 2.8 290 26 0 error 2.5 270 22 0 timeout 900   4900 9000 0 unknown 890   300 9900 0 out of memory 430     15000 5200    0 out of memory 430     15000 6200    0 timeout 900   4100 13000 0 true 11     12 130    2 unknown 29   710 290 0 timeout (timeout) 900    7400 11000   0 timeout 900   860 13000 0 timeout 900   4800 13000 0 timeout 900   1000 8300 0 true 17   220 89 2 true 430   1200 3800 2
array-examples/standard_sentinel_true-unreach-call_true-termination.i out of memory 110     15000 880    0 error (42) 870    3900 11000   0 error 2.5 270 24 0 error 2.5 270 26 0 true 6.5 480 66 2 unknown 100   75 1000 0 timeout 900     300 11000    0 timeout 900     300 11000    0 timeout 900   4800 14000 0 true 1.2   170 17    2 true 25   700 240 2 timeout (timeout) 900    410 9100   0 true 6.6 330 52 2 true 5.5 310 42 2 true 7.6 440 58 2 true 100   750 870 2 true 9.3 150 130 2
array-examples/standard_seq_init_true-unreach-call_ground.i out of memory 34     15000 420    0 out of memory 100    15000 1400   0 error 2.6 270 22 0 error 2.5 270 24 0 timeout 900   3400 11000 0 timeout 900   780 13000 0 timeout 900     6100 9900    0 timeout 900     6200 12000    0 timeout 900   4600 12000 0 true 9.1   11 120    2 unknown 40   700 450 0 true .93 33 11   2 timeout 900   1800 11000 0 timeout 900   4800 12000 0 timeout 900   790 11000 0 true 3.4 220 21 2 true 23   230 270 2
array-examples/standard_strcmp_true-unreach-call_ground.i false(unreach-call) 75     11000 870    -16 error (42) 870    3500 5500   0 error 2.6 270 26 0 error 2.6 270 23 0 timeout 900   3500 8800 0 unknown 120   120 1800 0 timeout 900     7200 10000    0 timeout 900     7300 11000    0 timeout 910   5000 10000 0 true 11     12 170    2 unknown 240   710 3300 0 timeout (timeout) 900    640 9600   0 timeout 900   5200 12000 0 timeout 900   6900 10000 0 timeout 900   3500 7700 0 true 3.5 220 23 2 true 130   670 1500 2
array-examples/standard_strcpy_original_true-unreach-call.i out of memory 33     15000 410    0 out of memory 73    15000 940   0 error 2.7 270 22 0 error 2.7 270 22 0 timeout 900   6500 8300 0 timeout 900   2300 11000 0 timeout 900     10000 10000    0 timeout 900     10000 11000    0 timeout 900   4500 10000 0 unknown 890     130 12000    0 unknown 30   710 300 0 unknown 28    2200 250   0 timeout 900   3700 11000 0 timeout 900   4800 13000 0 timeout 900   1300 11000 0 true 16   220 100 2 true 23   140 330 2
array-examples/standard_strcpy_true-unreach-call_ground.i out of memory 33     15000 420    0 out of memory 73    15000 1100   0 error 2.5 260 24 0 error 2.5 270 22 0 timeout 900   5900 8600 0 unknown 890   270 13000 0 timeout 900     10000 11000    0 timeout 900     10000 12000    0 timeout 900   4500 12000 0 unknown 890     120 11000    0 unknown 26   690 230 0 unknown 26    2200 180   0 timeout 900   3300 13000 0 timeout 900   4700 11000 0 timeout 900   1400 11000 0 true 15   210 110 2 true 24   140 340 2
array-examples/standard_two_index_01_true-unreach-call.i out of memory 250     15000 1600    0 out of memory 96    15000 1100   0 error 2.7 270 25 0 error 2.5 260 23 0 timeout 900   6600 8200 0 unknown 890   250 9700 0 timeout 900     10000 12000    0 timeout 900     10000 9600    0 timeout 900   4100 12000 0 true 300     50 2700    2 unknown 5.6 310 47 0 true .38 22 4.2 2 timeout 900   2900 10000 0 timeout 900   4800 14000 0 timeout 900   970 11000 0 true 15   220 110 2 true 18   140 270 2
array-examples/standard_two_index_02_true-unreach-call.i out of memory 34     15000 440    0 out of memory 68    15000 890   0 error 2.7 300 24 0 error 2.5 270 25 0 timeout 900   6200 11000 0 unknown 890   200 10000 0 timeout 900     10000 10000    0 timeout 900     10000 12000    0 timeout 900   4300 14000 0 unknown 900     120 11000    0 unknown 32   720 310 0 true 1.9  120 24   2 timeout 900   3000 9800 0 timeout 900   4800 11000 0 timeout 900   870 11000 0 true 15   220 110 2 true 29   140 360 2
array-examples/standard_two_index_03_true-unreach-call.i out of memory 240     15000 1800    0 out of memory 96    15000 1300   0 error 2.7 290 27 0 error 2.5 270 23 0 timeout 900   6200 11000 0 unknown 890   180 8600 0 timeout 900     10000 10000    0 timeout 900     10000 10000    0 timeout 900   4300 11000 0 true 290     49 2700    2 unknown 33   720 310 0 true .32 20 3.3 2 timeout 900   3000 10000 0 timeout 900   5000 14000 0 timeout 900   880 12000 0 true 17   220 100 2 true 18   140 220 2
array-examples/standard_two_index_04_true-unreach-call.i out of memory 33     15000 480    0 out of memory 68    15000 890   0 error 2.6 270 23 0 error 2.4 270 24 0 timeout 900   5700 8500 0 unknown 890   230 13000 0 timeout 900     10000 12000    0 timeout 900     10000 9700    0 timeout 900   4400 12000 0 unknown 900     130 11000    0 unknown 31   700 330 0 true 1.6  120 22   2 timeout 900   2800 9800 0 timeout 900   4800 12000 0 timeout 900   960 9900 0 true 16   220 100 2 true 28   150 410 2
array-examples/standard_two_index_05_true-unreach-call.i out of memory 34     15000 430    0 out of memory 68    15000 950   0 error 2.5 270 24 0 error 2.6 270 24 0 timeout 900   6000 10000 0 unknown 890   220 9700 0 timeout 900     9900 9800    0 timeout 900     10000 12000    0 timeout 900   4500 12000 0 unknown 890     120 11000    0 unknown 33   730 340 0 true 1.5  120 18   2 timeout 900   2900 9500 0 timeout 900   4800 12000 0 timeout 900   1100 10000 0 true 16   220 97 2 true 28   140 390 2
array-examples/standard_two_index_06_true-unreach-call.i out of memory 240     15000 1700    0 out of memory 96    15000 1400   0 error 2.6 270 24 0 error 2.5 260 23 0 timeout 900   6300 9000 0 unknown 890   180 8600 0 timeout 900     10000 9700    0 timeout 900     10000 10000    0 timeout 900   4600 12000 0 true 300     49 3000    2 unknown 32   780 320 0 true .33 20 3.6 2 timeout 900   3300 8900 0 timeout 900   4800 13000 0 timeout 900   980 11000 0 true 16   220 120 2 true 18   140 270 2
array-examples/standard_two_index_07_true-unreach-call.i out of memory 34     15000 420    0 out of memory 68    15000 860   0 error 2.5 270 25 0 error 2.5 260 24 0 timeout 900   6500 11000 0 unknown 890   230 9200 0 timeout 900     10000 10000    0 timeout 900     10000 11000    0 timeout 900   4500 11000 0 unknown 900     130 11000    0 unknown 34   740 400 0 true 1.5  120 19   2 timeout 900   2800 10000 0 timeout 900   4800 12000 0 timeout 900   1100 11000 0 true 17   220 96 2 true 27   140 320 2
array-examples/standard_two_index_08_true-unreach-call.i out of memory 34     15000 420    0 out of memory 68    15000 880   0 error 2.5 270 23 0 error 2.5 270 21 0 timeout 900   6200 8900 0 unknown 890   190 13000 0 timeout 900     10000 8500    0 timeout 900     9900 11000    0 timeout 900   4500 12000 0 unknown 900     130 11000    0 unknown 31   700 330 0 true 1.5  120 19   2 timeout 900   2900 10000 0 timeout 900   5000 12000 0 timeout 900   1300 13000 0 true 17   220 92 2 true 27   140 360 2
array-examples/standard_two_index_09_true-unreach-call.i out of memory 34     15000 430    0 out of memory 68    15000 900   0 error 2.6 270 24 0 error 2.6 270 25 0 timeout 900   5900 8400 0 unknown 890   180 8700 0 timeout 900     10000 10000    0 timeout 900     10000 10000    0 timeout 900   4500 13000 0 unknown 890     120 14000    0 unknown 32   740 350 0 true 1.4  120 18   2 timeout 900   2500 10000 0 timeout 900   4800 12000 0 timeout 900   1300 12000 0 true 17   220 110 2 true 27   140 400 2
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i out of memory 170     15000 1200    0 error (42) 870    4500 4900   0 error 2.7 290 24 0 error 2.5 270 22 0 timeout 900   5700 7700 0 unknown 98   100 1400 0 timeout 900     830 11000    0 timeout 900     830 11000    0 timeout 900   4200 11000 0 true .32  11 4.0  2 unknown 100   710 1400 0 timeout (timeout) 900    500 11000   0 timeout 900   4600 13000 0 timeout 900   3000 11000 0 timeout 900   2900 14000 0 true 15   210 100 2 error (1) 29   350 370 0
array-examples/standard_vector_difference_true-unreach-call_ground.i out of memory 32     15000 400    0 error (6) 120    15000 1600   0 error 2.8 290 26 0 error 2.5 260 22 0 timeout 900   6600 8400 0 timeout 900   2400 12000 0 timeout 900     4500 9900    0 timeout 900     4500 9700    0 timeout 900   4400 13000 0 true 9.8   13 140    2 unknown 49   720 510 0 true 1.6  170 19   2 timeout 900   1900 11000 0 timeout 900   4800 11000 0 timeout 900   850 9300 0 true 3.6 220 23 2 true 21   130 270 2
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i out of memory 32     15000 380    0 out of memory 60    15000 770   0 error 2.6 270 22 0 error 2.7 270 24 0 timeout 900   4900 9900 0 unknown 890   330 9300 0 timeout 900     6400 9900    0 timeout 900     6400 9600    0 timeout 900   4000 11000 0 false(unreach-call) 3.2   30 45    1 unknown 25   690 280 0 false(unreach-call) .42 44 6.1 1 timeout 900   2500 11000 0 timeout 900   4900 10000 0 timeout 900   1100 12000 0 timeout 900   8700 9300 0 false(unreach-call) 12   520 160 1
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i out of memory 34     15000 500    0 out of memory 410    15000 3800   0 timeout 900   4200 8400 0 timeout 900   4200 11000 0 timeout 900   6300 8600 0 unknown 890   300 9800 0 timeout 900     5200 10000    0 timeout 900     5200 10000    0 timeout 900   4000 12000 0 false(unreach-call) 3.2   11 50    1 unknown 5.0 290 42 0 false(unreach-call) .39 38 4.8 1 timeout 900   5100 9400 0 timeout 900   5200 7300 0 timeout 900   5200 7100 0 out of memory 220   15000 2400 0 unknown 15   110 210 0
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i out of memory 26     15000 330    0 out of memory 71    15000 930   0 error 2.5 270 22 0 error 2.5 270 22 0 timeout 900   4000 8900 0 unknown 890   250 9900 0 timeout 900     5000 11000    0 timeout 900     5000 13000    0 timeout 900   4200 12000 0 timeout 900     4000 6100    0 unknown 150   730 1700 0 false(unreach-call) 2.0  200 25   1 timeout 900   5100 13000 0 timeout 900   4900 12000 0 timeout 900   2000 9900 0 false(unreach-call) 16   220 100 1 unknown 220   1300 2300 0
array-industry-pattern/array_range_init_false-unreach-call.i true 38     15000 460    -32 out of memory 440    15000 6400   0 error 2.6 270 25 0 error 2.5 260 22 0 timeout 900   5100 9900 0 unknown 890   190 9700 0 timeout 900     4600 11000    0 timeout 900     4600 10000    0 timeout 900   4200 11000 0 out of memory 32     15000 390    0 unknown 28   680 320 0 false(unreach-call) .45 42 5.9 1 timeout 900   5200 6700 0 timeout 900   5200 7100 0 timeout 900   5000 8700 0 false(unreach-call) 120   210 1500 1 false(unreach-call) 12   100 160 1
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i out of memory 26     15000 340    0 out of memory 71    15000 960   0 error 2.6 270 23 0 error 2.5 270 23 0 timeout 900   4500 10000 0 unknown 890   250 9600 0 timeout 900     5000 12000    0 timeout 900     5000 11000    0 timeout 900   4200 12000 0 unknown 900     3200 9300    0 unknown 41   710 420 0 timeout (timeout) 900    3900 9400   0 timeout 900   5100 11000 0 timeout 900   5900 9900 0 timeout 900   1800 11000 0 false(unreach-call) 16   220 120 0 unknown 220   1400 2700 0
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i error (134) .079 23 .65 0 error (134) 23    12000 300   0 timeout 900   5600 9300 0 timeout 900   6400 11000 0 timeout 900   6600 9100 0 timeout 900   5900 9600 0 timeout 900     3500 7700    0 timeout 900     3500 7600    0 timeout 900   4800 11000 0 out of memory 57     15000 720    0 unknown 54   700 590 0 timeout (timeout) 900    1200 11000   0 timeout 900   5300 12000 0 timeout 900   4900 11000 0 timeout 900   4400 12000 0 timeout 900   9100 9000 0 false(unreach-call) 22   110 270 0
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i out of memory 29     15000 370    0 out of memory 100    15000 1300   0 error 2.5 270 23 0 error 2.7 260 23 0 timeout 900   5300 8600 0 unknown 890   230 9000 0 timeout 900     4200 10000    0 timeout 900     4200 10000    0 timeout 900   4200 11000 0 unknown 900     3700 9800    0 unknown 350   700 3900 0 out of memory 20    15000 230   0 timeout 900   3400 11000 0 timeout 900   4900 11000 0 timeout 900   910 11000 0 true 15   220 100 2 true 21   210 270 2
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i out of memory 30     15000 370    0 out of memory 120    15000 1500   0 error 2.5 270 22 0 error 2.7 270 22 0 timeout 900   4700 11000 0 unknown 890   1700 9800 0 timeout 900     4200 11000    0 timeout 900     4100 8700    0 timeout 900   4300 13000 0 unknown 3.3   11 38    0 unknown 28   700 300 0 out of memory 14    15000 180   0 timeout 900   1700 10000 0 timeout 900   5200 13000 0 timeout 900   1900 12000 0 timeout 900   9000 13000 0 true 54   340 780 2
array-industry-pattern/array_of_struct_break_true-unreach-call.i true 36     13000 390    2 out of memory 250    15000 2500   0 timeout 900   4200 9500 0 timeout 900   4200 9900 0 timeout 900   7700 7600 0 unknown 890   220 9400 0 out of memory 660     15000 5000    0 out of memory 670     15000 4800    0 timeout 900   4000 13000 0 true 17     13 220    2 unknown 5.4 330 42 0 true .86 32 12   2 timeout 900   5300 8800 0 timeout 900   5200 7500 0 timeout 900   5300 8700 0 true 17   220 120 2 true 18   230 230 2
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i error (5) 110     7000 820    0 out of memory 280    15000 3900   0 timeout 900   4000 12000 0 timeout 900   4200 9300 0 timeout 900   7000 8400 0 timeout 900   3700 7100 0 timeout 900     6400 9800    0 timeout 900     6400 9800    0 timeout 900   4100 12000 0 unknown .35  12 3.7  0 unknown 5.3 300 49 0 unknown 11    360 140   0 timeout 900   5900 7400 0 timeout 900   6000 8800 0 timeout 900   5800 8100 0 true 19   220 140 2 unknown 3.4 92 50 0
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i error (134) .16  24 1.6  0 out of memory 150    15000 1800   0 timeout 900   5700 8800 0 timeout 910   11000 4400 0 timeout 900   6900 8200 0 unknown 540   650 5000 0 timeout 900     8400 11000    0 timeout 900     8400 13000    0 timeout 900   4500 14000 0 true 11     50 140    2 unknown 5.7 310 51 0 true 3.0  110 41   2 true 9.6 500 83 2 timeout 900   4900 11000 0 true 14   640 110 2 true 93   1200 780 2 unknown 4.3 92 59 0
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i error (5) 100     7000 830    0 out of memory 290    15000 3300   0 timeout 900   3900 11000 0 timeout 900   4200 9200 0 timeout 900   6400 11000 0 timeout 900   4100 8200 0 timeout 900     4800 8900    0 timeout 900     4900 9900    0 timeout 900   4200 11000 0 unknown 900     3500 8700    0 unknown 5.5 310 49 0 timeout (timeout) 900    3700 8200   0 timeout 900   5900 7900 0 timeout 900   6000 8500 0 timeout 900   5800 7000 0 true 21   220 140 2 unknown 3.3 92 50 0
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i out of memory 34     15000 440    0 out of memory 560    15000 8100   0 timeout 900   4200 7800 0 timeout 900   5100 11000 0 timeout 900   5800 9800 0 unknown 890   230 11000 0 timeout 900     2500 11000    0 timeout 900     2400 9300    0 timeout 900   4300 13000 0 unknown 3.2   11 40    0 unknown 5.9 330 48 0 out of memory 330    15000 4200   0 timeout 900   5900 7800 0 timeout 900   6400 7600 0 timeout 900   6100 8700 0 true 22   220 180 2 unknown 2.5 92 32 0
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i out of memory 26     15000 320    0 out of memory 130    15000 1700   0 timeout 900   4300 8800 0 timeout 900   3800 10000 0 timeout 900   6300 10000 0 unknown 890   250 9500 0 timeout 900     1600 11000    0 timeout 900     1600 11000    0 timeout 900   4100 12000 0 unknown 900     120 11000    0 unknown 5.1 300 48 0 true 2.9  110 34   2 timeout 900   5900 9600 0 timeout 900   6400 8600 0 timeout 900   5900 11000 0 true 20   220 150 2 unknown 24   130 310 0
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i error (5) 130     11000 1200    0 out of memory 430    15000 5200   0 timeout 900   4300 12000 0 timeout 900   3900 10000 0 timeout 900   5200 8600 0 unknown 890   430 8600 0 timeout 900     7300 11000    0 timeout 900     7300 9500    0 timeout 900   4000 11000 0 true 9.1   30 130    2 unknown 5.6 320 57 0 true 1.9  71 25   2 timeout 900   5800 7200 0 timeout 900   6200 6500 0 timeout 900   6000 9700 0 true 17   220 110 2 unknown 3.3 92 40 0
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i true 29     12000 360    2 out of memory 200    15000 2500   0 timeout 900   3900 12000 0 timeout 900   7800 6400 0 timeout 900   5000 9900 0 unknown 890   390 9500 0 timeout 900     4300 10000    0 timeout 900     4400 9700    0 timeout 900   4200 13000 0 unknown 900     3200 9800    0 unknown 5.9 350 55 0 timeout (timeout) 900    3700 8000   0 timeout 900   5900 9400 0 timeout 900   6000 8700 0 timeout 900   5900 8000 0 true 22   220 170 2 unknown 3.4 92 51 0
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i timeout 900     14000 3700    0 error (42) 870    5600 5100   0 timeout 900   11000 6600 0 false(unreach-call) 3.9 290 33 -16 timeout 900   6600 8700 0 timeout 900   4100 8700 0 timeout 900     190 13000    0 timeout 900     180 11000    0 timeout 900   5000 11000 0 true .50  12 5.6  2 unknown 140   710 1600 0 unknown .19 11 2.1 0 timeout 900   3700 12000 0 timeout 900   2700 12000 0 timeout 900   1400 10000 0 true 15   220 110 2 true 14   130 180 2
reducercommutativity/rangesum05_false-unreach-call_true-termination.i error (134) .089 22 .64 0 false(unreach-call) .67 34 6.4 1 false(unreach-call) 6.2 400 60 1 false(unreach-call) 6.5 410 60 1 false(unreach-call) 81   670 810 1 false(unreach-call) 490   210 5400 0 false(unreach-call) 1.1   28 10    1 false(unreach-call) 1.8   55 22    1 false(unreach-call) 42   1500 380 1 false(unreach-call) .57  13 7.6  0 false(unreach-call) 6.0 390 53 1 false(unreach-call) .21 12 2.4 1 false(unreach-call) 9.8 530 83 1 false(unreach-call) 9.9 480 84 1 false(unreach-call) 25   840 230 1 false(unreach-call) 61   510 670 1 false(unreach-call) 25   120 320 1
reducercommutativity/rangesum10_false-unreach-call_true-termination.i error (134) .11  22 .64 0 false(unreach-call) 1.1  34 9.8 1 false(unreach-call) 7.6 430 65 1 false(unreach-call) 7.7 530 58 1 false(unreach-call) 370   2300 3800 1 false(unreach-call) 500   210 6800 0 false(unreach-call) 2.0   29 14    1 false(unreach-call) 2.5   57 23    1 false(unreach-call) 55   2400 490 1 false(unreach-call) .68  17 8.9  1 false(unreach-call) 6.5 410 56 1 false(unreach-call) .21 13 2.8 1 false(unreach-call) 25   730 250 1 false(unreach-call) 18   700 170 1 false(unreach-call) 31   1000 240 1 false(unreach-call) 70   510 780 0 false(unreach-call) 25   110 310 1
reducercommutativity/rangesum20_false-unreach-call.i error (134) .092 22 .76 0 false(unreach-call) 2.0  35 26   0 false(unreach-call) 9.5 580 67 1 false(unreach-call) 13   740 120 1 timeout 900   2700 8000 0 false(unreach-call) 640   210 8400 0 false(unreach-call) 4.1   32 35    1 false(unreach-call) 4.5   55 49    1 false(unreach-call) 360   3900 4500 1 false(unreach-call) 1.2   28 16    1 false(unreach-call) 7.0 430 68 1 false(unreach-call) .52 24 7.1 1 timeout 900   1400 13000 0 false(unreach-call) 39   1000 390 1 unknown 90   1400 890 0 false(unreach-call) 89   1000 930 0 false(unreach-call) 25   96 340 1
reducercommutativity/rangesum40_false-unreach-call.i error (134) .094 22 .82 0 false(unreach-call) 4.9  41 61   0 timeout 900   5400 11000 0 false(unreach-call) 92   3700 900 1 timeout 900   3900 7700 0 unknown 890   250 12000 0 false(unreach-call) 15     45 170    1 false(unreach-call) 16     57 160    1 false(unreach-call) 220   3900 2900 1 false(unreach-call) 1.7   30 23    1 false(unreach-call) 21   620 200 1 false(unreach-call) .46 27 6.0 1 timeout 900   860 11000 0 timeout 900   1900 10000 0 unknown 55   1900 530 0 false(unreach-call) 140   2700 1300 1 false(unreach-call) 25   98 330 1
reducercommutativity/rangesum60_false-unreach-call.i error (134) .11  23 .63 0 false(unreach-call) 8.9  59 110   0 timeout 900   5400 9800 0 false(unreach-call) 210   4600 2200 1 timeout 900   5700 8500 0 unknown 890   210 13000 0 false(unreach-call) 180     170 2600    0 false(unreach-call) 180     170 2500    0 false(unreach-call) 740   4400 8600 1 false(unreach-call) 2.2   37 27    1 unknown 67   950 560 0 false(unreach-call) .74 32 10   1 timeout 900   2400 11000 0 timeout 900   3300 8700 0 unknown 600   2400 8100 0 false(unreach-call) 270   3800 3400 1 false(unreach-call) 25   120 420 1
reducercommutativity/rangesum_false-unreach-call_true-termination.i error (134) .097 22 .63 0 false(unreach-call) .96 58 12   1 false(unreach-call) 17   590 120 1 false(unreach-call) 15   650 110 0 false(unreach-call) 30   560 360 1 false(unreach-call) 490   210 6000 1 false(unreach-call) 1.2   31 11    1 false(unreach-call) 2.2   57 23    1 false(unreach-call) 19   970 160 0 true 4.4   33 53    -32 unknown 8.6 440 72 0 unknown .21 12 2.0 0 false(unreach-call) 10   540 88 1 false(unreach-call) 17   680 190 1 false(unreach-call) 39   760 350 1 false(unreach-call) 180   590 2000 1 unknown 360   340 4500 0
reducercommutativity/avg05_true-unreach-call_true-termination.i true 110     360 1300    2 true 35    51 500   2 false(unreach-call) 5.8 370 52 -16 false(unreach-call) 5.5 380 52 -16 timeout 900   2500 11000 0 timeout 900   2200 11000 0 true 42     72 630    2 true 43     75 480    2 false(unreach-call) 45   2000 380 -16 true .38  11 4.6  2 true 16   840 140 2 true .19 11 1.9 2 timeout 900   5300 9400 0 timeout 900   710 11000 0 timeout 900   6300 11000 0 true 3.6 220 23 2 true 41   240 450 2
reducercommutativity/avg10_true-unreach-call_true-termination.i timeout 900     710 12000    0 true 530    180 6000   2 false(unreach-call) 7.2 420 64 -16 false(unreach-call) 7.4 450 57 -16 timeout 900   5100 7400 0 timeout 900   3400 11000 0 true 490     190 5600    2 true 490     190 6000    2 false(unreach-call) 110   3700 1200 -16 timeout 900     110 11000    0 true 17   690 170 2 true .19 11 2.0 2 timeout 900   7700 8800 0 timeout 900   960 12000 0 timeout 900   7400 8100 0 true 3.5 220 26 2 true 25   250 340 2
reducercommutativity/avg20_true-unreach-call.i timeout 900     810 12000    0 error (42) 870    280 10000   0 false(unreach-call) 9.1 560 81 -16 false(unreach-call) 10   680 89 -16 timeout 900   2800 9200 0 timeout 900   700 6500 0 timeout 900     290 11000    0 timeout 900     290 11000    0 timeout 900   4400 11000 0 true 110     42 1400    2 true 20   660 180 2 true .20 11 1.5 2 timeout 900   2200 7400 0 timeout 900   1500 10000 0 timeout 900   1800 9600 0 true 3.4 230 25 2 true 320   660 4300 2
reducercommutativity/avg40_true-unreach-call.i timeout 900     890 7700    0 error (42) 870    300 11000   0 false(unreach-call) 53   2400 530 -16 false(unreach-call) 180   3200 1500 -16 timeout 900   2700 9000 0 unknown 890   260 7300 0 timeout 900     370 11000    0 timeout 900     380 13000    0 false(unreach-call) 210   3900 2500 -16 timeout 900     140 12000    0 true 23   900 240 2 true .17 11 1.9 2 timeout 900   4100 12000 0 error (7) 310   4300 3700 0 timeout 900   1800 11000 0 true 3.6 220 26 2 true 25   250 300 2
reducercommutativity/avg60_true-unreach-call.i timeout 900     1000 8800    0 error (42) 870    350 11000   0 false(unreach-call) 120   4000 1200 -16 false(unreach-call) 630   4600 7000 -16 timeout 900   3100 10000 0 unknown 890   260 8300 0 timeout 900     440 10000    0 timeout 900     420 10000    0 false(unreach-call) 790   4600 9100 -16 timeout 900     140 11000    0 unknown 60   840 540 0 true .18 11 2.6 2 timeout 900   2900 9600 0 error (7) 800   5000 11000 0 timeout 900   1700 11000 0 true 3.6 220 23 2 true 25   260 340 2
reducercommutativity/avg_true-unreach-call_true-termination.i timeout 900     1600 7200    0 error (42) 870    220 11000   0 timeout 900   7800 8000 0 false(unreach-call) 5.8 410 50 -16 timeout 900   3000 7700 0 unknown 890   180 10000 0 timeout 900     150 12000    0 timeout 900     140 13000    0 false(unreach-call) 13   610 100 -16 true .51  12 6.4  2 unknown 26   710 230 0 unknown .21 12 2.1 0 timeout 900   660 9900 0 timeout 900   510 12000 0 timeout 900   2900 9900 0 true 2.0 150 17 2 unknown 330   270 4700 0
reducercommutativity/max05_true-unreach-call_true-termination.i true 6.0   89 85    2 true 2.4  35 27   2 false(unreach-call) 8.5 520 72 -16 false(unreach-call) 5.6 300 51 -16 true 210   2400 1600 2 timeout 900   1500 10000 0 true .65  28 8.3  2 true .70  28 9.1  2 timeout 900   4500 13000 0 true 14     15 200    2 true 17   450 200 2 true 3.9  14 53   2 timeout 900   1600 10000 0 timeout 900   11000 11000 0 timeout 910   8000 10000 0 true 4.1 220 32 2 true 180   250 2100 2
reducercommutativity/max10_true-unreach-call_true-termination.i true 300     480 3800    2 true 87    66 970   2 false(unreach-call) 14   520 100 -16 false(unreach-call) 7.2 430 64 -16 timeout 900   2700 6600 0 timeout 900   2400 8700 0 true 17     44 210    2 true 17     42 200    2 timeout 900   4300 12000 0 unknown 900     110 10000    0 true 18   450 200 2 true 200    20 3300   2 timeout 900   2400 10000 0 timeout 900   13000 12000 0 timeout 900   2000 14000 0 true 4.3 220 32 2 true 250   450 3200 2
reducercommutativity/max20_true-unreach-call.i timeout 900     1000 11000    0 error (42) 870    200 11000   0 false(unreach-call) 18   710 140 -16 false(unreach-call) 11   540 93 -16 timeout 900   2900 10000 0 unknown 890   190 11000 0 timeout 900     140 11000    0 timeout 900     140 10000    0 timeout 900   4400 12000 0 unknown 900     180 11000    0 true 22   560 230 2 timeout (timeout) 900    58 13000   0 timeout 900   3400 10000 0 timeout 900   6200 15000 0 timeout 900   2300 11000 0 true 4.0 220 33 2 true 370   680 4200 2
reducercommutativity/max40_true-unreach-call.i timeout 900     1400 9000    0 error (42) 870    230 14000   0 timeout 900   4400 12000 0 false(unreach-call) 370   3000 4800 -16 timeout 900   2200 11000 0 unknown 890   270 7900 0 timeout 900     190 13000    0 timeout 900     190 13000    0 false(unreach-call) 540   4100 6600 -16 unknown 900     210 12000    0 unknown 47   740 520 0 timeout (timeout) 900    89 12000   0 timeout 900   4400 11000 0 timeout 900   7400 9400 0 timeout 900   1900 11000 0 true 4.1 230 32 2 true 250   640 3100 2
reducercommutativity/max60_true-unreach-call.i timeout 900     1900 5600    0 error (42) 870    260 9500   0 timeout 900   4400 11000 0 timeout 900   4000 12000 0 timeout 900   3600 8700 0 unknown 890   230 8900 0 timeout 900     260 11000    0 timeout 900     250 12000    0 timeout 900   4200 10000 0 unknown 900     240 11000    0 unknown 24   690 240 0 timeout (timeout) 900    130 12000   0 timeout 900   2900 9900 0 timeout 900   6800 7600 0 timeout 900   2100 10000 0 true 4.1 220 28 2 true 250   450 3100 2
reducercommutativity/max_true-unreach-call_true-termination.i timeout 900     2500 3700    0 error (42) 870    230 12000   0 false(unreach-call) 260   3200 3100 -16 false(unreach-call) 9.2 470 75 -16 timeout 900   5300 8400 0 unknown 890   250 9400 0 timeout 900     110 11000    0 timeout 900     100 13000    0 false(unreach-call) 31   1500 260 -16 true .51  12 5.5  2 unknown 22   680 200 0 unknown .21 11 2.3 0 timeout 900   1200 11000 0 timeout 900   2900 13000 0 timeout 900   3200 13000 0 true 7.0 160 76 2 unknown 340   560 4500 0
reducercommutativity/sep05_true-unreach-call_true-termination.i true 2.1   69 24    2 true .93 35 8.9 2 false(unreach-call) 13   500 100 -16 false(unreach-call) 6.5 360 56 -16 true 860   3800 11000 2 true 790   1600 9900 2 true .11  26 .89 2 true .17  27 1.7  2 true 160   3800 1800 2 true 3.5   12 52    2 true 6.7 350 63 2 true .17 11 1.9 2 timeout 900   1700 13000 0 timeout 900   4600 7300 0 timeout 900   1600 13000 0 true 120   720 1200 2 unknown 350   440 4600 0
reducercommutativity/sep10_true-unreach-call.i true 3.3   100 41    2 true 1.5  38 18   2 false(unreach-call) 34   1200 240 -16 false(unreach-call) 14   660 100 -16 timeout 900   5300 7200 0 timeout 900   4900 9200 0 true .10  26 1.2  2 true .19  27 1.8  2 timeout 900   4500 11000 0 true 150     35 1600    2 true 9.8 420 84 2 true .19 11 1.9 2 timeout 910   8000 13000 0 timeout 900   6100 13000 0 timeout 900   2000 13000 0 true 130   950 1300 2 unknown 350   470 4800 0
reducercommutativity/sep20_true-unreach-call.i true 12     280 120    2 true 4.8  48 59   2 false(unreach-call) 140   3900 1600 -16 false(unreach-call) 63   3200 670 -16 timeout 900   4300 8600 0 unknown 900   190 10000 0 true .17  26 1.4  2 true .23  27 2.2  2 timeout 900   4600 12000 0 timeout 900     3500 8400    0 unknown 37   800 410 0 true .19 11 2.1 2 timeout 900   7100 9700 0 timeout 910   13000 8400 0 timeout 900   2600 13000 0 true 150   1100 1600 2 unknown 350   510 4200 0
reducercommutativity/sep40_true-unreach-call.i timeout 900     1400 9300    0 true 35    87 490   2 timeout 910   9900 6900 0 false(unreach-call) 850   9200 7100 -16 timeout 900   2700 9600 0 unknown 900   190 9400 0 true .21  26 2.2  2 true .30  27 3.3  2 false(unreach-call) 640   4500 8500 -16 unknown 900     3300 6200    0 unknown 41   920 410 0 true .18 11 2.3 2 timeout 900   3900 11000 0 timeout 910   13000 8400 0 timeout 900   1800 14000 0 true 220   830 2500 2 unknown 350   510 4500 0
reducercommutativity/sep60_true-unreach-call.i timeout 900     2200 9400    0 true 150    160 2100   2 timeout 910   10000 7700 0 timeout 910   9700 7300 0 timeout 900   3800 9000 0 unknown 890   190 9400 0 true .33  26 3.5  2 true .39  28 4.2  2 timeout 910   4200 11000 0 unknown 900     3400 6800    0 unknown 21   690 190 0 true .21 11 2.2 2 timeout 900   3000 10000 0 timeout 900   13000 8100 0 timeout 900   1900 11000 0 timeout 900   510 11000 0 unknown 350   470 4100 0
reducercommutativity/sep_true-unreach-call_true-termination.i timeout 900     10000 7000    0 error (42) 880    9700 4300   0 timeout 900   3900 12000 0 false(unreach-call) 880   6700 12000 -16 timeout 900   5600 7400 0 unknown 890   190 7500 0 timeout 900     120 12000    0 timeout 900     130 10000    0 false(unreach-call) 390   4100 4900 -16 true .50  12 6.1  2 unknown 19   680 190 0 unknown .20 12 2.4 0 timeout 900   1500 11000 0 timeout 900   1800 13000 0 timeout 900   4600 13000 0 timeout 900   2700 11000 0 unknown 240   500 2900 0
reducercommutativity/sum05_true-unreach-call_true-termination.i true 20     170 270    2 true 4.7  39 56   2 false(unreach-call) 5.3 320 43 -16 false(unreach-call) 5.2 320 37 -16 timeout 900   2000 11000 0 timeout 900   4000 10000 0 true .12  26 .88 2 true .14  27 1.8  2 true 46   1600 310 2 true .42  11 4.4  2 true 16   650 180 2 true .19 11 2.1 2 true 310   3200 3700 2 true 40   2600 370 2 timeout 900   6000 6600 0 true 3.6 220 24 2 true 43   240 500 2
reducercommutativity/sum10_true-unreach-call_true-termination.i timeout 900     760 11000    0 true 180    130 2200   2 false(unreach-call) 6.5 360 46 -16 false(unreach-call) 7.3 430 59 -16 timeout 900   6500 7300 0 timeout 900   1900 13000 0 true .099 26 1.0  2 true .15  27 1.9  2 true 110   3100 1400 2 timeout 900     56 12000    0 true 17   420 170 2 true .19 11 2.2 2 timeout 900   5700 9400 0 true 230   4500 2700 2 timeout 900   5100 6800 0 true 3.4 220 24 2 true 26   250 310 2
reducercommutativity/sum20_true-unreach-call.i timeout 900     720 8100    0 error (42) 870    270 10000   0 false(unreach-call) 8.1 480 68 -16 false(unreach-call) 11   620 110 -16 timeout 900   4400 9100 0 unknown 890   240 8100 0 true .14  26 1.5  2 true .20  27 2.4  2 true 690   4000 9000 2 true .57  12 7.5  2 true 17   450 210 2 true .20 11 2.0 2 timeout 900   4700 11000 0 timeout 900   5300 6400 0 timeout 900   4700 12000 0 true 3.4 220 23 2 true 320   600 3600 2
reducercommutativity/sum40_true-unreach-call.i timeout 900     860 8600    0 error (42) 870    270 11000   0 false(unreach-call) 55   2500 480 -16 false(unreach-call) 160   3500 1800 -16 timeout 900   3600 8200 0 unknown 890   200 9000 0 true .17  26 2.2  2 true .23  27 2.6  2 false(unreach-call) 210   3900 2300 -16 true .70  12 9.4  2 true 21   670 190 2 true .19 11 2.2 2 timeout 900   4600 12000 0 timeout 900   5200 11000 0 timeout 900   1700 11000 0 true 3.5 220 24 2 true 26   250 330 2
reducercommutativity/sum60_true-unreach-call.i timeout 900     1000 6100    0 error (42) 870    270 9900   0 false(unreach-call) 120   3900 1100 -16 false(unreach-call) 630   4500 7200 -16 timeout 900   3500 9600 0 unknown 890   230 6900 0 true .25  26 2.7  2 true .32  27 3.2  2 false(unreach-call) 800   4600 9100 -16 true .93  12 12    2 unknown 25   720 240 0 true .19 11 2.1 2 timeout 900   2400 10000 0 timeout 900   5600 8400 0 timeout 900   1700 10000 0 true 3.6 220 23 2 true 25   250 300 2
reducercommutativity/sum_true-unreach-call_true-termination.i timeout 900     1900 8000    0 error (42) 870    220 13000   0 false(unreach-call) 93   3600 1000 -16 false(unreach-call) 4.9 310 41 -16 timeout 900   5500 8800 0 unknown 890   200 9000 0 timeout 900     150 12000    0 timeout 900     130 11000    0 false(unreach-call) 9.2 470 76 -16 true .49  12 5.8  2 unknown 22   690 220 0 unknown .20 12 2.2 0 timeout 900   4900 8400 0 timeout 900   2000 13000 0 timeout 900   4700 6400 0 true 1.7 150 15 2 unknown 330   460 4600 0
array-tiling/mlceu_false-unreach-call.i out of memory 670     15000 3200    0 error (42) 870    5800 8700   0 error 58   2900 560 0 false(unreach-call) 3.4 280 31 0 timeout 900   6700 6900 0 timeout 900   3500 7800 0 timeout 900     180 11000    0 timeout 900     180 13000    0 timeout 900   5100 14000 0 true .45  12 4.9  -32 unknown 170   730 1900 0 unknown .17 12 2.2 0 timeout 900   1600 12000 0 timeout 900   3100 11000 0 timeout 900   1100 12000 0 false(unreach-call) 15   220 110 0 unknown 17   120 260 0
array-tiling/skippedu_false-unreach-call.i false(unreach-call) .33  38 3.4  1 false(unreach-call) .26 33 2.8 1 false(unreach-call) 3.9 300 34 1 false(unreach-call) 3.6 290 30 1 false(unreach-call) 3.4 270 30 1 false(unreach-call) 1.1 100 13 0 false(unreach-call) .13  28 1.9  1 false(unreach-call) .14  28 1.4  1 false(unreach-call) 160   3700 1900 0 unknown .055 11 .27 0 unknown 200   720 2200 0 unknown .21 12 2.4 0 false(unreach-call) 6.4 290 58 1 false(unreach-call) 5.2 290 43 1 false(unreach-call) 7.5 370 62 1 false(unreach-call) 22   220 190 0 unknown 89   490 1100 0
array-tiling/mbpr2_true-unreach-call.i out of memory 510     15000 2500    0 error (134) 81    13000 690   0 error 50   2400 440 0 false(unreach-call) 4.0 300 36 -16 timeout 900   5800 8000 0 unknown 890   160 10000 0 timeout 900     240 13000    0 timeout 900     180 13000    0 false(unreach-call) 42   2200 330 -16 unknown .068 11 .23 0 unknown 57   730 640 0 unknown .21 11 2.0 0 error (7) 20   330 220 0 timeout 900   880 12000 0 error (7) 23   360 240 0 true 16   220 120 2 true 38   200 430 2
array-tiling/mbpr3_true-unreach-call.i out of memory 410     15000 2000    0 error (134) 230    13000 1400   0 error 56   2500 490 0 false(unreach-call) 4.5 310 38 -16 timeout 900   6500 7700 0 unknown 890   220 9700 0 timeout 900     240 11000    0 timeout 900     180 11000    0 false(unreach-call) 380   3900 4300 -16 unknown .035 11 .41 0 unknown 41   740 380 0 unknown .21 12 2.2 0 timeout 900   1300 10000 0 timeout 900   1100 12000 0 error (7) 29   560 280 0 true 20   220 140 2 true 57   200 750 2
array-tiling/mbpr4_true-unreach-call.i out of memory 440     15000 2600    0 error (134) 210    13000 2000   0 error 45   1800 380 0 false(unreach-call) 5.0 310 48 -16 timeout 900   6800 8400 0 unknown 890   300 9100 0 timeout 900     200 12000    0 timeout 900     210 10000    0 false(unreach-call) 94   3700 900 -16 unknown .035 11 .31 0 unknown 34   850 350 0 unknown .20 12 2.5 0 error (7) 21   380 160 0 timeout 900   920 11000 0 timeout 900   830 11000 0 true 28   220 250 2 true 100   360 1500 2
array-tiling/mbpr5_true-unreach-call.i timeout 900     12000 4400    0 error (134) 150    14000 1400   0 error 47   1700 430 0 false(unreach-call) 5.6 320 48 -16 timeout 900   5800 9500 0 unknown 890   350 9600 0 timeout 900     210 11000    0 timeout 900     190 11000    0 false(unreach-call) 650   4200 8000 -16 unknown .058 12 .27 0 unknown 42   750 450 0 unknown .22 12 2.3 0 error (7) 93   790 980 0 timeout 900   1100 12000 0 error (7) 26   550 220 0 true 38   230 350 2 true 330   6200 4100 2
array-tiling/nr2_true-unreach-call.i out of memory 680     15000 3300    0 error (134) 60    14000 720   0 error 48   1900 430 0 false(unreach-call) 3.8 290 37 -16 timeout 900   5800 6100 0 unknown 890   420 8900 0 timeout 900     220 11000    0 timeout 900     220 13000    0 false(unreach-call) 520   4200 7700 -16 unknown .061 11 .19 0 unknown 140   730 1700 0 unknown .21 11 2.3 0 timeout 900   2400 11000 0 timeout 900   2300 12000 0 timeout 900   1500 11000 0 timeout 900   6000 11000 0 true 31   230 430 2
array-tiling/nr3_true-unreach-call.i out of memory 490     15000 4500    0 error (134) 56    13000 660   0 error 45   2000 370 0 false(unreach-call) 3.8 300 34 -16 timeout 900   6500 8400 0 unknown 890   470 8900 0 timeout 900     160 13000    0 timeout 900     190 13000    0 false(unreach-call) 99   3700 1000 -16 unknown .062 11 .26 0 unknown 160   840 1900 0 unknown .22 12 2.2 0 timeout 900   830 13000 0 timeout 900   2500 11000 0 timeout 900   980 12000 0 timeout 900   3000 12000 0 true 30   220 490 2
array-tiling/nr4_true-unreach-call.i out of memory 400     15000 2100    0 error (134) 84    13000 960   0 error 33   1200 300 0 false(unreach-call) 3.8 290 33 -16 timeout 900   4800 9600 0 unknown 890   440 8700 0 timeout 900     220 12000    0 timeout 900     160 12000    0 false(unreach-call) 430   4100 5600 -16 unknown .041 11 .37 0 unknown 170   750 1700 0 unknown .22 12 2.3 0 timeout 900   890 10000 0 timeout 900   1900 14000 0 timeout 900   790 11000 0 timeout 900   220 14000 0 true 30   230 410 2
array-tiling/nr5_true-unreach-call.i out of memory 590     15000 4100    0 error (134) 110    13000 870   0 error 30   1200 240 0 false(unreach-call) 3.8 300 37 -16 timeout 900   5700 7000 0 unknown 890   450 10000 0 timeout 900     140 11000    0 timeout 900     160 13000    0 false(unreach-call) 510   4300 6800 -16 unknown .062 11 .25 0 unknown 180   760 2000 0 unknown .20 12 2.3 0 timeout 900   870 11000 0 timeout 900   2000 11000 0 timeout 900   990 13000 0 timeout 900   2000 11000 0 true 30   230 380 2
array-tiling/pnr2_true-unreach-call.i out of memory 560     15000 3500    0 error (134) 660    13000 5100   0 error 5.1 300 42 0 false(unreach-call) 3.6 300 33 -16 timeout 900   3800 6600 0 unknown 890   140 11000 0 timeout 900     260 10000    0 timeout 900     220 11000    0 false(unreach-call) 77   3700 810 -16 unknown .039 11 .29 0 unknown 26   720 250 0 unknown .22 12 2.0 0 timeout 900   2300 12000 0 timeout 900   1800 14000 0 timeout 900   1400 11000 0 true 16   220 110 2 true 30   220 420 2
array-tiling/pnr3_true-unreach-call.i out of memory 580     15000 2700    0 error (42) 870    3700 4500   0 error 4.4 310 35 0 false(unreach-call) 3.7 310 34 -16 timeout 900   4300 5600 0 unknown 890   200 14000 0 timeout 900     270 11000    0 timeout 900     240 13000    0 false(unreach-call) 71   3700 740 -16 unknown .062 11 .27 0 unknown 28   720 280 0 unknown .19 12 2.1 0 timeout 900   1700 12000 0 timeout 900   1700 13000 0 timeout 900   1500 11000 0 true 18   220 130 2 true 31   220 420 2
array-tiling/pnr4_true-unreach-call.i out of memory 530     15000 1800    0 error (42) 870    6200 5600   0 error 4.6 320 40 0 false(unreach-call) 3.7 290 31 -16 timeout 900   4000 6800 0 unknown 890   240 9600 0 timeout 900     280 8700    0 timeout 900     280 11000    0 false(unreach-call) 81   3700 820 -16 unknown .061 11 .24 0 unknown 28   720 290 0 unknown .21 12 2.0 0 timeout 900   2600 12000 0 timeout 900   2100 13000 0 timeout 900   3200 12000 0 true 26   220 230 2 true 40   210 590 2
array-tiling/pnr5_true-unreach-call.i out of memory 350     15000 1800    0 error (42) 870    2700 5800   0 error 4.7 310 38 0 false(unreach-call) 4.0 310 31 -16 timeout 900   4300 7400 0 unknown 890   280 8800 0 timeout 900     290 10000    0 timeout 900     430 11000    0 false(unreach-call) 90   3700 1000 -16 unknown .072 11 .25 0 unknown 30   740 290 0 unknown .22 12 2.3 0 timeout 900   3400 12000 0 timeout 900   4700 13000 0 timeout 900   1900 9900 0 true 94   220 1200 2 true 57   210 640 2
array-tiling/poly1_true-unreach-call.i timeout 900     10000 4200    0 error (42) 880    11000 7500   0 error 41   1600 370 0 false(unreach-call) 3.5 290 35 -16 timeout 900   4100 7400 0 unknown 890   190 12000 0 unknown .10  26 .80 0 unknown .10  26 .73 0 timeout 900   5200 12000 0 true .43  12 4.7  2 true 120   1400 1100 2 unknown .20 12 2.0 0 timeout 900   930 11000 0 timeout 900   1300 12000 0 true 5.9 300 53 2 true 1.7 160 15 2 true 13   140 190 2
array-tiling/poly2_true-unreach-call.i timeout 900     11000 4700    0 error (134) 160    13000 1600   0 error 100   3800 890 0 false(unreach-call) 3.7 280 30 -16 timeout 900   5200 6400 0 unknown 890   160 10000 0 unknown .058 15 .29 0 unknown .033 15 .27 0 timeout 910   4900 13000 0 unknown .071 11 .31 0 unknown 220   1400 2400 0 unknown 74    40 280   0 timeout 900   1700 11000 0 timeout 900   2700 12000 0 true 8.1 390 63 2 true 1.9 160 17 2 true 16   150 200 2
array-tiling/pr2_true-unreach-call.i out of memory 460     15000 2800    0 error (134) 130    13000 1700   0 error 7.7 430 70 0 false(unreach-call) 3.6 280 37 -16 timeout 900   4100 6200 0 unknown 890   260 11000 0 timeout 900     230 12000    0 timeout 900     270 14000    0 false(unreach-call) 68   3600 690 -16 unknown .040 11 .33 0 true 4.3 270 43 2 unknown .20 12 2.3 0 timeout 900   1200 11000 0 timeout 900   1200 14000 0 timeout 900   900 11000 0 true 16   220 110 2 true 30   220 400 2
array-tiling/pr3_true-unreach-call.i out of memory 380     15000 2100    0 error (134) 220    13000 1800   0 error 5.1 330 46 0 false(unreach-call) 4.0 300 34 -16 timeout 900   3800 6900 0 unknown 890   230 11000 0 timeout 900     240 12000    0 timeout 900     250 12000    0 false(unreach-call) 63   3600 560 -16 unknown .036 11 .35 0 true 4.6 360 37 2 unknown .21 12 2.1 0 timeout 900   1200 14000 0 timeout 900   1200 12000 0 timeout 900   1000 10000 0 true 19   220 140 2 true 33   230 400 2
array-tiling/pr4_true-unreach-call.i out of memory 400     15000 2100    0 error (134) 280    13000 2300   0 error 4.9 310 43 0 false(unreach-call) 3.8 290 36 -16 timeout 900   3800 7100 0 unknown 890   240 9500 0 timeout 900     390 11000    0 timeout 900     280 13000    0 false(unreach-call) 66   3700 700 -16 unknown .063 11 .27 0 true 4.4 270 43 2 unknown .20 12 3.0 0 timeout 900   910 13000 0 timeout 900   970 11000 0 timeout 900   760 13000 0 true 27   210 230 2 true 41   210 510 2
array-tiling/pr5_true-unreach-call.i out of memory 280     15000 2100    0 error (42) 880    9500 3900   0 error 5.6 340 52 0 false(unreach-call) 4.0 310 33 -16 timeout 900   3600 6400 0 unknown 890   280 9500 0 timeout 900     280 12000    0 timeout 900     290 12000    0 false(unreach-call) 70   3700 790 -16 unknown .059 11 .26 0 true 4.3 270 39 2 unknown .22 11 2.2 0 timeout 900   1300 11000 0 timeout 900   950 11000 0 timeout 900   1100 11000 0 true 29   220 290 2 true 65   230 740 2
array-tiling/revcpyswp2_true-unreach-call.i timeout 900     11000 5500    0 error (42) 870    1400 5600   0 error 4.8 310 44 0 false(unreach-call) 4.4 290 37 -16 timeout 900   4200 7300 0 timeout 900   5600 8100 0 timeout 900     250 12000    0 timeout 900     240 11000    0 timeout 900   4900 12000 0 true .51  12 5.7  2 unknown 41   750 410 0 unknown .18 12 2.4 0 timeout 900   1600 14000 0 timeout 900   5200 12000 0 timeout 900   1000 11000 0 timeout 900   3700 7400 0 true 130   440 1600 2
array-tiling/rew_true-unreach-call.i out of memory 540     15000 2900    0 error (134) 470    14000 3500   0 error 40   1500 360 0 false(unreach-call) 3.6 290 33 -16 timeout 900   5100 7400 0 timeout 900   3400 9100 0 timeout 900     210 11000    0 timeout 900     230 11000    0 false(unreach-call) 530   4100 6500 -16 true .46  12 4.7  2 unknown 6.8 340 55 0 unknown .20 12 2.1 0 timeout 900   2000 10000 0 timeout 900   1900 12000 0 timeout 900   1500 12000 0 true 17   220 130 2 true 15   150 200 2
array-tiling/rewnif_true-unreach-call.i out of memory 500     15000 3300    0 error (134) 660    14000 5900   0 error 46   1500 300 0 false(unreach-call) 3.6 290 33 -16 timeout 900   4600 6700 0 timeout 900   4900 10000 0 timeout 900     210 11000    0 timeout 900     200 12000    0 false(unreach-call) 360   4000 4200 -16 true .47  12 4.6  2 unknown 6.8 350 52 0 unknown .19 12 2.0 0 timeout 900   1200 13000 0 timeout 900   2100 14000 0 timeout 900   1200 9900 0 true 24   220 210 2 true 15   170 210 2
array-tiling/rewnifrev2_true-unreach-call.i out of memory 610     15000 4700    0 error (6) 130    14000 1100   0 false(unreach-call) 4.8 300 44 -16 false(unreach-call) 3.4 290 31 -16 timeout 900   3800 7800 0 timeout 900   5000 8400 0 timeout 900     380 11000    0 timeout 900     350 11000    0 false(unreach-call) 87   3700 930 -16 true .81  12 10    2 unknown 160   720 2000 0 unknown .21 12 2.1 0 timeout 900   3100 9300 0 timeout 900   2900 10000 0 timeout 900   2600 8400 0 true 40   220 430 2 unknown 170   310 2100 0
array-tiling/rewnifrev_true-unreach-call.i out of memory 560     15000 3900    0 error (134) 130    14000 1300   0 error 3.6 290 34 0 false(unreach-call) 3.9 290 37 -16 timeout 900   4300 6800 0 timeout 900   2600 11000 0 timeout 900     390 10000    0 timeout 900     400 11000    0 false(unreach-call) 160   3800 2400 -16 true .88  12 12    2 unknown 91   750 960 0 unknown .20 12 2.2 0 timeout 900   2100 10000 0 timeout 900   4300 14000 0 timeout 900   1100 11000 0 unknown 780   220 9500 0 true 66   330 570 2
array-tiling/rewrev_true-unreach-call.i out of memory 580     15000 3300    0 error (134) 120    14000 1500   0 timeout 900   1000 13000 0 false(unreach-call) 3.9 300 37 -16 timeout 900   4500 6800 0 timeout 900   3800 11000 0 timeout 900     410 11000    0 timeout 900     330 12000    0 false(unreach-call) 90   3700 1100 -16 true .84  12 11    2 true 32   720 390 2 unknown .22 12 2.3 0 timeout 900   2200 12000 0 timeout 900   2600 11000 0 timeout 900   1400 12000 0 true 25   220 250 2 true 16   210 210 2
array-tiling/skipped_true-unreach-call.i out of memory 780     15000 2800    0 error (134) 560    14000 4900   0 error 4.2 310 39 0 false(unreach-call) 3.7 290 32 -16 timeout 900   3100 7300 0 unknown 890   100 11000 0 timeout 900     230 8300    0 timeout 900     390 11000    0 false(unreach-call) 77   3200 830 -16 unknown .039 11 .27 0 unknown 190   720 2500 0 unknown .20 12 2.2 0 timeout 900   1500 12000 0 timeout 900   840 12000 0 timeout 900   1400 12000 0 true 20   220 150 2 unknown 130   610 1400 0
array-tiling/tcpy_true-unreach-call.i timeout 900     14000 6500    0 error (42) 870    1000 4200   0 error 3.7 300 37 0 true 3.6 280 33 2 timeout 900   3500 6700 0 unknown 890   170 14000 0 timeout 900     180 13000    0 timeout 900     170 11000    0 false(unreach-call) 34   1700 270 -16 unknown .064 11 .30 0 unknown 170   760 2200 0 unknown .23 12 2.3 0 timeout 900   2600 10000 0 timeout 900   1800 11000 0 timeout 900   2500 11000 0 true 20   220 160 2 true 30   220 440 2
array-programs/copysome1_false-unreach-call.i out of memory 25     15000 310    0 error (134) 130    15000 1500   0 error 2.5 260 21 0 error 2.5 270 22 0 timeout 900   11000 9300 0 unknown 890   280 10000 0 timeout 900     9300 10000    0 timeout 900     9700 9400    0 timeout 900   4200 11000 0 unknown 900     140 11000    0 unknown 31   690 300 0 unknown 3.2  270 41   0 timeout 900   4300 8800 0 timeout 900   4900 12000 0 timeout 900   2500 9500 0 false(unreach-call) 18   3100 130 0 false(unreach-call) 22   1300 290 0
array-programs/copysome2_false-unreach-call.i out of memory 27     15000 340    0 error (134) 130    14000 1800   0 error 2.6 270 23 0 error 2.5 270 20 0 timeout 900   8700 9300 0 unknown 890   310 9300 0 timeout 900     9600 10000    0 timeout 900     9600 10000    0 timeout 900   4000 11000 0 unknown 900     150 12000    0 unknown 6.5 330 56 0 unknown 3.2  270 36   0 timeout 900   3300 9400 0 timeout 900   5000 14000 0 timeout 900   2800 8400 0 false(unreach-call) 19   4900 150 0 false(unreach-call) 26   1600 350 0
array-programs/copysome1_true-unreach-call.i out of memory 25     15000 340    0 error (134) 130    15000 2100   0 error 2.5 270 24 0 error 2.5 260 22 0 timeout 900   9500 8500 0 unknown 890   280 7900 0 timeout 900     9700 10000    0 timeout 900     9700 9400    0 timeout 900   4200 11000 0 unknown 900     140 11000    0 unknown 31   690 350 0 unknown 3.2  270 41   0 timeout 900   2600 9000 0 timeout 900   4900 13000 0 timeout 900   2800 9200 0 true 16   220 100 2 true 71   230 960 2
array-programs/copysome2_true-unreach-call.i out of memory 27     15000 380    0 error (134) 130    14000 1700   0 error 2.6 270 25 0 error 2.5 260 22 0 timeout 900   7600 9800 0 unknown 890   260 9300 0 timeout 900     9600 9700    0 timeout 900     9600 12000    0 timeout 900   4000 11000 0 unknown 890     140 11000    0 unknown 6.4 320 55 0 unknown 3.1  270 36   0 timeout 900   3200 8800 0 timeout 900   4900 11000 0 timeout 900   2800 10000 0 true 17   220 110 2 true 97   270 1200 2
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
total 167 38000    1900000 300000   -55 167 46000   1800000 440000 26 167 21000   200000 220000 -297 167 16000   160000 170000 -758 167 140000 870000 1400000 16 167 140000 160000 1500000 3 167 130000 790000 1500000 34 167 130000 780000 1500000 38 167 120000 690000 1600000 -545 167 52000    260000 650000   34 167 7500 100000 81000 52 167 27000 270000 300000 146 167 140000 590000 1600000 16 167 140000 720000 1800000 15 167 140000 360000 1600000 18 167 35000 310000 420000 235 167 15000 82000 180000 209
    correct results 13 600    60000 7500   25 15 1000   1000 13000 26 6 47   2600 380 7 8 340   11000 3500 10 10 1700 15000 20000 16 2 1300 1800 16000 3 20 570 800 6700 34 22 580 970 7000 38 10 2400 29000 29000 15 68 1700    1300 19000   130 29 480 15000 4700 52 88 350 10000 5200 146 10 390 6900 4500 16 10 380 11000 4100 15 11 150 5600 1300 18 126 10000 99000 120000 235 115 7000 50000 86000 209
        correct true 12 600    60000 7500   24 11 1000   860 12000 22 1 2.8 280 29 2 2 6.4 550 58 4 6 1300 12000 15000 12 1 790 1600 9900 2 14 550 600 6400 28 16 550 660 6700 32 5 1000 13000 12000 10 62 1700    1100 19000   124 23 430 12000 4300 46 58 280 4000 4400 116 6 340 4800 4000 12 5 290 8000 3200 10 7 52 2600 430 14 109 2200 28000 19000 218 94 6600 34000 80000 188
        correct false 1 .33 38 3.4 1 4 2.9 160 31 4 5 44   2300 350 5 6 340   10000 3400 6 4 490 3800 5000 4 1 490 210 6000 1 6 24 190 240 6 6 28 310 280 6 5 1400 16000 17000 5 6 12    150 170   6 6 52 2500 490 6 30 69 6100 890 30 4 51 2100 480 4 5 89 3200 870 5 4 100 3000 880 4 17 7800 71000 100000 17 21 460 16000 6300 21
    correct-unconfimed results 0 3 16   130 200 0 0 2 19   930 140 0 0 4 1600 740 21000 0 1 180 170 2600 0 1 180 170 2500 0 2 180 4700 2000 0 1 .57 13 7.6 0 0 0 0 0 0 16 4100 33000 57000 0 9 230 16000 3000 0
        correct-unconfirmed true 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        correct-unconfirmed false 0 3 16   130 200 0 0 2 19   930 140 0 0 4 1600 740 21000 0 1 180 170 2600 0 1 180 170 2500 0 2 180 4700 2000 0 1 .57 13 7.6 0 0 0 0 0 0 16 4100 33000 57000 0 9 230 16000 3000 0
    incorrect results 3 150    38000 1700   -80 0 19 970   30000 10000 -304 48 4000   52000 44000 -768 0 0 0 0 35 8400 120000 100000 -560 3 11    59 140   -96 0 0 0 0 0 0 0
        incorrect true 2 71    27000 860   -64 0 0 0 0 0 0 0 0 3 11    59 140   -96 0 0 0 0 0 0 0
        incorrect false 1 75    11000 870   -16 0 19 970   30000 10000 -304 48 4000   52000 44000 -768 0 0 0 0 35 8400 120000 100000 -560 0 0 0 0 0 0 0 0
score (167 tasks, max score: 290) -55 26 -297 -758 16 3 34 38 -545 34 52 146 16 15 18 235 209
Run set 2ls.sv-comp18.ReachSafety-Arrays cbmc.sv-comp18.ReachSafety-Arrays cpa-bam-bnb.sv-comp18.ReachSafety-Arrays cpa-bam-slicing.sv-comp18.ReachSafety-Arrays cpa-seq.sv-comp18.ReachSafety-Arrays depthk.sv-comp18.ReachSafety-Arrays esbmc-incr.sv-comp18.ReachSafety-Arrays esbmc-kind.sv-comp18.ReachSafety-Arrays interpchecker.sv-comp18.ReachSafety-Arrays map2check.sv-comp18.ReachSafety-Arrays skink.sv-comp18.ReachSafety-Arrays symbiotic.sv-comp18.ReachSafety-Arrays uautomizer.sv-comp18.ReachSafety-Arrays ukojak.sv-comp18.ReachSafety-Arrays utaipan.sv-comp18.ReachSafety-Arrays veriabs.sv-comp18.ReachSafety-Arrays viap.sv-comp18.ReachSafety-Arrays