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 true 30   830 260 2 true 150   1600 1600 2 true 30   820 310 2 timeout 900   1200 10000 0 error (1) 870   1100 11000 0 out of memory 820   15000 7300 0
loop-invgen/apache-get-tag_true-unreach-call.i.p+sep-reducer.c out of memory 46     15000 450    0 error (42) 880     6200   10000    0 error (42) 880     2900   9000    0 true 280   2300 3200 2 out of memory 180    15000 2200   0 error - divine failed with exitcode 1 .15 17 1.3 0 error - divine failed with exitcode 1 .13 17 1.3 0 out of memory 170     15000 1800    0 unknown .49 33 5.7 0 true 90 2700 770 2 out of memory 73    15000 1000   0 unknown 2.9 180 34 0 disqualified 890   600 10000 0 timeout (verification) 900    2500 9300   0 true 39   1000 330 2 true 56   1400 620 2 true 39   1100 350 2 timeout 900   6700 13000 0 error (1) 870   1400 12000 0 out of memory 760   15000 6900 0
loop-invgen/apache-get-tag_true-unreach-call.i.v+lhb-reducer.c error (6) .10  25 .88 0 error (42) 880     4600   12000    0 out of memory 620     15000   7500    0 true 210   1600 2600 2 unknown 900    5200 10000   0 unknown 8.4  430 110   0 timeout 900    470 8500   0 timeout 900     2800 10000    0 unknown 1.0  43 12   0 true 21 1400 150 2 out of memory 67    15000 990   0 unknown 300   2000 2700 0 disqualified 880   390 10000 0 timeout (verification) 900    3000 9100   0 true 17   600 150 2 true 23   630 230 2 true 17   530 150 2 timeout 900   870 10000 0 error (1) 860   180 10000 0 unknown 14   160 170 0
loop-invgen/apache-get-tag_true-unreach-call.i.v+nlh-reducer.c error (6) .10  25 .87 0 error (42) 880     4500   13000    0 out of memory 610     15000   7600    0 true 210   1900 3100 2 unknown 900    5200 14000   0 unknown 8.2  430 95   0 timeout 900    470 8000   0 timeout 900     2800 9400    0 unknown .95 42 11   0 true 20 1300 150 2 out of memory 67    15000 1000   0 unknown 120   1800 1200 0 disqualified 880   330 12000 0 timeout (verification) 900    3000 9900   0 true 16   570 130 2 true 21   590 220 2 true 16   560 140 2 timeout 900   840 11000 0 error (1) 870   180 12000 0 unknown 6.8 130 100 0
loop-invgen/id_build_true-unreach-call.i.p+nlh-reducer.c out of memory 57     15000 560    0 error (42) 880     900   11000    0 error (42) 880     590   9800    0 true 13   450 120 2 unknown 9.0  210 120   0 error - divine failed with exitcode 1 .11 16 1.3 0 error - divine failed with exitcode 1 .11 16 1.5 0 true 2.2   80 25    2 unknown .48 32 5.9 0 timeout 920 6000 11000 0 out of memory 42    15000 650   0 unknown 2.6 170 27 0 disqualified 4.0 200 50 0 timeout (verification) 900    1200 12000   0 true 15   590 120 1 true 18   520 140 2 true 16   570 120 1 timeout 900   1200 8700 0 timeout 900   400 11000 0 unknown 20   130 250 0
loop-invgen/id_build_true-unreach-call.i.p+sep-reducer.c error (6) .32  47 3.2  0 error (42) 880     1000   12000    0 error (42) 880     660   9100    0 true 13   460 120 2 unknown 900    1300 12000   0 unknown 8.5  430 94   0 timeout 900    620 9700   0 true 3.5   88 41    2 unknown 1.3  46 14   0 timeout 930 6000 9900 0 out of memory 42    15000 640   0 timeout 900   5100 7800 0 disqualified 3.9 200 50 0 timeout (verification) 900    1200 9600   0 true 15   570 120 2 true 19   530 160 2 true 15   510 120 2 timeout 900   1600 9000 0 timeout 900   400 12000 0 out of memory 590   15000 4700 0
loop-invgen/id_build_true-unreach-call.i.v+lhb-reducer.c timeout 900     24 11000    0 error (42) 880     870   10000    0 error (42) 880     230   10000    0 true 4.6 290 48 2 unknown 1.8  66 24   0 unknown 8.2  430 120   0 timeout 900    600 9600   0 true .11  26 1.2  2 unknown .87 41 11   0 timeout 960 4800 11000 0 out of memory 41    15000 470   0 timeout 900   5100 8000 0 disqualified 880   730 10000 0 timeout (verification) 900    1200 9800   0 true 9.2 380 67 2 true 11   560 87 2 true 9.1 360 62 2 timeout 900   740 7900 0 error (1) 7.5 150 88 0 unknown 2.5 130 30 0
loop-lit/afnp2014_true-unreach-call_true-termination.c.i timeout 900     2000 12000    0 true 15     120   190    2 witness invalid (true) 61     130   540    0 true 11   610 94 2 unknown 91    62 1100   0 true 8.9  370 120   2 true 8.9  370 94   2 true 660     1500 9500    2 unknown .75 39 9.1 0 true 19 1300 150 2 true 19    6300 280   2 unknown 370   1400 3300 0 disqualified 880   660 13000 0 true 12    25 170   2 true 8.3 370 60 2 timeout 900   1300 10000 0 true 9.9 390 78 2 true 6.1 200 48 2 timeout 900   150 13000 0 true 5.7 130 84 2
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i timeout 900     290 10000    0 error (42) 880     530   11000    0 out of memory 240     15000   3400    0 timeout 970   2900 12000 0 unknown 720    76 8800   0 unknown 8.1  430 100   0 timeout 900    450 7000   0 timeout 900     150 11000    0 killed by signal 9 850    4000 7800   0 timeout 960 4000 10000 0 timeout 900    440 8100   0 true 77   720 840 2 disqualified 880   120 10000 0 timeout (verification) 900    38 12000   0 true 10   480 87 2 true 9.8 370 72 2 true 11   480 97 2 true 19   570 170 2 timeout 900   150 13000 0 true 260   330 3000 2
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true .17  24 1.6  2 true .057 7.3 .52 2 true .065 7.0 .38 2 true 2.8 250 25 2 unknown 1.5  67 21   0 true 8.2  370 100   2 true 8.2  370 92   2 true .14  26 1.2  2 timeout 900    85 10000   0 true 13 1000 84 2 true .39 58 3.1 2 true 26   1000 330 2 disqualified 2.4 76 27 0 true .15 16 1.6 2 true 9.7 380 75 2 true 10   490 80 2 true 9.2 410 73 2 true 15   460 150 2 timeout 900   150 11000 0 true 4.9 130 57 2
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i timeout 900     1600 10000    0 error (42) 880     3500   4500    0 error (42) 870     160   11000    0 timeout 970   7100 9300 0 unknown 67    42 820   0 unknown 8.1  430 92   0 timeout 900    730 8900   0 timeout 900     400 11000    0 timeout 900    2100 11000   0 timeout 970 12000 9100 0 timeout 900    460 4000   0 true 7.5 330 75 2 disqualified 330   530 4600 0 true .19 17 2.0 2 true 9.9 410 89 2 true 9.0 340 68 2 true 11   460 90 2 true 16   460 120 2 timeout 900   150 11000 0 true 5.6 130 68 2
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i timeout 900     5200 7000    0 true .19  7.2 2.0  2 witness invalid (true) .16  6.9 1.9  0 true 4.2 270 40 2 unknown 900    660 11000   0 true 8.0  370 91   2 true 8.2  370 98   2 true .41  28 5.2  2 unknown .84 40 9.9 0 true 15 1200 100 2 true .41 58 3.9 2 true 4.1 230 41 2 disqualified 67   1200 910 0 true .14 16 1.7 2 true 8.3 350 67 2 true 8.5 360 74 2 true 8.9 380 76 2 true 6.5 220 50 2 timeout 900   200 13000 0 true 13   160 200 2
loop-lit/css2003_true-unreach-call_true-termination.c.i timeout 900     310 12000    0 error (42) 880     650   3700    0 error (42) 880     11000   12000    0 true 4.5 280 46 2 unknown .86 67 9.0 0 unknown 8.1  430 100   0 timeout 900    690 9800   0 true .14  26 1.4  2 timeout 900    160 10000   0 true 12 1200 88 2 out of memory 43    15000 460   0 true 3.9 230 38 2 disqualified 480   420 6300 0 true 8.1  340 130   2 true 8.9 360 69 2 true 8.9 370 80 2 true 8.8 370 78 2 true 6.3 200 51 2 timeout 900   150 9900 0 true 88   450 1300 2
loop-lit/ddlm2013_true-unreach-call.i timeout 900     2000 11000    0 error (42) 880     1500   7300    0 error (42) 880     590   8600    0 timeout 910   7000 9300 0 unknown 220    86 3200   0 unknown 8.2  430 120   0 timeout 900    750 9600   0 timeout 900     1600 10000    0 timeout 900    4000 8000   0 timeout 910 11000 9100 0 timeout 900    890 12000   0 unknown 310   1300 3900 0 disqualified 880   320 14000 0 timeout (verification) 900    55 11000   0 true 12   470 90 2 timeout 900   680 11000 0 true 15   500 130 2 true 770   1500 9000 2 error (1) 860   190 10000 0 true 110   210 1300 2
loop-lit/gj2007_true-unreach-call_true-termination.c.i true 5.0   90 57    2 true .15  7.2 1.5  2 true .24  6.4 1.1  2 true 3.6 260 30 2 unknown 63    58 920   0 true 8.3  370 110   2 true 8.3  370 110   2 true .25  26 3.0  2 timeout 900    84 9900   0 true 15 1100 110 2 true .42 58 3.3 2 true 3.9 210 40 2 disqualified 880   460 11000 0 true .14 16 2.4 2 true 71   1100 690 2 true 290   1200 3400 2 true 120   1100 1200 2 true 81   1500 880 2 timeout 900   150 11000 0 true 110   230 1300 2
loop-lit/gj2007b_true-unreach-call_true-termination.c.i timeout 900     1200 11000    0 error (42) 880     1500   7600    0 out of memory 320     15000   4200    0 timeout 960   4100 10000 0 unknown 86    59 1100   0 unknown 8.4  430 120   0 timeout 900    440 8500   0 timeout 900     1000 9700    0 killed by signal 9 890    4000 7300   0 timeout 960 3800 11000 0 timeout 900    480 7900   0 true 23   740 240 2 disqualified 880   350 11000 0 timeout (verification) 900    120 12000   0 true 8.8 360 64 2 true 10   500 77 2 true 10   440 81 2 true 20   460 150 2 error (1) 7.3 190 110 0 unknown 190   270 2900 0
loop-lit/gr2006_true-unreach-call_true-termination.c.i true 9.0   130 130    2 true .17  6.8 2.1  2 true .17  6.3 1.9  2 true 3.7 260 30 2 unknown .78 66 8.4 0 true 8.1  370 110   2 true 8.1  370 91   2 true .28  26 3.4  2 timeout 900    83 9400   0 true 15 1200 110 2 true .40 58 3.6 2 unknown 220   1200 3100 0 disqualified 600   480 7600 0 true .14 15 1.8 2 true 120   1300 1500 2 timeout 900   1200 8300 0 true 110   970 1300 2 true 110   1700 990 2 timeout 900   150 12000 0 true 160   200 1900 2
loop-lit/gsv2008_true-unreach-call_true-termination.c.i timeout 900     670 9000    0 true 220     520   1700    2 error (42) 880     85   9800    0 timeout 970   6400 9800 0 unknown 440    54 5500   0 unknown 8.1  430 120   0 timeout 900    450 8500   0 timeout 900     99 11000    0 timeout 900    2100 9600   0 true 740 9000 6500 1 timeout 900    8000 4900   0 true 67   720 800 2 disqualified 880   320 13000 0 timeout (verification) 900    53 12000   0 true 7.8 330 63 2 true 9.2 390 87 2 true 9.0 370 67 2 true 380   1100 4200 2 timeout 900   150 13000 0 true 8.5 130 120 2
loop-lit/hhk2008_true-unreach-call_true-termination.c.i timeout 900     340 12000    0 error (42) 880     230   12000    0 error (42) 870     71   12000    0 timeout 970   7200 8800 0 unknown 66    42 830   0 unknown 8.1  430 110   0 timeout 900    630 8000   0 timeout 900     380 12000    0 timeout 900    4200 10000   0 timeout 910 12000 7800 0 timeout 900    460 5000   0 true 6.7 320 63 2 disqualified 140   320 1800 0 true .17 18 2.2 2 true 8.6 350 72 2 true 7.9 330 60 2 true 9.7 400 81 2 true 15   480 120 2 timeout 900   150 11000 0 true 5.4 130 60 2
loop-lit/jm2006_true-unreach-call_true-termination.c.i timeout 900     1400 11000    0 error (42) 880     4900   4400    0 error (42) 880     220   9500    0 true 4.4 290 41 2 unknown 26    38 420   0 unknown 8.2  430 120   0 timeout 900    410 8800   0 timeout 900     1200 11000    0 timeout 900    92 9300   0 true 13 1100 91 2 timeout 900    500 7400   0 true 4.0 220 38 2 disqualified 880   930 11000 0 true .17 17 1.8 2 true 10   500 83 2 true 9.5 420 72 2 true 12   550 110 2 true 15   450 120 2 error (1) 890   150 12000 0 true 5.0 130 64 2
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i timeout 900     1600 11000    0 error (42) 880     4300   4500    0 error (42) 870     230   10000    0 timeout 960   7400 10000 0 unknown 28    38 410   0 unknown 8.1  430 88   0 timeout 900    450 8600   0 timeout 900     1500 13000    0 timeout 900    3800 9500   0 timeout 910 5900 11000 0 timeout 900    490 3600   0 true 7.0 330 67 2 disqualified 320   670 4400 0 true .17 18 1.9 2 true 10   470 93 2 true 10   380 71 2 true 11   490 84 2 true 15   440 110 2 timeout 900   150 11000 0 true 5.4 130 77 2
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i error (134) .17  24 1.9  0 out of memory 480     13000   5300    0 error (42) 880     4600   12000    0 timeout 960   4700 8700 0 unknown 900    98 12000   0 unknown 8.4  430 95   0 unknown 1.5  200 22   0 timeout 900     160 13000    0 timeout 900    2200 9900   0 timeout 960 6700 8500 0 out of memory 700    15000 9400   0 unknown 11   290 94 0 disqualified 880   360 12000 0 timeout (verification) 900    2300 12000   0 timeout 900   880 12000 0 timeout 900   960 8400 0 timeout 900   860 13000 0 true 150   1300 1400 1 timeout 900   160 12000 0 true 7.9 230 92 1
loop-lit/gcnr2008_false-unreach-call_false-termination.i false(unreach-call) .13  24 .94 1 false(unreach-call) .061 10   .73 1 false(unreach-call) .070 9.2 .40 1 false(unreach-call) 3.5 260 31 1 false(unreach-call) .15 33 1.8 1 false(unreach-call) 8.2  430 96   1 false(unreach-call) 8.4  430 110   1 false(unreach-call) .087 26 .86 1 false(unreach-call) .47 83 6.0 1 false(unreach-call) 13 1100 98 1 false(unreach-call) .86 58 10   1 false(unreach-call) 6.4 320 66 1 disqualified 3.0 81 37 0 false(unreach-call) .20 18 2.3 1 false(unreach-call) 8.1 380 66 1 false(unreach-call) 8.2 350 62 1 false(unreach-call) 6.9 330 61 1 false(unreach-call) 14   270 100 1 false(unreach-call) 3.6 150 38 1 false(unreach-call) 7.2 130 91 1
loop-lit/gj2007_true-unreach-call.c.i.p+lhb-reducer.c error (6) .13  25 .93 0 true .18  6.8 1.7  2 witness invalid (true) .18  6.3 1.7  0 true 4.0 260 35 2 unknown .98 67 12   0 true 8.0  370 120   2 true 8.2  370 95   2 out of memory 110     15000 1300    0 timeout 900    84 11000   0 timeout 900 1700 10000 0 true .38 59 3.7 2 true 3.7 210 37 2 disqualified 880   390 11000 0 true .14 15 1.4 2 true 78   1100 770 2 true 290   1200 4100 2 true 110   1100 1300 2 true 86   1400 790 2 timeout 900   160 14000 0 unknown 2.5 130 41 0
loop-lit/gj2007_true-unreach-call.c.i.p+nlh-reducer.c out of memory 48     15000 500    0 true .32  8.2 4.0  2 witness invalid (true) .33  9.5 4.7  0 true 4.1 260 42 2 out of memory 94    15000 1300   0 true 8.1  370 86   2 true 8.4  370 110   2 out of memory 110     15000 1300    0 unknown .84 40 9.6 0 true 15 1300 120 2 true .43 63 3.4 2 true 3.9 210 35 2 disqualified 15   130 190 0 true .16 15 1.9 2 true 97   1100 960 2 true 150   1400 1800 2 true 110   1100 1400 2 true 89   1100 790 2 timeout 900   260 13000 0 unknown 4.5 130 67 0
loop-lit/gsv2008_true-unreach-call.c.i.p+cfa-reducer.c timeout 900     810 9600    0 true 230     590   1900    2 error (42) 880     100   11000    0 timeout 960   7700 9300 0 unknown 450    59 5300   0 unknown 8.2  430 95   0 timeout 900    450 9300   0 timeout 900     650 11000    0 timeout 900    2200 10000   0 true 830 9800 7700 2 timeout 900    7700 4300   0 true 68   790 770 2 disqualified 880   300 11000 0 timeout (verification) 900    290 9800   0 true 8.9 360 66 2 true 12   560 110 2 true 8.0 360 65 2 true 440   1200 4600 2 timeout 900   150 12000 0 true 11   130 190 2
loop-lit/gsv2008_true-unreach-call.c.i.v+cfa-reducer.c timeout 900     810 11000    0 true 230     590   2500    2 error (42) 880     100   9900    0 timeout 960   7500 9100 0 unknown 450    58 6400   0 unknown 8.3  430 94   0 timeout 900    450 9600   0 timeout 900     650 10000    0 timeout 900    2100 9100   0 true 730 9200 6900 2 timeout 900    8100 5800   0 true 68   770 820 2 disqualified 880   300 10000 0 timeout (verification) 900    290 9600   0 true 8.3 370 65 2 true 12   550 95 2 true 7.9 340 68 2 true 450   1100 4700 2 timeout 900   150 11000 0 true 11   130 140 2
loop-lit/gsv2008_true-unreach-call.c.i.v+lhb-reducer.c timeout 900     890 8100    0 true 240     690   2500    2 error (42) 880     110   11000    0 timeout 970   4100 10000 0 unknown 1.2  67 12   0 unknown 8.1  430 110   0 timeout 900    440 8600   0 timeout 900     700 11000    0 unknown .77 39 9.2 0 timeout 970 4400 9700 0 timeout 900    8000 4400   0 true 70   920 880 2 disqualified 880   280 12000 0 timeout (verification) 900    280 12000   0 true 9.3 370 67 2 true 12   510 100 2 true 9.0 370 69 2 unknown 840   940 7500 0 timeout 900   150 14000 0 true 13   130 160 2
loop-lit/jm2006_true-unreach-call.c.i.v+cfa-reducer.c timeout 900     1700 9700    0 error (42) 880     3200   7200    0 error (42) 880     270   9500    0 true 4.4 280 42 2 unknown 41    52 490   0 unknown 8.3  430 110   0 timeout 900    390 8900   0 timeout 900     14000 7900    0 timeout 900    100 10000   0 true 13 1100 91 2 timeout 900    630 6400   0 true 3.8 240 36 2 disqualified 880   940 12000 0 true .16 20 1.9 2 true 9.5 400 91 2 true 8.6 360 68 2 true 11   470 88 2 unknown 740   710 7400 0 error (1) 6.6 150 69 0 true 7.6 130 91 2
loop-new/count_by_1_true-unreach-call_true-termination.i true .22  23 2.1  2 true 90     2900   1000    2 true 90     3400   990    2 true 350   1800 5100 2 unknown .79 66 8.8 0 true 83    650 770   2 true 84    650 910   2 timeout 900     15000 12000    0 unknown .76 39 9.1 0 true 13 1100 96 2 true 170    3700 2500   2 true 3.9 210 37 2 disqualified 2.0 70 23 0 true .14 16 1.5 2 true 9.0 390 69 2 timeout 900   4800 8500 0 true 9.7 400 74 2 true 14   460 110 2 timeout 900   150 12000 0 true 4.6 130 62 2
loop-new/count_by_1_variant_true-unreach-call_true-termination.i true .21  23 1.8  2 true 260     15000   3000    1 witness invalid (true) 220     8100   2500    0 true 350   1800 4500 2 unknown .79 66 8.2 0 true 94    650 920   2 true 94    650 950   2 true .088 26 .82 2 timeout 900    75 9900   0 true 13 1100 82 2 true 220    7400 2600   2 true 3.5 220 36 2 disqualified 47   170 700 0 true 3.6  360 47   2 true 9.4 380 82 2 true 8.9 370 73 2 true 10   380 80 2 true 18   450 150 2 timeout 900   150 10000 0 true 61   330 1000 2
loop-new/count_by_2_true-unreach-call_true-termination.i timeout 900     1200 14000    0 true 44     1400   530    1 true 46     1700   530    1 timeout 970   8700 10000 0 unknown 39    44 500   0 true 45    480 450   1 true 46    480 530   1 timeout 900     15000 11000    0 timeout 900    76 6900   0 timeout 970 11000 8700 0 true 87    1900 1000   1 true 3.3 210 36 1 disqualified 2.0 70 25 0 true .14 16 1.3 1 timeout 900   1400 13000 0 timeout 900   4800 8900 0 timeout 900   1100 13000 0 true 140   1300 1400 2 timeout 900   150 11000 0 true 4.5 130 60 1
loop-new/count_by_k_true-unreach-call_true-termination.i timeout 900     1200 11000    0 error (42) 880     6000   4300    0 error (42) 880     140   11000    0 timeout 970   5100 8800 0 unknown 170    60 2400   0 unknown 8.4  430 120   0 timeout 900    480 9600   0 timeout 900     260 14000    0 timeout 900    1700 9500   0 timeout 960 6700 9200 0 timeout 900    8700 6600   0 unknown 220   890 2300 0 disqualified 820   320 12000 0 timeout (verification) 900    18 10000   0 timeout 900   960 9800 0 timeout 900   4200 11000 0 timeout 900   960 9600 0 true 120   1100 1500 1 timeout 900   150 13000 0 true 9.0 180 110 1
loop-new/count_by_nondet_true-unreach-call_true-termination.i timeout 900     2000 10000    0 error (42) 880     1300   9700    0 error (42) 880     170   12000    0 timeout 960   6900 9700 0 unknown 200    81 2900   0 unknown 8.3  430 120   0 timeout 900    510 8700   0 timeout 900     3200 11000    0 timeout 900    4100 11000   0 timeout 970 5000 10000 0 timeout 900    4900 12000   0 unknown 430   1400 3300 0 disqualified 69   220 1100 0 timeout (verification) 900    75 9500   0 timeout 900   2700 11000 0 timeout 900   4200 9400 0 timeout 900   1500 12000 0 timeout 900   1200 9800 0 timeout 900   150 11000 0 true 160   270 2000 1
loop-new/gauss_sum_true-unreach-call_true-termination.i timeout 900     1500 13000    0 true 21     110   250    1 error (42) 880     110   12000    0 true 260   2900 2900 2 unknown 130    77 1900   0 unknown 8.2  430 100   0 timeout 900    480 9500   0 true 540     1000 7200    1 timeout 900    2200 12000   0 true 57 2300 490 2 true 42    15000 580   1 true 15   560 150 1 disqualified 880   270 12000 0 true .51 22 7.3 1 timeout 900   800 14000 0 timeout 900   1300 10000 0 true 16   440 160 1 true 33   200 380 1 timeout 900   150 13000 0 true 7.9 180 91 1
loop-new/half_true-unreach-call_true-termination.i timeout 900     1700 10000    0 error (42) 880     4900   4600    0 error (42) 880     110   12000    0 timeout 950   5800 8800 0 unknown 87    65 1100   0 unknown 8.3  430 100   0 timeout 900    560 9100   0 timeout 900     1600 12000    0 timeout 900    620 8700   0 timeout 960 7800 10000 0 timeout 900    360 5900   0 unknown 69   1200 870 0 disqualified 880   230 11000 0 timeout (verification) 900    1600 12000   0 true 13   560 110 2 timeout 900   940 6700 0 true 22   510 220 2 unknown 590   1200 6700 0 timeout 900   150 11000 0 true 200   150 2500 2
loop-new/nested_true-unreach-call_true-termination.i timeout 900     2400 5900    0 error (42) 880     3800   5400    0 error (42) 870     11000   10000    0 timeout 960   5600 9800 0 unknown 900    410 12000   0 unknown 8.4  430 110   0 timeout 900    960 8600   0 timeout 900     570 14000    0 timeout 900    3000 11000   0 timeout 970 5500 10000 0 timeout 900    10000 9800   0 true 6.8 320 65 2 disqualified 880   460 12000 0 true .35 20 5.8 2 true 160   4700 2000 2 true 380   1600 3400 2 true 190   4800 2100 2 timeout 900   720 8100 0 timeout 900   150 10000 0 true 110   160 1400 2
loop-new/gauss_sum_true-unreach-call.i.p+cfa-reducer.c timeout 900     1400 12000    0 true 25     120   310    1 error (42) 880     120   11000    0 true 310   3500 3300 1 unknown 130    77 1900   0 unknown 8.1  430 100   0 timeout 900    480 8900   0 true 540     1000 7700    1 timeout 900    2200 11000   0 true 110 2600 830 1 true 44    15000 540   1 true 17   660 200 1 disqualified 880   490 11000 0 true .53 22 6.4 1 timeout 900   710 11000 0 timeout 900   2100 7800 0 true 21   500 220 1 true 400   1800 4400 1 timeout 900   150 11000 0 true 13   190 160 1
loop-new/gauss_sum_true-unreach-call.i.p+lhb-reducer.c timeout 900     1400 13000    0 true 31     120   370    1 error (42) 870     120   12000    0 true 310   3300 3100 2 unknown 130    76 1700   0 unknown 8.6  430 100   0 timeout 900    480 9100   0 true .097 26 1.1  1 timeout 900    2200 9900   0 true 100 2900 880 2 true 44    15000 730   1 true 18   590 180 1 disqualified 880   490 10000 0 true 1.5  24 19   1 timeout 900   940 9000 0 timeout 900   810 8700 0 true 20   470 250 1 true 400   1600 4500 1 timeout 900   150 11000 0 true 49   180 680 1
loop-new/gauss_sum_true-unreach-call.i.v+cfa-reducer.c timeout 900     1400 11000    0 true 25     120   340    1 error (42) 870     120   11000    0 true 310   3100 3200 1 unknown 130    77 1600   0 unknown 8.3  430 100   0 timeout 900    480 8800   0 true 540     1000 6500    1 timeout 900    2200 10000   0 true 110 2500 910 1 true 44    15000 570   1 true 18   660 190 1 disqualified 880   500 12000 0 true .51 21 6.1 1 timeout 900   710 10000 0 timeout 900   1000 7200 0 true 15   490 150 1 true 350   1400 4200 1 timeout 900   150 13000 0 true 13   190 150 1
loop-industry-pattern/aiob_1_true-unreach-call.c true .70  42 8.7  2 true 2.1   49   24    2 witness invalid (true) 2.3   51   34    0 true 46   1400 410 2 unknown .93 67 9.6 0 true 8.2  370 100   2 true 8.3  370 100   2 true .18  27 2.5  2 timeout 900    86 9000   0 true 53 2100 430 2 error (8) 1.1  70 9.6 0 unknown 8.6 280 82 0 disqualified 880   420 10000 0 true .17 18 2.5 2 error (7) 11   330 88 0 error (7) 11   330 81 0 error (7) 11   330 99 0 true 89   1100 700 2 timeout 900   160 11000 0 unknown 2.4 130 31 0
loop-industry-pattern/aiob_2_true-unreach-call.c true .71  42 7.4  2 true 2.0   49   30    2 witness invalid (true) 2.3   51   29    0 true 42   1300 410 2 unknown .92 66 10   0 true 8.3  370 98   2 true 8.5  370 110   2 true .15  28 1.7  2 timeout 900    86 9000   0 true 49 1700 440 2 error (8) 1.1  70 9.3 0 unknown 9.3 280 96 0 disqualified 880   460 9200 0 true .18 18 2.3 2 error (7) 11   320 92 0 error (7) 12   300 91 0 error (7) 11   340 85 0 true 88   1300 630 2 timeout 900   210 11000 0 unknown 2.4 130 34 0
loop-industry-pattern/aiob_3_true-unreach-call.c true .72  42 9.0  2 true 2.1   49   28    2 witness invalid (true) 2.3   51   30    0 true 45   1500 410 2 unknown .88 65 10   0 true 8.1  370 130   2 true 8.2  370 100   2 true .15  27 2.1  2 timeout 900    85 9900   0 true 49 1700 370 2 error (8) 1.1  70 10   0 unknown 8.8 280 77 0 disqualified 880   400 11000 0 true .19 18 2.8 2 error (7) 11   330 95 0 error (7) 11   310 81 0 error (7) 12   330 92 0 true 89   1300 640 2 timeout 900   160 11000 0 unknown 2.4 130 36 0
loop-industry-pattern/aiob_4_true-unreach-call.c true .51  34 5.9  2 true .92  11   11    2 witness invalid (true) 1.0   14   11    0 true 40   1300 330 2 unknown .88 66 9.7 0 true 8.2  370 100   2 true 8.3  370 110   2 true .15  27 1.9  2 timeout 900    85 12000   0 true 48 1600 400 2 error (8) 1.1  70 9.2 0 unknown 7.2 220 68 0 disqualified 880   470 10000 0 true .17 17 2.5 2 error (7) 11   330 87 0 error (7) 11   310 85 0 error (7) 11   330 81 0 true 85   1300 700 2 timeout 900   160 13000 0 unknown 2.4 130 35 0
loop-industry-pattern/aiob_4_true-unreach-call.c.v+cfa-reducer.c error (6) .28  31 2.4  0 true 1.2   12   17    2 witness invalid (true) 1.3   14   17    0 true 47   1600 440 2 unknown 77    120 900   0 true 8.1  370 110   2 true 8.2  370 98   2 true 1.8   89 23    2 timeout 900    85 9900   0 true 56 2100 400 2 error (8) 1.1  70 9.7 0 unknown 6.9 210 65 0 disqualified 25   160 330 0 true .14 16 1.6 2 timeout 910   14000 4400 0 true 490   1200 3500 2 true 19   650 170 2 true 99   1300 910 2 timeout 900   160 8900 0 unknown 2.4 130 31 0
loop-industry-pattern/aiob_4_true-unreach-call.c.v+lh-reducer.c true .76  47 7.7  2 true 1.2   12   15    2 witness invalid (true) 1.3   14   17    0 true 48   1600 420 2 unknown .92 67 9.3 0 true 8.0  370 99   2 true 8.1  370 90   2 true .15  28 1.8  2 timeout 900    85 8300   0 true 56 2300 480 2 error (8) 1.1  70 11   0 unknown 7.4 210 70 0 disqualified 25   160 380 0 true .14 16 1.6 2 true 16   580 140 2 true 230   1200 2200 2 true 18   540 160 2 true 95   1200 680 2 error (1) 870   160 11000 0 unknown 2.4 130 32 0
loop-industry-pattern/aiob_4_true-unreach-call.c.v+lhb-reducer.c true 2.0   160 22    2 true 1.7   13   21    2 witness invalid (true) 1.5   16   22    0 true 59   2300 530 2 unknown 1.0  67 11   0 true 8.1  370 110   2 true 8.3  370 100   2 true .25  32 2.8  2 timeout 900    85 10000   0 true 62 2000 530 2 error (8) 1.2  74 13   0 unknown 8.3 270 72 0 disqualified 24   160 330 0 true .16 16 1.7 2 true 24   570 210 2 true 170   1200 1500 2 true 35   840 310 2 true 110   1300 840 2 error (1) 870   200 13000 0 unknown 2.4 130 40 0
loop-industry-pattern/aiob_4_true-unreach-call.c.v+nlh-reducer.c true 4.6   1200 50    2 true .81  42   11    2 witness invalid (true) .80  56   11    0 true 6.4 310 54 2 unknown 2.1  67 27   0 true 8.2  370 110   2 true 8.0  370 100   2 true .81  78 11    2 timeout 900    85 8200   0 true 26 1600 200 2 error (8) 1.4  100 11   0 unknown 7.2 220 65 0 disqualified 3.8 160 48 0 true .20 16 2.7 2 true 36   840 330 2 true 34   870 270 2 true 31   720 270 2 true 71   1700 700 2 timeout 900   330 13000 0 unknown 2.4 130 35 0
loop-industry-pattern/mod3_true-unreach-call.c true .67  24 8.3  2 error (42) 870     350   9700    0 out of memory 220     15000   2900    0 true 17   310 210 2 unknown 900    69 13000   0 unknown 8.2  430 110   0 unknown 8.4  430 110   0 timeout 900     82 14000    0 timeout 900    4000 12000   0 true 16 1100 110 2 out of memory 630    15000 7700   0 unknown 640   2200 7400 0 disqualified 2.5 78 27 0 timeout (verification) 900    47 11000   0 true 9.2 370 70 2 true 9.2 360 71 2 true 9.3 350 84 2 true 29   450 300 2 error (1) 12   230 140 0 true 27   230 340 2
loop-industry-pattern/mod3_true-unreach-call.c.v+cfa-reducer.c error (6) .092 24 .87 0 error (42) 880     1600   6800    0 out of memory 200     15000   2700    0 true 17   300 190 2 out of memory 24    15000 310   0 unknown 8.2  430 130   0 unknown 8.3  430 96   0 out of memory 24     15000 290    0 timeout 900    4200 7500   0 true 23 1200 220 2 out of memory 630    15000 7500   0 unknown 450   1400 4700 0 disqualified 2.4 77 28 0 timeout (verification) 900    48 9300   0 true 7.6 340 58 2 true 11   370 87 2 true 7.7 350 64 2 unknown 770   740 8000 0 error (1) 880   190 12000 0 error (1) 4.6 130 57 0
loop-industry-pattern/mod3_true-unreach-call.c.v+lhb-reducer.c error (6) .094 24 1.6  0 error (42) 880     760   7900    0 out of memory 180     15000   2100    0 true 9.0 300 94 2 out of memory 46    15000 610   0 unknown 8.1  430 110   0 unknown 8.5  430 120   0 out of memory 64     15000 540    0 timeout 900    5300 7500   0 true 17 1100 130 2 out of memory 630    15000 8100   0 unknown 350   1900 3500 0 disqualified 880   200 11000 0 timeout (verification) 900    2600 8300   0 true 8.8 380 69 1 true 13   380 110 1 true 9.2 370 72 1 timeout 900   720 11000 0 error (1) 7.6 180 87 0 unknown 2.5 130 32 0
loop-industry-pattern/mod3_true-unreach-call.c.v+sep-reducer.c error (6) .088 25 .70 0 error (42) 880     420   9900    0 out of memory 180     15000   2100    0 true 9.2 300 110 2 out of memory 450    15000 4900   0 unknown 8.3  430 95   0 unknown 8.4  430 110   0 out of memory 500     15000 3200    0 timeout 900    4000 6900   0 true 15 1200 150 2 out of memory 630    15000 8400   0 unknown 390   2100 4900 0 disqualified 880   200 10000 0 timeout (verification) 900    2600 8000   0 true 10   390 87 1 true 14   340 130 1 true 9.0 350 84 1 timeout 900   630 8600 0 error (1) 880   180 13000 0 unknown 2.5 130 39 0
loop-industry-pattern/nested_true-unreach-call.c timeout 900     300 9000    0 out of memory 390     15000   4400    0 out of memory 120     15000   1600    0 timeout 960   6100 9200 0 unknown 900    960 12000   0 unknown 8.1  430 95   0 unknown 8.3  430 120   0 timeout 900     9800 11000    0 timeout 900    75 9000   0 timeout 960 4600 9000 0 out of memory 190    15000 2500   0 timeout 900   3200 8100 0 disqualified 880   390 12000 0 probably out of memory (killed (signal 9, verification)) 230    15000 3200   0 timeout 900   5800 11000 0 timeout 900   5200 11000 0 true 33   890 290 2 true 75   1600 680 2 error (1) 54   160 600 0 timeout 900   230 13000 0
loop-industry-pattern/ofuf_1_true-unreach-call.c error (134) .24  31 2.9  0 error (42) 880     800   8900    0 out of memory 230     15000   2800    0 true 58   2200 550 2 unknown 2.5  290 28   0 true 8.5  370 110   2 true 8.1  370 110   2 true .49  68 6.1  2 unknown .92 40 10   0 true 71 2300 740 2 error (8) .79 71 9.1 0 unknown 15   480 140 0 disqualified 9.0 200 95 0 timeout (verification) 900    55 9000   0 true 12   430 100 2 true 12   450 98 2 true 12   450 100 2 true 30   470 280 2 timeout 900   170 11000 0 unknown 2.4 130 35 0
loop-industry-pattern/ofuf_2_true-unreach-call.c error (134) .30  30 2.4  0 error (42) 880     770   7000    0 out of memory 250     15000   3100    0 true 59   2200 560 2 unknown 2.5  290 34   0 true 8.2  370 99   2 true 8.1  370 98   2 true .48  68 6.2  2 unknown .91 40 13   0 true 82 2600 700 2 error (8) .82 71 6.8 0 unknown 15   480 130 0 disqualified 8.2 220 90 0 timeout (verification) 900    57 13000   0 true 11   440 87 2 true 12   430 92 2 true 12   450 93 2 true 27   500 240 2 timeout 900   170 12000 0 unknown 2.4 130 33 0
loop-industry-pattern/ofuf_3_true-unreach-call.c error (134) .25  30 2.5  0 error (42) 880     1200   9200    0 out of memory 250     15000   2800    0 true 59   2200 540 2 unknown 2.5  290 34   0 true 8.4  370 100   2 true 8.3  370 100   2 true .49  68 6.5  2 unknown .90 40 11   0 true 80 2600 730 2 error (8) .81 71 7.2 0 unknown 15   480 130 0 disqualified 9.7 220 90 0 timeout (verification) 900    55 8600   0 true 10   390 82 2 true 12   430 79 2 true 12   450 95 2 true 27   500 220 2 timeout 900   170 12000 0 unknown 2.4 130 36 0
loop-industry-pattern/ofuf_4_true-unreach-call.c error (134) .24  30 3.2  0 error (42) 880     870   7900    0 out of memory 240     15000   3000    0 true 56   2100 560 2 unknown 2.4  290 25   0 true 8.1  370 92   2 true 8.2  370 95   2 true .44  47 5.3  2 unknown .91 40 11   0 true 73 2500 740 2 error (8) .80 71 7.0 0 unknown 15   480 110 0 disqualified 7.9 220 82 0 timeout (verification) 900    59 10000   0 true 11   430 89 2 true 11   460 88 2 true 12   470 100 2 true 27   500 240 2 timeout 900   170 11000 0 unknown 2.4 130 35 0
loop-industry-pattern/ofuf_5_true-unreach-call.c error (134) .26  30 2.3  0 error (42) 880     920   8600    0 out of memory 300     15000   4100    0 true 56   2000 560 2 unknown 2.4  290 24   0 true 8.3  370 95   2 true 8.3  370 110   2 true .43  47 5.5  2 unknown .89 40 13   0 true 69 2300 760 2 error (8) .77 71 9.9 0 unknown 14   480 130 0 disqualified 5.2 180 67 0 timeout (verification) 900    54 9800   0 true 11   430 90 2 true 12   460 90 2 true 12   460 93 2 true 28   510 250 2 timeout 900   170 12000 0 unknown 2.4 130 30 0
loops/heavy_true-unreach-call.c error (134) 28     15000 370    0 error (42) 870     14000   13000    0 error (42) 880     1500   11000    0 true 93   990 1300 2 unknown 65    4300 920   0 timeout 900    460 8500   0 timeout 900    460 9000   0 true 23     3900 290    2 timeout 900    81 9900   0 true 12 1000 81 2 timeout 900    14000 11000   0 true 3.9 250 39 2 disqualified 900   6400 11000 0 true .45 37 5.6 2 true 33   2900 230 2 timeout 900   5100 11000 0 timeout 900   9200 7000 0 true 110   6600 720 2 error (1) 11   760 120 0 unknown 2.4 130 39 0
loops/compact_false-unreach-call.c out of memory 390     15000 4600    0 out of memory 200     15000   2600    0 out of memory 620     15000   5100    0 timeout 960   3600 8700 0 unknown 170    130 2200   0 timeout 900    1500 8200   0 out of memory (unknown error) 97    15000 860   0 timeout 900     12000 12000    0 unknown 7.0  5700 85   0 timeout 960 6700 6900 0 out of memory 150    15000 1400   0 unknown 170   850 1200 0 disqualified 890   1300 12000 0 timeout (verification) 900    310 11000   0 timeout 900   1400 12000 0 timeout 900   1600 7800 0 timeout 900   4500 7100 0 false(unreach-call) 15   190 100 0 false(unreach-call) 4.0 150 46 0 unknown 2.4 130 32 0
loops/heavy_false-unreach-call.c error (134) 28     15000 360    0 out of memory 250     15000   3800    0 error (42) 880     15000   11000    0 timeout 960   6500 9900 0 unknown 900    4100 9800   0 timeout 900    460 9300   0 timeout 900    460 9000   0 timeout 900     4400 11000    0 timeout 900    81 11000   0 timeout 960 5900 7800 0 timeout 900    14000 12000   0 unknown 9.7 290 100 0 disqualified 900   6400 12000 0 probably out of memory (killed (signal 9, cex-confirmation)) 470    15000 6900   0 timeout 900   6200 11000 0 timeout 900   5100 11000 0 timeout 900   9600 8300 0 false(unreach-call) 220   5500 2600 0 error (1) 11   760 130 0 unknown 2.4 130 30 0
loops-crafted-1/Mono1_false-unreach-call1.c timeout 900     1500 13000    0 out of memory 270     15000   4000    0 out of memory 210     15000   3000    0 timeout 920   2100 11000 0 unknown 61    52 880   0 timeout 900    3500 8800   0 timeout 900    3500 9800   0 timeout 900     9000 10000    0 false(unreach-call) 1.6  82 20   1 timeout 910 4200 10000 0 out of memory 530    15000 7200   0 unknown 240   1200 2200 0 disqualified 880   380 11000 0 probably out of memory (killed (signal 9, cex-confirmation)) 170    15000 2500   0 timeout 900   580 13000 0 timeout 900   5500 11000 0 timeout 900   670 11000 0 false(unreach-call) 370   11000 5800 1 false(unreach-call) 3.8 150 38 1 false(unreach-call) 5.9 130 82 1
loops-crafted-1/Mono3_false-unreach-call1.c timeout 900     1400 13000    0 out of memory 480     15000   6400    0 out of memory 590     15000   8100    0 timeout 920   10000 8700 0 unknown 88    58 1100   0 false(unreach-call) 300    5400 3500   1 false(unreach-call) 290    5400 3600   1 timeout 900     9700 12000    0 false(unreach-call) .46 83 5.6 1 timeout 930 11000 10000 0 timeout 900    12000 10000   0 unknown 220   1200 2100 0 disqualified 3.2 110 44 0 false(unreach-call) 5.6  820 78   1 timeout 900   680 10000 0 timeout 900   1100 12000 0 timeout 900   700 10000 0 false(unreach-call) 640   11000 7500 1 false(unreach-call) 3.5 150 34 1 false(unreach-call) 5.8 130 93 1
loops-crafted-1/Mono4_false-unreach-call1.c timeout 900     1600 12000    0 false(unreach-call) 410     13000   4900    0 out of memory 430     15000   6100    0 timeout 970   6900 8300 0 unknown 68    58 810   0 false(unreach-call) 290    5400 4000   1 false(unreach-call) 290    5400 3800   1 timeout 900     8800 11000    0 false(unreach-call) .50 83 6.6 1 timeout 960 6700 7700 0 timeout 900    13000 13000   0 unknown 210   1300 2600 0 disqualified 880   560 11000 0 false(unreach-call) 5.7  820 90   1 timeout 900   1400 13000 0 timeout 900   5400 9700 0 timeout 900   1300 14000 0 false(unreach-call) 620   9200 7600 1 false(unreach-call) 3.4 150 28 1 false(unreach-call) 5.8 130 73 1
loops-crafted-1/Mono5_false-unreach-call1.c timeout 900     1700 12000    0 out of memory 320     15000   3900    0 out of memory 230     15000   3800    0 timeout 920   3800 8200 0 unknown 80    61 1100   0 timeout 900    5400 10000   0 timeout 900    5400 8800   0 timeout 900     8800 14000    0 false(unreach-call) .71 82 8.6 1 timeout 920 4600 7800 0 out of memory 740    15000 8500   0 unknown 220   1200 2300 0 disqualified 13   540 190 0 false(unreach-call) 54    8100 760   1 timeout 900   730 11000 0 timeout 900   870 6600 0 timeout 900   750 11000 0 false(unreach-call) 370   9600 4900 1 false(unreach-call) 3.6 150 34 1 false(unreach-call) 64   11000 870 1
loops-crafted-1/Mono6_false-unreach-call1.c timeout 900     1700 10000    0 out of memory 310     15000   4200    0 out of memory 230     15000   3100    0 timeout 920   6100 9300 0 unknown 66    57 850   0 timeout 900    5600 9600   0 timeout 900    5600 8900   0 timeout 900     8800 10000    0 false(unreach-call) .81 81 9.7 1 timeout 930 6300 9300 0 out of memory 730    15000 8600   0 unknown 220   1400 2100 0 disqualified 13   480 160 0 false(unreach-call) 56    8100 910   1 timeout 900   610 14000 0 timeout 900   1200 12000 0 timeout 900   920 9400 0 false(unreach-call) 380   9700 4800 1 false(unreach-call) 3.4 150 34 1 false(unreach-call) 63   11000 840 1
loops-crafted-1/nested3_false-unreach-call.c timeout 900     3700 4900    0 out of memory 310     15000   4800    0 out of memory 230     15000   2900    0 timeout 920   6500 8400 0 unknown 900    920 11000   0 timeout 900    4300 9900   0 timeout 900    4300 8800   0 timeout 900     14000 11000    0 false(unreach-call) 5.7  83 64   1 timeout 930 5700 7800 0 out of memory 760    15000 9000   0 false(unreach-call) 4.6 270 47 1 disqualified 880   280 12000 0 false(unreach-call) .17 16 1.7 1 timeout 900   590 12000 0 timeout 900   810 9900 0 timeout 900   640 12000 0 false(unreach-call) 220   2500 2600 1 false(unreach-call) 4.6 150 47 1 unknown 65   170 850 0
loops-crafted-1/nested5_false-unreach-call.c out of memory 460     15000 2600    0 out of memory 650     15000   6600    0 out of memory 710     15000   7700    0 timeout 960   6800 9000 0 unknown 900    1200 12000   0 timeout 900    4600 8900   0 timeout 900    4600 9100   0 timeout 900     14000 12000    0 false(unreach-call) 9.4  83 140   1 timeout 970 7000 9100 0 out of memory 730    15000 9300   0 false(unreach-call) 5.3 270 44 1 disqualified 880   550 9900 0 false(unreach-call) .17 16 2.1 1 timeout 900   580 12000 0 timeout 900   790 10000 0 timeout 900   790 10000 0 false(unreach-call) 220   2000 2700 1 false(unreach-call) 4.8 150 47 1 unknown 190   310 2200 0
loops-crafted-1/Mono1_true-unreach-call1.c timeout 900     1400 12000    0 out of memory 270     15000   4300    0 out of memory 210     15000   2600    0 timeout 910   2100 9100 0 unknown 62    52 890   0 timeout 900    3400 8900   0 timeout 900    3500 9100   0 timeout 900     9000 11000    0 timeout 900    75 10000   0 timeout 910 4200 10000 0 out of memory 530    15000 7500   0 unknown 240   1000 2300 0 disqualified 880   360 11000 0 true 110    8200 1500   1 timeout 900   580 11000 0 timeout 900   2700 9300 0 timeout 900   670 11000 0 true 270   11000 3100 1 timeout 900   150 11000 0 unknown 160   280 2000 0
loops-crafted-1/nested3_true-unreach-call.c timeout 900     5600 4100    0 out of memory 310     15000   4400    0 out of memory 230     15000   3500    0 true 350   1700 4100 2 unknown 900    920 14000   0 timeout 900    4100 9300   0 timeout 900    4100 9300   0 timeout 900     14000 13000    0 timeout 900    75 9700   0 true 14 1100 96 2 out of memory 770    15000 9500   0 unknown 190   1000 1600 0 disqualified 880   340 12000 0 probably out of memory (killed (signal 9, verification)) 170    15000 2700   0 timeout 900   1000 10000 0 timeout 900   1000 12000 0 timeout 900   1300 10000 0 true 52   680 520 2 error (1) 53   150 620 0 true 16   150 220 1
loops-crafted-1/nested5_true-unreach-call.c out of memory 160     15000 1500    0 error (42) 870     12000   11000    0 error (42) 880     15000   10000    0 true 93   1000 1300 2 unknown 900    1200 12000   0 timeout 900    4000 9100   0 timeout 900    4000 8800   0 timeout 900     11000 9500    0 timeout 900    75 10000   0 true 14 1100 100 2 out of memory 700    15000 9800   0 true 4.1 220 40 2 disqualified 890   750 11000 0 probably out of memory (killed (signal 9, verification)) 170    15000 2400   0 true 26   430 310 2 true 12   490 97 2 true 18   500 210 2 true 28   480 280 2 error (1) 53   150 620 0 true 17   190 230 2
loop-invariants/bin-suffix-5_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c timeout 900     1600 13000    0 error (42) 880     5000   3700    0 error (42) 870     330   5500    0 timeout 940   12000 11000 0 unknown 25    38 330   0 timeout 900    850 8100   0 timeout 900    840 9800   0 timeout 900     2200 11000    0 timeout 900    4300 7500   0 timeout (exception) 910 12000 9300 0 timeout 900    630 12000   0 unknown 47   1000 450 0 disqualified 900   300 12000 0 timeout (verification) 900    62 9000   0 true 14   360 110 2 timeout 900   840 7600 0 true 13   340 100 2 true 13   440 100 2 error (1) 860   190 12000 0 true 4.7 130 55 2
loop-invariants/const_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c timeout 900     1400 12000    0 error (42) 880     4700   7300    0 out of memory 160     15000   2100    0 true 2.8 250 24 2 unknown 42    48 540   0 true 8.3  370 110   2 true 8.3  370 96   2 timeout 900     1500 11000    0 timeout 900    4000 7000   0 true 13 1000 85 2 timeout 900    620 13000   0 true 4.2 220 40 2 disqualified 900   270 10000 0 timeout (verification) 900    2900 11000   0 true 8.7 380 62 2 true 9.1 370 77 2 true 8.2 370 59 2 true 13   470 120 2 error (1) 860   180 10000 0 true 110   200 1300 2
loop-invariants/eq1_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c timeout 900     360 11000    0 error (42) 880     67   11000    0 out of memory 270     15000   3400    0 true 4.2 280 44 2 unknown 150    93 1800   0 unknown 8.1  430 110   0 timeout 900    410 7000   0 timeout 900     2500 10000    0 timeout 900    4400 7800   0 true 14 1100 87 2 timeout 900    490 5900   0 true 290   1000 3100 2 disqualified 880   150 12000 0 timeout (verification) 900    2900 9700   0 true 7.8 350 69 2 true 7.6 350 57 2 true 8.3 370 64 2 true 14   470 120 2 error (1) 860   190 10000 0 true 57   210 700 2
loop-invariants/eq2_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c timeout 900     350 9600    0 error (42) 880     280   11000    0 error (42) 870     240   9500    0 true 4.0 280 37 2 unknown 27    38 340   0 unknown 8.1  430 94   0 timeout 900    400 9800   0 timeout 900     1900 10000    0 timeout 900    4800 6800   0 timeout 950 11000 8800 0 timeout 900    500 4600   0 true 4.1 220 37 2 disqualified 880   390 11000 0 true .15 16 1.7 2 true 8.1 340 61 2 true 8.6 370 60 2 true 7.6 340 54 2 true 14   470 130 2 error (1) 860   190 12000 0 true 4.7 130 64 2
loop-invariants/even_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c timeout 900     1500 11000    0 error (42) 880     5000   3300    0 error (42) 880     330   7600    0 timeout 940   12000 9900 0 unknown 25    38 390   0 timeout 900    840 9600   0 timeout 900    840 8300   0 timeout 900     2100 11000    0 timeout 900    4800 7300   0 timeout 960 8600 9700 0 timeout 900    630 12000   0 true 3.7 220 37 2 disqualified 880   300 11000 0 true .15 16 1.8 2 true 7.4 350 66 2 true 8.2 380 66 2 true 8.6 360 64 2 true 140   1400 1400 2 error (1) 860   190 11000 0 true 4.5 130 59 2
loop-invariants/mod4_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c timeout 900     1600 13000    0 error (42) 880     5000   3600    0 error (42) 880     320   5800    0 timeout 960   12000 11000 0 unknown 25    38 300   0 timeout 900    850 8800   0 timeout 900    840 8900   0 timeout 900     2100 11000    0 timeout 900    4600 7000   0 timeout 970 9100 11000 0 timeout 900    630 15000   0 true 4.0 220 40 2 disqualified 880   310 12000 0 true .17 16 1.9 2 true 8.4 380 71 2 true 8.4 350 68 2 true 7.7 350 62 2 true 140   1400 1600 2 error (1) 860   190 12000 0 true 4.5 130 60 2
loop-invariants/odd_true-unreach-call_true-valid-memsafety_true-no-overflow_false-termination.c timeout 900     1500 11000    0 error (42) 880     4800   3600    0 error (42) 880     330   6900    0 timeout 950   12000 9700 0 unknown 25    38 280   0 timeout 900    840 10000   0 timeout 900    830 8100   0 timeout 900     2100 12000    0 timeout 900    4400 6900   0 timeout 960 8400 9700 0 timeout 900    630 14000   0 unknown 220   1100 1500 0 disqualified 880   300 11000 0 timeout (verification) 900    62 10000   0 true 9.6 360 95 2 timeout 900   1100 11000 0 true 11   400 100 2 true 140   1400 1500 1 error (1) 860   190 11000 0 true 4.6 130 58 2
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score 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 208 70000 430000 770000 140 208 76000 810000 760000 136 208 71000 1300000 850000 65 208 74000 610000 750000 226 208 37000   180000 470000 38 208 29000 180000 300000 85 208 86000 200000 840000 123 208 86000     610000 1100000   130 208 110000   270000 1200000 -79 208 70000 710000 680000 224 208 81000 1300000 750000 95 208 19000 170000 180000 190 208 95000 99000 1200000 0 208 63000   370000 710000 180 208 55000 160000 670000 212 208 69000 230000 710000 224 208 51000 160000 630000 222 208 38000 310000 400000 275 208 120000   76000 1600000 48 208 18000 250000 220000 178
    correct results 86 500 20000 3500 138 83 1200 13000 12000 124 49 150 9400 1700 61 129 7000 100000 83000 218 38 86   2100 1100 38 46 1100 28000 14000 80 73 2200 39000 25000 118 97 1700     13000 22000   153 44 1300   12000 16000 46 126 4800 190000 42000 212 54 570 50000 7300 84 105 1600 44000 18000 175 0 106 180   20000 2600 165 135 3700 70000 40000 235 128 4700 69000 47000 220 138 3700 71000 40000 242 150 12000 180000 130000 251 48 200   7700 2100 48 90 3500 40000 45000 152
        correct true 52 100 7800 1300 104 41 1200 7900 12000 82 12 97 4500 1100 24 89 6400 84000 76000 178 0 34 440 13000 5000 68 45 1300 17000 14000 90 56 1500     9300 20000   112 2 400   4400 5100 4 86 3700 140000 32000 172 30 530 47000 6800 60 70 1400 33000 16000 140 0 59 51   1700 690 118 100 2000 54000 20000 200 92 4100 52000 41000 184 104 2500 55000 27000 208 101 6200 79000 61000 202 0 62 3200 12000 40000 124
        correct false 34 400 12000 2200 34 42 70 4800 930 42 37 53 4900 660 37 40 650 20000 6700 40 38 86   2100 1100 38 12 670 15000 8500 12 28 870 22000 11000 28 41 150     3500 2000   41 42 910   7400 10000 42 40 1100 53000 9700 40 24 39 3300 490 24 35 250 11000 2400 35 0 47 130   19000 2000 47 35 1700 16000 20000 35 36 660 16000 6400 36 34 1200 16000 13000 34 49 6000 98000 72000 49 48 200   7700 2100 48 28 310 28000 4200 28
    correct-unconfimed results 3 380 2600 2300 2 14 890 35000 11000 12 6 170 5200 1800 4 9 940 14000 9900 8 1 6.3 38 79 0 5 82 2200 880 5 9 130 4000 1500 5 10 1700     4300 23000   9 3 9.9 8900 120 3 12 1400 30000 13000 12 11 310 74000 4100 11 15 290 9400 3300 15 0 18 480   8600 5900 15 9 430 5600 4800 9 4 800 2300 9200 4 12 260 6200 2800 12 32 5400 61000 58000 24 2 8.4 300 96 0 34 1000 7000 12000 26
        correct-unconfirmed true 2 14 850 140 2 12 470 21000 5500 12 4 140 4600 1400 4 8 710 10000 7300 8 0 5 82 2200 880 5 5 83 2200 980 5 9 1700     4300 23000   9 3 9.9 8900 120 3 12 1400 30000 13000 12 11 310 74000 4100 11 15 290 9400 3300 15 0 15 470   8500 5800 15 9 430 5600 4800 9 4 800 2300 9200 4 12 260 6200 2800 12 24 4100 41000 43000 24 0 26 950 5300 12000 26
        correct-unconfirmed false 1 370 1800 2200 0 2 430 14000 5100 0 2 33 620 330 0 1 230 3600 2600 0 1 6.3 38 79 0 0 4 47 1700 560 0 1 .38  26 6.4 0 0 0 0 0 0 3 7.5 58 110 0 0 0 0 8 1400 20000 15000 0 2 8.4 300 96 0 8 63 1700 860 0
    incorrect results 0 0 0 0 0 0 0 1 .081 26 1.1 -32 4 110   9000 1400 -128 0 0 0 0 0 1 40 860 340 -32 0 1 44 910 360 -32 0 0 0
        incorrect true 0 0 0 0 0 0 0 1 .081 26 1.1 -32 4 110   9000 1400 -128 0 0 0 0 0 1 40 860 340 -32 0 1 44 910 360 -32 0 0 0
        incorrect false 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
score (208 tasks, max score: 357) 140 136 65 226 38 85 123 130 -79 224 95 190 0 180 212 224 222 275 48 178
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