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-Loops cbmc.sv-comp18.ReachSafety-Loops cpa-bam-bnb.sv-comp18.ReachSafety-Loops cpa-bam-slicing.sv-comp18.ReachSafety-Loops cpa-seq.sv-comp18.ReachSafety-Loops depthk.sv-comp18.ReachSafety-Loops esbmc-incr.sv-comp18.ReachSafety-Loops esbmc-kind.sv-comp18.ReachSafety-Loops interpchecker.sv-comp18.ReachSafety-Loops map2check.sv-comp18.ReachSafety-Loops skink.sv-comp18.ReachSafety-Loops symbiotic.sv-comp18.ReachSafety-Loops uautomizer.sv-comp18.ReachSafety-Loops ukojak.sv-comp18.ReachSafety-Loops utaipan.sv-comp18.ReachSafety-Loops veriabs.sv-comp18.ReachSafety-Loops viap.sv-comp18.ReachSafety-Loops
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
loops/array_false-unreach-call_true-termination.i false(unreach-call) .15  24 .97 1 false(unreach-call) .22 33 2.4 1 false(unreach-call) 3.5 290 29 1 false(unreach-call) 3.4 290 29 1 false(unreach-call) 3.4 270 32 1 false(unreach-call) 1.1  75 19   0 false(unreach-call) .22  28 2.2  1 false(unreach-call) .22  28 2.1  1 false(unreach-call) 4.6 290 42 1 true .43  12 4.7  -32 false(unreach-call) 5.4 310 53 1 false(unreach-call) .19 12 1.8 1 false(unreach-call) 4.8 280 39 1 false(unreach-call) 4.7 280 43 1 false(unreach-call) 4.9 270 39 1 false(unreach-call) 1.8 150 17 1 unknown 25   160 380 0
loops/bubble_sort_false-unreach-call.i error (134) .25  27 2.0  0 false(unreach-call) 2.1  200 24   0 false(unreach-call) 5.3 310 42 1 false(unreach-call) 5.0 300 43 1 false(unreach-call) 4.9 310 43 1 false(unreach-call) 3.0  240 36   0 false(unreach-call) 5.5   140 61    1 false(unreach-call) 7.3   230 79    1 timeout 900   4400 12000 0 unknown .39  12 4.2  0 unknown 8.7 460 82 0 false(unreach-call) .26 12 2.7 1 error (7) 8.0 230 67 0 error (7) 7.8 230 70 0 error (7) 7.7 240 58 0 unknown 330   700 2500 0 unknown 2.5 92 33 0
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) .11  22 .68 1 false(unreach-call) .22 33 2.2 1 false(unreach-call) 3.2 280 31 1 false(unreach-call) 3.1 280 29 1 false(unreach-call) 2.5 250 21 1 false(unreach-call) .54 75 5.6 1 false(unreach-call) .20  28 1.4  1 false(unreach-call) .20  28 2.0  1 false(unreach-call) 2.8 280 26 1 false(unreach-call) .35  11 3.7  1 false(unreach-call) 5.1 310 46 1 false(unreach-call) .16 11 1.9 1 false(unreach-call) 4.2 260 35 1 false(unreach-call) 4.2 250 35 1 false(unreach-call) 4.4 270 38 1 false(unreach-call) 11   280 79 1 unknown 11   110 160 0
loops/eureka_01_false-unreach-call_true-termination.i false(unreach-call) 1.1   60 13    1 false(unreach-call) .89 36 8.3 1 error 13   480 110 0 true 23   860 190 -32 timeout 900   4400 11000 0 false(unreach-call) 2.9  190 34   0 false(unreach-call) .48  28 4.0  0 false(unreach-call) .79  29 8.0  0 false(unreach-call) 20   830 170 0 false(unreach-call) 2.6   13 33    1 unknown 58   760 660 0 false(unreach-call) .97 15 13   0 false(unreach-call) 110   1700 1300 1 false(unreach-call) 94   2000 1200 1 false(unreach-call) 130   1500 1600 1 false(unreach-call) 480   370 6200 0 true 110   400 1200 -32
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) .20  25 1.8  1 false(unreach-call) .26 33 2.0 1 false(unreach-call) 3.7 300 35 1 false(unreach-call) 3.5 280 31 0 false(unreach-call) 3.6 270 33 1 false(unreach-call) 1.2  76 14   1 false(unreach-call) .36  28 3.7  1 false(unreach-call) .21  28 2.0  1 false(unreach-call) 3.2 260 29 1 true .52  12 5.3  -32 false(unreach-call) 5.5 330 52 1 false(unreach-call) .16 11 1.6 1 false(unreach-call) 5.9 290 51 1 false(unreach-call) 7.1 420 58 1 false(unreach-call) 6.5 320 50 1 false(unreach-call) 14   280 100 1 false(unreach-call) 12   100 170 0
loops/insertion_sort_false-unreach-call_true-termination.i false(unreach-call) 450     7700 1500    1 false(unreach-call) 1.8  190 19   1 error 4.1 300 35 0 false(unreach-call) 3.5 290 31 0 false(unreach-call) 51   2300 430 1 false(unreach-call) 3.6  130 54   1 false(unreach-call) 1.4   30 15    1 false(unreach-call) .77  28 8.5  0 false(unreach-call) 420   4100 5000 0 true .37  11 3.9  -32 unknown 7.1 340 68 0 unknown .19 11 1.9 0 false(unreach-call) 87   1100 860 1 timeout 900   680 12000 0 timeout 900   1700 9800 0 false(unreach-call) 570   3300 6400 1 unknown 220   330 2700 0
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) .71  44 10    1 false(unreach-call) .77 41 8.2 1 false(unreach-call) 5.8 340 48 1 false(unreach-call) 4.4 300 39 0 false(unreach-call) 210   2100 2900 1 false(unreach-call) 1.9  130 23   0 false(unreach-call) .59  28 5.1  1 false(unreach-call) .64  28 5.5  1 false(unreach-call) 520   4500 6600 1 unknown .38  12 4.0  0 unknown 6.3 320 55 0 unknown .22 12 2.2 0 false(unreach-call) 11   540 110 1 false(unreach-call) 13   580 110 1 false(unreach-call) 15   670 150 1 false(unreach-call) 34   340 270 1 false(unreach-call) 14   310 190 0
loops/linear_search_false-unreach-call.i error (134) .076 22 .71 0 false(unreach-call) 1.9  35 26   1 error 3.5 310 31 0 unknown 3.2 280 28 0 false(unreach-call) 13   540 99 1 false(unreach-call) 16    76 230   0 false(unreach-call) .47  28 5.2  0 false(unreach-call) .53  28 5.9  0 timeout 900   2800 11000 0 true .37  11 4.8  -32 false(unreach-call) 25   720 260 0 unknown .19 12 2.3 0 timeout 900   760 10000 0 timeout 900   4500 7100 0 timeout 900   2200 11000 0 false(unreach-call) 18   280 150 0 unknown 4.3 92 57 0
loops/ludcmp_false-unreach-call.i timeout 900     3900 6300    0 false(unreach-call) 2.6  130 35   0 false(unreach-call) 5.0 330 42 1 false(unreach-call) 3.2 270 29 1 false(unreach-call) 6.8 530 65 1 false(unreach-call) 7.1  350 79   0 false(unreach-call) .088 29 1.3  1 false(unreach-call) .18  31 2.2  1 false(unreach-call) 16   650 140 0 false(unreach-call) .39  11 4.8  1 unknown 5.6 330 45 0 false(unreach-call) .16 11 1.7 1 timeout 900   3200 12000 0 timeout 900   3400 12000 0 timeout 900   4200 12000 0 false(unreach-call) 270   1300 3500 0 false(unreach-call) 32   130 410 1
loops/matrix_false-unreach-call_true-termination.i false(unreach-call) 160     2400 630    1 false(unreach-call) .28 35 2.5 1 false(unreach-call) 3.9 300 34 1 false(unreach-call) 4.0 290 36 0 false(unreach-call) 3.7 280 31 1 false(unreach-call) 480    180 6700   1 false(unreach-call) .54  28 4.2  1 false(unreach-call) .36  28 3.0  1 false(unreach-call) 44   1900 390 1 unknown 900     410 9000    0 timeout 900   1400 8800 0 timeout (timeout) 900    1700 9700   0 false(unreach-call) 5.8 280 46 1 false(unreach-call) 6.9 370 51 1 false(unreach-call) 5.5 280 40 1 false(unreach-call) 470   3200 4600 1 unknown 230   1800 2700 0
loops/n.c24_false-unreach-call.i error (134) .20  25 1.3  0 error (134) 680    14000 3800   0 timeout 900   4400 10000 0 timeout 900   4300 11000 0 timeout 900   5000 9200 0 unknown 900    1400 8300   0 out of memory 460     15000 3700    0 out of memory 440     15000 4400    0 timeout 900   5100 12000 0 unknown 900     1500 10000    0 unknown 4.3 300 39 0 timeout (timeout) 900    1800 11000   0 timeout 900   5400 14000 0 timeout 900   4700 12000 0 timeout 900   4800 13000 0 timeout 900   3700 6100 0 unknown 4.4 92 63 0
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) .11  23 .85 1 false(unreach-call) .25 33 1.9 1 false(unreach-call) 3.3 280 29 1 false(unreach-call) 3.2 280 29 1 false(unreach-call) 2.6 260 22 1 false(unreach-call) .54 75 7.0 1 false(unreach-call) .16  28 1.1  1 false(unreach-call) .11  28 1.3  1 false(unreach-call) 2.9 270 24 1 unknown .31  11 2.9  0 false(unreach-call) 5.3 310 44 1 error (1) .12 11 1.0 0 false(unreach-call) 4.7 270 37 1 false(unreach-call) 4.6 250 35 1 false(unreach-call) 4.5 270 39 1 false(unreach-call) 18   280 120 1 false(unreach-call) 7.1 93 90 1
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1.1   75 12    1 false(unreach-call) .41 50 3.9 1 false(unreach-call) 4.1 320 32 1 false(unreach-call) 3.2 280 29 1 false(unreach-call) 2.8 260 23 1 false(unreach-call) 1.2  76 17   0 false(unreach-call) .24  28 2.1  1 false(unreach-call) .20  28 2.3  1 false(unreach-call) 3.1 270 31 1 unknown .30  11 4.0  0 false(unreach-call) 5.5 300 45 1 false(unreach-call) .17 11 2.4 1 false(unreach-call) 4.8 290 41 1 false(unreach-call) 4.9 280 37 1 false(unreach-call) 4.9 280 35 1 false(unreach-call) 23   290 190 1 unknown 15   120 230 0
loops/s3_false-unreach-call.i error (134) .73  170 9.3  0 false(unreach-call) 21    770 240   1 witness invalid (false(unreach-call)) 13   530 96 0 false(unreach-call) 16   540 120 0 false(unreach-call) 44   2500 430 1 unknown 890    1600 11000   0 false(unreach-call) 15     600 180    1 false(unreach-call) 18     740 210    1 false(unreach-call) 86   3500 770 0 unknown .096 13 .70 0 unknown 9.7 530 77 0 unknown .47 12 4.6 0 false(unreach-call) 420   1500 4800 1 error (7) 400   3300 4800 0 false(unreach-call) 170   950 1900 1 unknown 630   1800 7600 0 unknown 2.6 92 30 0
loops/string_false-unreach-call_true-termination.i false(unreach-call) .66  37 7.4  1 false(unreach-call) .64 33 7.3 1 false(unreach-call) 6.2 330 52 1 false(unreach-call) 5.3 300 48 0 false(unreach-call) 3.3 270 28 1 false(unreach-call) 4.0  190 53   0 false(unreach-call) .81  28 6.6  0 false(unreach-call) .61  28 7.5  0 false(unreach-call) 6.1 310 54 0 true 1.2   12 15    -32 unknown 13   590 120 0 false(unreach-call) .20 12 2.4 1 false(unreach-call) 16   480 120 1 false(unreach-call) 17   520 140 1 false(unreach-call) 18   490 140 1 false(unreach-call) 36   320 250 1 unknown 21   130 290 0
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) .31  29 4.0  1 false(unreach-call) 1.0  33 10   1 false(unreach-call) 4.5 310 36 1 false(unreach-call) 4.1 300 34 0 false(unreach-call) 4.1 280 42 1 false(unreach-call) 3.8  76 54   1 false(unreach-call) .16  28 1.7  1 false(unreach-call) .15  28 2.3  1 false(unreach-call) 7.0 440 57 1 true .70  12 8.8  -32 false(unreach-call) 8.2 340 63 1 false(unreach-call) .20 11 1.9 1 false(unreach-call) 8.9 530 79 1 false(unreach-call) 9.5 460 72 1 false(unreach-call) 13   590 120 1 false(unreach-call) 19   330 130 1 false(unreach-call) 8.5 140 120 1
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) .23  27 2.9  1 false(unreach-call) .61 35 6.5 1 false(unreach-call) 4.2 300 37 1 false(unreach-call) 3.7 290 32 0 false(unreach-call) 3.7 280 36 1 false(unreach-call) 2.8  75 34   1 false(unreach-call) .16  28 1.5  1 false(unreach-call) .20  28 1.9  1 false(unreach-call) 6.6 420 51 1 false(unreach-call) .60  12 6.6  1 false(unreach-call) 6.7 330 54 1 false(unreach-call) .17 11 2.3 1 false(unreach-call) 7.8 390 61 1 false(unreach-call) 7.5 470 60 1 false(unreach-call) 9.4 540 78 1 false(unreach-call) 17   290 130 1 false(unreach-call) 8.3 190 120 1
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) .28  29 2.7  1 false(unreach-call) 1.0  33 9.3 1 false(unreach-call) 4.7 300 43 1 false(unreach-call) 4.2 290 34 0 false(unreach-call) 5.0 280 45 1 false(unreach-call) 6.0  75 86   1 false(unreach-call) .21  28 1.9  1 false(unreach-call) .20  28 2.1  1 false(unreach-call) 7.4 440 56 1 true .82  12 11    -32 false(unreach-call) 10   470 85 1 false(unreach-call) .19 11 2.0 1 false(unreach-call) 9.4 550 76 1 false(unreach-call) 10   500 96 1 false(unreach-call) 13   600 110 1 false(unreach-call) 19   340 140 1 false(unreach-call) 8.5 210 110 1
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) .20  26 1.8  1 false(unreach-call) 1.0  33 8.5 1 false(unreach-call) 4.8 310 46 1 false(unreach-call) 4.2 290 33 1 false(unreach-call) 3.6 270 29 1 false(unreach-call) 5.8  75 76   1 false(unreach-call) .13  28 .86 1 false(unreach-call) .14  28 1.1  1 false(unreach-call) 10   470 84 1 false(unreach-call) .33  11 3.8  1 false(unreach-call) 10   420 92 1 false(unreach-call) .17 11 1.8 1 false(unreach-call) 190   600 2600 1 false(unreach-call) 21   720 200 1 false(unreach-call) 540   670 6500 1 false(unreach-call) 19   460 140 1 unknown 94   15000 1300 0
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) .26  27 2.5  1 false(unreach-call) .99 33 9.3 1 false(unreach-call) 3.9 290 34 1 false(unreach-call) 3.5 280 33 1 false(unreach-call) 3.0 260 25 1 false(unreach-call) 4.7  75 58   1 false(unreach-call) .12  28 .78 1 false(unreach-call) .12  28 1.2  1 false(unreach-call) 5.0 290 45 1 false(unreach-call) .33  11 3.6  1 false(unreach-call) 4.9 290 50 1 false(unreach-call) .16 11 1.7 1 false(unreach-call) 6.1 300 48 1 false(unreach-call) 6.9 380 59 1 false(unreach-call) 8.4 470 67 1 false(unreach-call) 17   310 140 1 false(unreach-call) 7.7 93 99 1
loops/sum_array_false-unreach-call.i false(unreach-call) .33  41 3.4  1 false(unreach-call) .26 33 2.4 1 false(unreach-call) 4.1 300 32 1 false(unreach-call) 4.0 290 35 0 false(unreach-call) 3.8 280 33 1 false(unreach-call) 1.4  160 17   1 false(unreach-call) .30  28 2.9  1 false(unreach-call) .28  28 2.7  1 false(unreach-call) 72   3700 760 1 true .38  15 4.3  -32 false(unreach-call) 6.4 330 59 1 unknown .21 12 2.0 0 false(unreach-call) 5.9 290 43 1 false(unreach-call) 6.9 340 54 1 false(unreach-call) 5.8 290 46 1 false(unreach-call) 2.0 160 17 0 unknown 230   820 2200 0
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) .13  22 .73 1 false(unreach-call) .25 33 2.3 1 false(unreach-call) 3.3 280 28 1 false(unreach-call) 2.9 270 26 1 false(unreach-call) 2.5 250 26 1 false(unreach-call) .53 75 6.3 1 false(unreach-call) .16  28 1.2  1 false(unreach-call) .13  28 1.4  1 false(unreach-call) 2.8 260 22 1 false(unreach-call) .34  11 4.0  1 false(unreach-call) 5.0 300 46 1 false(unreach-call) .16 11 1.4 1 false(unreach-call) 4.7 280 41 1 false(unreach-call) 4.7 260 39 1 false(unreach-call) 4.9 290 40 1 false(unreach-call) 11   280 77 1 unknown 3.8 92 60 0
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) .13  23 .83 1 false(unreach-call) .25 33 2.0 1 false(unreach-call) 3.2 280 32 1 false(unreach-call) 2.9 280 26 1 false(unreach-call) 2.6 260 21 1 false(unreach-call) .40 75 4.4 1 false(unreach-call) .22  28 1.5  1 false(unreach-call) .18  28 2.4  1 false(unreach-call) 2.9 270 27 1 false(unreach-call) .43  12 6.1  1 false(unreach-call) 5.8 320 52 1 false(unreach-call) .17 11 1.5 1 false(unreach-call) 4.5 270 34 1 false(unreach-call) 4.4 260 37 1 false(unreach-call) 4.5 270 35 1 false(unreach-call) 15   280 110 1 unknown 110   220 1300 0
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) .10  22 .85 1 false(unreach-call) .25 33 2.1 1 false(unreach-call) 3.4 280 32 1 false(unreach-call) 3.3 290 26 1 false(unreach-call) 3.3 270 28 1 false(unreach-call) .55 75 6.5 1 false(unreach-call) .19  28 1.5  1 false(unreach-call) .14  28 1.8  1 false(unreach-call) 2.9 280 29 1 false(unreach-call) .56  13 6.7  1 false(unreach-call) 5.6 310 49 1 false(unreach-call) .15 11 1.5 1 false(unreach-call) 4.6 280 39 1 false(unreach-call) 4.4 260 33 1 false(unreach-call) 4.8 290 43 1 false(unreach-call) 11   280 86 1 false(unreach-call) 8.1 96 98 1
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) .12  23 1.3  1 false(unreach-call) .24 33 2.1 1 false(unreach-call) 3.3 280 28 1 false(unreach-call) 3.2 290 27 0 false(unreach-call) 2.6 250 20 1 false(unreach-call) .62 160 8.7 1 false(unreach-call) .21  28 1.4  1 false(unreach-call) .25  28 2.5  1 false(unreach-call) 2.7 260 23 1 unknown .30  11 3.5  0 false(unreach-call) 6.4 330 56 1 false(unreach-call) .19 11 1.8 1 false(unreach-call) 4.7 270 36 1 false(unreach-call) 4.6 250 42 1 false(unreach-call) 4.6 280 40 1 false(unreach-call) 16   280 130 1 unknown 33   130 420 0
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) .13  22 .83 1 false(unreach-call) .22 33 2.0 1 false(unreach-call) 3.2 280 31 1 false(unreach-call) 3.1 270 31 1 false(unreach-call) 2.6 280 24 1 false(unreach-call) .41 75 5.0 1 false(unreach-call) .13  28 1.3  1 false(unreach-call) .11  28 1.5  1 false(unreach-call) 2.7 280 23 1 false(unreach-call) .40  12 5.1  1 false(unreach-call) 22   770 200 1 false(unreach-call) .16 11 1.7 1 false(unreach-call) 4.3 260 38 1 false(unreach-call) 4.2 260 38 1 false(unreach-call) 4.4 270 40 1 false(unreach-call) 15   280 120 1 unknown 11   120 130 0
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) .097 22 1.0  1 false(unreach-call) .24 33 2.1 1 false(unreach-call) 3.3 280 29 1 false(unreach-call) 3.3 290 30 1 false(unreach-call) 3.2 270 32 1 false(unreach-call) .40 75 5.1 1 false(unreach-call) .19  28 2.3  1 false(unreach-call) .43  28 2.9  1 false(unreach-call) 3.1 280 31 1 unknown .30  11 3.6  0 false(unreach-call) 6.0 340 53 1 false(unreach-call) .19 12 2.2 1 false(unreach-call) 4.7 270 40 1 false(unreach-call) 6.5 350 59 1 false(unreach-call) 4.5 270 41 1 false(unreach-call) 15   280 140 1 false(unreach-call) 8.6 98 110 1
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i error (134) .11  22 .61 0 false(unreach-call) .66 33 6.1 1 false(unreach-call) 3.3 310 29 1 false(unreach-call) 11   470 87 1 false(unreach-call) 2.7 280 22 1 false(unreach-call) 1.4  75 19   0 false(unreach-call) .19  28 2.1  1 false(unreach-call) .21  28 2.1  1 false(unreach-call) 2.9 270 29 1 false(unreach-call) .34  11 3.9  1 unknown 4.6 290 43 0 false(unreach-call) .16 11 1.7 1 false(unreach-call) 6.9 320 58 1 false(unreach-call) 6.4 340 50 1 false(unreach-call) 8.8 540 73 1 false(unreach-call) 19   300 130 1 unknown 2.5 92 28 0
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i false(unreach-call) .71  40 7.4  1 false(unreach-call) .71 34 6.3 1 false(unreach-call) 4.5 320 38 1 false(unreach-call) 3.8 290 36 0 false(unreach-call) 4.2 280 37 1 false(unreach-call) 2.0  130 25   0 false(unreach-call) .16  28 1.6  1 false(unreach-call) .26  28 3.0  0 false(unreach-call) 5.7 300 48 1 unknown .31  11 3.8  0 unknown 4.5 300 44 0 false(unreach-call) .20 12 2.3 1 false(unreach-call) 12   540 100 1 false(unreach-call) 8.9 470 74 1 false(unreach-call) 46   2600 430 1 false(unreach-call) 27   290 220 1 unknown 4.3 92 57 0
loops/vogal_false-unreach-call.i false(unreach-call) 2.3   140 27    1 false(unreach-call) 1.2  38 12   0 false(unreach-call) 7.3 380 67 1 false(unreach-call) 7.8 420 65 0 false(unreach-call) 52   510 620 1 false(unreach-call) 12    210 140   1 false(unreach-call) .82  35 8.4  0 false(unreach-call) .95  36 8.9  0 false(unreach-call) 190   2200 2100 0 false(unreach-call) 1.8   12 22    1 false(unreach-call) 18   670 170 1 false(unreach-call) .18 12 2.2 1 timeout 900   4700 12000 0 false(unreach-call) 41   990 400 1 timeout 900   4600 13000 0 false(unreach-call) 30   470 210 1 unknown 650   560 7700 0
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) .13  22 .88 1 false(unreach-call) .23 33 2.4 1 false(unreach-call) 3.3 280 30 1 false(unreach-call) 3.1 270 27 1 false(unreach-call) 2.6 260 22 1 false(unreach-call) .38 75 4.8 1 false(unreach-call) .075 28 .95 1 false(unreach-call) .11  28 .87 1 false(unreach-call) 2.8 270 25 1 false(unreach-call) .32  11 4.0  1 false(unreach-call) 5.0 300 51 1 false(unreach-call) .16 11 1.8 1 false(unreach-call) 4.5 270 42 1 false(unreach-call) 4.5 250 36 1 false(unreach-call) 4.6 270 36 1 false(unreach-call) 14   280 100 1 out of memory 92   15000 1300 0
loops/array_true-unreach-call_true-termination.i true .14  24 1.1  2 true .41 33 4.4 2 true 3.1 270 31 2 true 3.1 270 28 2 true 3.5 270 32 2 true 4.3  280 42   2 true .10  26 .82 2 true .095 26 .95 2 true 4.5 280 35 2 true .45  12 4.9  2 true 3.8 250 33 2 true .18 12 2.3 2 true 6.7 310 63 2 true 5.4 310 46 2 true 8.6 490 82 2 true 1.7 150 15 2 true 13   200 150 1
loops/bubble_sort_true-unreach-call_true-termination.i error (134) .11  22 .61 0 error (42) 870    15000 5400   0 true 3.2 300 29 2 true 2.6 260 25 2 true 93   470 1200 2 unknown 900    450 12000   0 timeout 900     1600 7800    0 true .13  27 1.3  2 true 2.8 260 25 2 true .36  11 3.9  2 unknown 4.6 300 41 0 true .15 11 1.6 2 true 4.4 250 43 2 true 5.1 270 42 2 true 4.5 250 39 2 true 12   270 96 2 unknown 24   120 390 0
loops/count_up_down_true-unreach-call_true-termination.i timeout 900     1400 11000    0 error (42) 870    5100 3600   0 error 3.0 280 25 0 unknown 2.8 270 24 0 timeout 900   7000 9200 0 unknown 69    75 900   0 timeout 900     1400 11000    0 timeout 900     1400 12000    0 true 4.2 290 33 2 unknown 900     1200 12000    0 true 4.0 250 41 2 true .17 11 1.5 2 true 19   350 210 2 true 5.6 310 52 2 true 17   470 200 1 true 84   1300 700 1 true 9.1 110 110 1
loops/eureka_01_true-unreach-call.i true 16     840 140    1 true 2.3  35 22   1 true 11   570 89 1 true 10   580 82 1 true 3.9 260 36 1 unknown 890    310 7700   0 true .15  27 1.7  1 true .33  28 5.0  1 timeout 900   4200 13000 0 true .37  11 4.4  1 unknown 29   710 300 0 true .17 11 1.9 1 timeout 900   1100 11000 0 timeout 900   4600 14000 0 timeout 900   1100 11000 0 true 63   720 590 1 true 150   470 2200 1
loops/eureka_05_true-unreach-call_true-termination.i true .92  60 10    2 true .80 33 7.9 2 true 4.9 290 46 2 true 3.7 280 33 2 true 2.9 250 24 2 true 6.2  260 61   2 true .11  27 .77 2 true .12  26 .80 2 true 33   1100 250 2 true .34  11 4.3  2 true 4.7 300 41 2 true .17 11 2.0 2 true 51   1000 560 2 true 160   2600 2600 1 true 130   1400 1700 2 true 66   900 640 2 true 56   280 600 1
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true .090 22 .66 2 out of memory 420    15000 5900   0 true 2.8 270 25 2 true 2.8 270 24 2 true 93   2200 910 2 unknown 38    75 470   0 timeout 900     11000 11000    0 true .075 26 .84 2 true 3.0 280 26 2 unknown 890     12 12000    0 true 3.9 260 41 2 timeout (timeout) 900    15000 14000   0 true 4.8 280 37 2 true 5.4 300 47 2 true 4.5 280 38 2 true 12   290 79 2 unknown 110   15000 1500 0
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true .11  22 .71 2 out of memory 420    15000 6100   0 true 2.8 270 24 2 true 2.8 270 26 2 true 93   2300 1000 2 unknown 37    75 560   0 timeout 900     11000 9500    0 timeout 900     11000 12000    0 true 2.9 280 26 2 unknown 900     11 13000    0 true 4.1 250 35 2 timeout (timeout) 900    15000 14000   0 true 4.8 280 40 2 true 5.1 290 44 2 true 4.8 280 40 2 true 11   280 78 2 unknown 110   15000 1500 0
loops/insertion_sort_true-unreach-call_true-termination.i out of memory 380     15000 1700    0 error (42) 870    2200 5500   0 error 4.2 310 34 0 false(unreach-call) 3.5 280 36 -16 timeout 900   4600 6500 0 unknown 890    190 9900   0 timeout 900     130 11000    0 timeout 900     140 12000    0 timeout 900   4600 11000 0 true .38  12 4.5  1 unknown 6.4 330 57 0 unknown .20 12 2.1 0 timeout 900   1600 11000 0 timeout 900   890 11000 0 timeout 900   1100 11000 0 unknown 800   220 9100 0 true 16   130 200 1
loops/invert_string_true-unreach-call_true-termination.i true .40  35 5.2  2 true .77 33 8.8 2 false(unreach-call) 5.3 330 46 -16 false(unreach-call) 3.9 290 38 -16 true 35   810 310 2 true 17    460 230   2 true .11  26 .69 2 true .12  26 .94 2 true 15   640 110 2 true .39  11 5.0  2 true 4.0 250 42 2 true .18 11 2.0 2 true 150   880 1900 2 true 130   1500 1600 2 true 250   980 3300 2 true 36   530 310 2 true 18   170 210 1
loops/linear_sea.ch_true-unreach-call.i timeout 900     5200 5300    0 error (6) 790    8400 3500   0 error 3.5 310 33 0 unknown 3.2 290 27 0 timeout 910   9100 8700 0 unknown 120    76 1400   0 timeout 900     980 11000    0 timeout 900     980 12000    0 timeout 900   2600 11000 0 true .38  11 5.1  1 unknown 280   720 3500 0 unknown .18 12 1.9 0 timeout 900   750 12000 0 timeout 900   1000 12000 0 timeout 900   1800 10000 0 true 92   1200 970 1 unknown 4.4 92 61 0
loops/lu.cmp_true-unreach-call.i true 9.5   3700 100    1 true 2.3  51 31   1 true 4.3 280 42 1 true 3.5 270 33 1 true 3.3 260 30 1 true 9.2  350 97   1 true .12  27 1.4  1 true .23  29 2.1  1 true 10   450 75 1 true .44  11 5.0  1 true 6.8 390 63 1 true .16 11 1.8 1 timeout 900   4100 11000 0 timeout 900   3900 13000 0 timeout 900   3700 11000 0 true 250   1200 2700 1 error (1) 45   120 680 0
loops/matrix_true-unreach-call_true-termination.i true .17  26 1.5  2 true .42 33 4.0 2 true 3.2 270 32 2 true 3.2 280 32 2 true 3.9 280 32 2 true 15    370 160   2 true .086 26 .85 2 true .12  26 .81 2 true 9.6 450 76 2 true .47  12 5.1  2 true 4.2 250 39 2 true .20 12 2.4 2 true 8.5 410 62 2 true 8.7 470 69 2 true 14   620 120 2 true 21   290 140 2 true 20   240 240 1
loops/n.c11_true-unreach-call_false-termination.i timeout 900     1700 11000    0 error (42) 870    2900 5100   0 true 3.0 270 29 2 true 3.0 270 29 2 true 2.5 250 26 2 unknown 58    75 680   0 timeout 900     2500 12000    0 timeout 900     2500 13000    0 true 4.5 280 37 2 unknown .27  11 3.2  0 true 25   720 260 2 timeout (timeout) 900    77 12000   0 true 6.9 350 59 2 true 7.0 410 57 2 true 8.5 490 66 2 true 380   2500 2700 2 true 110   160 1400 1
loops/n.c40_true-unreach-call_true-termination.i true .14  28 1.1  2 true .41 33 3.9 2 true 3.4 280 32 2 true 3.2 270 35 2 true 5.2 280 54 2 true 4.4  280 39   2 true .10  26 .84 2 true .10  26 .74 2 true 3.5 270 30 2 true .37  12 3.6  2 true 7.4 330 62 2 true .17 11 1.7 2 true 6.9 360 55 2 true 7.6 490 58 2 true 6.5 370 53 2 true 36   280 310 2 unknown 210   760 3100 0
loops/nec40_true-unreach-call_true-termination.i true .12  27 .99 2 true .40 33 4.0 2 true 3.1 280 30 2 true 3.0 270 31 2 true 4.1 280 38 2 true 4.5  280 46   2 true .10  26 .63 2 true .10  26 .68 2 true 3.5 270 29 2 true .35  12 4.5  2 true 8.2 340 65 2 true .18 11 1.6 2 true 6.9 370 57 2 true 7.8 480 63 2 true 6.9 370 52 2 true 54   290 520 2 unknown 110   780 1600 0
loops/string_true-unreach-call_true-termination.i true .13  23 .84 2 true 1.3  34 12   2 true 3.0 270 26 2 true 3.0 270 28 2 true 3.5 260 30 2 true 4.6  260 53   2 true .25  27 2.3  2 true .11  26 .75 2 timeout 900   1400 12000 0 true 18     13 210    2 true 5.2 310 50 2 true .17 11 2.4 2 true 7.9 390 64 2 true 6.9 390 55 2 true 11   540 92 2 true 18   220 130 2 unknown 21   130 270 0
loops/sum01_true-unreach-call_true-termination.i timeout 900     1600 11000    0 true 22    130 300   2 true 3.9 280 35 2 true 3.9 270 38 2 true 260   3200 3000 2 true 300    3600 2800   1 true 380     830 4300    2 true 380     830 4400    2 true 3.7 270 33 2 true 74     64 900    2 true 4.1 290 35 2 true .15 11 2.1 2 true 7.4 380 64 2 true 6.3 370 51 2 true 8.5 510 75 2 witness invalid (true) 83   1200 670 0 true 10   110 130 1
loops/sum03_true-unreach-call_false-termination.i true .28  26 2.7  2 out of memory 460    15000 5800   0 true 4.0 290 33 2 true 5.8 410 52 2 true 180   2300 2100 2 true 180    2200 2300   2 timeout 900     10000 11000    0 timeout 900     10000 9600    0 true 3.0 280 27 2 unknown 890     11 14000    0 true 4.2 260 41 2 timeout (timeout) 900    15000 13000   0 true 4.9 290 41 2 true 5.1 270 42 2 true 4.8 290 44 2 true 12   290 87 2 unknown 85   15000 1100 0
loops/sum04_true-unreach-call_true-termination.i true .21  26 2.4  2 true 1.1  33 10   2 true 3.0 270 27 2 true 2.9 270 29 2 true 2.3 250 23 2 true 3.3  250 33   2 true .078 26 .90 2 true .081 26 1.0  2 true 6.2 420 59 2 true .30  11 4.2  2 true 3.8 240 34 2 true .14 11 1.8 2 true 9.7 460 75 2 true 8.9 470 78 2 true 9.8 530 82 2 true 13   280 98 2 true 9.7 110 150 1
loops/sum_array_true-unreach-call.i timeout 900     13000 4500    0 error (42) 870    1500 4100   0 error 7.1 360 57 0 false(unreach-call) 4.1 290 38 -16 timeout 900   4500 6400 0 unknown 890    290 9000   0 timeout 900     250 13000    0 timeout 900     310 11000    0 timeout 900   4500 11000 0 unknown .036 13 .39 0 unknown 21   680 190 0 unknown .20 12 2.0 0 timeout 900   1400 10000 0 timeout 900   990 11000 0 timeout 900   1600 14000 0 true 23   220 190 1 unknown 230   680 2400 0
loops/terminator_02_true-unreach-call_true-termination.i true .11  23 .86 2 error (42) 870    350 10000   0 true 2.9 270 27 2 true 2.9 270 29 2 true 3.4 260 27 2 true 4.1  260 48   2 timeout 900     83 11000    0 timeout 900     78 14000    0 true 3.3 270 27 2 true .61  12 6.2  2 true 32   740 330 2 timeout (timeout) 900    3100 9100   0 true 5.3 290 49 2 true 5.2 290 43 2 true 5.6 290 47 2 true 13   280 100 2 true 15   140 220 1
loops/terminator_03_true-unreach-call_true-termination.i true .11  22 .70 2 error (42) 870    510 8400   0 true 3.1 270 26 2 true 2.8 270 26 2 true 3.3 260 30 2 true 3.8  270 39   2 timeout 900     89 12000    0 timeout 900     85 11000    0 true 3.5 280 29 2 unknown 900     66 14000    0 true 4.0 250 40 2 timeout (timeout) 900    69 11000   0 true 4.9 290 40 2 true 4.7 260 40 2 true 5.0 290 36 2 true 13   310 84 2 unknown 12   120 140 0
loops/trex01_true-unreach-call_true-termination.i true 3.7   110 50    2 error (42) 870    4400 4800   0 true 6.3 340 57 2 true 6.4 350 55 2 true 16   590 160 2 true 160    2300 1900   2 timeout 900     900 12000    0 timeout 900     910 11000    0 true 2.9 270 27 2 unknown .28  11 3.4  0 true 9.8 400 91 2 true .26 12 3.3 2 true 4.8 290 37 2 true 4.8 270 37 2 true 4.9 280 43 2 true 14   300 100 2 unknown 32   130 430 0
loops/trex02_true-unreach-call_true-termination.i true .12  22 .70 2 error (42) 870    1300 8300   0 true 2.9 270 25 2 true 2.8 270 27 2 true 3.1 270 27 2 true 3.7  260 32   2 timeout 900     460 10000    0 timeout 900     460 12000    0 true 2.8 280 26 2 true .34  12 4.4  2 true 4.2 270 41 2 true .14 11 1.6 2 true 4.7 280 42 2 true 4.4 260 38 2 true 4.9 280 39 2 true 11   280 100 2 true 9.5 120 120 1
loops/trex03_true-unreach-call_true-termination.i true .11  23 .73 2 error (42) 870    840 10000   0 error 3.5 290 35 0 unknown 3.2 290 32 0 true 3.4 270 29 2 true 4.0  270 36   2 timeout 900     370 10000    0 timeout 900     370 10000    0 true 5.8 300 45 2 unknown .31  11 3.3  0 timeout 900   1300 9800 0 timeout (timeout) 900    2400 9000   0 true 4.9 280 45 2 true 4.9 280 37 2 true 4.7 270 43 2 true 13   280 100 2 true 11   130 130 1
loops/trex04_true-unreach-call_false-termination.i true .10  23 .79 2 error (42) 870    2700 5800   0 true 3.1 270 29 2 true 2.8 270 27 2 true 3.3 270 28 2 true 4.6  280 45   2 timeout 900     110 11000    0 timeout 900     110 11000    0 true 3.1 270 29 2 true .39  12 4.3  2 true 4.3 290 43 2 true .18 11 1.7 2 true 4.8 280 39 2 true 5.0 280 35 2 true 5.0 280 47 2 true 13   280 100 2 timeout 900   100 8100 0
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i error (134) .088 22 .73 0 true .78 33 7.1 2 true 3.1 300 29 2 true 12   470 98 2 true 3.5 280 31 2 true 4.1  280 41   2 true .095 26 1.1  2 true .11  26 .76 2 true 2.9 270 24 1 true .31  11 3.8  2 unknown 5.1 310 38 0 true .14 11 1.6 2 true 7.1 320 54 2 true 6.9 460 58 2 true 9.8 540 75 1 true 82   1200 710 2 unknown 2.5 92 34 0
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i true .14  25 .89 2 true 2.5  44 30   2 true 19   800 140 2 true 17   790 120 2 true 150   1300 1700 2 true 160    2300 1800   2 true .29  28 4.5  2 true .087 27 .86 2 true 4.4 280 40 2 true 700     79 8600    2 unknown 4.5 300 43 0 true .65 12 6.6 2 true 5.9 290 49 2 true 5.9 320 47 2 true 6.3 290 52 2 true 50   600 460 2 unknown 4.4 92 56 0
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true .092 23 .83 2 true 1.1  33 13   2 true 3.2 280 29 2 true 3.2 270 28 2 true 4.0 270 40 2 true 5.4  280 50   2 true .088 26 1.0  2 true .075 26 .80 2 true 7.0 420 57 2 true 3.0   12 39    2 true 4.8 310 41 2 true .14 11 1.7 2 true 4.8 280 35 2 true 4.8 250 35 2 true 5.0 280 40 2 true 16   280 130 2 unknown 8.3 92 99 0
loops/vogal_true-unreach-call.i true 1.4   66 19    2 true .84 33 7.3 2 true 60   2900 670 2 true 58   3100 590 2 true 250   1900 2800 2 true 330    2300 3800   2 true .13  27 .93 2 true .17  26 1.8  2 timeout 900   4000 11000 0 true 13     13 150    2 unknown 23   680 220 0 true .19 11 2.1 2 timeout 900   5200 12000 0 timeout 900   1700 11000 0 timeout 900   4600 11000 0 true 77   800 610 2 unknown 30   120 360 0
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true .096 22 .86 2 out of memory 410    15000 4600   0 true 2.9 270 24 2 true 2.8 270 25 2 true 2.3 240 20 2 true 3.2  260 33   2 timeout 900     14000 13000    0 timeout 900     14000 11000    0 true 2.8 270 25 2 unknown 890     11 11000    0 true 4.1 240 36 2 timeout (timeout) 900    15000 13000   0 true 6.4 360 58 2 true 4.2 260 37 2 true 4.7 280 38 2 true 11   270 88 2 unknown 90   15000 1300 0
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true .088 22 .74 2 out of memory 410    15000 4200   0 true 2.9 270 26 2 true 2.7 270 24 2 true 2.4 240 22 2 true 3.0  250 26   2 timeout 900     14000 11000    0 true .077 26 .79 2 true 2.9 280 27 2 unknown 890     11 15000    0 true 3.9 240 33 2 timeout (timeout) 900    15000 12000   0 true 4.8 290 41 2 true 4.3 260 41 2 true 4.7 280 38 2 true 10   280 84 2 out of memory 90   15000 1200 0
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true .10  22 .58 2 out of memory 430    15000 6400   0 true 2.8 270 28 2 true 2.8 270 27 2 true 2.4 250 21 2 true 3.2  260 28   2 timeout 900     12000 12000    0 timeout 900     12000 12000    0 true 3.0 280 27 2 unknown 900     11 12000    0 true 4.0 250 33 2 timeout (timeout) 900    15000 12000   0 true 4.9 280 39 2 true 4.6 260 41 2 true 4.8 280 41 2 true 11   270 76 2 unknown 92   15000 1300 0
loop-acceleration/array_false-unreach-call1_true-termination.i out of memory 380     15000 3200    0 false(unreach-call) 22    1800 280   0 timeout 900   4200 8800 0 timeout 900   3900 12000 0 false(unreach-call) 140   2100 1700 1 unknown 890    250 9700   0 false(unreach-call) 71     270 580    1 false(unreach-call) 72     270 620    1 timeout 900   4700 13000 0 false(unreach-call) .34  11 3.9  1 unknown 140   720 1400 0 false(unreach-call) .18 11 1.7 1 timeout 900   2800 11000 0 timeout 900   5000 12000 0 timeout 900   980 11000 0 false(unreach-call) 250   3700 2800 1 false(unreach-call) 8.7 190 100 1
loop-acceleration/array_false-unreach-call2_true-termination.i out of memory 270     15000 1700    0 false(unreach-call) 45    3700 510   0 timeout 900   4300 10000 0 timeout 900   4200 12000 0 timeout 900   8700 12000 0 unknown 890    320 9500   0 false(unreach-call) 310     990 2800    1 false(unreach-call) 300     990 2900    1 timeout 900   4600 14000 0 false(unreach-call) .36  11 5.4  1 false(unreach-call) 5.1 290 43 1 false(unreach-call) .17 12 1.9 1 timeout 900   2700 12000 0 timeout 900   4700 14000 0 timeout 900   1000 12000 0 false(unreach-call) 5.8 220 52 1 false(unreach-call) 9.9 380 130 1
loop-acceleration/array_false-unreach-call3_true-termination.i out of memory 660     15000 3500    0 false(unreach-call) 21    1000 240   0 timeout 900   4200 8600 0 timeout 900   4200 9700 0 timeout 900   7500 10000 0 timeout 900    8200 11000   0 false(unreach-call) 71     390 610    0 false(unreach-call) 70     390 650    0 timeout 900   4300 12000 0 unknown 890     53 11000    0 unknown 49   700 560 0 false(unreach-call) 2.2  13 31   0 timeout 900   4200 11000 0 timeout 900   4700 12000 0 timeout 900   990 10000 0 false(unreach-call) 490   3700 7100 0 false(unreach-call) 11   290 120 0
loop-acceleration/const_false-unreach-call1.i timeout 900     1600 12000    0 false(unreach-call) 4.1  34 47   1 timeout 900   4300 10000 0 timeout 900   4200 12000 0 false(unreach-call) 74   1200 840 1 unknown 54    75 670   0 false(unreach-call) 11     150 120    1 false(unreach-call) 11     140 140    1 timeout 900   5000 14000 0 false(unreach-call) .34  11 4.7  1 unknown 220   700 2500 0 false(unreach-call) .16 11 1.5 1 timeout 900   750 14000 0 timeout 900   3900 11000 0 timeout 900   710 11000 0 false(unreach-call) 240   3700 2700 1 false(unreach-call) 8.6 190 130 1
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) .82  32 11    1 false(unreach-call) 3.0  55 32   1 false(unreach-call) 45   1900 380 1 false(unreach-call) 52   1800 420 1 false(unreach-call) 45   1100 580 1 false(unreach-call) 32    75 400   1 false(unreach-call) 2.5   28 29    1 false(unreach-call) 2.8   28 23    1 false(unreach-call) 34   1800 290 1 false(unreach-call) .36  11 4.2  1 unknown 20   690 200 0 false(unreach-call) .15 11 1.8 1 timeout 900   750 13000 0 timeout 900   710 10000 0 timeout 900   750 11000 0 false(unreach-call) 86   1900 900 1 false(unreach-call) 8.7 100 110 1
loop-acceleration/functions_false-unreach-call1_true-termination.i timeout 900     1400 11000    0 out of memory 420    15000 5600   0 timeout 900   4400 7700 0 timeout 900   4300 7800 0 timeout 900   8100 10000 0 unknown 36    75 510   0 out of memory 820     15000 8900    0 out of memory 800     15000 10000    0 timeout 900   4700 13000 0 unknown 890     11 13000    0 false(unreach-call) 5.1 300 40 1 false(unreach-call) .14 11 1.6 1 timeout 900   690 11000 0 timeout 900   4700 12000 0 timeout 900   790 13000 0 unknown 86   220 880 0 false(unreach-call) 10   92 170 1
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) .091 22 .96 1 false(unreach-call) .23 33 1.9 1 false(unreach-call) 3.1 280 25 1 false(unreach-call) 3.1 280 26 1 false(unreach-call) 2.5 260 20 1 false(unreach-call) .52 75 6.4 1 false(unreach-call) .20  28 1.6  1 false(unreach-call) .22  28 1.3  1 false(unreach-call) 2.9 280 26 1 false(unreach-call) .34  11 3.9  1 false(unreach-call) 4.8 300 46 1 false(unreach-call) .15 11 1.7 1 false(unreach-call) 4.4 260 36 1 false(unreach-call) 4.2 240 37 1 false(unreach-call) 4.5 270 40 1 false(unreach-call) 11   280 92 1 unknown 10   110 140 0
loop-acceleration/nested_false-unreach-call1.i timeout 900     10000 9800    0 out of memory 380    15000 5100   0 timeout 900   4100 11000 0 timeout 900   4200 9400 0 timeout 900   5200 10000 0 timeout 900    1400 9200   0 timeout 900     9500 10000    0 timeout 900     9600 11000    0 timeout 900   5300 13000 0 unknown 890     11 13000    0 false(unreach-call) 4.6 280 40 1 false(unreach-call) .14 11 1.6 1 timeout 900   1100 10000 0 timeout 900   4300 12000 0 timeout 900   1200 11000 0 unknown 300   7300 3500 0 false(unreach-call) 13   96 160 1
loop-acceleration/phases_false-unreach-call1.i timeout 900     1200 10000    0 out of memory 360    15000 4600   0 timeout 900   4100 12000 0 timeout 900   4100 12000 0 timeout 900   5700 9500 0 unknown 180    75 2700   0 timeout 900     7600 9600    0 timeout 900     7600 10000    0 timeout 900   4800 12000 0 unknown 890     11 14000    0 unknown 280   760 3400 0 out of memory 220    15000 3300   0 timeout 900   670 11000 0 timeout 900   9600 12000 0 timeout 900   620 10000 0 false(unreach-call) 400   7200 4800 1 false(unreach-call) 8.9 100 110 1
loop-acceleration/phases_false-unreach-call2_false-termination.i false(unreach-call) .14  24 1.0  1 false(unreach-call) .22 33 2.0 1 false(unreach-call) 3.1 280 28 1 false(unreach-call) 2.9 280 27 0 false(unreach-call) 2.5 250 25 1 false(unreach-call) .53 75 7.0 1 false(unreach-call) .16  28 1.2  1 false(unreach-call) .11  28 1.6  1 false(unreach-call) 2.8 270 27 1 false(unreach-call) .40  11 4.7  1 false(unreach-call) 5.9 330 54 1 false(unreach-call) .18 11 1.7 1 false(unreach-call) 4.5 260 37 1 false(unreach-call) 4.4 250 37 1 false(unreach-call) 4.5 270 39 1 false(unreach-call) 18   290 150 1 timeout 900   100 11000 0
loop-acceleration/simple_false-unreach-call1.i timeout 900     1400 10000    0 out of memory 320    15000 4100   0 timeout 900   4200 8200 0 timeout 900   4300 11000 0 timeout 910   7300 10000 0 unknown 54    75 790   0 timeout 900     11000 12000    0 timeout 900     11000 9400    0 timeout 900   4900 12000 0 unknown 900     11 12000    0 false(unreach-call) 5.3 400 49 1 false(unreach-call) .14 11 1.7 1 timeout 900   610 14000 0 timeout 900   2300 12000 0 timeout 900   660 11000 0 false(unreach-call) 240   3700 2600 1 false(unreach-call) 8.1 93 120 1
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) .11  22 .75 1 false(unreach-call) .23 33 1.9 1 false(unreach-call) 3.1 280 26 1 false(unreach-call) 3.1 280 31 1 false(unreach-call) 2.5 250 21 1 false(unreach-call) .38 75 4.1 1 false(unreach-call) .082 28 .81 1 false(unreach-call) .15  28 1.3  1 false(unreach-call) 2.8 280 25 1 false(unreach-call) .30  11 3.5  1 false(unreach-call) 4.9 300 44 1 false(unreach-call) .17 11 1.8 1 false(unreach-call) 4.3 260 35 1 false(unreach-call) 4.2 250 36 1 false(unreach-call) 4.5 260 40 1 false(unreach-call) 11   280 82 1 false(unreach-call) 8.3 92 120 1
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) .11  22 .87 1 false(unreach-call) .21 33 1.9 1 false(unreach-call) 3.2 280 27 1 false(unreach-call) 3.0 280 26 1 false(unreach-call) 2.6 250 22 1 false(unreach-call) .54 75 7.6 1 false(unreach-call) .12  28 .72 1 false(unreach-call) .080 28 .81 1 false(unreach-call) 2.8 260 23 1 false(unreach-call) .30  11 4.0  1 false(unreach-call) 5.1 290 49 1 false(unreach-call) .16 11 1.5 1 false(unreach-call) 4.7 270 36 1 false(unreach-call) 4.5 250 35 1 false(unreach-call) 4.5 270 38 1 false(unreach-call) 15   280 120 1 false(unreach-call) 7.9 92 98 1
loop-acceleration/simple_false-unreach-call4.i timeout 900     1300 9500    0 out of memory 320    15000 4200   0 timeout 900   4300 8500 0 timeout 900   4300 13000 0 timeout 900   7000 9800 0 unknown 53    75 710   0 timeout 900     11000 10000    0 timeout 900     11000 11000    0 timeout 900   4800 11000 0 unknown 890     11 11000    0 false(unreach-call) 4.8 280 41 1 false(unreach-call) .14 11 1.5 1 timeout 900   620 9300 0 timeout 900   2900 10000 0 timeout 900   810 13000 0 false(unreach-call) 220   2100 3100 1 out of memory 36   15000 570 0
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) .18  25 1.5  1 false(unreach-call) .97 33 9.3 1 false(unreach-call) 3.7 290 27 1 false(unreach-call) 3.3 290 34 1 false(unreach-call) 2.7 250 24 1 false(unreach-call) 3.5  75 42   1 false(unreach-call) .081 28 .88 1 false(unreach-call) .087 28 .85 1 false(unreach-call) 4.1 290 35 1 false(unreach-call) .33  11 4.0  1 false(unreach-call) 5.1 300 44 1 false(unreach-call) .15 11 1.6 1 false(unreach-call) 6.6 320 57 1 false(unreach-call) 6.8 380 59 1 false(unreach-call) 8.7 570 76 1 false(unreach-call) 15   290 110 1 false(unreach-call) 8.5 92 120 1
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) .17  25 1.9  1 false(unreach-call) .96 33 10   1 false(unreach-call) 3.7 290 29 1 false(unreach-call) 3.4 280 31 1 false(unreach-call) 2.8 260 25 1 false(unreach-call) 3.5  75 44   1 false(unreach-call) .080 28 .94 1 false(unreach-call) .083 28 .87 1 false(unreach-call) 3.8 280 31 1 false(unreach-call) .32  11 3.9  1 false(unreach-call) 5.0 310 45 1 false(unreach-call) .15 11 1.6 1 false(unreach-call) 6.8 310 52 1 false(unreach-call) 7.0 380 57 1 false(unreach-call) 7.8 470 76 1 false(unreach-call) 15   290 120 1 false(unreach-call) 8.5 92 120 1
loop-acceleration/array_true-unreach-call1_true-termination.i true 35     710 380    2 true 12    1100 170   2 timeout 900   4200 8900 0 timeout 900   3900 11000 0 true 92   460 1200 2 true 99    330 1400   2 true 15     150 190    2 true 15     150 200    2 timeout 900   4700 12000 0 true .37  11 4.1  2 true 21   690 180 2 true .17 11 1.6 2 true 6.1 300 51 2 timeout 900   4800 12000 0 true 6.7 340 55 2 true 18   280 140 2 true 16   250 200 1
loop-acceleration/array_true-unreach-call2_true-termination.i out of memory 260     15000 1700    0 true 26    2200 330   1 timeout 900   4300 11000 0 timeout 900   4200 9300 0 timeout 900   8600 11000 0 unknown 900    230 9400   0 true 88     510 930    1 true 89     510 1100    1 timeout 900   4600 11000 0 true .39  11 4.6  1 true 3.8 240 35 1 true .17 11 1.8 1 timeout 900   3200 11000 0 timeout 900   4800 12000 0 timeout 900   890 11000 0 true 3.1 210 23 1 unknown 110   550 1100 0
loop-acceleration/array_true-unreach-call3_true-termination.i true 4.1   170 40    2 true 11    640 130   2 timeout 900   4300 8900 0 timeout 900   4200 9000 0 true 10   660 89 2 true 15    1200 160   2 true 17     280 190    2 true 17     280 200    2 timeout 900   4300 9900 0 unknown 890     53 11000    0 true 4.3 260 34 2 true 7.9  15 93   2 true 7.0 340 52 2 timeout 900   4800 12000 0 true 6.2 290 45 2 true 15   220 94 2 true 17   220 190 1
loop-acceleration/array_true-unreach-call4_true-termination.i out of memory 630     15000 4300    0 true 11    640 140   1 timeout 900   4200 9500 0 timeout 900   4200 11000 0 true 11   470 86 1 unknown 900    220 9200   0 true 19     350 220    1 true 19     350 270    1 timeout 900   4600 14000 0 unknown 890     71 12000    0 unknown 48   700 610 0 true 7.1  15 84   1 timeout 910   13000 3300 0 timeout 900   4800 11000 0 timeout 900   1100 9800 0 true 15   220 120 1 true 12   140 170 1
loop-acceleration/const_true-unreach-call1.i true .18  25 1.9  2 true 3.8  34 40   2 true 3.1 270 30 2 true 3.0 270 29 2 true 5.2 280 46 2 true 7.1  450 71   2 true 11     130 140    2 true .074 26 .88 2 true 3.0 270 27 2 true .33  11 4.2  2 true 4.3 260 43 2 true .17 11 1.5 2 true 6.0 290 50 2 timeout 900   2800 12000 0 true 5.6 300 45 2 true 12   280 88 2 true 9.0 110 120 1
loop-acceleration/diamond_true-unreach-call1_true-termination.i true .81  31 9.0  2 true 3.8  58 39   1 error 54   2400 570 0 unknown 64   2400 470 0 true 160   1900 2100 2 true 280    2800 3200   2 true 1.9   31 24    2 true 1.8   31 27    2 true 140   3800 2000 2 true .38  11 4.5  2 unknown 20   710 180 0 true .15 11 1.6 2 timeout 900   720 11000 0 timeout 900   600 10000 0 timeout 900   710 9600 0 true 37   740 310 2 unknown 210   260 3200 0
loop-acceleration/diamond_true-unreach-call2.i true .17  28 1.5  2 true .88 35 10   2 true 9.4 470 72 2 true 10   470 79 2 true 5.8 310 51 2 true 9.3  290 98   2 true .14  26 1.5  2 true .19  26 1.5  2 true 23   1600 220 2 true .44  11 5.3  2 unknown 26   750 270 0 true .19 11 1.8 2 true 58   740 710 2 timeout 900   4700 12000 0 true 130   720 1400 2 true 25   480 200 2 true 350   250 4600 1
loop-acceleration/functions_true-unreach-call1_true-termination.i timeout 900     1400 12000    0 out of memory 430    15000 5600   0 timeout 900   4400 11000 0 timeout 900   4300 9800 0 timeout 900   8000 9400 0 unknown 36    75 530   0 out of memory 810     15000 9100    0 out of memory 810     15000 9000    0 timeout 900   4700 13000 0 unknown 890     11 12000    0 true 3.6 240 34 1 true .17 11 1.7 1 timeout 900   740 11000 0 timeout 900   4700 14000 0 timeout 900   800 11000 0 true 79   1200 760 1 unknown 31   110 390 0
loop-acceleration/multivar_true-unreach-call1_true-termination.i timeout 900     1600 12000    0 true 89    270 1000   2 true 2.8 270 26 2 true 2.7 270 26 2 true 2.9 260 27 2 unknown 63    75 910   0 true 450     840 6000    2 true 440     840 5200    2 true 2.9 280 26 2 true 67     64 860    2 true 4.2 250 38 2 true .16 11 1.8 2 true 5.0 270 41 2 true 4.5 260 40 2 true 4.9 280 39 2 true 12   270 98 2 true 9.4 110 130 1
loop-acceleration/nested_true-unreach-call1.i true .18  25 1.5  2 out of memory 380    15000 4900   0 timeout 900   4000 11000 0 timeout 900   4200 9300 0 true 350   3600 5200 2 true 360    3500 4100   2 timeout 900     9300 11000    0 timeout 900     9400 9500    0 timeout 900   5200 10000 0 unknown 890     11 12000    0 true 3.9 240 39 2 true .17 11 1.4 2 true 16   380 180 2 timeout 900   4600 11000 0 true 41   560 440 2 true 11   270 97 2 true 150   110 2000 1
loop-acceleration/overflow_true-unreach-call1.i timeout 900     1300 11000    0 out of memory 310    15000 4100   0 true 3.0 270 27 1 true 3.3 270 31 1 timeout 900   6800 9200 0 unknown 54    75 680   0 timeout 900     11000 11000    0 timeout 900     11000 11000    0 true 2.9 270 24 1 unknown 890     11 12000    0 true 3.6 240 37 1 true .16 11 1.7 1 timeout 900   650 12000 0 timeout 900   2400 11000 0 true 5.6 280 49 1 true 79   1200 730 1 unknown 180   110 1800 0
loop-acceleration/phases_true-unreach-call1.i timeout 900     1500 11000    0 out of memory 360    15000 5200   0 timeout 900   4100 7700 0 timeout 900   4100 9400 0 timeout 900   6400 9200 0 unknown 130    75 1900   0 timeout 900     7500 11000    0 timeout 900     7500 11000    0 timeout 900   4800 11000 0 unknown 890     11 12000    0 unknown 280   760 3200 0 true 200    7800 3400   1 timeout 900   740 11000 0 timeout 900   8700 13000 0 timeout 900   760 11000 0 true 240   7200 2600 1 unknown 230   380 2900 0
loop-acceleration/phases_true-unreach-call2_false-termination.i true .11  24 1.2  2 error (42) 870    5900 5600   0 error 3.3 290 31 0 unknown 3.2 290 29 0 true 3.1 260 26 2 true 5.1  270 45   2 timeout 900     390 10000    0 timeout 900     440 12000    0 false(unreach-call) 3.2 280 31 -16 unknown 890     12 11000    0 unknown 280   1100 2400 0 timeout (timeout) 900    11000 9100   0 true 6.1 300 50 2 true 9.6 270 100 2 true 11   440 88 2 true 12   300 100 2 timeout 900   100 12000 0
loop-acceleration/simple_true-unreach-call1.i timeout 900     1400 12000    0 out of memory 310    15000 3800   0 timeout 900   4300 9300 0 timeout 900   4300 9300 0 timeout 910   7300 9000 0 unknown 53    75 680   0 timeout 900     11000 9100    0 timeout 900     11000 11000    0 timeout 900   4900 13000 0 unknown 890     11 12000    0 true 4.0 240 36 1 true .15 11 1.6 1 timeout 900   570 10000 0 timeout 900   2800 11000 0 true 6.0 290 49 2 true 79   1200 800 1 true 20   110 200 1
loop-acceleration/simple_true-unreach-call2_true-termination.i true .082 22 .83 2 error (42) 870    3900 6300   0 true 3.0 270 28 2 true 2.8 270 26 2 true 3.1 260 23 2 true 3.5  270 34   2 timeout 900     250 11000    0 timeout 900     250 13000    0 true 2.8 260 25 2 true .30  11 3.9  2 true 3.8 250 37 2 true .14 11 1.8 2 true 4.8 280 40 2 true 4.5 260 41 2 true 4.6 280 40 2 true 12   280 91 2 true 31   110 310 1
loop-acceleration/simple_true-unreach-call3_true-termination.i timeout 900     1200 10000    0 error (42) 870    8100 3000   0 timeout 910   8400 6700 0 timeout 900   8500 7100 0 timeout 900   6600 8900 0 unknown 57    75 720   0 timeout 900     1500 10000    0 timeout 900     1500 11000    0 false(unreach-call) 3.3 280 31 -16 unknown 900     1100 11000    0 true 4.1 250 36 1 true .16 11 1.8 1 timeout 900   630 12000 0 timeout 900   2100 12000 0 true 6.7 310 53 2 true 80   1200 750 1 true 8.9 110 140 1
loop-acceleration/simple_true-unreach-call4.i true .097 22 .85 2 out of memory 320    15000 4700   0 timeout 900   4300 8700 0 timeout 900   4300 9100 0 true 150   1300 1800 2 true 150    2200 1600   2 timeout 900     11000 13000    0 timeout 900     11000 9700    0 timeout 900   4800 11000 0 unknown 890     11 12000    0 true 3.9 240 32 2 true .14 11 1.5 2 true 5.7 290 48 2 timeout 900   2600 11000 0 true 6.3 290 51 2 true 12   270 99 2 true 20   110 220 1
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true .16  25 1.6  2 true 1.2  33 11   2 true 3.5 280 30 2 true 4.0 280 34 2 true 2.4 240 21 2 true 5.8  260 65   2 true .078 26 .72 2 true .13  26 .95 2 true 5.0 300 44 2 true .33  11 3.5  2 true 3.6 240 36 2 true .16 11 1.5 2 true 55   450 670 2 timeout 900   490 10000 0 true 130   570 1800 2 true 16   300 110 2 true 12   120 160 1
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true .10  23 1.0  2 true 1.1  33 11   2 true 2.9 270 25 2 true 3.0 270 26 2 true 2.4 250 21 2 true 3.3  250 32   2 true .11  26 .78 2 true .11  26 .74 2 true 4.2 290 38 2 true .30  11 3.5  2 true 3.8 240 34 2 true .17 11 1.6 2 true 6.1 290 49 2 true 7.3 440 61 2 true 6.9 360 53 2 true 11   280 86 2 true 11   120 130 1
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i false(unreach-call) 4.3   1400 45    1 false(unreach-call) 9.8  1100 68   1 error 2.6 290 21 0 error 2.6 260 21 0 false(unreach-call) 2.9 260 26 1 false(unreach-call) .54 75 7.8 0 false(unreach-call) .16  28 1.3  1 false(unreach-call) .15  28 1.3  1 false(unreach-call) 4.3 290 36 1 false(unreach-call) .38  19 4.6  1 false(unreach-call) 5.4 310 45 1 false(unreach-call) .24 24 3.0 1 false(unreach-call) 4.5 270 36 1 false(unreach-call) 4.4 260 36 1 false(unreach-call) 4.6 270 37 1 false(unreach-call) 560   5400 8500 1 timeout 900   98 11000 0
loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i out of memory 670     15000 4000    0 true 9.0  580 110   1 timeout 900   4200 8400 0 timeout 900   3900 11000 0 timeout 900   3700 9400 0 unknown 890    150 10000   0 true 16     160 220    1 true 16     160 220    1 timeout 900   4100 11000 0 true .47  11 6.3  1 unknown 28   680 240 0 true .19 11 1.6 1 timeout 900   710 12000 0 timeout 900   2800 12000 0 timeout 900   810 11000 0 true 15   220 89 1 true 17   130 230 1
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i out of memory 260     15000 2600    0 out of memory 140    15000 2000   0 error 2.8 290 25 0 error 2.5 270 22 0 timeout 900   3400 9900 0 unknown 900    170 10000   0 timeout 900     3400 10000    0 timeout 900     3400 9900    0 timeout 900   4100 13000 0 unknown 900     75 10000    0 unknown 43   720 520 0 true 280    58 4000   1 timeout 900   770 12000 0 timeout 900   2000 12000 0 timeout 900   830 9800 0 true 16   220 96 1 unknown 220   270 2400 0
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i out of memory 270     15000 2600    0 out of memory 140    15000 1700   0 error 2.6 270 22 0 error 2.5 260 24 0 timeout 900   5800 8100 0 unknown 890    170 10000   0 timeout 900     6700 9600    0 timeout 900     6600 9600    0 timeout 900   4600 12000 0 true 1.6   11 21    1 unknown 45   710 430 0 true .24 13 3.1 1 timeout 900   810 11000 0 timeout 900   2300 13000 0 timeout 900   790 11000 0 true 15   220 100 1 true 14   130 200 1
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i out of memory 250     15000 1900    0 error (134) 35    14000 560   0 error 2.6 270 23 0 error 2.5 260 22 0 true 7.7 490 88 2 unknown 890    100 12000   0 timeout 900     230 12000    0 timeout 900     240 13000    0 timeout 900   5100 11000 0 true 1.2   160 14    2 true 40   750 460 2 timeout (timeout) 900    260 10000   0 true 68   510 930 1 timeout 900   3200 11000 0 true 69   550 880 1 true 17   220 120 2 unknown 15   110 170 0
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i true .67  30 8.5  2 out of memory 430    15000 6200   0 true 4.3 290 42 2 true 5.2 330 47 2 true 350   2700 4200 2 unknown 38    75 470   0 timeout 900     10000 10000    0 true .88  29 12    2 true 2.9 280 25 2 unknown 890     11 14000    0 true 4.3 260 37 2 true 240    15000 2900   2 true 4.8 290 40 2 true 5.6 310 50 2 true 4.8 280 41 2 true 12   280 99 2 error (1) 17   190 240 0
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i timeout 900     370 11000    0 out of memory 480    15000 6300   0 true 4.6 290 43 2 true 6.8 410 55 2 true 150   2300 1700 2 true 160    2400 1700   2 timeout 900     11000 12000    0 true .075 26 .94 2 true 3.4 270 34 2 unknown 890     11 14000    0 true 4.1 260 40 2 true 240    15000 3700   2 true 4.9 290 39 2 timeout 900   1700 10000 0 true 5.0 290 39 2 true 12   280 96 2 error (1) 11   170 140 0
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) .12  23 .86 1 false(unreach-call) .27 35 2.2 1 false(unreach-call) 3.8 290 34 1 false(unreach-call) 3.6 290 32 0 false(unreach-call) 3.4 270 29 1 false(unreach-call) .60 76 7.8 1 false(unreach-call) .22  28 2.6  1 false(unreach-call) .26  28 1.8  1 false(unreach-call) 3.0 280 29 1 false(unreach-call) .58  12 7.8  1 false(unreach-call) 6.0 330 51 1 false(unreach-call) .19 12 1.9 1 false(unreach-call) 5.6 290 42 1 false(unreach-call) 6.5 380 55 1 false(unreach-call) 6.8 330 51 1 false(unreach-call) 16   280 120 1 unknown 15   120 230 0
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i timeout 900     420 8900    0 error (42) 870    200 9700   0 true 3.5 280 34 2 true 3.5 270 32 2 timeout 900   3200 9400 0 unknown 900    77 12000   0 timeout 900     85 13000    0 timeout 900     91 10000    0 timeout 900   5400 11000 0 unknown 900     660 11000    0 true 38   740 370 2 timeout (timeout) 900    1400 14000   0 true 6.9 350 53 2 true 8.4 470 67 2 true 8.2 480 75 2 true 83   860 790 2 unknown 38   170 480 0
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i true .16  24 1.4  2 error (42) 870    11000 4500   0 true 4.8 290 38 2 true 5.3 290 52 2 timeout 910   10000 9300 0 unknown 54    75 760   0 timeout 900     790 11000    0 true .11  26 1.4  2 timeout 900   5600 11000 0 unknown 900     910 11000    0 true 4.4 260 41 2 timeout (timeout) 900    1100 11000   0 true 7.2 370 52 2 true 8.2 480 72 2 true 9.1 490 78 2 true 80   1300 790 2 true 13   140 180 1
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i true 2.1   46 27    2 error (42) 870    470 8600   0 true 68   3600 660 2 true 98   4000 1100 2 true 8.4 340 95 2 unknown 890    110 9800   0 timeout 900     410 11000    0 timeout 900     400 11000    0 true 5.8 300 47 2 unknown 900     170 11000    0 unknown 63   720 720 0 timeout (timeout) 900    1500 7300   0 true 10   520 91 2 true 22   830 230 2 true 86   2000 810 2 true 95   850 810 2 unknown 270   320 2900 0
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i timeout 900     2100 10000    0 error (42) 870    480 12000   0 true 15   620 110 2 true 12   610 100 1 true 4.7 280 38 2 unknown 890    100 9900   0 timeout 900     82 11000    0 timeout 900     81 8700    0 timeout 900   5800 11000 0 unknown 890     130 13000    0 unknown 39   740 420 0 timeout (timeout) 900    3300 13000   0 true 9.8 540 77 2 true 19   710 180 2 true 37   870 330 2 timeout 900   9400 8400 0 unknown 170   220 2800 0
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i true .63  30 6.9  2 error (42) 870    690 9800   0 true 13   630 110 2 true 17   730 120 2 true 210   2500 2500 2 unknown 890    100 12000   0 timeout 900     140 11000    0 timeout 900     150 11000    0 timeout 900   5600 11000 0 unknown 900     320 10000    0 unknown 75   720 1000 0 timeout (timeout) 900    3600 9000   0 true 8.6 470 70 2 true 12   490 82 2 true 9.7 550 91 2 timeout 900   4600 7800 0 unknown 350   370 4500 0
loop-invgen/down_true-unreach-call_true-termination.i timeout 900     1600 8700    0 error (42) 870    2600 5900   0 timeout 900   4100 10000 0 timeout 900   4100 13000 0 timeout 910   12000 9300 0 unknown 89    100 1100   0 timeout 900     510 11000    0 timeout 900     510 13000    0 timeout 900   4900 9700 0 unknown 890     400 8200    0 true 28   750 320 1 timeout (timeout) 900    420 11000   0 timeout 900   5300 11000 0 timeout 900   5300 12000 0 true 7.7 390 60 1 true 89   1400 750 1 true 13   130 220 1
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i timeout 900     3000 11000    0 error (42) 870    1600 6400   0 timeout 900   4200 13000 0 timeout 900   4200 12000 0 timeout 900   11000 8800 0 unknown 92    130 1300   0 timeout 900     1000 11000    0 timeout 900     1000 11000    0 timeout 900   4900 13000 0 unknown 900     190 12000    0 true 28   710 320 1 timeout (timeout) 900    1400 8600   0 timeout 900   5200 13000 0 timeout 900   5300 12000 0 timeout 900   5200 12000 0 true 13   230 75 1 true 17   160 220 1
loop-invgen/half_2_true-unreach-call_true-termination.i timeout 900     1900 11000    0 error (42) 870    1100 6800   0 timeout 900   4100 7800 0 timeout 900   4100 9300 0 timeout 900   7700 8800 0 unknown 170    110 2500   0 timeout 900     480 12000    0 timeout 900     470 11000    0 timeout 900   4400 12000 0 unknown 900     840 8200    0 true 30   740 300 1 timeout (timeout) 900    1700 11000   0 timeout 900   5000 12000 0 timeout 900   4700 13000 0 timeout 900   3000 12000 0 true 91   1100 650 1 true 20   160 240 1
loop-invgen/heapsort_true-unreach-call_true-termination.i timeout 900     2000 5300    0 error (42) 870    12000 7100   0 true 64   2900 660 2 true 60   2900 620 2 timeout 900   5100 9200 0 unknown 890    710 10000   0 timeout 900     560 11000    0 timeout 900     620 11000    0 true 41   2200 350 2 unknown 900     900 8800    0 unknown 110   840 1300 0 timeout (timeout) 900    1200 12000   0 true 88   1100 1100 2 true 91   1800 1100 2 error (7) 460   1300 4800 0 true 140   890 1300 2 unknown 36   130 540 0
loop-invgen/id_build_true-unreach-call_true-termination.i true .21  26 2.0  2 error (134) 380    12000 4800   0 true 3.2 270 31 2 true 3.2 270 32 2 true 200   1800 2700 2 true 210    1100 2800   2 timeout 900     1000 12000    0 true .17  26 1.9  2 true 2.9 280 29 2 unknown 900     680 13000    0 true 38   750 420 2 timeout (timeout) 900    1700 12000   0 true 5.5 290 41 2 true 7.0 450 61 2 true 8.4 420 64 2 true 13   290 96 2 true 16   130 180 1
loop-invgen/large_const_true-unreach-call_true-termination.i true .22  27 2.4  2 true .44 35 3.9 2 true 4.2 290 35 2 true 4.2 280 37 2 true 3.8 270 35 2 true 4.5  280 40   2 true .12  26 .79 2 true .083 26 .78 2 true 5.3 300 42 2 true .89  12 11    2 true 39   760 480 2 true .16 12 1.9 2 true 7.6 380 59 2 true 7.5 460 59 2 true 16   720 130 2 true 20   290 140 2 unknown 15   110 220 0
loop-invgen/nest-if3_true-unreach-call_true-termination.i true .78  35 8.3  2 error (134) 710    13000 4800   0 true 4.6 290 40 2 true 4.6 280 46 2 timeout 900   5000 11000 0 unknown 900    310 7600   0 timeout 900     360 10000    0 timeout 900     320 11000    0 true 3.2 280 25 2 unknown 890     460 11000    0 timeout 900   1500 9600 0 timeout (timeout) 900    38 12000   0 true 5.1 290 43 2 true 9.4 510 82 2 true 4.9 280 41 2 true 84   800 790 2 unknown 230   470 2500 0
loop-invgen/nested6_true-unreach-call_true-termination.i timeout 900     2700 4400    0 error (42) 870    500 3600   0 true 140   3900 1500 2 true 120   4100 1200 2 timeout 910   8900 9400 0 unknown 900    4000 8100   0 timeout 900     730 9800    0 timeout 900     700 12000    0 true 6.8 430 58 2 unknown 900     700 10000    0 timeout 900   1400 8800 0 timeout (timeout) 900    3500 9100   0 true 8.6 470 67 2 true 9.5 490 75 2 true 43   950 480 2 error 900   8000 5900 0 true 470   440 4700 1
loop-invgen/nested9_true-unreach-call_true-termination.i timeout 900     330 7900    0 error (134) 230    12000 1800   0 true 11   470 79 2 true 10   460 83 2 timeout 900   6100 9200 0 timeout 900    6100 8000   0 timeout 900     4300 10000    0 timeout 900     4300 11000    0 true 6.3 390 54 2 unknown 890     67 11000    0 timeout 900   1500 10000 0 timeout (timeout) 900    520 14000   0 true 9.5 500 81 2 true 18   680 180 2 true 11   550 81 2 true 90   860 890 2 true 350   1000 4300 1
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i timeout 900     2100 11000    0 error (42) 870    3800 8200   0 true 12   580 85 2 true 14   600 99 2 timeout 900   9700 8700 0 unknown 230    82 2700   0 timeout 900     920 11000    0 timeout 900     910 12000    0 true 7.3 440 59 2 unknown 890     40 11000    0 true 30   750 300 2 timeout (timeout) 900    900 13000   0 true 14   630 130 1 true 21   710 230 2 true 27   840 230 1 true 760   3900 6500 1 unknown 430   370 5700 0
loop-invgen/seq_true-unreach-call_true-termination.i timeout 900     830 6700    0 error (42) 870    240 6000   0 timeout 900   4000 14000 0 timeout 900   4000 10000 0 timeout 900   11000 10000 0 timeout 900    9900 9400   0 timeout 900     280 11000    0 timeout 900     270 10000    0 timeout 900   4900 12000 0 unknown 900     200 11000    0 true 35   730 430 1 timeout (timeout) 900    1500 13000   0 timeout 900   1400 15000 0 timeout 900   5300 14000 0 timeout 900   1500 11000 0 true 98   1000 870 1 true 18   170 200 1
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i error (6) .093 22 .61 0 error (42) 870    9600 5700   0 timeout 900   4300 8800 0 timeout 900   4100 9600 0 timeout 900   10000 9200 0 unknown 900    15000 13000   0 out of memory 290     15000 3300    0 out of memory 300     15000 3000    0 true 2.9 270 24 1 unknown 890     98 11000    0 unknown 250   750 2800 0 timeout (timeout) 900    300 10000   0 timeout 900   4200 15000 0 timeout 900   6000 13000 0 true 8.3 430 63 1 true 93   1300 800 1 unknown 4.3 92 52 0
loop-invgen/up_true-unreach-call_true-termination.i timeout 900     1900 9800    0 error (42) 870    1400 9600   0 timeout 900   4100 10000 0 timeout 900   4100 11000 0 out of memory 810   15000 7200 0 unknown 71    100 860   0 timeout 900     730 11000    0 timeout 900     720 13000    0 timeout 900   5000 13000 0 unknown 900     420 8900    0 true 29   740 290 1 timeout (timeout) 900    1800 11000   0 timeout 900   5300 13000 0 timeout 900   5300 13000 0 timeout 900   5100 14000 0 true 88   1400 740 1 true 14   130 190 1
loop-lit/afnp2014_true-unreach-call_true-termination.c.i timeout 900     2000 10000    0 true 17    150 190   2 timeout 900   4000 11000 0 timeout 900   4000 11000 0 true 8.2 460 70 1 unknown 86    75 1100   0 true 680     1300 8100    2 true 680     1300 8200    2 timeout 900   4200 11000 0 unknown 890     29 12000    0 unknown 400   740 4100 0 true 6.4  14 91   2 true 5.8 300 49 2 timeout 900   5200 11000 0 true 6.5 340 54 2 true 7.9 220 58 2 true 11   110 130 1
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i timeout 900     280 12000    0 error (42) 870    370 10000   0 true 3.0 270 28 2 true 3.0 270 26 1 timeout 900   2000 9700 0 timeout 900    2700 11000   0 timeout 900     140 11000    0 timeout 900     140 11000    0 true 4.6 300 37 2 unknown 900     580 11000    0 true 52   790 570 2 timeout (timeout) 900    21 11000   0 true 7.4 420 64 2 true 5.8 340 43 2 true 10   530 93 2 true 120   720 1300 2 true 320   370 3800 1
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true .19  25 1.6  2 true .76 33 7.5 2 true 2.9 280 26 2 true 2.9 270 25 2 true 2.5 250 22 2 true 3.4  260 30   2 true .085 26 .67 2 true .11  26 1.1  2 true 4.5 290 39 2 true .35  11 3.7  2 true 23   700 190 2 true .16 11 1.6 2 true 6.6 340 57 2 true 7.2 460 62 2 true 7.2 420 69 2 true 13   280 97 2 true 8.9 110 120 1
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i timeout 900     1600 10000    0 error (42) 870    2700 4600   0 true 3.1 280 27 2 true 3.2 270 29 2 timeout 910   7100 9100 0 timeout 900    8700 9000   0 timeout 900     350 11000    0 timeout 900     340 13000    0 true 3.8 280 30 2 unknown 900     330 11000    0 true 6.1 320 56 2 true .15 11 1.7 2 true 6.4 320 49 2 true 6.0 340 45 2 true 7.6 420 70 2 true 81   1400 700 2 true 11   110 140 1
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i timeout 900     5300 6700    0 true 2.8  33 28   2 true 4.0 280 33 2 true 4.3 280 39 2 true 4.1 270 35 2 true 4.6  270 47   2 true .24  26 3.3  2 true .29  27 3.3  2 true 4.3 280 36 2 true .33  11 4.7  2 true 4.3 260 36 2 true .16 11 1.7 2 true 5.9 280 46 2 true 6.4 370 57 2 true 7.6 390 62 2 true 8.8 230 61 2 true 26   170 320 1
loop-lit/css2003_true-unreach-call_true-termination.c.i timeout 900     340 8000    0 error (42) 870    900 3800   0 true 5.9 370 47 2 true 3.2 270 27 2 true 3.4 270 34 2 unknown 51    77 730   0 timeout 900     5600 10000    0 true .16  26 1.8  2 true 3.5 280 32 2 true 150     12 1900    2 true 31   750 340 2 true 7.5  160 100   2 true 5.1 290 42 2 true 5.6 320 47 2 true 4.9 290 41 2 true 9.3 210 70 2 true 14   150 180 1
loop-lit/ddlm2013_true-unreach-call.i timeout 900     2000 11000    0 error (42) 870    1300 9200   0 timeout 900   4200 13000 0 true 270   4000 2800 2 timeout 900   7000 12000 0 unknown 210    310 2300   0 timeout 900     1400 9900    0 timeout 900     1400 11000    0 timeout 900   4500 10000 0 unknown 890     30 13000    0 unknown 40   800 530 0 timeout (timeout) 900    76 14000   0 true 10   530 81 2 timeout 900   5600 10000 0 true 17   530 180 2 unknown 560   2200 5600 0 true 220   220 3000 1
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 5.5   89 69    2 true 2.6  33 25   2 true 87   3900 820 2 true 100   3600 1000 2 true 3.3 260 30 2 unknown 37    76 550   0 true .27  26 2.8  2 true .28  26 2.8  2 true 66   3700 630 2 true .34  11 3.9  2 true 3.6 240 31 2 true .15 11 1.9 2 true 65   1500 660 2 true 240   3200 3100 2 true 100   1400 1100 2 true 19   440 130 2 true 210   240 3000 1
loop-lit/gj2007b_true-unreach-call_true-termination.c.i timeout 900     1300 12000    0 error (42) 870    2700 6400   0 true 16   630 120 2 true 24   890 160 2 timeout 900   4500 9500 0 unknown 200    130 2800   0 timeout 900     870 9900    0 timeout 900     870 11000    0 true 5.5 310 47 2 unknown 900     1000 12000    0 true 21   670 200 2 timeout (timeout) 900    1600 9700   0 true 6.5 310 59 2 true 6.9 470 57 2 true 9.6 520 76 2 true 86   1100 770 2 unknown 260   380 3200 0
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 9.6   130 120    2 true 2.7  33 28   2 true 47   2300 440 2 true 66   2300 720 2 true 3.7 260 29 2 unknown 170    120 1900   0 true .32  26 3.1  2 true .30  26 4.0  2 true 110   3800 1200 2 true .34  11 3.9  2 unknown 300   740 3300 0 true .16 11 1.8 2 true 140   3500 1500 2 true 880   5300 12000 2 true 180   2400 2200 2 true 30   610 190 2 unknown 210   200 2600 0
loop-lit/gsv2008_true-unreach-call_true-termination.c.i timeout 900     800 9900    0 true 220    620 2500   2 true 3.6 280 31 2 true 3.5 270 30 1 true 570   2600 7300 1 unknown 900    580 6500   0 timeout 900     94 10000    0 timeout 900     92 11000    0 true 3.0 270 26 2 unknown 900     40 11000    0 true 54   850 540 2 timeout (timeout) 900    39 12000   0 true 5.4 290 48 2 true 6.4 420 49 2 true 6.1 310 47 2 true 160   800 1900 2 true 19   160 290 1
loop-lit/hhk2008_true-unreach-call_true-termination.c.i timeout 900     380 8800    0 error (42) 870    270 10000   0 true 3.2 280 29 2 true 3.4 270 27 2 timeout 910   7900 9600 0 timeout 900    8000 9000   0 timeout 900     330 12000    0 timeout 900     330 13000    0 true 4.3 280 36 2 unknown 900     330 11000    0 true 6.7 340 53 2 true .17 11 1.5 2 true 6.1 290 51 2 true 5.7 310 46 2 true 6.9 350 57 2 true 82   1300 720 2 true 12   120 180 1
loop-lit/jm2006_true-unreach-call_true-termination.c.i timeout 900     1400 9200    0 error (42) 870    5400 4200   0 true 3.1 280 29 2 true 3.0 270 26 2 true 3.4 270 29 2 true 4.0  270 42   2 timeout 900     1000 11000    0 timeout 900     1000 10000    0 true 3.0 270 25 2 unknown 900     680 9600    0 true 4.0 250 41 2 true .15 11 1.8 2 true 6.2 300 51 2 true 5.6 320 47 2 true 7.3 350 59 2 true 82   1300 650 1 true 11   120 140 1
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i timeout 900     1600 12000    0 error (42) 870    4200 5000   0 true 4.2 290 36 2 true 4.0 290 32 2 timeout 900   6900 9900 0 timeout 900    10000 8400   0 timeout 900     1300 11000    0 timeout 900     1300 11000    0 timeout 900   5400 11000 0 unknown 900     650 11000    0 true 6.9 340 55 2 true .18 12 1.7 2 true 6.2 300 47 2 true 5.7 330 49 2 true 7.3 400 57 2 true 82   1300 740 2 true 13   120 200 1
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i error (134) .16  23 1.6  0 error (42) 870    13000 6800   0 false(unreach-call) 4.0 300 37 -16 false(unreach-call) 5.2 300 45 -16 timeout 900   4300 8400 0 unknown 890    100 13000   0 timeout 900     190 12000    0 timeout 900     200 13000    0 false(unreach-call) 5.1 300 41 -16 true .43  12 4.8  1 unknown 6.0 330 51 0 unknown 140    270 1700   0 timeout 900   700 13000 0 timeout 900   2800 11000 0 timeout 900   860 12000 0 true 100   620 1200 1 unknown 4.8 92 59 0
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) .13  23 .90 1 false(unreach-call) .26 33 1.8 1 false(unreach-call) 92   4200 820 1 false(unreach-call) 89   4300 760 1 false(unreach-call) 2.6 250 22 1 false(unreach-call) 16    81 200   1 false(unreach-call) .12  28 .82 1 false(unreach-call) .11  28 .97 1 false(unreach-call) 2.8 260 27 1 false(unreach-call) .39  12 4.4  1 false(unreach-call) 5.6 310 48 1 false(unreach-call) .19 11 1.8 1 false(unreach-call) 4.7 270 40 1 false(unreach-call) 4.5 260 38 1 false(unreach-call) 4.5 280 35 1 false(unreach-call) 16   280 120 1 false(unreach-call) 10   100 130 1
loop-new/count_by_1_true-unreach-call_true-termination.i true .14  24 1.1  2 true 120    3400 1400   2 timeout 900   4200 9600 0 timeout 900   4200 8500 0 true 350   3100 4200 2 true 350    3100 4000   2 timeout 900     12000 12000    0 timeout 900     12000 11000    0 timeout 910   5000 12000 0 true 17     11 220    2 true 3.8 250 41 2 true .16 11 1.5 2 true 5.6 290 48 2 timeout 900   5700 12000 0 true 5.3 290 44 2 true 11   290 85 2 true 8.5 110 110 1
loop-new/count_by_1_variant_true-unreach-call_true-termination.i true .15  24 1.1  2 out of memory 840    15000 10000   0 true 3.7 280 31 2 true 4.3 280 41 2 true 350   3600 3800 2 unknown 37    75 440   0 timeout 900     11000 10000    0 true .078 26 .74 2 true 3.4 280 29 2 true 92     11 1400    2 true 4.1 250 43 2 true 2.9  180 46   2 true 6.4 310 51 2 true 5.8 350 45 2 true 5.5 300 51 2 true 14   280 120 2 true 73   330 930 1
loop-new/count_by_2_true-unreach-call_true-termination.i timeout 900     1200 11000    0 true 60    1700 680   1 timeout 900   4200 10000 0 timeout 900   4300 12000 0 timeout 900   6700 8400 0 unknown 57    75 730   0 timeout 900     12000 10000    0 timeout 900     12000 13000    0 timeout 900   4900 11000 0 true 8.1   11 120    1 true 4.0 250 36 1 true .14 11 1.8 1 timeout 900   4800 13000 0 timeout 900   5700 12000 0 timeout 900   2600 14000 0 true 79   1200 700 1 true 8.6 110 100 1
loop-new/count_by_k_true-unreach-call_true-termination.i timeout 900     1200 11000    0 error (42) 870    8000 3500   0 timeout 900   4100 12000 0 timeout 900   4100 10000 0 timeout 900   3500 9600 0 unknown 76    76 980   0 timeout 900     240 11000    0 timeout 900     240 9400    0 timeout 900   4000 11000 0 unknown 900     26 12000    0 unknown 270   710 3200 0 timeout (timeout) 900    12 12000   0 timeout 900   1500 13000 0 timeout 900   5100 13000 0 timeout 900   1400 12000 0 true 78   1100 710 1 true 14   180 190 1
loop-new/count_by_nondet_true-unreach-call_true-termination.i timeout 900     2000 11000    0 error (42) 870    1500 7900   0 timeout 900   4300 8700 0 timeout 900   4400 10000 0 timeout 900   3300 9300 0 timeout 900    3700 10000   0 timeout 900     2900 11000    0 timeout 900     2900 10000    0 timeout 900   5300 10000 0 timeout 900     73 12000    0 unknown 480   770 5300 0 timeout (timeout) 900    56 12000   0 timeout 900   4800 11000 0 timeout 900   5900 14000 0 timeout 900   3600 11000 0 timeout 900   850 7500 0 unknown 310   350 3500 0
loop-new/gauss_sum_true-unreach-call_true-termination.i timeout 900     1600 14000    0 true 22    130 250   1 error 3.3 290 29 0 unknown 3.1 280 31 0 true 240   2500 2700 1 unknown 550    110 7900   0 true 550     880 7200    1 true 550     880 6200    1 false(unreach-call) 3.0 270 26 -16 true 78     65 900    1 unknown 17   320 210 0 true .66 12 8.3 1 timeout 900   1100 15000 0 timeout 900   2700 9600 0 unknown 850   960 12000 0 true 79   230 940 1 true 13   210 150 1
loop-new/half_true-unreach-call_true-termination.i timeout 900     1800 11000    0 error (42) 870    6100 5200   0 true 4.9 300 40 2 true 4.6 290 44 2 timeout 900   6200 9500 0 unknown 74    76 910   0 timeout 900     1300 12000    0 timeout 900     1300 9900    0 true 5.8 360 48 2 unknown 900     1600 9700    0 unknown 26   720 290 0 timeout (timeout) 900    1900 12000   0 true 11   490 93 2 timeout 900   4100 13000 0 true 21   630 220 2 unknown 590   3500 6300 0 unknown 300   180 3400 0
loop-new/nested_true-unreach-call_true-termination.i timeout 900     2600 5600    0 error (42) 870    3900 4000   0 true 130   2600 1500 2 true 120   2500 1400 2 timeout 900   5100 9400 0 unknown 900    480 7500   0 timeout 900     530 12000    0 timeout 900     540 13000    0 true 210   4000 2400 2 unknown 890     680 12000    0 true 6.7 350 67 2 true .26 12 3.3 2 true 140   4600 1500 2 true 230   3800 3800 2 true 150   4600 1800 2 timeout 900   3900 5600 0 unknown 420   190 6300 0
loop-industry-pattern/aiob_1_true-unreach-call.c true .37  32 3.5  2 true 8.6  38 110   1 true 140   2300 1700 2 true 79   2600 850 2 true 30   680 260 2 true 58    620 730   2 true .73  48 9.3  2 true .14  28 1.4  2 true 65   3700 640 2 true .40  12 4.6  2 unknown 5.6 350 51 0 true .20 11 2.1 2 timeout 900   2700 5400 0 timeout 900   5000 9700 0 timeout 900   6200 7200 0 true 46   690 380 2 unknown 2.5 92 35 0
loop-industry-pattern/aiob_2_true-unreach-call.c true .41  32 3.6  2 true 9.1  39 88   1 true 140   2400 1800 2 true 82   2500 910 2 true 29   700 270 2 true 59    590 660   2 true .71  48 8.9  2 true .14  28 1.3  2 true 58   3700 570 1 true .38  11 4.5  2 unknown 5.2 340 52 0 true .19 11 1.9 2 timeout 900   1700 6000 0 timeout 900   5000 11000 0 timeout 900   6200 6600 0 true 43   680 410 2 unknown 2.4 92 31 0
loop-industry-pattern/aiob_3_true-unreach-call.c true .38  32 3.2  2 true 9.0  38 83   1 true 140   2200 1500 2 true 78   2600 870 2 true 28   700 260 2 true 58    600 820   2 true .72  48 8.2  2 true .13  28 1.3  2 true 60   3700 630 1 true .37  12 4.2  2 unknown 5.5 330 49 0 true .18 11 2.2 2 timeout 900   2300 4600 0 timeout 900   5000 11000 0 timeout 900   6300 7000 0 true 45   680 340 2 unknown 2.5 92 39 0
loop-industry-pattern/aiob_4_true-unreach-call.c true .38  32 3.4  2 true 8.8  41 84   1 true 130   2300 1600 2 true 86   2800 870 2 true 29   700 320 2 true 46    630 570   2 true .71  48 10    2 true .12  28 1.5  2 true 65   3700 710 2 true .40  12 4.4  2 unknown 4.1 270 41 0 true .20 11 1.5 2 timeout 900   1800 6100 0 timeout 900   5100 9500 0 timeout 900   5900 9400 0 true 43   690 360 2 unknown 2.5 92 31 0
loop-industry-pattern/mod3_true-unreach-call.c true .65  30 7.6  2 error (42) 870    240 9500   0 true 3.3 280 31 2 true 3.2 270 29 2 true 20   290 240 2 unknown 890    90 12000   0 timeout 900     82 12000    0 timeout 900     84 10000    0 true 4.2 290 33 2 unknown 900     260 11000    0 unknown 260   1100 2600 0 timeout (timeout) 900    22 12000   0 true 24   290 270 2 timeout 900   4300 12000 0 true 33   300 370 2 true 17   330 160 2 true 34   250 410 1
loop-industry-pattern/nested_true-unreach-call.c timeout 900     320 8800    0 error (6) 440    15000 5000   0 timeout 900   4100 11000 0 timeout 900   4000 10000 0 timeout 900   5200 9600 0 unknown 900    580 8200   0 timeout 900     7700 8400    0 timeout 900     7800 9200    0 timeout 900   5100 11000 0 unknown 900     11 12000    0 timeout 900   1200 8400 0 timeout (timeout) 900    11000 13000   0 true 56   1600 500 2 timeout 900   5100 12000 0 true 24   830 190 2 true 89   880 850 2 timeout 900   250 8800 0
loop-industry-pattern/ofuf_1_true-unreach-call.c error (5) .29  30 2.8  0 error (6) .54 38 4.9 0 error 13   520 110 0 unknown 13   670 99 0 true 63   2500 550 2 unknown 510    640 5600   0 timeout 900     500 9600    0 true .20  28 2.3  2 false(unreach-call) 10   460 86 -16 true .41  12 5.2  2 unknown 7.4 510 60 0 timeout (timeout) 900    58 14000   0 true 8.8 380 79 2 true 10   520 78 2 true 9.6 400 72 2 true 26   350 230 2 unknown 2.5 92 31 0
loop-industry-pattern/ofuf_2_true-unreach-call.c error (5) .32  30 3.2  0 error (6) .55 38 5.0 0 error 13   540 110 0 unknown 13   680 90 0 true 59   2500 540 2 unknown 510    640 6000   0 timeout 900     230 11000    0 true .20  28 2.4  2 false(unreach-call) 9.8 470 70 -16 true .44  12 5.0  2 unknown 7.6 520 64 0 timeout (timeout) 900    60 14000   0 true 8.1 370 63 2 true 9.4 500 70 2 true 8.5 390 73 2 true 27   330 240 2 unknown 2.5 92 30 0
loop-industry-pattern/ofuf_3_true-unreach-call.c error (5) .33  30 2.6  0 error (6) .51 38 4.9 0 error 14   530 110 0 unknown 13   670 100 0 true 60   2400 550 2 unknown 510    640 7200   0 timeout 900     230 12000    0 true .22  28 2.5  2 false(unreach-call) 10   460 86 -16 true .42  12 4.8  2 unknown 7.7 510 59 0 timeout (timeout) 900    59 12000   0 true 8.3 370 67 2 true 9.5 500 76 2 true 8.7 390 63 2 true 26   350 240 2 unknown 2.5 92 31 0
loop-industry-pattern/ofuf_4_true-unreach-call.c error (5) .32  30 3.0  0 error (6) .52 38 6.2 0 error 13   540 99 0 unknown 14   630 110 0 true 59   2500 550 2 unknown 490    580 5800   0 timeout 900     560 8800    0 true .19  28 2.4  2 false(unreach-call) 11   470 85 -16 true .42  12 4.8  2 unknown 7.5 510 64 0 timeout (timeout) 900    62 14000   0 true 9.1 390 74 2 true 9.9 500 83 2 true 20   580 160 2 true 27   340 220 2 unknown 2.5 92 34 0
loop-industry-pattern/ofuf_5_true-unreach-call.c error (5) .30  30 2.7  0 error (6) .54 38 4.7 0 error 12   540 100 0 unknown 14   650 110 0 true 58   2400 550 2 unknown 490    580 6900   0 false(unreach-call) 13     110 180    -16 true .21  28 2.2  2 false(unreach-call) 11   470 95 -16 true .42  12 4.7  2 unknown 7.5 560 56 0 timeout (timeout) 900    59 12000   0 true 8.3 370 65 2 true 10   500 76 2 true 20   580 160 2 true 26   340 210 2 unknown 2.5 92 37 0
loops/heavy_true-unreach-call.c error (134) 27     15000 370    0 out of memory 330    15000 4000   0 true 3.0 300 27 1 true 2.8 270 23 1 true 93   2200 1300 1 true 330    5300 5000   1 timeout 900     4500 9700    0 true 16     4100 230    1 true 5.8 300 41 1 unknown 900     41 12000    0 true 6.6 790 60 1 true .41 30 5.8 1 timeout 910   9200 7900 0 timeout 900   11000 7900 0 timeout 900   9200 7300 0 true 23   770 190 1 unknown 3.8 92 48 0
loops/compact_false-unreach-call.c out of memory 410     15000 3800    0 out of memory 140    15000 2100   0 timeout 900   4200 8800 0 timeout 900   4300 10000 0 timeout 900   6200 8400 0 unknown 78    100 1100   0 timeout 900     10000 9500    0 timeout 900     10000 10000    0 timeout 900   4200 12000 0 unknown 900     99 12000    0 unknown 110   690 1200 0 timeout (timeout) 900    1100 8700   0 timeout 900   5200 7700 0 timeout 900   5300 5700 0 timeout 900   5200 7200 0 false(unreach-call) 140   450 1600 0 unknown 3.8 92 50 0
loops/heavy_false-unreach-call.c error (134) 27     15000 380    0 out of memory 340    15000 4100   0 timeout 900   5000 11000 0 false(unreach-call) 3.0 280 28 0 timeout 900   3100 9700 0 unknown 890    5400 11000   0 timeout 900     4500 12000    0 timeout 900     4500 11000    0 timeout 900   4400 13000 0 unknown 890     39 12000    0 timeout 900   1400 6500 0 false(unreach-call) .41 30 4.3 0 timeout 900   8700 7200 0 timeout 900   11000 5700 0 timeout 900   9200 9100 0 timeout 900   12000 7900 0 unknown 3.8 92 62 0
../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 163 48000 310000 500000 139 163 50000 640000 440000 106 163 34000   230000 370000 137 163 33000 230000 370000 59 163 51000 430000 540000 178 163 43000 150000 490000 119 163 74000 370000 890000 91 163 62000 300000 760000 134 163 48000 320000 610000 13 163 59000   20000 760000 -134 163 12000 82000 120000 154 163 43000   210000 550000 152 163 47000 190000 560000 189 163 61000 330000 770000 159 163 44000 180000 530000 191 163 20000 180000 200000 216 163 15000 170000 180000 44
    correct results 86 690 15000 3200 137 66 570 10000 6600 94 100 1700   65000 17000 165 85 1700 66000 17000 148 106 4900 85000 57000 171 72 3400 39000 41000 116 70 2000 7400 23000 101 82 1900 7700 22000 127 91 1800 63000 19000 150 69 1200   1100 15000 112 87 860 32000 8300 141 88 520   31000 7100 137 111 2300 53000 24000 187 96 2400 52000 29000 158 109 2900 58000 32000 184 114 6500 81000 66000 188 21 210 2800 2800 21
        correct true 51 73 2500 820 102 28 510 7100 6000 56 65 1400   49000 15000 130 63 1500 54000 15000 126 65 4100 64000 48000 130 44 2800 36000 33000 88 31 1600 4300 19000 62 45 1500 4500 18000 90 59 970 43000 10000 118 43 1100   820 14000 86 54 640 21000 6400 108 49 510   30000 7000 98 76 1300 38000 13000 152 62 2000 38000 25000 124 75 1800 41000 20000 150 74 3000 38000 26000 148 0
        correct false 35 620 13000 2300 35 38 56 3300 580 38 35 270   16000 2400 35 22 220 12000 1800 22 41 740 21000 8600 41 28 580 2600 8000 28 39 420 3100 3900 39 37 410 3300 4100 37 32 780 20000 9000 32 26 14   310 170 26 33 220 11000 2000 33 39 6.7 450 72 39 35 1000 15000 11000 35 34 350 14000 3400 34 34 1100 17000 12000 34 40 3500 43000 40000 40 21 210 2800 2800 21
    correct-unconfimed results 2 26 4600 240 2 18 270 13000 3100 12 4 22   1400 180 4 23 120 7500 980 7 7 930 8800 12000 7 14 670 11000 8400 3 11 750 2500 9200 6 14 770 6600 8700 7 13 870 21000 9600 7 10 90   170 1100 10 14 210 7000 2300 13 18 490   8100 7600 15 2 82 1100 1100 2 1 160 2600 2600 1 7 140 3500 1600 7 34 4200 39000 44000 28 58 3100 11000 39000 55
        correct-unconfirmed true 2 26 4600 240 2 12 170 5600 2000 12 4 22   1400 180 4 7 39 2500 330 7 7 930 8800 12000 7 3 630 9200 7900 3 6 670 2000 8600 6 7 690 6000 8000 7 7 140 9000 1400 7 10 90   170 1100 10 13 190 6300 2000 13 15 490   8000 7600 15 2 82 1100 1100 2 1 160 2600 2600 1 7 140 3500 1600 7 28 2800 33000 26000 28 55 3100 10000 39000 55
        correct-unconfirmed false 0 6 94 6900 1100 0 0 16 77 5000 650 0 0 11 42 1600 550 0 5 74 510 640 0 7 74 570 690 0 6 730 12000 8200 0 0 1 25 720 260 0 3 3.6 58 49 0 0 0 0 6 1400 6200 18000 0 3 37 710 470 0
    incorrect results 0 0 2 9.3 630 83 -32 5 40 2000 340 -96 0 0 1 13 110 180 -16 0 9 67 3500 550 -144 8 4.8 97 58 -256 0 0 0 0 0 0 1 110 400 1200 -32
        incorrect true 0 0 0 1 23 860 190 -32 0 0 0 0 0 8 4.8 97 58 -256 0 0 0 0 0 0 1 110 400 1200 -32
        incorrect false 0 0 2 9.3 630 83 -32 4 17 1200 160 -64 0 0 1 13 110 180 -16 0 9 67 3500 550 -144 0 0 0 0 0 0 0 0
score (163 tasks, max score: 274) 139 106 137 59 178 119 91 134 13 -134 154 152 189 159 191 216 44
Run set 2ls.sv-comp18.ReachSafety-Loops cbmc.sv-comp18.ReachSafety-Loops cpa-bam-bnb.sv-comp18.ReachSafety-Loops cpa-bam-slicing.sv-comp18.ReachSafety-Loops cpa-seq.sv-comp18.ReachSafety-Loops depthk.sv-comp18.ReachSafety-Loops esbmc-incr.sv-comp18.ReachSafety-Loops esbmc-kind.sv-comp18.ReachSafety-Loops interpchecker.sv-comp18.ReachSafety-Loops map2check.sv-comp18.ReachSafety-Loops skink.sv-comp18.ReachSafety-Loops symbiotic.sv-comp18.ReachSafety-Loops uautomizer.sv-comp18.ReachSafety-Loops ukojak.sv-comp18.ReachSafety-Loops utaipan.sv-comp18.ReachSafety-Loops veriabs.sv-comp18.ReachSafety-Loops viap.sv-comp18.ReachSafety-Loops