Tool 2LS 0.7.2-sv-comp19 CBMC CBMC Path 5.10 () CPAchecker 1.7-svn 29852 DepthK 3.1 DIVINE ESBMC version 6.0.0 64-bit x86_64 linux Map2Check v7.2-Flock : Tue Nov 27 22:00:00 -04 2018 PeSCo 1.7-svn b8d6131600+ Pinaka 0.1 skink 2.0 SMACK 1.9.3 symbiotic 6.0.3-77d4af47 ULTIMATE Automizer 0.1.23-635dfa2a ULTIMATE Kojak 0.1.23-635dfa2a ULTIMATE Taipan 0.1.23-635dfa2a VeriAbs 1.3.10 VeriFuzz 1.0.0 VerifierIntegerAssignmentPrograms 1.1.12(Date 28/11/2018)
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-04 22:44:17 CET 2018-12-04 22:48:40 CET 2018-12-04 22:45:10 CET 2018-12-05 05:46:16 CET 2018-12-05 09:36:33 CET 2018-12-10 10:00:20 CET 2018-12-06 11:06:04 CET 2018-12-06 11:03:31 CET 2018-12-06 12:20:21 CET 2018-12-06 12:44:04 CET 2018-12-06 20:14:43 CET 2018-12-07 12:00:55 CET 2018-12-07 19:13:55 CET 2018-12-07 21:42:05 CET 2018-12-08 07:42:40 CET 2018-12-08 11:04:44 CET 2018-12-08 14:19:36 CET 2018-12-10 16:50:17 CET 2018-12-09 02:47:33 CET 2018-12-09 18:49:43 CET
Run set 2ls.sv-comp19_prop-reachsafety.ReachSafety-Loops cbmc.sv-comp19_prop-reachsafety.ReachSafety-Loops cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Loops cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Loops depthk.sv-comp19_prop-reachsafety.ReachSafety-Loops divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-Loops divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Loops esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Loops map2check.sv-comp19_prop-reachsafety.ReachSafety-Loops pesco.sv-comp19_prop-reachsafety.ReachSafety-Loops pinaka.sv-comp19_prop-reachsafety.ReachSafety-Loops skink.sv-comp19_prop-reachsafety.ReachSafety-Loops smack.sv-comp19_prop-reachsafety.ReachSafety-Loops symbiotic.sv-comp19_prop-reachsafety.ReachSafety-Loops uautomizer.sv-comp19_prop-reachsafety.ReachSafety-Loops ukojak.sv-comp19_prop-reachsafety.ReachSafety-Loops utaipan.sv-comp19_prop-reachsafety.ReachSafety-Loops veriabs.sv-comp19_prop-reachsafety.ReachSafety-Loops verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Loops viap.sv-comp19_prop-reachsafety.ReachSafety-Loops
Options --graphml-witness witness.graphml --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp19 -heap 10000M -benchmark -timelimit 900s --no-symbolic -s kinduction -svcomp19-pesco -heap 10000M -stack 2048k -benchmark -timelimit 900s --graphml-witness witness.graphml -w error-witness.graphml --witness witness.graphml --full-output --full-output --full-output
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
loops/array_false-unreach-call_true-termination.i false(unreach-call) .14  24 1.1  1 false(unreach-call) .065 9.7 .49 1 false(unreach-call) .058 9.1 .49 1 false(unreach-call) 5.3 310 52 1 false(unreach-call) .35 34 5.1 1 unknown 8.3  430 98   0 false(unreach-call) 8.8  430 130   1 false(unreach-call) .090 26 1.0  1 false(unreach-call) .42 83 5.6 1 false(unreach-call) 14 1100 99 1 false(unreach-call) .35 58 3.4 1 false(unreach-call) 4.9 260 50 1 disqualified 2.6 74 35 0 false(unreach-call) .22 18 2.2 1 false(unreach-call) 7.8 360 70 1 false(unreach-call) 8.5 370 74 1 false(unreach-call) 7.1 340 61 1 false(unreach-call) 3.0 150 29 1 false(unreach-call) 3.8 150 39 1 false(unreach-call) 5.3 130 70 1
loops/bubble_sort_false-unreach-call.i error (134) .21  28 1.8  0 false(unreach-call) 1.1   110   15    1 false(unreach-call) 7.4   590   93    1 false(unreach-call) 5.9 320 57 1 false(unreach-call) 4.7  140 63   1 unknown 8.1  430 120   0 error - divine failed with signal 6 (.../lart/abstract/vpa.cpp: 82: encountered unknown parent instruction:) 1.6  200 18   0 false(unreach-call) 4.7   140 62    1 unknown 2.0  58 22   0 false(unreach-call) 16 1200 110 1 timeout 900    2100 9900   0 unknown 15   370 130 0 disqualified 3.9 97 54 0 false(unreach-call) .25 18 2.9 1 false(unreach-call) 12   450 87 1 false(unreach-call) 15   450 130 1 false(unreach-call) 11   430 86 1 false(unreach-call) 480   2200 3800 1 false(unreach-call) 7.5 580 88 1 unknown 2.4 130 31 0
loops/count_up_down_false-unreach-call_true-termination.i false(unreach-call) .12  23 .93 1 false(unreach-call) .079 8.7 .36 1 false(unreach-call) .068 9.2 .40 1 false(unreach-call) 3.3 260 31 1 false(unreach-call) .17 33 1.6 1 unknown 8.1  430 110   0 false(unreach-call) 9.0  430 110   1 false(unreach-call) .084 26 .97 1 false(unreach-call) .46 83 4.9 1 false(unreach-call) 13 1100 86 1 timeout 900    380 3800   0 false(unreach-call) 5.3 280 54 1 disqualified 3.0 81 43 0 false(unreach-call) .20 16 1.9 1 false(unreach-call) 7.5 370 60 1 false(unreach-call) 8.3 370 67 1 false(unreach-call) 6.8 340 59 1 false(unreach-call) 9.1 270 73 1 false(unreach-call) 5.5 150 58 1 false(unreach-call) 4.9 130 66 1
loops/eureka_01_false-unreach-call_true-termination.i false(unreach-call) 1.7   58 25    1 false(unreach-call) .21  14   2.3  1 out of memory 130     15000   1700    0 timeout 940   6600 8900 0 false(unreach-call) .88 37 11   1 unknown 8.2  430 110   0 unknown 14    430 140   0 false(unreach-call) .18  26 2.1  1 false(unreach-call) 520    100 5300   1 timeout 940 5000 7700 0 false(unreach-call) 4.4  890 69   1 unknown 150   1900 1900 0 disqualified 4.2 94 55 0 false(unreach-call) .38 18 4.9 1 false(unreach-call) 780   1900 10000 1 false(unreach-call) 92   1100 1100 1 false(unreach-call) 680   2300 8300 1 false(unreach-call) 44   680 440 0 false(unreach-call) 4.3 150 45 1 false(unreach-call) 14   130 210 0
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(unreach-call) .26  24 3.0  1 false(unreach-call) .096 9.7 .42 1 false(unreach-call) .075 8.9 .62 1 false(unreach-call) 4.5 280 46 1 false(unreach-call) .35 35 4.5 1 unknown 8.2  430 120   0 false(unreach-call) 10    430 120   0 false(unreach-call) .088 26 1.0  1 unknown 120    4000 1100   0 false(unreach-call) 18 1100 120 1 false(unreach-call) .36 58 3.2 1 false(unreach-call) 5.5 290 46 1 disqualified 3.1 82 40 0 false(unreach-call) .21 18 2.3 1 false(unreach-call) 8.2 350 74 1 false(unreach-call) 9.9 390 84 1 false(unreach-call) 9.9 370 74 1 false(unreach-call) 14   270 99 1 false(unreach-call) 5.6 150 66 1 false(unreach-call) 6.7 130 94 1
loops/insertion_sort_false-unreach-call_true-termination.i false(unreach-call) 320     7700 1700    1 false(unreach-call) 2.1   240   24    1 false(unreach-call) 9.1   310   110    1 false(unreach-call) 33   1300 300 1 false(unreach-call) 1.4  36 20   1 unknown 8.2  430 98   0 unknown 1.6  200 21   0 false(unreach-call) .78  28 11    1 true 1.1  75 13   -32 false(unreach-call) 62 2300 420 1 timeout 900    680 7000   0 unknown 56   1600 670 0 disqualified 3.5 84 43 0 timeout (verification) 900    510 10000   0 false(unreach-call) 360   1100 4200 1 false(unreach-call) 160   930 1600 1 timeout 900   1400 9800 0 false(unreach-call) 430   4200 4000 1 false(unreach-call) 6.7 150 77 1 false(unreach-call) 10   510 120 0
loops/invert_string_false-unreach-call_true-termination.i false(unreach-call) 1.1   43 15    1 false(unreach-call) .20  20   2.3  1 error (134) .056 6.9 .59 0 false(unreach-call) 21   790 150 1 false(unreach-call) .62 35 7.9 1 unknown 8.0  430 94   0 unknown 1.7  200 20   0 false(unreach-call) .11  26 1.1  1 timeout 900    5300 9600   0 false(unreach-call) 23 1300 170 1 timeout 900    11000 4900   0 unknown 11   300 110 0 disqualified 3.3 87 45 0 false(unreach-call) .40 19 5.5 0 false(unreach-call) 17   520 150 1 false(unreach-call) 17   660 160 1 false(unreach-call) 20   570 190 1 false(unreach-call) 28   290 210 1 false(unreach-call) 3.4 160 36 1 false(unreach-call) 8.1 310 110 0
loops/linear_search_false-unreach-call.i error (134) .076 24 .91 0 false(unreach-call) .33  9.6 4.0  1 false(unreach-call) 1.2   11   16    0 false(unreach-call) 15   570 130 1 false(unreach-call) 6.3  38 79   0 unknown 8.1  430 120   0 unknown 1.6  200 23   0 false(unreach-call) .38  26 6.4  0 true 1.4  75 19   -32 false(unreach-call) 22 1300 190 1 false(unreach-call) .41 58 3.9 1 unknown 30   1100 310 0 disqualified 24   120 370 0 false(unreach-call) 2.0  19 26   0 timeout 900   710 11000 0 timeout 900   660 12000 0 timeout 900   840 13000 0 false(unreach-call) 18   280 130 0 false(unreach-call) 3.7 150 35 1 unknown 2.4 130 37 0
loops/ludcmp_false-unreach-call.i timeout 900     3900 9300    0 false(unreach-call) .85  93   11    1 false(unreach-call) .92  94   12    1 false(unreach-call) 8.0 540 84 1 false(unreach-call) 6.4  350 68   1 false(unreach-call) 8.3  430 120   1 false(unreach-call) 8.3  430 100   1 false(unreach-call) .19  40 2.6  1 false(unreach-call) 1.1  87 12   1 false(unreach-call) 18 1500 160 1 false(unreach-call) 1.2  59 16   1 unknown 11   300 98 0 disqualified 86   590 950 0 false(unreach-call) .20 16 2.3 1 true 40   860 340 -32 error (7) 63   850 500 0 true 44   910 360 -32 false(unreach-call) 31   1500 320 0 false(unreach-call) 3.6 160 38 1 false(unreach-call) 30   140 410 1
loops/matrix_false-unreach-call_true-termination.i false(unreach-call) 65     2400 330    1 false(unreach-call) .17  19   1.7  1 false(unreach-call) .15  14   1.5  1 false(unreach-call) 12   420 97 1 false(unreach-call) .81 40 11   1 unknown 8.2  430 130   0 unknown 1.6  200 20   0 false(unreach-call) .16  26 1.4  1 true 98    92 1300   -32 false(unreach-call) 20 1300 130 1 error (8) .36 58 3.0 0 unknown 37   1400 400 0 disqualified 3.3 87 41 0 false(unreach-call) .77 20 12   1 false(unreach-call) 9.4 370 78 1 false(unreach-call) 9.1 360 73 1 false(unreach-call) 10   380 79 1 false(unreach-call) 510   9100 3600 0 false(unreach-call) 4.4 150 50 0 unknown 430   900 5000 0
loops/n.c24_false-unreach-call.i error (134) .16  26 1.5  0 out of memory 57     14000   690    0 out of memory 190     15000   2100    0 timeout 910   4100 9100 0 unknown 900    1700 7800   0 unknown 8.4  430 100   0 error - divine failed with signal 6 (.../lart/abstract/stash.cpp: 167: encountered unsupported unstash of constant expression.) 1.6  200 20   0 out of memory 460     15000 2800    0 killed by signal 9 370    4500 3200   0 unknown 100 1400 1200 0 error (8) 1.5  120 16   0 unknown 9.0 280 83 0 disqualified 880   1700 7900 0 timeout (verification) 900    2700 9600   0 timeout 900   3800 10000 0 timeout 900   5200 8400 0 timeout 900   4600 12000 0 timeout 900   3000 10000 0 timeout 900   160 11000 0 unknown 2.5 130 34 0
loops/nec11_false-unreach-call_false-termination.i false(unreach-call) .12  23 .88 1 false(unreach-call) .060 9.4 .57 1 false(unreach-call) .058 9.0 .57 1 false(unreach-call) 3.6 260 37 1 false(unreach-call) .15 33 1.4 1 unknown 8.1  430 98   0 false(unreach-call) 8.6  430 120   1 false(unreach-call) .10  26 .94 1 false(unreach-call) .46 83 5.4 1 false(unreach-call) 14 1100 100 1 out of memory 710    15000 11000   0 false(unreach-call) 5.3 280 47 1 disqualified 3.1 82 41 0 false(unreach-call) .19 17 2.4 1 false(unreach-call) 8.0 370 60 1 false(unreach-call) 7.2 340 65 1 false(unreach-call) 7.5 340 60 1 false(unreach-call) 13   260 100 1 false(unreach-call) 5.4 150 60 1 false(unreach-call) 5.0 130 83 1
loops/nec20_false-unreach-call_true-termination.i false(unreach-call) 1.1   74 11    1 false(unreach-call) .18  28   2.1  1 false(unreach-call) .20  29   2.5  1 false(unreach-call) 4.0 270 34 1 false(unreach-call) .35 34 5.2 1 unknown 8.4  430 100   0 false(unreach-call) 9.0  430 110   1 false(unreach-call) .11  26 1.5  1 false(unreach-call) .45 83 4.9 1 false(unreach-call) 14 1100 89 1 false(unreach-call) 1.6  86 20   1 false(unreach-call) 6.0 320 53 1 disqualified 3.1 84 43 0 false(unreach-call) .21 17 2.4 1 false(unreach-call) 8.6 380 68 1 false(unreach-call) 8.2 380 59 1 false(unreach-call) 7.8 370 68 1 false(unreach-call) 19   290 140 1 false(unreach-call) 3.8 150 34 1 false(unreach-call) 7.7 130 120 1
loops/s3_false-unreach-call.i false(unreach-call) 370     1800 2200    0 false(unreach-call) 24     530   350    1 out of memory 290     15000   2600    0 false(unreach-call) 130   2200 1500 1 false(unreach-call) 27    370 330   1 unknown 12    430 160   0 error - divine failed with signal 11 1.8  200 23   0 false(unreach-call) 13     600 150    1 timeout 900    2200 6900   0 false(unreach-call) 57 1500 480 1 error (8) .93 80 8.5 0 unknown 15   490 150 0 disqualified 14   240 150 0 error(unknown, verification-finished) 1.2  19 16   0 error (7) 14   340 99 0 error (7) 14   340 110 0 error (7) 44   740 380 0 false(unreach-call) 92   870 1000 0 error (1) 870   6900 11000 0 unknown 2.5 130 31 0
loops/string_false-unreach-call_true-termination.i false(unreach-call) .69  32 8.0  1 false(unreach-call) .11  9.8 1.3  1 false(unreach-call) .12  9.6 1.2  1 false(unreach-call) 4.5 280 45 1 unknown 12    40 160   0 unknown 8.2  430 100   0 false(unreach-call) 11    430 140   1 unknown .086 26 1.0  0 timeout 900    600 6800   0 false(unreach-call) 13 1200 99 1 false(unreach-call) .41 58 3.6 1 unknown 73   1800 790 0 disqualified 3.3 88 41 0 false(unreach-call) .27 18 3.7 1 false(unreach-call) 21   570 180 1 false(unreach-call) 21   530 180 1 false(unreach-call) 25   600 210 1 false(unreach-call) 32   300 230 1 false(unreach-call) 3.8 150 35 1 unknown 17   130 260 0
loops/sum01_bug02_false-unreach-call_true-termination.i false(unreach-call) .29  23 5.0  1 false(unreach-call) .13  8.7 .99 1 false(unreach-call) .15  9.6 1.4  1 false(unreach-call) 5.3 300 56 1 false(unreach-call) 1.6  36 23   1 unknown 8.3  430 110   0 false(unreach-call) 12    430 150   0 true .081 26 1.1  -32 false(unreach-call) 10    82 130   1 false(unreach-call) 18 1200 120 1 timeout 900    510 5600   0 false(unreach-call) 8.4 320 73 1 disqualified 3.2 84 36 0 false(unreach-call) .28 17 3.7 1 false(unreach-call) 12   490 100 1 false(unreach-call) 12   550 100 1 false(unreach-call) 13   520 130 1 false(unreach-call) 16   290 140 1 false(unreach-call) 5.6 150 69 1 false(unreach-call) 5.3 130 69 1
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(unreach-call) .21  23 2.6  1 false(unreach-call) .10  9.5 .55 1 false(unreach-call) .093 8.9 .74 1 false(unreach-call) 4.7 290 44 1 false(unreach-call) 1.1  36 14   1 unknown 8.2  430 99   0 false(unreach-call) 11    430 120   0 false(unreach-call) .14  26 1.6  1 false(unreach-call) 3.7  81 44   1 false(unreach-call) 15 1100 100 1 timeout 900    500 4200   0 false(unreach-call) 7.7 330 66 1 disqualified 3.1 84 33 0 false(unreach-call) .29 18 2.8 1 false(unreach-call) 11   470 91 1 false(unreach-call) 9.9 420 82 1 false(unreach-call) 11   500 96 1 false(unreach-call) 15   290 120 1 false(unreach-call) 5.7 150 59 1 false(unreach-call) 5.5 140 68 0
loops/sum01_false-unreach-call_true-termination.i false(unreach-call) .28  23 3.3  1 false(unreach-call) .12  9.0 .88 1 false(unreach-call) .16  9.2 1.8  1 false(unreach-call) 6.3 320 55 1 false(unreach-call) 2.7  36 34   1 unknown 8.1  430 110   0 false(unreach-call) 15    440 170   0 false(unreach-call) .15  26 2.8  1 false(unreach-call) 5.2  82 65   1 false(unreach-call) 18 1200 130 1 timeout 900    450 5800   0 false(unreach-call) 11   380 98 1 disqualified 3.4 85 40 0 false(unreach-call) .37 19 3.8 1 false(unreach-call) 12   560 99 1 false(unreach-call) 13   500 97 1 false(unreach-call) 13   500 110 1 false(unreach-call) 16   300 140 1 false(unreach-call) 6.2 150 69 1 false(unreach-call) 5.6 150 78 0
loops/sum03_false-unreach-call_true-termination.i false(unreach-call) .21  24 2.6  1 false(unreach-call) .12  9.6 .75 1 false(unreach-call) .088 9.2 1.1  1 false(unreach-call) 4.7 280 42 1 false(unreach-call) 2.8  36 35   1 false(unreach-call) 8.6  430 120   1 false(unreach-call) 8.4  430 110   1 false(unreach-call) .12  26 1.7  1 false(unreach-call) .42 83 4.5 1 false(unreach-call) 14 1100 110 1 false(unreach-call) .37 58 3.5 1 false(unreach-call) 11   410 99 1 disqualified 5.3 89 74 0 false(unreach-call) .20 15 2.0 1 false(unreach-call) 230   560 3100 1 false(unreach-call) 39   800 390 1 false(unreach-call) 160   520 2000 1 false(unreach-call) 15   310 130 1 false(unreach-call) 3.3 150 35 1 unknown 98   15000 1500 0
loops/sum04_false-unreach-call_true-termination.i false(unreach-call) .30  24 2.7  1 false(unreach-call) .14  9.3 .64 1 false(unreach-call) .093 9.7 .72 1 false(unreach-call) 4.1 260 40 1 false(unreach-call) 1.9  37 25   1 false(unreach-call) 8.3  430 120   1 false(unreach-call) 8.4  430 96   1 false(unreach-call) .098 26 .96 1 false(unreach-call) .43 83 4.9 1 false(unreach-call) 14 1100 100 1 false(unreach-call) .38 58 3.0 1 false(unreach-call) 4.7 270 44 1 disqualified 2.6 73 36 0 false(unreach-call) .18 16 2.1 1 false(unreach-call) 9.5 370 75 1 false(unreach-call) 10   380 75 1 false(unreach-call) 10   410 83 1 false(unreach-call) 16   300 110 1 false(unreach-call) 3.4 150 34 1 false(unreach-call) 5.2 130 71 1
loops/sum_array_false-unreach-call.i false(unreach-call) .36  39 4.2  1 false(unreach-call) .14  9.2 .92 1 false(unreach-call) .22  14   3.4  1 false(unreach-call) 14   630 100 1 false(unreach-call) .38 35 4.7 1 unknown 8.2  430 100   0 unknown 1.6  200 20   0 false(unreach-call) .11  26 1.1  1 true 7.8  8800 95   -32 false(unreach-call) 22 1300 140 1 timeout 900    10000 6000   0 false(unreach-call) 13   340 120 1 disqualified 3.3 88 41 0 false(unreach-call) .29 17 3.4 1 false(unreach-call) 9.3 380 72 1 false(unreach-call) 9.5 360 85 1 false(unreach-call) 9.5 380 71 1 false(unreach-call) 3.0 140 27 1 false(unreach-call) 5.3 150 56 1 false(unreach-call) 8.0 200 110 0
loops/terminator_01_false-unreach-call_true-termination.i false(unreach-call) .12  23 .88 1 false(unreach-call) .065 9.0 .48 1 false(unreach-call) .064 9.2 .37 1 false(unreach-call) 3.4 260 29 1 false(unreach-call) .14 34 1.6 1 unknown 8.4  430 100   0 false(unreach-call) 8.6  430 120   1 false(unreach-call) .075 26 1.1  1 false(unreach-call) .42 83 5.0 1 false(unreach-call) 12 1200 86 1 timeout 900    370 4900   0 false(unreach-call) 5.5 270 53 1 disqualified 3.0 79 37 0 false(unreach-call) .18 16 2.0 1 false(unreach-call) 7.8 350 64 1 false(unreach-call) 7.9 360 63 1 false(unreach-call) 8.5 360 63 1 false(unreach-call) 8.7 270 78 1 false(unreach-call) 3.4 150 37 1 unknown 2.4 130 34 0
loops/terminator_02_false-unreach-call_true-termination.i false(unreach-call) .12  23 .87 1 false(unreach-call) .11  8.0 .30 1 false(unreach-call) .072 9.0 .37 1 false(unreach-call) 3.4 260 35 1 false(unreach-call) .13 33 1.4 1 unknown 8.2  430 120   0 false(unreach-call) 11    430 120   1 false(unreach-call) .077 26 .96 1 false(unreach-call) .43 83 7.2 1 false(unreach-call) 14 1100 110 1 timeout 900    340 3600   0 false(unreach-call) 6.2 320 54 1 disqualified 3.0 83 41 0 false(unreach-call) .21 18 2.2 1 false(unreach-call) 7.8 370 71 1 false(unreach-call) 6.7 330 57 1 false(unreach-call) 7.8 330 58 1 false(unreach-call) 14   280 120 1 false(unreach-call) 3.5 150 28 1 false(unreach-call) 5.8 130 72 1
loops/terminator_03_false-unreach-call_true-termination.i false(unreach-call) .10  23 .92 1 false(unreach-call) .071 9.5 .31 1 false(unreach-call) .061 9.0 .48 1 false(unreach-call) 4.3 280 38 1 false(unreach-call) .14 33 1.4 1 unknown 8.1  430 93   0 false(unreach-call) 9.7  430 120   1 false(unreach-call) .076 26 .96 1 false(unreach-call) .43 83 6.5 1 false(unreach-call) 14 1100 98 1 timeout 900    7100 3600   0 false(unreach-call) 5.9 290 56 1 disqualified 3.0 79 37 0 false(unreach-call) .20 18 1.9 1 false(unreach-call) 8.2 350 59 1 false(unreach-call) 8.0 350 59 1 false(unreach-call) 7.4 340 67 1 false(unreach-call) 9.0 270 74 1 false(unreach-call) 3.4 150 31 1 false(unreach-call) 5.3 130 81 1
loops/trex01_false-unreach-call_true-termination.i false(unreach-call) .12  24 1.2  1 false(unreach-call) .083 9.5 .49 1 false(unreach-call) .072 8.8 .43 1 false(unreach-call) 3.4 260 33 1 false(unreach-call) .14 34 1.5 1 unknown 8.5  430 120   0 false(unreach-call) 17    430 230   1 false(unreach-call) .10  26 .95 1 false(unreach-call) .49 83 5.9 1 false(unreach-call) 14 1100 110 1 false(unreach-call) .39 58 3.3 1 false(unreach-call) 6.5 330 58 1 disqualified 3.2 88 41 0 false(unreach-call) .22 17 2.8 1 false(unreach-call) 8.0 350 66 1 false(unreach-call) 7.7 350 62 1 false(unreach-call) 8.0 360 60 1 false(unreach-call) 14   270 110 1 false(unreach-call) 5.4 150 53 1 error (1) 4.8 130 69 0
loops/trex02_false-unreach-call_true-termination.i false(unreach-call) .11  23 .82 1 false(unreach-call) .072 9.4 .44 1 false(unreach-call) .10  8.7 .30 1 false(unreach-call) 3.4 260 35 1 false(unreach-call) .14 34 1.5 1 unknown 8.2  430 100   0 false(unreach-call) 10    430 120   1 false(unreach-call) .080 26 1.0  1 unknown 99    4300 880   0 false(unreach-call) 14 1100 99 1 timeout 900    310 5200   0 false(unreach-call) 25   900 280 1 disqualified 3.0 79 37 0 false(unreach-call) .21 19 2.6 1 false(unreach-call) 8.1 370 63 1 false(unreach-call) 8.0 370 65 1 false(unreach-call) 7.6 350 64 1 false(unreach-call) 13   270 96 1 error (1) 8.8 150 100 0 unknown 5.9 130 74 0
loops/trex03_false-unreach-call_true-termination.i false(unreach-call) .11  24 1.2  1 false(unreach-call) .079 9.3 .64 1 false(unreach-call) .068 9.7 .57 1 false(unreach-call) 4.1 280 40 1 false(unreach-call) .14 34 1.4 1 unknown 8.3  430 100   0 false(unreach-call) 17    430 190   1 false(unreach-call) .083 26 .88 1 false(unreach-call) 320    4000 4300   1 false(unreach-call) 12 1200 95 1 timeout 900    340 6000   0 false(unreach-call) 7.0 330 63 1 disqualified 3.2 85 44 0 false(unreach-call) .22 18 3.4 1 false(unreach-call) 8.0 380 66 1 false(unreach-call) 7.3 340 67 1 false(unreach-call) 7.9 370 62 1 false(unreach-call) 14   270 120 1 error (1) 7.5 150 94 0 witness invalid (false(unreach-call)) 6.5 130 92 0
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i error (134) .085 23 .70 0 false(unreach-call) .074 9.5 1.1  1 false(unreach-call) .086 9.4 .73 1 false(unreach-call) 3.5 260 29 1 false(unreach-call) .58 35 8.6 1 false(unreach-call) 8.2  430 110   1 false(unreach-call) 8.2  430 100   1 false(unreach-call) .097 26 1.4  1 false(unreach-call) .42 83 4.6 1 false(unreach-call) 13 1100 92 1 false(unreach-call) .39 58 3.2 1 unknown 10   280 98 0 disqualified 3.0 77 35 0 false(unreach-call) .17 16 1.8 1 false(unreach-call) 9.5 370 76 1 false(unreach-call) 9.2 360 65 1 false(unreach-call) 10   440 87 1 false(unreach-call) 17   300 120 1 false(unreach-call) 3.5 150 34 1 unknown 2.4 130 34 0
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i error (134) .17  25 1.4  0 false(unreach-call) .38  18   3.7  1 false(unreach-call) .82  40   9.9  1 false(unreach-call) 4.8 300 41 1 false(unreach-call) .82 36 13   1 unknown 8.2  430 110   0 unknown 8.2  430 100   0 false(unreach-call) .16  26 2.0  1 timeout 900    87 9200   0 false(unreach-call) 15 1200 110 1 false(unreach-call) .76 61 8.7 1 unknown 8.7 280 77 0 disqualified 3.4 91 42 0 error(unknown, cex-confirmation) .20 15 2.2 0 false(unreach-call) 15   490 120 1 false(unreach-call) 11   540 89 1 false(unreach-call) 17   630 150 1 false(unreach-call) 29   280 270 1 error (1) 3.8 160 39 0 unknown 2.5 130 33 0
loops/vogal_false-unreach-call.i false(unreach-call) 2.5   150 28    1 false(unreach-call) .29  17   3.6  1 out of memory 130     15000   1500    0 false(unreach-call) 47   2000 410 1 false(unreach-call) 11    79 140   1 unknown 8.1  430 99   0 false(unreach-call) 35    450 360   1 false(unreach-call) .43  32 5.3  1 false(unreach-call) .58 80 6.7 1 false(unreach-call) 51 1700 380 1 false(unreach-call) 7.9  940 100   1 false(unreach-call) 19   760 200 1 disqualified 4.3 110 63 0 false(unreach-call) .25 18 3.1 1 timeout 900   990 11000 0 false(unreach-call) 64   720 660 1 timeout 900   1000 12000 0 false(unreach-call) 62   370 680 1 false(unreach-call) 3.7 150 44 1 unknown 340   550 4100 0
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(unreach-call) .11  24 1.0  1 false(unreach-call) .069 9.4 .44 1 false(unreach-call) .058 9.8 .40 1 false(unreach-call) 3.6 260 33 1 false(unreach-call) .14 34 1.4 1 false(unreach-call) 8.3  430 100   1 false(unreach-call) 8.3  430 110   1 false(unreach-call) .080 26 .86 1 false(unreach-call) .45 83 4.7 1 false(unreach-call) 12 1200 82 1 false(unreach-call) .35 58 3.9 1 false(unreach-call) 5.0 280 45 1 disqualified 3.0 77 38 0 false(unreach-call) .17 16 1.9 1 false(unreach-call) 7.0 350 65 1 false(unreach-call) 8.1 360 58 1 false(unreach-call) 8.0 370 62 1 false(unreach-call) 14   300 100 1 false(unreach-call) 3.5 150 34 1 unknown 97   15000 1600 0
loops/array_true-unreach-call_true-termination.i true .13  24 1.8  2 true .046 7.0 .38 2 true .052 6.5 .45 2 true 4.9 310 44 1 unknown .83 67 9.9 0 unknown 8.3  430 93   0 true 8.6  370 110   2 true .11  26 .82 2 timeout 900    4200 10000   0 true 14 1100 95 2 true .36 58 2.8 2 true 3.6 220 33 2 disqualified 2.0 71 27 0 true .19 18 2.4 2 true 9.6 420 76 2 true 9.8 370 77 2 true 11   480 100 2 true 3.1 150 27 2 timeout 900   150 12000 0 true 18   250 180 2
loops/bubble_sort_true-unreach-call_true-termination.i error (134) .087 24 .76 0 error (42) 880     13000   7000    0 out of memory 110     15000   1500    0 true 94   3300 880 2 unknown 2.9  100 42   0 true 8.1  370 110   2 unknown 1.6  200 26   0 true .15  26 1.2  2 unknown .92 41 14   0 true 11 1200 84 2 timeout 900    9200 4500   0 unknown 8.7 270 88 0 disqualified 2.5 80 31 0 true .15 16 2.1 2 true 8.5 370 63 2 true 8.7 370 75 2 true 8.1 350 56 2 true 17   430 140 2 error (1) 860   160 10000 0 true 9.5 130 140 1
loops/count_up_down_true-unreach-call_true-termination.i timeout 900     1400 11000    0 error (42) 880     4600   4700    0 error (42) 870     220   11000    0 timeout 970   9400 9300 0 unknown 25    38 330   0 unknown 8.2  430 90   0 timeout 900    400 9200   0 timeout 900     1600 12000    0 timeout 900    81 9800   0 timeout 960 11000 9700 0 timeout 900    380 3700   0 true 4.1 220 37 2 disqualified 880   960 11000 0 true .15 16 1.5 2 true 11   450 90 2 true 10   440 83 2 true 10   460 89 2 true 15   450 120 2 error (1) 880   150 10000 0 true 4.6 130 55 2
loops/eureka_01_true-unreach-call.i true 13     790 130    1 true .42  12   4.7  1 out of memory 99     15000   1400    0 true 4.2 260 41 1 unknown 7.8  68 98   0 true 8.3  370 110   1 true 8.2  370 100   1 true .26  27 3.3  1 timeout 900    83 11000   0 true 20 1600 170 1 true .41 59 4.7 1 unknown 110   2200 1300 0 disqualified 880   1000 8700 0 true .15 15 1.7 1 timeout 900   4400 11000 0 timeout 900   5700 11000 0 timeout 900   6900 12000 0 true 140   1100 1500 2 timeout 900   150 12000 0 true 110   420 1500 1
loops/eureka_05_true-unreach-call_true-termination.i true 1.0   56 13    1 true .077 6.3 .56 1 true .14  8.3 1.6  1 true 3.3 250 29 1 unknown 1.8  66 23   0 true 8.0  370 97   1 true 8.2  370 110   1 true .10  26 .97 1 unknown .85 40 13   0 true 15 1200 110 1 true .39 58 3.3 1 true 4.6 270 47 1 disqualified 2.6 85 35 0 true .17 15 1.6 1 timeout 900   1300 11000 0 true 400   990 3700 1 timeout 900   1700 12000 0 true 110   930 1000 1 timeout 900   150 13000 0 true 8.4 230 95 1
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true .095 23 1.2  2 out of memory 240     15000   2900    0 out of memory 190     15000   2400    0 true 93   1400 860 2 unknown .82 67 7.8 0 unknown 8.4  430 99   0 timeout 900    4400 8400   0 true .11  26 .81 2 timeout 900    75 6600   0 true 11 1200 82 2 out of memory 450    15000 5600   0 true 3.8 220 41 2 disqualified 2.4 73 28 0 probably out of memory (killed (signal 9, verification)) 170    15000 2600   0 true 8.4 360 60 2 true 9.0 370 65 2 true 7.3 330 59 2 true 13   460 110 2 error (1) 890   150 9900 0 unknown 110   15000 1600 0
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true .10  24 .95 2 out of memory 240     15000   3400    0 out of memory 190     15000   2400    0 true 93   1400 1100 2 unknown .83 67 8.6 0 unknown 8.3  430 92   0 timeout 900    4400 8200   0 timeout 900     12000 12000    0 timeout 900    75 6200   0 true 11 1200 79 2 out of memory 460    15000 6400   0 true 4.1 220 37 2 disqualified 2.4 74 29 0 probably out of memory (killed (signal 9, verification)) 170    15000 2400   0 true 8.3 360 65 2 true 9.2 370 71 2 true 8.2 380 71 2 true 13   460 110 2 error (1) 890   150 13000 0 unknown 110   15000 1700 0
loops/insertion_sort_true-unreach-call_true-termination.i out of memory 340     15000 2200    0 error (42) 880     3300   5300    0 error (42) 880     9700   11000    0 timeout 970   3900 5700 0 unknown 900    120 12000   0 unknown 8.2  430 93   0 unknown 1.6  200 20   0 timeout 900     140 11000    0 true 1.0  75 11   1 timeout 960 3300 6600 0 timeout 900    560 6200   0 unknown 43   1600 530 0 disqualified 880   230 12000 0 timeout (verification) 900    510 11000   0 timeout 900   2800 9500 0 timeout 900   850 8000 0 timeout 900   1200 9600 0 unknown 790   6300 7400 0 timeout 900   150 12000 0 true 35   530 360 1
loops/invert_string_true-unreach-call_true-termination.i true .38  25 4.3  2 true .091 5.8 .48 2 true .13  8.2 1.4  2 true 23   550 210 2 unknown 1.6  67 19   0 unknown 8.3  430 110   0 true 8.6  370 96   2 true .11  26 .93 2 timeout 900    75 10000   0 true 27 1300 220 2 true .35 58 3.1 2 true 4.0 220 40 2 disqualified 2.6 83 32 0 true .15 15 1.8 2 true 290   1200 3500 1 true 250   890 2600 2 timeout 900   970 9900 0 true 100   770 940 2 timeout 900   150 9800 0 true 59   430 670 2
loops/linear_sea.ch_true-unreach-call.i error (134) .087 24 .79 0 error (42) 880     4600   8200    0 error (42) 880     160   9500    0 timeout 940   7400 9700 0 unknown 66    48 860   0 unknown 8.1  430 100   0 unknown 1.5  200 24   0 timeout 900     870 11000    0 true 1.0  75 14   1 timeout 940 7700 9000 0 out of memory 840    15000 4300   0 unknown 38   1500 430 0 disqualified 880   320 11000 0 timeout (verification) 900    44 13000   0 timeout 900   770 11000 0 timeout 900   620 12000 0 timeout 900   690 13000 0 true 130   1300 1400 1 timeout 900   250 11000 0 unknown 2.4 130 37 0
loops/lu.cmp_true-unreach-call.i true 9.9   3700 130    2 true .85  22   10    2 witness invalid (true) .89  23   13    0 true 3.8 250 37 2 unknown 7.0  360 78   0 true 8.1  370 96   2 true 8.3  370 100   2 true .22  40 2.5  2 true 2.0  87 24   2 true 14 1100 91 2 true 8.1  59 110   2 true 6.3 370 59 2 disqualified 880   720 6000 0 true .16 16 2.3 2 true 11   480 96 2 true 19   560 160 2 true 49   960 480 2 true 64   3600 700 2 timeout 900   160 10000 0 error (1) 160   130 2100 0
loops/matrix_true-unreach-call_true-termination.i true .18  24 1.5  2 true .053 6.3 .34 2 true .046 7.2 .48 2 true 6.0 360 55 2 unknown .93 66 11   0 unknown 8.2  430 100   0 true 8.9  370 100   2 true .092 26 .99 2 timeout 900    4100 9700   0 true 13 1200 95 2 true .37 58 3.5 2 true 4.0 220 40 2 disqualified 2.0 71 25 0 true .17 19 2.3 2 true 11   510 100 2 true 12   490 99 2 timeout 900   1800 14000 0 true 28   510 230 2 timeout 900   150 14000 0 true 60   570 720 2
loops/n.c11_true-unreach-call_false-termination.i timeout 900     1700 10000    0 error (42) 880     3000   6500    0 error (42) 880     270   7700    0 true 2.8 250 27 2 unknown 57    53 730   0 unknown 8.2  430 99   0 timeout 900    1400 9600   0 timeout 900     2600 12000    0 timeout 900    5800 11000   0 true 13 1000 91 2 timeout 900    1200 13000   0 true 29   960 290 2 disqualified 900   470 9900 0 timeout (verification) 900    73 9600   0 true 11   440 87 2 true 10   380 77 2 true 11   500 110 2 true 27   510 200 2 error (1) 860   150 11000 0 true 56   150 830 2
loops/n.c40_true-unreach-call_true-termination.i true .14  24 1.0  2 true .10  5.4 .21 2 witness invalid (true) .052 6.0 .18 0 true 4.9 300 47 1 unknown .77 65 8.5 0 unknown 8.0  430 98   0 true 8.4  370 98   2 true .098 26 .87 2 timeout 900    2200 8900   0 true 14 1100 96 2 true .35 58 3.1 2 true 7.8 340 77 2 disqualified 2.6 84 35 0 true .22 22 1.7 2 error (7) 27   350 310 0 true 8.8 360 72 2 true 12   420 98 2 true 31   530 270 2 timeout 900   150 12000 0 unknown 160   510 1800 0
loops/nec40_true-unreach-call_true-termination.i true .15  23 1.3  2 true .050 6.9 .33 2 witness invalid (true) .042 6.1 .28 0 true 5.0 300 41 2 unknown .79 67 8.2 0 unknown 8.1  430 94   0 true 8.5  370 95   2 true .087 26 .81 2 timeout 900    2200 10000   0 true 12 1200 84 2 true .36 58 2.9 2 true 7.9 340 67 2 disqualified 2.6 79 33 0 true .16 17 2.3 2 error (7) 30   370 310 0 true 9.5 370 71 2 true 12   440 94 2 true 32   510 270 2 timeout 900   150 14000 0 unknown 160   570 1600 0
loops/string_true-unreach-call_true-termination.i true .11  24 .80 2 true .17  8.6 2.2  2 witness invalid (true) 300     8900   3700    0 true 4.0 260 35 2 unknown .84 66 9.2 0 unknown 8.1  430 120   0 true 250    380 2800   2 true .10  26 .97 2 timeout 900    4300 9300   0 true 18 1200 120 2 true .54 59 5.8 2 true 5.0 280 43 2 disqualified 2.6 82 35 0 true .23 18 2.9 2 true 10   440 79 2 true 10   360 75 2 true 12   510 89 2 true 18   200 130 2 timeout 900   150 11000 0 unknown 17   130 220 0
loops/sum01_true-unreach-call_true-termination.i timeout 900     1600 11000    0 true 22     110   280    2 error (42) 870     110   13000    0 true 290   3100 3300 2 unknown 78    51 970   0 unknown 8.1  430 120   0 timeout 900    540 8800   0 true 360     950 4100    2 timeout 900    2200 11000   0 true 97 3300 800 2 true 38    13000 490   2 true 4.0 220 36 2 disqualified 880   770 12000 0 true .17 18 1.8 2 true 10   470 77 2 true 8.5 350 61 2 true 11   500 95 2 true 16   530 130 2 timeout 900   150 12000 0 true 5.5 130 65 2
loops/sum03_true-unreach-call_false-termination.i true .32  23 4.8  2 out of memory 280     15000   4200    0 out of memory 220     15000   3600    0 true 190   1300 1600 2 unknown .98 66 12   0 timeout 900    3400 8600   0 timeout 900    3700 8500   0 true .086 26 1.0  2 timeout 900    75 10000   0 true 14 1100 110 2 out of memory 660    15000 8500   0 true 3.6 220 36 2 disqualified 900   270 9700 0 probably out of memory (killed (signal 9, verification)) 170    15000 2500   0 true 8.3 360 63 2 true 9.2 360 76 2 true 8.5 370 60 2 true 13   440 120 2 error (1) 860   150 10000 0 unknown 88   15000 1400 0
loops/sum04_true-unreach-call_true-termination.i true .22  24 2.4  2 true .090 6.5 .51 2 true .064 7.5 .76 2 true 2.8 240 30 2 unknown 2.3  66 28   0 true 8.1  370 98   2 true 8.0  370 100   2 true .094 26 1.0  2 timeout 900    85 11000   0 true 13 1000 87 2 true .37 58 3.0 2 true 3.8 210 39 2 disqualified 2.0 66 24 0 true .16 16 1.5 2 true 11   500 99 2 true 12   700 100 2 true 12   540 100 2 true 17   580 140 2 timeout 900   150 12000 0 true 5.2 130 73 2
loops/sum_array_true-unreach-call.i timeout 900     11000 4000    0 error (42) 880     3200   5500    0 error (42) 880     1400   11000    0 timeout 960   4100 6900 0 unknown 900    260 11000   0 unknown 8.1  430 100   0 unknown 1.6  200 18   0 timeout 900     220 13000    0 true 7.8  8800 94   1 timeout 970 4000 7000 0 out of memory 37    15000 540   0 unknown 42   1500 440 0 disqualified 880   500 11000 0 error(unknown, verification-finished) 660    2200 8500   0 timeout 900   2100 12000 0 timeout 900   840 9500 0 timeout 900   1200 10000 0 true 23   200 200 1 timeout 900   230 11000 0 unknown 470   430 5800 0
loops/terminator_02_true-unreach-call_true-termination.i true .11  23 .83 2 error (42) 880     580   9200    0 out of memory 280     15000   3800    0 true 4.1 280 35 2 unknown 8.6  66 120   0 unknown 8.3  430 110   0 timeout 900    430 6900   0 timeout 900     81 12000    0 timeout 900    4300 12000   0 true 14 1100 81 2 out of memory 250    15000 3300   0 true 37   1500 450 2 disqualified 2.4 79 37 0 timeout (verification) 900    3100 9300   0 true 9.1 380 69 2 true 8.4 380 79 2 true 8.6 370 70 2 true 14   470 120 2 timeout 900   150 11000 0 true 5.8 130 81 2
loops/terminator_03_true-unreach-call_true-termination.i true .12  24 .82 2 error (42) 880     760   7200    0 error (42) 880     230   9800    0 true 4.2 280 42 2 unknown 890    130 11000   0 unknown 8.2  430 100   0 timeout 900    490 8000   0 timeout 900     85 13000    0 timeout 900    120 9100   0 true 14 1100 87 2 timeout 900    7700 4400   0 true 6.9 330 59 2 disqualified 2.4 74 27 0 timeout (verification) 900    87 9200   0 true 8.9 370 66 2 true 8.7 360 64 2 true 7.7 340 57 2 true 13   450 120 2 timeout 900   150 12000 0 unknown 7.5 130 96 0
loops/trex01_true-unreach-call_true-termination.i true 3.4   110 51    2 error (42) 880     2700   8800    0 error (42) 880     15000   10000    0 true 19   520 180 2 unknown 250    91 3200   0 unknown 8.5  430 110   0 timeout 900    470 7300   0 timeout 900     990 11000    0 timeout 900    75 8500   0 true 15 1100 95 2 timeout 900    470 4200   0 true 23   950 220 2 disqualified 2.5 81 35 0 true .41 18 6.4 2 true 8.6 380 68 2 true 7.8 360 65 2 true 7.9 360 70 2 true 13   440 100 2 timeout 900   150 13000 0 true 9.5 150 140 2
loops/trex02_true-unreach-call_true-termination.i true .097 24 .72 2 error (42) 880     1100   9400    0 out of memory 270     15000   3300    0 true 4.0 280 37 2 unknown .95 65 9.3 0 unknown 8.0  430 120   0 timeout 900    400 7400   0 timeout 900     470 10000    0 timeout 900    4200 10000   0 true 12 1200 93 2 timeout 900    310 3900   0 true 4.4 240 41 2 disqualified 2.4 77 29 0 true .17 15 2.0 2 true 7.5 340 72 2 true 7.2 350 67 2 true 7.8 340 66 2 true 13   450 110 2 error (1) 9.0 150 120 0 true 4.7 130 53 2
loops/trex03_true-unreach-call_true-termination.i true .098 23 .77 2 error (42) 880     1500   8500    0 out of memory 190     15000   2800    0 true 4.4 280 39 2 unknown 1.4  66 15   0 unknown 8.2  430 120   0 timeout 900    440 6800   0 timeout 900     400 13000    0 timeout 900    4000 9500   0 true 12 1200 97 2 timeout 900    330 4800   0 timeout 900   3800 6300 0 disqualified 880   440 11000 0 timeout (verification) 900    2900 11000   0 true 8.3 370 59 2 true 7.5 350 59 2 true 8.2 360 75 2 true 14   470 120 2 error (1) 7.5 150 86 0 true 5.7 130 67 2
loops/trex04_true-unreach-call_false-termination.i true .10  24 .80 2 error (42) 880     3600   5500    0 error (42) 870     860   7600    0 true 4.4 280 40 2 unknown 1.6  66 17   0 unknown 8.4  430 100   0 timeout 900    500 7500   0 timeout 900     110 10000    0 timeout 900    86 9700   0 true 14 1100 94 2 timeout 900    370 4100   0 true 4.5 270 46 2 disqualified 2.5 80 35 0 true .19 18 3.7 2 true 7.8 340 57 2 true 8.7 370 58 2 true 7.8 350 60 2 true 13   460 110 2 timeout 900   150 10000 0 timeout 900   130 8600 0
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i error (134) .092 23 1.3  0 true .072 6.9 .52 2 true .15  8.2 1.9  2 true 4.5 290 35 2 unknown .84 66 10   0 true 8.4  370 110   2 true 8.1  370 120   2 true .091 26 1.1  2 timeout 900    85 9600   0 true 12 1200 84 2 true .37 58 3.0 2 unknown 10   300 87 0 disqualified 2.4 75 34 0 true .14 16 1.6 2 true 10   410 81 2 true 9.9 460 92 2 true 10   460 76 2 true 18   470 170 2 timeout 900   150 11000 0 unknown 2.4 130 36 0
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i error (134) .17  25 1.3  0 true 3.1   60   41    2 out of memory 200     15000   2600    0 timeout 910   2500 8800 0 unknown 5.5  120 65   0 unknown 8.2  430 120   0 timeout 900    400 8500   0 true .11  26 1.1  2 unknown 1.2  44 18   0 true 22 1200 150 2 true 30    2500 390   2 unknown 8.3 270 84 0 disqualified 5.6 120 66 0 true 5.2  60 66   2 true 9.0 350 73 2 true 9.2 370 74 2 true 9.0 380 76 2 true 47   480 480 2 timeout 900   160 12000 0 unknown 2.5 130 37 0
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i true .098 23 1.1  2 true .089 6.4 .93 2 witness invalid (true) .10  6.3 1.1  0 true 5.5 310 48 2 unknown .81 66 8.5 0 unknown 8.2  430 110   0 true 22    370 220   2 true .087 26 .88 2 timeout 900    4300 7600   0 true 12 1200 97 2 true .37 59 4.4 2 true 4.5 270 38 2 disqualified 2.6 84 33 0 true .15 15 1.7 2 true 8.0 360 66 2 true 7.3 350 57 2 true 8.4 370 65 2 true 18   470 150 2 timeout 900   150 11000 0 unknown 2.7 130 39 0
loops/vogal_true-unreach-call.i true 1.6   70 21    2 true .11  6.0 .79 2 out of memory 210     15000   3000    0 true 58   1900 560 1 unknown 2.5  67 33   0 unknown 8.0  430 96   0 true 460    440 4800   2 true .20  28 2.4  2 true 400    4300 5100   2 true 81 2700 710 1 true 1.6  170 17   2 unknown 62   1500 690 0 disqualified 5.0 96 62 0 true .20 17 2.1 2 timeout 900   940 11000 0 timeout 900   850 8900 0 timeout 900   1200 13000 0 true 130   950 1200 2 timeout 900   150 12000 0 true 240   350 3500 2
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true .090 24 .92 2 out of memory 220     15000   2800    0 out of memory 180     15000   2300    0 true 2.8 250 25 2 unknown .79 66 9.5 0 true 7.8  370 93   2 true 8.1  370 120   2 out of memory 870     15000 11000    0 timeout 900    74 6200   0 true 12 1000 83 2 out of memory 98    15000 1000   0 true 3.9 220 41 2 disqualified 2.3 74 27 0 probably out of memory (killed (signal 9, verification)) 170    15000 2200   0 true 8.0 370 65 2 true 6.8 340 62 2 true 7.2 350 56 2 true 13   460 94 2 error (1) 860   150 11000 0 out of memory 96   15000 1600 0
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true .091 24 .79 2 out of memory 220     15000   2900    0 out of memory 180     15000   2200    0 true 2.7 250 24 2 unknown .78 65 10   0 true 8.1  370 98   2 true 8.2  370 100   2 true .079 26 .91 2 timeout 900    75 6600   0 true 13 1000 91 2 out of memory 97    15000 1100   0 true 4.0 220 38 2 disqualified 2.3 74 31 0 probably out of memory (killed (signal 9, verification)) 170    15000 2500   0 true 7.9 360 68 2 true 6.9 350 67 2 true 8.5 370 67 2 true 12   420 110 2 error (1) 860   160 12000 0 out of memory 95   15000 1300 0
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true .10  23 .78 2 out of memory 190     15000   2800    0 out of memory 160     15000   2100    0 true 2.7 250 21 2 unknown .79 67 8.4 0 true 8.3  370 100   2 true 8.0  370 85   2 timeout 900     14000 12000    0 timeout 900    75 7400   0 true 12 1000 89 2 out of memory 370    15000 4500   0 true 3.6 220 37 2 disqualified 2.3 74 26 0 probably out of memory (killed (signal 9, verification)) 410    15000 5600   0 true 8.2 370 64 2 true 8.0 360 58 2 true 7.6 350 65 2 true 12   440 110 2 error (1) 870   150 11000 0 out of memory 97   15000 1400 0
loop-acceleration/array_false-unreach-call1_true-termination.i out of memory 410     15000 3700    0 false(unreach-call) 9.9   1100   140    1 false(unreach-call) 8.6   1100   130    1 false(unreach-call) 200   2200 2300 1 unknown 27    40 350   0 false(unreach-call) 8.7  440 110   1 false(unreach-call) 8.5  440 98   1 false(unreach-call) 15     270 200    1 false(unreach-call) .42 83 5.0 1 false(unreach-call) 370 4300 4300 1 false(unreach-call) 2.2  65 26   1 unknown 230   1200 1700 0 disqualified 18   350 220 0 false(unreach-call) .17 16 2.0 1 timeout 900   910 11000 0 timeout 900   5100 8000 0 timeout 900   1000 11000 0 false(unreach-call) 240   1900 3400 1 false(unreach-call) 3.3 150 35 1 false(unreach-call) 4.7 130 67 1
loop-acceleration/array_false-unreach-call2_true-termination.i out of memory 280     15000 2000    0 false(unreach-call) 26     2300   330    1 false(unreach-call) 22     2300   280    1 timeout 910   8000 8400 0 unknown 28    40 320   0 unknown 8.9  430 110   0 unknown 8.9  430 130   0 false(unreach-call) 83     990 1200    1 false(unreach-call) .41 83 6.0 1 timeout 910 7200 9400 0 false(unreach-call) 5.5  95 75   1 false(unreach-call) 5.2 270 49 1 disqualified 170   3500 1900 0 false(unreach-call) .16 16 2.2 1 timeout 900   730 10000 0 timeout 900   5300 8200 0 timeout 900   930 10000 0 false(unreach-call) 4.6 190 35 1 false(unreach-call) 3.6 150 40 1 false(unreach-call) 4.7 130 70 1
loop-acceleration/array_false-unreach-call3_true-termination.i out of memory 870     15000 4300    0 false(unreach-call) 14     630   180    0 false(unreach-call) 32     610   310    0 false(unreach-call) 230   3600 2600 0 unknown 100    47 1400   0 unknown 8.6  430 99   0 timeout 900    430 9900   0 false(unreach-call) 17     390 200    1 false(unreach-call) .47 83 6.3 1 out of memory 590 15000 5900 0 false(unreach-call) 5.8  130 79   1 unknown 72   1400 860 0 disqualified 880   1100 9500 0 false(unreach-call) 5.1  20 76   0 timeout 900   1000 11000 0 timeout 900   5200 10000 0 timeout 900   1200 11000 0 false(unreach-call) 470   2000 6400 0 false(unreach-call) 3.3 150 39 1 false(unreach-call) 5.5 130 79 0
loop-acceleration/const_false-unreach-call1.i timeout 900     1600 11000    0 false(unreach-call) 1.0   22   12    1 false(unreach-call) .98  27   12    1 timeout (exception) 910   15000 10000 0 unknown 22    38 250   0 false(unreach-call) 8.5  430 110   1 false(unreach-call) 8.3  430 120   1 false(unreach-call) 8.9   150 130    1 false(unreach-call) .42 83 5.0 1 timeout 910 13000 8200 0 false(unreach-call) 2.0  59 24   1 unknown 190   960 1600 0 disqualified 3.5 72 56 0 false(unreach-call) .16 17 1.9 1 timeout 900   590 12000 0 timeout 900   990 11000 0 timeout 900   650 12000 0 false(unreach-call) 220   2500 3100 1 false(unreach-call) 3.4 150 31 1 false(unreach-call) 4.7 130 63 1
loop-acceleration/diamond_false-unreach-call1.i false(unreach-call) .76  27 9.8  1 false(unreach-call) .82  44   11    1 out of memory 97     15000   1400    0 false(unreach-call) 46   990 470 1 false(unreach-call) 15    40 190   1 unknown 8.3  430 110   0 false(unreach-call) 19    440 200   1 false(unreach-call) .47  26 5.7  1 false(unreach-call) .43 83 4.9 1 false(unreach-call) 39 2200 290 1 false(unreach-call) .44 58 3.9 1 unknown 48   1000 430 0 disqualified 480   160 6000 0 false(unreach-call) .20 18 1.9 1 timeout 900   610 12000 0 timeout 900   750 11000 0 timeout 900   860 13000 0 false(unreach-call) 48   590 580 1 false(unreach-call) 3.3 150 36 1 false(unreach-call) 5.8 130 76 1
loop-acceleration/functions_false-unreach-call1_true-termination.i timeout 900     1400 11000    0 out of memory 250     15000   3200    0 out of memory 190     15000   2200    0 timeout 970   9100 8600 0 unknown 27    40 380   0 timeout 900    3300 8500   0 timeout 900    3300 9500   0 out of memory 690     15000 8400    0 false(unreach-call) 2.8  82 34   1 timeout (exception) 910 11000 7900 0 out of memory 680    15000 8800   0 false(unreach-call) 5.1 270 49 1 disqualified 880   1100 12000 0 probably out of memory (killed (signal 9, verification)) 230    15000 3300   0 timeout 900   620 10000 0 timeout 900   5300 8900 0 timeout 900   660 12000 0 unknown 41   280 390 0 false(unreach-call) 4.8 150 50 1 false(unreach-call) 5.9 130 80 1
loop-acceleration/multivar_false-unreach-call1_true-termination.i false(unreach-call) .15  23 .86 1 false(unreach-call) .080 9.2 .43 1 false(unreach-call) .060 9.8 .44 1 false(unreach-call) 3.4 260 33 1 false(unreach-call) .13 34 1.7 1 unknown 8.3  430 100   0 false(unreach-call) 9.0  430 110   1 false(unreach-call) .076 26 1.1  1 false(unreach-call) .45 83 5.3 1 false(unreach-call) 11 1200 86 1 false(unreach-call) 2.2  79 22   1 false(unreach-call) 5.4 270 50 1 disqualified 3.0 81 35 0 false(unreach-call) .18 15 2.0 1 false(unreach-call) 6.8 330 52 1 false(unreach-call) 7.8 360 56 1 false(unreach-call) 7.4 340 60 1 false(unreach-call) 9.0 270 76 1 false(unreach-call) 3.4 150 32 1 false(unreach-call) 4.7 130 70 1
loop-acceleration/nested_false-unreach-call1.i timeout 900     9500 9300    0 out of memory 310     15000   3800    0 out of memory 240     15000   3100    0 timeout 910   6700 9900 0 unknown 900    390 10000   0 timeout 900    3700 9600   0 timeout 900    3600 9700   0 timeout 900     12000 9500    0 false(unreach-call) 2.8  83 38   1 timeout 960 4000 11000 0 out of memory 810    15000 13000   0 false(unreach-call) 5.1 270 43 1 disqualified 880   940 13000 0 false(unreach-call) .17 15 1.9 1 timeout 900   860 11000 0 timeout 900   800 6000 0 timeout 900   880 11000 0 false(unreach-call) 220   3100 2900 1 error (1) 53   150 680 0 false(unreach-call) 26   2600 240 1
loop-acceleration/phases_false-unreach-call1.i timeout 900     1200 11000    0 out of memory 310     15000   4400    0 out of memory 230     15000   3600    0 timeout 910   2900 9400 0 unknown 48    47 620   0 timeout 900    3500 9400   0 timeout 900    3400 8200   0 timeout 900     9100 11000    0 false(unreach-call) 3.2  82 38   1 timeout 910 4200 8300 0 out of memory 800    15000 10000   0 unknown 240   1300 2000 0 disqualified 880   460 12000 0 probably out of memory (killed (signal 9, verification)) 230    15000 3600   0 timeout 900   570 11000 0 timeout 900   1500 7900 0 timeout 900   740 11000 0 false(unreach-call) 370   9600 5000 1 false(unreach-call) 4.0 150 44 1 false(unreach-call) 6.1 130 81 1
loop-acceleration/phases_false-unreach-call2_false-termination.i false(unreach-call) .13  23 1.1  1 false(unreach-call) .073 9.8 .37 1 false(unreach-call) .064 8.8 .46 1 false(unreach-call) 3.6 260 33 1 false(unreach-call) .17 33 1.5 1 unknown 8.3  430 87   0 false(unreach-call) 9.4  430 140   1 false(unreach-call) .082 26 .89 1 timeout 900    75 9700   0 false(unreach-call) 12 1200 82 1 out of memory 300    15000 3700   0 false(unreach-call) 5.8 300 56 1 disqualified 880   180 13000 0 false(unreach-call) .20 18 2.4 1 false(unreach-call) 8.3 370 62 1 false(unreach-call) 7.1 330 56 1 false(unreach-call) 7.9 370 64 1 false(unreach-call) 8.7 270 80 1 false(unreach-call) 6.2 150 64 1 timeout 900   130 14000 0
loop-acceleration/simple_false-unreach-call1.i timeout 900     1400 13000    0 out of memory 280     15000   4000    0 out of memory 200     15000   2500    0 timeout 960   9300 9600 0 unknown 26    39 310   0 timeout 900    3500 9500   0 timeout 900    3500 9900   0 timeout 900     14000 11000    0 false(unreach-call) .42 83 5.0 1 timeout 970 7400 9200 0 out of memory 800    15000 11000   0 false(unreach-call) 5.0 260 46 1 disqualified 880   960 13000 0 false(unreach-call) .16 17 1.8 1 timeout 900   580 14000 0 timeout 900   2300 8800 0 timeout 900   820 13000 0 false(unreach-call) 220   2100 2500 1 false(unreach-call) 4.0 150 38 1 false(unreach-call) 4.9 130 73 1
loop-acceleration/simple_false-unreach-call2_true-termination.i false(unreach-call) .13  24 .97 1 false(unreach-call) .061 9.0 .45 1 false(unreach-call) .14  7.4 .34 1 false(unreach-call) 3.5 260 29 1 false(unreach-call) .16 33 1.4 1 unknown 8.1  430 110   0 unknown 8.3  430 110   0 false(unreach-call) .078 26 .79 1 false(unreach-call) 2.8  82 43   1 false(unreach-call) 13 1100 95 1 timeout 900    380 3900   0 false(unreach-call) 5.2 270 50 1 disqualified 3.0 76 34 0 false(unreach-call) .19 16 1.7 1 false(unreach-call) 7.8 350 60 1 false(unreach-call) 7.8 360 62 1 false(unreach-call) 8.0 360 59 1 false(unreach-call) 9.3 310 76 1 error (1) 3.9 150 40 0 false(unreach-call) 5.1 130 68 0
loop-acceleration/simple_false-unreach-call3_true-termination.i false(unreach-call) .11  24 .88 1 false(unreach-call) .064 9.4 .47 1 false(unreach-call) .065 9.2 .39 1 false(unreach-call) 3.4 260 32 1 false(unreach-call) .16 34 1.4 1 unknown 8.2  430 91   0 unknown 8.0  430 120   0 false(unreach-call) .10  26 .82 1 false(unreach-call) .42 83 6.4 1 false(unreach-call) 13 1100 94 1 timeout 900    410 5100   0 false(unreach-call) 5.2 270 53 1 disqualified 3.0 77 34 0 false(unreach-call) .16 16 2.1 1 false(unreach-call) 7.5 340 51 1 false(unreach-call) 7.6 370 67 1 false(unreach-call) 7.1 340 63 1 false(unreach-call) 13   270 98 1 false(unreach-call) 3.5 150 37 1 false(unreach-call) 4.7 130 60 1
loop-acceleration/simple_false-unreach-call4.i timeout 900     1300 12000    0 out of memory 280     15000   3600    0 out of memory 210     15000   3200    0 timeout 970   9600 12000 0 unknown 35    42 530   0 timeout 900    3500 9600   0 timeout 900    3500 9700   0 timeout 900     14000 11000    0 false(unreach-call) 1.6  82 18   1 timeout 960 7900 8300 0 out of memory 820    15000 11000   0 false(unreach-call) 5.0 270 47 1 disqualified 880   950 11000 0 false(unreach-call) .18 15 2.9 1 timeout 900   720 13000 0 timeout 900   2200 8100 0 timeout 900   690 11000 0 false(unreach-call) 220   2100 3200 1 false(unreach-call) 3.9 150 39 1 out of memory 39   15000 500 0
loop-acceleration/underapprox_false-unreach-call1_true-termination.i false(unreach-call) .16  24 1.8  1 false(unreach-call) .21  7.7 .64 1 false(unreach-call) .089 9.7 .69 1 false(unreach-call) 3.9 260 34 1 false(unreach-call) 1.5  35 19   1 false(unreach-call) 8.1  430 100   1 false(unreach-call) 8.1  430 99   1 false(unreach-call) .13  26 1.2  1 false(unreach-call) .46 83 4.7 1 false(unreach-call) 13 1100 110 1 false(unreach-call) .35 58 4.3 1 false(unreach-call) 4.9 270 43 1 disqualified 2.6 71 34 0 false(unreach-call) .17 17 1.9 1 false(unreach-call) 9.1 380 79 1 false(unreach-call) 9.3 370 80 1 false(unreach-call) 10   440 88 1 false(unreach-call) 14   280 110 1 false(unreach-call) 3.4 150 34 1 false(unreach-call) 4.8 130 60 1
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(unreach-call) .17  24 1.4  1 false(unreach-call) .097 9.7 .67 1 false(unreach-call) .10  9.5 .71 1 false(unreach-call) 3.9 260 38 1 false(unreach-call) 1.3  35 16   1 false(unreach-call) 8.3  430 96   1 false(unreach-call) 8.2  430 92   1 false(unreach-call) .11  26 .75 1 false(unreach-call) .43 82 5.9 1 false(unreach-call) 14 1100 110 1 false(unreach-call) .36 58 3.4 1 false(unreach-call) 5.5 290 49 1 disqualified 2.5 70 35 0 false(unreach-call) .16 15 2.0 1 false(unreach-call) 10   400 79 1 false(unreach-call) 9.1 350 79 1 false(unreach-call) 11   500 89 1 false(unreach-call) 9.1 280 77 1 false(unreach-call) 3.5 150 34 1 false(unreach-call) 4.8 130 60 1
loop-acceleration/array_true-unreach-call1_true-termination.i true 41     700 500    2 true 6.7   1100   96    2 true 6.0   1100   83    2 true 100   660 1400 2 unknown .83 65 9.9 0 true 8.3  380 97   2 true 8.3  380 100   2 true 13     180 170    2 timeout 900    84 9400   0 true 21 1600 160 2 true .73 58 9.3 2 true 24   1000 260 2 disqualified 6.9 300 100 0 true .14 16 1.6 2 true 12   400 100 2 timeout 900   5300 9600 0 true 13   480 110 2 true 38   1200 410 2 timeout 900   150 12000 0 true 7.6 240 86 2
loop-acceleration/array_true-unreach-call2_true-termination.i out of memory 270     15000 2000    0 true 17     2200   240    1 true 15     2200   220    1 timeout 910   7100 9400 0 unknown 28    40 400   0 unknown 9.0  430 110   0 unknown 9.0  430 110   0 true 75     660 870    1 timeout 900    84 11000   0 unknown 100 3200 1300 0 true 1.5  58 17   1 true 3.9 210 33 1 disqualified 71   3400 940 0 true .15 16 1.6 1 timeout 900   930 10000 0 timeout 900   5400 8100 0 timeout 900   740 10000 0 true 4.2 190 30 1 timeout 900   150 10000 0 true 55   200 640 1
loop-acceleration/array_true-unreach-call3_true-termination.i true 13     430 140    2 true 7.8   620   100    2 witness invalid (true) 69     610   560    0 true 11   610 94 2 unknown .79 66 8.2 0 unknown 8.8  430 120   0 timeout 900    440 9500   0 true .087 26 1.0  2 timeout 900    4400 5700   0 true 21 1500 170 2 true 33    13000 420   2 true 3.9 230 36 2 disqualified 880   980 8600 0 true 12    21 160   2 true 9.4 410 69 2 timeout 900   5200 7800 0 true 10   440 83 2 true 15   200 100 2 timeout 900   200 11000 0 true 8.0 220 88 2
loop-acceleration/array_true-unreach-call4_true-termination.i out of memory 780     15000 5100    0 true 9.2   620   120    1 true 74     660   690    1 true 11   550 110 1 unknown 110    45 1400   0 unknown 8.5  430 110   0 timeout 900    440 8400   0 true 17     350 260    1 timeout 900    4900 6600   0 true 50 3500 410 1 true 32    12000 460   1 unknown 83   2700 890 0 disqualified 880   850 7200 0 true 13    21 170   1 timeout 900   770 12000 0 timeout 900   5000 8200 0 timeout 900   1100 10000 0 true 15   200 100 1 timeout 900   150 11000 0 true 6.6 140 80 1
loop-acceleration/const_true-unreach-call1.i true .18  23 1.7  2 true .67  16   8.0  2 witness invalid (true) .59  10   7.1  0 true 6.2 460 62 2 unknown .82 65 8.2 0 true 8.2  370 92   2 true 8.3  370 99   2 true .086 26 .78 2 timeout 900    85 11000   0 true 19 1200 140 2 true .68 58 7.5 2 true 4.1 220 42 2 disqualified 2.9 72 43 0 true .14 15 1.7 2 true 9.5 380 67 2 timeout 900   990 10000 0 true 8.5 370 62 2 true 14   460 130 2 timeout 900   150 12000 0 true 4.4 130 70 2
loop-acceleration/diamond_true-unreach-call1_true-termination.i true .76  28 11    2 true 1.4   45   16    1 out of memory 97     15000   1200    0 true 150   1500 1800 2 unknown 43    69 520   0 unknown 8.3  430 100   0 true 21    380 210   2 true 1.7   32 22    2 timeout 900    2200 12000   0 true 35 1600 300 1 true .45 59 4.4 2 unknown 46   990 400 0 disqualified 880   240 10000 0 true .19 18 1.8 2 timeout 900   760 12000 0 timeout 900   580 11000 0 timeout 900   690 11000 0 true 74   800 720 2 timeout 900   150 12000 0 true 140   240 1900 2
loop-acceleration/diamond_true-unreach-call2.i true .15  24 1.6  2 true .17  11   1.8  2 out of memory 78     15000   1100    0 true 7.1 360 58 2 unknown 2.8  67 35   0 unknown 8.2  430 120   0 true 29    380 310   2 true .24  26 3.2  2 timeout 900    2200 9700   0 true 20 1200 130 1 true .38 60 4.3 2 unknown 65   1200 720 0 disqualified 5.0 120 60 0 true .18 18 2.4 2 true 280   760 3700 2 true 370   580 5300 1 true 280   700 3400 2 true 51   850 510 2 timeout 900   160 10000 0 true 310   230 4900 2
loop-acceleration/functions_true-unreach-call1_true-termination.i timeout 900     1400 12000    0 out of memory 250     15000   3000    0 out of memory 190     15000   2600    0 timeout 970   9500 11000 0 unknown 34    43 480   0 timeout 900    3300 10000   0 timeout 900    3300 9000   0 out of memory 690     15000 8400    0 timeout 900    75 11000   0 timeout (exception) 910 11000 8200 0 out of memory 680    15000 7900   0 true 4.0 220 37 1 disqualified 880   1100 10000 0 probably out of memory (killed (signal 9, verification)) 230    15000 3400   0 timeout 900   770 10000 0 timeout 900   5300 8100 0 timeout 900   840 11000 0 true 120   1300 1400 2 error (1) 890   150 10000 0 true 23   130 340 1
loop-acceleration/multivar_true-unreach-call1_true-termination.i timeout 900     1600 12000    0 true 94     220   950    2 error (42) 880     150   11000    0 true 3.9 280 37 2 unknown 24    38 280   0 unknown 8.1  430 87   0 timeout 900    490 9300   0 true 430     1000 5900    2 timeout 900    2100 7800   0 true 13 1100 84 2 out of memory 42    15000 590   0 true 3.8 220 39 2 disqualified 880   950 12000 0 true .17 16 1.8 2 true 8.4 370 62 2 true 7.3 350 67 2 true 7.1 340 65 2 true 13   430 100 2 timeout 900   150 14000 0 true 4.6 130 62 2
loop-acceleration/nested_true-unreach-call1.i true .25  24 2.5  2 out of memory 320     15000   4000    0 out of memory 240     15000   2900    0 true 350   2700 5100 2 unknown .82 67 9.3 0 timeout 900    3600 8200   0 timeout 900    3600 9400   0 timeout 900     12000 11000    0 timeout 900    85 11000   0 true 13 1100 83 2 out of memory 800    15000 10000   0 true 3.8 210 35 2 disqualified 880   900 13000 0 true .14 16 1.5 2 true 47   910 550 2 timeout 900   860 6400 0 true 68   850 950 2 true 43   550 450 2 error (1) 54   200 640 0 true 150   130 1700 2
loop-acceleration/overflow_true-unreach-call1.i timeout 900     1300 11000    0 out of memory 270     15000   4300    0 out of memory 200     15000   3000    0 timeout 970   9100 10000 0 unknown 36    43 440   0 timeout 900    3500 9600   0 timeout 900    3500 9700   0 timeout 900     14000 10000    0 timeout 900    85 10000   0 timeout 970 7700 8500 0 out of memory 790    15000 11000   0 true 4.0 210 34 1 disqualified 880   920 12000 0 true .14 16 1.6 1 timeout 900   570 12000 0 timeout 900   740 11000 0 true 8.9 370 67 2 true 120   1300 1100 2 error (1) 53   150 650 0 true 190   130 1800 1
loop-acceleration/phases_true-unreach-call1.i timeout 900     1500 11000    0 out of memory 300     15000   3700    0 out of memory 230     15000   3400    0 timeout 910   2100 10000 0 unknown 48    47 630   0 timeout 900    3500 8400   0 timeout 900    3500 8200   0 timeout 900     9100 13000    0 timeout 900    75 9200   0 timeout 920 4300 9700 0 out of memory 800    15000 10000   0 unknown 240   1200 2200 0 disqualified 880   350 10000 0 probably out of memory (killed (signal 9, verification)) 230    15000 3400   0 timeout 900   580 12000 0 timeout 900   2700 8200 0 timeout 900   850 11000 0 true 270   9800 3500 1 error (1) 890   150 11000 0 true 120   260 1600 1
loop-acceleration/phases_true-unreach-call2_false-termination.i timeout 900     140 10000    0 error (42) 880     5500   8100    0 out of memory 630     15000   8400    0 true 4.1 280 40 2 unknown 120    180 1400   0 unknown 8.4  430 96   0 true 9.6  370 120   2 timeout 900     400 11000    0 timeout 900    75 10000   0 true 13 1100 90 2 out of memory 300    15000 3700   0 timeout 900   1700 10000 0 disqualified 880   180 12000 0 timeout (verification) 900    30 13000   0 true 11   380 110 2 true 77   1100 850 2 true 12   380 110 2 true 14   450 110 2 error (1) 890   150 12000 0 timeout 900   130 12000 0
loop-acceleration/simple_true-unreach-call1.i timeout 900     1400 10000    0 out of memory 270     15000   4000    0 out of memory 200     15000   2700    0 timeout 970   9300 9300 0 unknown 34    41 530   0 timeout 900    3500 9300   0 timeout 900    3500 9800   0 timeout 900     14000 12000    0 timeout 900    85 10000   0 timeout 970 10000 9000 0 out of memory 790    15000 12000   0 true 3.9 210 37 1 disqualified 880   940 13000 0 true .13 15 1.6 1 timeout 900   560 13000 0 timeout 900   2400 9300 0 true 9.1 380 73 2 true 120   1300 1200 2 error (1) 890   150 10000 0 true 16   130 170 1
loop-acceleration/simple_true-unreach-call2_true-termination.i true .090 24 1.0  2 error (42) 880     5400   5400    0 error (42) 870     220   11000    0 true 3.9 270 36 2 unknown .88 66 10   0 unknown 8.4  540 110   0 unknown 8.1  430 100   0 timeout 900     300 11000    0 timeout 900    84 10000   0 true 13 1100 93 2 timeout 900    380 4000   0 true 3.5 210 35 2 disqualified 2.4 75 34 0 true .14 16 1.4 2 true 7.7 370 72 2 true 7.6 350 64 2 true 8.1 360 72 2 true 12   460 110 2 timeout 900   150 8900 0 true 26   130 320 2
loop-acceleration/simple_true-unreach-call3_true-termination.i timeout 900     1200 12000    0 error (42) 880     6000   3600    0 error (42) 870     330   5900    0 timeout 970   9300 8900 0 unknown 41    41 520   0 unknown 8.1  430 110   0 timeout 900    470 8800   0 timeout 900     1800 9600    0 timeout 900    2200 11000   0 timeout 960 7400 7500 0 timeout 900    400 4200   0 true 3.9 220 34 2 disqualified 880   400 11000 0 true .17 16 1.5 2 true 10   390 95 2 true 8.3 370 63 2 true 9.7 370 100 2 true 120   1200 1300 2 timeout 900   150 14000 0 true 4.5 130 54 2
loop-acceleration/simple_true-unreach-call4.i true .11  23 .86 2 out of memory 280     15000   3400    0 out of memory 210     15000   2900    0 true 150   1000 2000 2 unknown .79 68 8.5 0 timeout 900    3500 9200   0 timeout 900    3600 10000   0 timeout 900     14000 11000    0 timeout 900    85 11000   0 true 13 1100 88 2 out of memory 820    15000 12000   0 true 4.0 210 40 2 disqualified 880   920 13000 0 true .14 16 1.4 2 true 8.7 370 67 2 timeout 900   860 9900 0 true 8.8 350 70 2 true 15   470 120 2 error (1) 890   150 11000 0 true 16   130 170 2
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true .18  24 1.7  2 true .082 6.7 .58 2 witness invalid (true) .061 6.2 .44 0 true 2.8 250 25 2 unknown 2.0  67 24   0 true 8.0  370 120   2 true 8.1  370 100   2 true .16  26 1.5  2 timeout 900    84 11000   0 true 13 1000 95 2 true .36 58 3.3 2 true 4.0 210 35 2 disqualified 2.0 67 22 0 true .16 15 1.7 2 true 15   480 150 2 timeout 900   710 12000 0 true 140   490 1800 2 true 29   600 240 2 timeout 900   150 12000 0 true 6.0 130 85 2
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true .14  24 1.4  2 true .069 6.8 .62 2 true .068 7.2 .82 2 true 2.7 240 28 2 unknown .79 66 8.8 0 true 8.1  370 110   2 true 8.1  370 100   2 true .085 26 .94 2 timeout 900    84 9800   0 true 11 1200 83 2 true .38 58 3.0 2 true 3.4 210 34 2 disqualified 2.0 67 27 0 true .14 17 1.6 2 true 8.5 360 66 2 true 9.6 370 79 2 true 10   470 87 2 true 14   470 130 2 timeout 900   150 10000 0 true 5.2 130 75 2
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i false(unreach-call) 4.4   1300 53    1 error (42) 880     1000   12000    0 false(unreach-call) .17  56   2.0  1 false(unreach-call) 3.8 270 35 1 false(unreach-call) .14 33 1.7 1 unknown 8.2  430 100   0 unknown 9.1  430 100   0 false(unreach-call) .084 26 .88 1 killed by signal 9 770    4300 6300   0 false(unreach-call) 12 1200 88 1 timeout 900    2500 7900   0 false(unreach-call) 5.4 270 52 1 disqualified 3.1 82 35 0 false(unreach-call) .22 24 2.9 1 false(unreach-call) 8.3 370 62 1 false(unreach-call) 7.5 350 65 1 false(unreach-call) 8.4 370 61 1 false(unreach-call) 300   6600 3600 1 timeout 900   150 11000 0 timeout 900   130 11000 0
loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i out of memory 780     15000 5300    0 true 28     1200   330    1 error (42) 870     570   13000    0 timeout 900   3700 12000 0 unknown 82    45 1200   0 true 8.4  370 93   1 true 8.2  370 99   1 true 14     200 170    1 timeout 900    82 10000   0 true 230 1700 3000 1 true .98 59 13   1 unknown 72   1600 960 0 disqualified 890   11000 3200 0 true .15 16 1.8 1 timeout 900   620 12000 0 timeout 900   1500 9600 0 timeout 900   860 14000 0 true 16   190 110 1 timeout 900   150 12000 0 true 11   240 130 1
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i out of memory 290     15000 1700    0 out of memory 96     12000   1400    0 error (42) 870     890   13000    0 timeout 960   9900 10000 0 unknown 94    63 1100   0 unknown 8.1  430 110   0 timeout 900    1000 8400   0 timeout 900     4300 10000    0 timeout 900    5000 10000   0 timeout 910 6300 11000 0 out of memory 41    15000 610   0 unknown 82   1400 970 0 disqualified 880   830 9800 0 true 350    53 4100   1 timeout 900   880 12000 0 timeout 900   910 9600 0 timeout 900   1000 12000 0 true 16   200 120 1 timeout 900   150 11000 0 unknown 160   250 2000 0
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i out of memory 270     15000 3000    0 out of memory 160     15000   2000    0 error (42) 880     9200   14000    0 timeout 960   2800 11000 0 unknown 91    48 1100   0 true 12    630 130   1 true 12    630 130   1 timeout 900     8200 11000    0 timeout 900    77 7700   0 timeout 960 6500 7600 0 true 12    230 150   1 unknown 93   1500 1100 0 disqualified 880   510 13000 0 true .23 19 3.3 1 timeout 900   670 11000 0 timeout 900   710 10000 0 timeout 900   690 11000 0 true 16   190 100 1 timeout 900   150 10000 0 true 10   240 130 1
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i error (134) .12  24 .72 0 out of memory 41     13000   660    0 error (42) 880     6200   10000    0 timeout 960   4400 8700 0 unknown 900    160 13000   0 unknown 48    430 720   0 unknown 9.0  430 120   0 timeout 900     210 13000    0 timeout 900    3800 11000   0 true 16 1300 130 1 error (139) 5.4  2000 64   0 true 54   1500 660 2 disqualified 2.7 89 33 0 timeout (verification) 900    2600 2500   0 true 54   480 740 2 true 410   660 5100 2 true 230   560 3400 2 true 17   200 140 2 error (1) 860   10000 10000 0 true 14   130 180 2
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i true .67  24 8.9  2 out of memory 300     15000   4300    0 out of memory 220     15000   3100    0 true 350   1600 4500 2 unknown 1.6  66 18   0 timeout 900    3300 9100   0 timeout 900    3400 9700   0 true .60  27 7.7  2 timeout 900    75 10000   0 true 14 1100 100 2 out of memory 760    15000 8900   0 true 3.6 220 39 2 disqualified 880   920 12000 0 probably out of memory (killed (signal 9, verification)) 170    15000 2900   0 true 7.7 350 59 2 true 8.7 370 64 2 true 7.9 370 65 2 true 14   450 110 2 error (1) 890   150 10000 0 true 29   190 460 2
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i timeout 900     330 8800    0 out of memory 310     15000   4500    0 out of memory 230     15000   3000    0 true 150   1100 1800 2 unknown .81 66 8.2 0 timeout 900    3100 8700   0 timeout 900    3100 8800   0 true .091 26 .94 2 timeout 900    74 11000   0 true 12 1200 88 1 out of memory 780    15000 9300   0 true 4.0 220 39 2 disqualified 880   850 9900 0 probably out of memory (killed (signal 9, verification)) 170    15000 2500   0 true 8.6 350 68 2 timeout 900   1200 9800 0 true 8.7 370 64 2 true 14   440 120 2 error (1) 890   200 14000 0 true 28   190 450 2
loop-crafted/simple_array_index_value_true-unreach-call4.i.v+lhb-reducer.c error (6) .092 24 .78 0 out of memory 41     13000   510    0 out of memory 230     13000   2600    0 timeout 960   3800 8300 0 unknown 65    160 1000   0 unknown 48    430 610   0 unknown 9.4  430 110   0 true .57  27 6.8  2 timeout 900    2500 4200   0 true 18 1300 150 2 error (139) 3.8  1100 44   0 true 66   1400 830 2 disqualified 2.4 76 33 0 timeout (verification) 900    2600 3300   0 true 26   600 290 1 timeout 900   700 11000 0 true 74   580 870 1 out of memory 49   15000 610 0 error (1) 870   11000 13000 0 unknown 2.6 130 34 0
loop-crafted/simple_array_index_value_true-unreach-call4.i.v+nlh-reducer.c error (6) .11  25 .72 0 out of memory 41     13000   580    0 out of memory 230     13000   3200    0 timeout 960   3300 8100 0 unknown 65    160 830   0 unknown 48    430 620   0 unknown 9.3  430 110   0 true .55  27 7.0  2 timeout 900    2500 3800   0 true 18 1300 150 2 error (139) 3.7  1100 44   0 true 65   1500 720 2 disqualified 880   320 8800 0 timeout (verification) 900    2600 3600   0 true 26   560 310 1 timeout 900   710 11000 0 true 29   510 320 1 out of memory 49   15000 600 0 error (1) 870   11000 12000 0 unknown 2.5 130 39 0
loop-invgen/id_trans_false-unreach-call_true-termination.i false(unreach-call) .12  24 1.1  1 false(unreach-call) .080 9.5 .53 1 false(unreach-call) .076 8.9 .72 1 false(unreach-call) 4.4 290 40 1 false(unreach-call) .14 33 1.9 1 unknown 8.4  430 110   0 false(unreach-call) 11    430 130   1 false(unreach-call) .092 26 .98 1 unknown 89    110 1300   0 false(unreach-call) 14 1100 110 1 false(unreach-call) .36 58 3.1 1 false(unreach-call) 5.6 300 54 1 disqualified 3.1 83 41 0 false(unreach-call) .29 23 3.3 1 false(unreach-call) 8.6 350 76 1 false(unreach-call) 9.4 370 82 1 false(unreach-call) 8.0 340 65 1 false(unreach-call) 14   270 100 1 false(unreach-call) 5.7 150 73 1 unknown 7.3 130 110 0
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i timeout 900     480 8000    0 error (42) 870     740   8300    0 out of memory 790     15000   10000    0 timeout 960   3500 11000 0 unknown 900    59 11000   0 unknown 8.2  430 98   0 timeout 900    550 10000   0 timeout 900     89 9700    0 timeout 900    4200 10000   0 timeout 960 3700 11000 0 out of memory 140    15000 1500   0 true 52   1400 680 2 disqualified 65   170 850 0 timeout (verification) 900    1200 11000   0 true 9.9 410 93 2 true 11   550 99 2 true 11   470 97 2 true 16   480 140 2 timeout 900   150 11000 0 error (1) 4.1 130 57 0
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i true .15  23 1.9  2 error (42) 880     1100   11000    0 out of memory 490     15000   6600    0 timeout 970   8100 10000 0 unknown .90 67 10   0 unknown 8.3  430 110   0 timeout 900    590 8400   0 true .14  26 1.7  2 unknown .75 39 9.1 0 timeout 970 7500 8800 0 out of memory 40    15000 550   0 true 3.7 210 37 2 disqualified 880   590 12000 0 timeout (verification) 900    330 11000   0 true 9.9 420 80 2 true 10   500 85 2 true 10   470 86 2 true 16   500 140 2 error (1) 890   150 12000 0 true 6.7 140 81 2
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i true 1.5   41 16    2 error (42) 880     900   9800    0 out of memory 300     15000   4500    0 true 9.6 320 92 2 unknown 900    300 13000   0 unknown 8.2  430 96   0 timeout 900    450 8200   0 timeout 900     420 11000    0 timeout 900    4100 8900   0 true 18 1200 150 2 out of memory 43    15000 620   0 unknown 81   1500 840 0 disqualified 880   350 8900 0 timeout (verification) 900    3600 11000   0 true 12   490 110 2 true 26   800 240 2 true 13   560 130 2 true 19   660 180 2 error (1) 7.4 150 84 0 timeout 900   130 11000 0
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i timeout 900     1900 11000    0 error (42) 880     150   13000    0 out of memory 470     15000   6600    0 true 5.9 300 55 2 unknown 900    67 14000   0 unknown 8.4  540 100   0 timeout 900    450 7200   0 timeout 900     85 13000    0 timeout 900    4100 13000   0 true 13 1200 110 2 out of memory 78    15000 1000   0 unknown 73   1700 790 0 disqualified 880   350 9600 0 timeout (verification) 900    2600 9000   0 true 12   550 97 2 true 23   730 180 2 true 12   580 110 2 timeout 900   1200 11000 0 timeout 900   150 11000 0 unknown 230   140 3300 0
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i true .61  24 8.5  2 error (42) 880     1800   9600    0 out of memory 300     15000   3700    0 true 210   1800 2600 2 unknown 900    89 11000   0 unknown 8.0  430 98   0 timeout 900    450 6900   0 timeout 900     150 11000    0 timeout 900    4500 7800   0 true 19 1300 120 2 out of memory 53    15000 690   0 unknown 110   1500 1200 0 disqualified 880   380 10000 0 timeout (verification) 900    3100 12000   0 true 11   520 110 2 true 13   490 100 2 true 11   540 110 2 timeout 900   1900 10000 0 error (1) 860   160 13000 0 unknown 500   290 6400 0
loop-invgen/down_true-unreach-call_true-termination.i timeout 900     1500 9400    0 error (42) 880     1200   8000    0 error (42) 880     1000   10000    0 timeout 940   11000 9100 0 unknown 140    62 1900   0 unknown 8.2  430 100   0 timeout 900    920 8000   0 timeout 900     610 13000    0 unknown .78 40 9.8 0 timeout 950 9700 9500 0 timeout 900    400 4700   0 true 36   1200 380 1 disqualified 880   390 11000 0 timeout (verification) 900    450 6400   0 timeout 900   1800 11000 0 timeout 900   1700 8700 0 timeout 900   1700 11000 0 true 150   1500 1400 1 error (1) 880   150 11000 0 true 6.2 130 86 1
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i timeout 900     3000 11000    0 error (42) 880     1400   8600    0 error (42) 880     1200   10000    0 timeout 930   10000 9700 0 unknown 130    66 2000   0 unknown 8.4  430 100   0 timeout 900    500 6400   0 timeout 900     1100 10000    0 timeout 900    4300 6600   0 timeout 950 8300 8400 0 timeout 900    680 12000   0 true 32   1100 430 1 disqualified 880   570 12000 0 timeout (verification) 900    1500 8900   0 timeout 900   2900 11000 0 timeout 900   1600 7500 0 timeout 900   2500 11000 0 true 12   200 85 1 timeout 900   200 13000 0 true 8.8 160 100 1
loop-invgen/half_2_true-unreach-call_true-termination.i timeout 900     1900 10000    0 error (42) 880     1200   10000    0 error (42) 880     4400   10000    0 timeout 960   6700 9000 0 unknown 170    65 2400   0 unknown 8.2  430 100   0 timeout 900    570 8200   0 timeout 900     560 13000    0 timeout 900    83 9300   0 timeout 960 6000 8400 0 timeout 900    380 4400   0 true 40   1200 500 1 disqualified 630   270 10000 0 timeout (verification) 900    880 11000   0 timeout 900   960 7200 0 timeout 900   920 7700 0 timeout 900   950 10000 0 true 140   1200 1200 1 timeout 900   150 12000 0 true 45   280 770 1
loop-invgen/heapsort_true-unreach-call_true-termination.i timeout 900     1400 5300    0 error (42) 880     1400   9300    0 out of memory 270     15000   3800    0 timeout 940   4900 6700 0 unknown 900    300 11000   0 unknown 8.2  430 110   0 timeout 900    430 8700   0 timeout 900     570 11000    0 unknown 41    3400 410   0 timeout 950 5000 8800 0 out of memory 48    15000 660   0 unknown 230   1600 2800 0 disqualified 880   400 6800 0 timeout (verification) 900    2000 11000   0 true 36   800 320 2 true 120   1200 1400 2 true 36   840 300 2 true 150   1000 1500 2 timeout 900   150 12000 0 unknown 180   190 2400 0
loop-invgen/id_build_true-unreach-call_true-termination.i true .28  23 4.2  2 error (42) 880     2000   11000    0 out of memory 400     15000   5000    0 true 210   2200 2900 2 unknown 900    340 12000   0 unknown 8.1  430 130   0 timeout 900    600 9100   0 timeout 900     1200 11000    0 timeout 900    75 9500   0 true 16 1200 100 2 out of memory 44    15000 550   0 true 54   1400 730 2 disqualified 890   520 10000 0 timeout (verification) 900    1300 9100   0 true 8.8 370 71 2 true 8.9 360 64 2 true 8.2 350 70 2 true 14   480 130 2 error (1) 890   150 11000 0 true 8.5 130 120 2
loop-invgen/large_const_true-unreach-call_true-termination.i true .24  24 2.7  2 true .062 6.4 .54 2 true .10  7.2 .99 2 true 5.0 290 47 2 unknown .96 66 9.6 0 unknown 8.3  430 100   0 true 13    370 170   2 true .11  26 .83 2 timeout 900    2200 8900   0 true 16 1200 100 2 true .44 64 3.7 2 true 12   460 100 2 disqualified 2.5 79 30 0 true .20 18 2.2 2 true 10   440 77 2 true 10   520 89 2 true 12   520 100 2 true 22   520 180 2 timeout 900   200 11000 0 true 34   160 370 2
loop-invgen/nest-if3_true-unreach-call_true-termination.i true .86  28 11    2 error (42) 880     1500   6800    0 out of memory 170     15000   2300    0 timeout 970   3300 10000 0 unknown 900    240 13000   0 unknown 8.1  430 100   0 timeout 900    440 8200   0 timeout 900     360 12000    0 timeout 900    270 8100   0 timeout 970 4300 7900 0 out of memory 82    15000 1200   0 timeout 900   2600 7500 0 disqualified 880   330 12000 0 timeout (verification) 900    44 11000   0 true 8.3 370 69 2 true 13   660 120 2 true 7.7 340 69 2 true 14   450 110 2 timeout 900   150 13000 0 unknown 110   450 1600 0
loop-invgen/nested6_true-unreach-call_true-termination.i timeout 900     2300 5500    0 error (42) 880     510   5700    0 out of memory 130     15000   1700    0 timeout 960   7600 9500 0 unknown 900    1200 11000   0 unknown 8.2  430 110   0 timeout 900    550 7200   0 timeout 900     640 10000    0 unknown 1.0  41 12   0 timeout 970 4800 9400 0 timeout 900    410 4400   0 timeout 900   4800 6100 0 disqualified 880   270 11000 0 timeout (verification) 900    3900 7400   0 true 11   510 83 2 true 12   560 94 2 true 12   500 90 2 timeout 900   2600 7900 0 timeout 900   150 11000 0 true 270   390 3000 2
loop-invgen/nested9_true-unreach-call_true-termination.i timeout 900     350 8700    0 out of memory 390     13000   3600    0 out of memory 430     15000   5600    0 timeout 960   7700 9500 0 unknown 900    1800 10000   0 unknown 8.1  430 100   0 timeout 900    1100 8700   0 timeout 900     5100 12000    0 timeout 900    86 8400   0 timeout 960 5900 7200 0 out of memory 45    15000 530   0 timeout 900   5100 8500 0 disqualified 880   540 11000 0 timeout (verification) 900    1000 13000   0 true 12   560 98 2 true 19   710 180 2 true 13   520 110 2 true 19   620 170 2 timeout 900   150 11000 0 true 180   900 2000 2
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i timeout 900     1900 10000    0 error (42) 880     2000   12000    0 out of memory 800     15000   10000    0 timeout 970   8600 9100 0 unknown 160    68 1800   0 unknown 8.2  430 120   0 timeout 900    460 8300   0 timeout 900     1100 11000    0 timeout 900    4200 11000   0 timeout 960 6800 8800 0 out of memory 43    15000 570   0 true 56   1500 710 2 disqualified 880   470 12000 0 timeout (verification) 900    1100 8500   0 true 19   660 170 1 true 25   780 290 2 true 19   720 190 1 true 820   1800 8900 1 timeout 900   150 12000 0 unknown 220   340 2800 0
loop-invgen/seq_true-unreach-call_true-termination.i timeout 900     820 7300    0 error (42) 880     560   6800    0 error (42) 880     2000   9800    0 timeout 950   11000 10000 0 unknown 280    80 4400   0 unknown 8.0  430 100   0 timeout 900    500 7300   0 timeout 900     310 13000    0 timeout 900    84 11000   0 timeout 950 7700 9200 0 timeout 900    370 3900   0 true 50   960 620 1 disqualified 880   350 11000 0 timeout (verification) 900    810 11000   0 timeout 900   900 12000 0 timeout 900   1400 9800 0 timeout 900   1200 14000 0 true 150   1100 1500 1 timeout 900   150 10000 0 true 7.6 130 98 1
loop-invgen/string_concat-noarr_true-unreach-call_false-termination.i error (6) .11  24 .69 0 error (42) 880     8500   7000    0 error (42) 880     5000   7300    0 timeout 920   13000 9000 0 unknown 900    14000 8500   0 timeout 900    3800 9400   0 timeout 900    3700 7900   0 out of memory 300     15000 3600    0 unknown .81 40 10   0 timeout 940 10000 9000 0 timeout 900    670 12000   0 unknown 210   1500 1800 0 disqualified 890   560 11000 0 timeout (verification) 900    140 7700   0 timeout 900   1100 12000 0 timeout 900   2100 7800 0 timeout 900   1000 15000 0 true 150   1400 1400 1 error (1) 11   150 120 0 unknown 2.4 130 32 0
loop-invgen/up_true-unreach-call_true-termination.i timeout 900     1800 7500    0 error (42) 880     1500   7400    0 error (42) 880     1100   9400    0 timeout 950   14000 9900 0 unknown 130    65 1500   0 unknown 8.2  430 110   0 timeout 900    810 8500   0 timeout 900     850 12000    0 timeout 900    1700 9800   0 timeout 960 9500 8800 0 timeout 900    400 3900   0 true 37   1100 410 1 disqualified 880   460 10000 0 timeout (verification) 900    1500 11000   0 timeout 900   1700 11000 0 timeout 900   1400 8400 0 timeout 900   1600 10000 0 true 150   1500 1400 1 error (1) 880   150 10000 0 true 6.1 130 72 1
loop-invgen/SpamAssassin-loop_true-unreach-call.i.v+cfa-reducer.c error (6) .091 25 .91 0 error (42) 880     410   10000    0 out of memory 210     15000   2700    0 true 9.4 330 110 2 out of memory 320    15000 2300   0 unknown 8.3  430 100   0 timeout 900    460 7400   0 out of memory 500     15000 3100    0 unknown 1.1  42 13   0 timeout 960 4500 11000 0 out of memory 49    15000 650   0 unknown 230   1600 2300 0 disqualified 880   380 7500 0 timeout (verification) 900    3200 12000   0 true 16   570 140 1 true 76   920 680 2 true 16   580 140 1 timeout 900   670 8000 0 error (1) 8.0 170 95 0 unknown 9.3 130 120 0
loop-invgen/apache-escape-absolute_true-unreach-call.i.v+cfa-reducer.c error (6) .11  25 1.0  0 error (42) 880     1200   9100    0 error (42) 880     15000   9200    0 true 6.8 340 68 2 out of memory 550    15000 6100   0 unknown 8.2  430 110   0 timeout 900    460 7100   0 true 12     90 150    2 unknown 1.2  45 14   0 true 14 1200 100 2 out of memory 72    15000 1200   0 unknown 89   3100 1000 0 disqualified 880   380 9600 0 timeout (verification) 900    2500 11000   0 true 19   660 150 1 true 41   960 480 2 true 20   670 170 1 timeout 900   1000 11000 0 error (1) 870   180 12000 0 unknown 2.9 130 44 0
loop-invgen/apache-get-tag_true-unreach-call.i.p+lhb-reducer.c out of memory 55     15000 530    0 error (42) 880     2000   11000    0 error (42) 880     6300   7900    0 true 220   1600 3000 2 unknown 900    5200 11000   0 unknown 8.2  430 93   0 timeout 900    430 8000   0 out of memory 810     15000 9200    0 unknown 1.5  51 20   0 timeout 900 6900 11000 0 out of memory 70    15000 890   0 unknown 140   1800 1400 0 disqualified 880   400 8900 0 timeout (verification) 900    3000 8600   0 true 17   550 150 2 true 35   910 350 2 true 19   670 150 2 timeout 900   820 9300 0 error (1) 860   210 11000 0 out of memory 720   15000 7500 0
loop-invgen/apache-get-tag_true-unreach-call.i.p+nlh-reducer.c out of memory 55     15000 470    0 error (42) 880     4000   12000    0 error (42) 880     3700   11000    0 true 260   1600 3300 2 unknown 900    13000 11000   0 error - divine failed with exitcode 1 .11 16 1.4 0 error - divine failed with exitcode 1 .11 16 1.3 0 timeout 900     11000 10000    0 unknown .49 33 5.9 0 true 65 2400 490 2 out of memory 68    15000 840   0 unknown 2.9 180 30 0 disqualified 880   520 9300 0 timeout (verification) 900    3000 9100   0