Tool 2LS 0.5.0 AProVE CBMC 5.6 Ceagle Ceagle 1.3 @ 53cfa89 CPAchecker 1.6.1-svn 23987 CPAchecker 1.6.1-svn 24048 DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 ESBMC ESBMC version 3.1 64-bit x86_64 linux HipTNT+ SMACK+Corral 1.7.2 symbiotic KLEE:7f3c74aa-dg:96e851cf-symbiotic:69a1d8e6-minisat:3db58943-stp:39fa956f-LLVMInstrumentation:f750b24a ULTIMATE Automizer f7c3ed31 ULTIMATE Kojak f7c3ed31 ULTIMATE Taipan f7c3ed31
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic Linux 4.4.0-57-generic Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-11 11:55:43 CET 2017-01-10 17:21:21 CET 2017-01-11 15:45:28 CET 2017-01-11 11:02:44 CET 2017-01-11 11:04:11 CET 2017-01-11 12:57:03 CET 2017-01-13 09:38:46 CET 2017-01-13 10:06:48 CET 2017-01-13 09:48:46 CET 2017-01-13 09:50:10 CET 2017-01-13 10:37:20 CET 2017-01-13 11:03:47 CET 2017-01-13 10:46:53 CET 2017-01-14 08:07:14 CET 2017-01-14 16:40:33 CET 2017-01-14 08:15:08 CET 2017-01-14 08:14:11 CET 2017-01-14 17:36:57 CET
Run set 2ls.sv-comp17.Termination-Other aprove.sv-comp17.Termination-Other cbmc.sv-comp17.Termination-Other ceagle.sv-comp17.Termination-Other cpa-bam-bnb.sv-comp17.Termination-Other cpa-kind.sv-comp17.Termination-Other cpa-seq.sv-comp17.Termination-Other depthk.sv-comp17.Termination-Other esbmc.sv-comp17.Termination-Other esbmc-falsi.sv-comp17.Termination-Other esbmc-incr.sv-comp17.Termination-Other esbmc-kind.sv-comp17.Termination-Other hiptnt.sv-comp17.Termination-Other smack.sv-comp17.Termination-Other symbiotic4.sv-comp17.Termination-Other uautomizer.sv-comp17.Termination-Other ukojak.sv-comp17.Termination-Other utaipan.sv-comp17.Termination-Other
Options --graphml-witness witness.graphml --graphml-witness witness.graphml --compiler clang-3.7 -sv-comp17-bam-bnb -disable-java-assertions -heap 10000m -sv-comp17-k-induction -heap 10000M -disable-java-assertions -sv-comp17 -heap 10000M -disable-java-assertions -s fixed -s falsi -s incr -s kinduction -w error-witness.graphml --witness witness.graphml
../../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
pthread-atomic/gcd_true-unreach-call_true-termination.i error (5) .21  27 1.7  0 error (1) 7.2 680 51 0 error (42) .012  1.2  .042 0 unknown .010  .92 .016  0 error (1) .42 38 3.6 0 error (1) .43 40 3.9 0 error 3.0 280 23 0 unknown 890    280 12000   0 error (1) .022 5.0 .085 0 error (1) .018 4.8 .18  0 error (1) .019 4.8 .16  0 error (1) .020 4.8 .13  0 unknown .054 13 .45 0 error (1) .041 7.2 .35 0 unknown .060 7.2 .56 0 unknown 5.3 310 38 0 error (1) .050 5.3 .14 0 error (1) .050 5.3 .19 0
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 1.2   360 14    2 timeout 900   3700 11000 0 error (42) .014  .98 .046 0 unknown .0088 1.0  .023  0 error (1) .47 37 3.8 0 error (1) .42 40 3.7 0 true 6.5 380 55 2 unknown 2.1  61 24   0 error (1) .021 4.7 .089 0 error (1) .020 4.7 .17  0 error (1) .047 4.9 .14  0 error (1) .021 4.7 .15  0 unknown .072 13 .84 0 error (1) .067 7.1 .30 0 unknown .089 7.3 .60 0 true 13   520 92 2 error (1) .054 5.4 .16 0 error (1) .026 5.5 .17 0
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 1.3   360 12    2 timeout 900   3700 12000 0 error (42) .016  1.4  .042 0 unknown .0044 .97 .017  0 error (1) .39 37 3.7 0 error (1) .41 37 3.9 0 true 6.2 380 48 2 unknown 8.0  150 100   0 error (1) .043 4.8 .12  0 error (1) .021 4.7 .11  0 error (1) .046 4.9 .12  0 error (1) .020 4.8 .12  0 unknown .092 14 .85 0 error (1) .069 7.4 .32 0 unknown .087 7.2 .54 0 true 13   520 100 2 error (1) .033 5.2 .20 0 error (1) .026 5.4 .15 0
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .52  96 5.4  2 timeout 900   3700 12000 0 error (42) .014  1.2  .047 0 unknown .010  .93 .016  0 error (1) .42 40 4.0 0 error (1) .39 37 4.3 0 true 23   770 190 2 unknown 3.4  58 46   0 error (1) .042 4.8 .15  0 error (1) .022 4.8 .13  0 error (1) .018 4.9 .16  0 error (1) .020 4.7 .13  0 unknown .089 13 .51 0 error (1) .063 7.2 .33 0 unknown .056 7.2 .52 0 true 9.4 500 67 2 error (1) .040 5.4 .13 0 error (1) .026 5.3 .23 0
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true .40  61 4.1  2 timeout 900   3500 11000 0 error (42) .019  1.1  .042 0 unknown .0042 1.0  .018  0 error (1) .43 37 4.0 0 error (1) .44 38 4.2 0 true 5.6 300 44 2 unknown 1.2  57 16   0 error (1) .031 4.8 .10  0 error (1) .044 4.8 .10  0 error (1) .044 4.8 .13  0 error (1) .038 4.8 .11  0 unknown .093 13 .50 0 error (1) .067 7.4 .35 0 unknown .055 7.2 .59 0 true 11   500 87 2 error (1) .026 5.5 .16 0 error (1) .054 5.3 .15 0
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .37  61 3.5  2 timeout 900   3700 11000 0 error (42) .012  1.2  .034 0 unknown .010  .95 .029  0 error (1) .46 40 3.7 0 error (1) .42 40 3.9 0 true 5.7 300 46 2 unknown 2.8  56 35   0 error (1) .018 4.7 .078 0 error (1) .030 4.8 .12  0 error (1) .019 4.8 .12  0 error (1) .041 4.8 .14  0 unknown .062 14 .70 0 error (1) .051 7.1 .46 0 unknown .057 7.2 .60 0 true 10   480 82 2 error (1) .023 5.4 .22 0 error (1) .047 5.3 .18 0
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true .53  120 5.0  2 timeout 900   3500 11000 0 error (42) .021  1.1  .043 0 unknown .011  1.1  .026  0 error (1) .45 38 3.8 0 error (1) .39 38 3.3 0 true 6.3 340 50 2 unknown 1.5  56 19   0 error (1) .030 4.8 .11  0 error (1) .044 4.8 .13  0 error (1) .044 4.8 .12  0 error (1) .044 4.7 .11  0 unknown .097 13 .54 0 error (1) .065 7.3 .30 0 unknown .086 7.3 .56 0 true 23   580 230 2 error (1) .051 5.5 .15 0 error (1) .056 5.4 .16 0
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .52  120 5.5  2 timeout 900   3700 13000 0 error (42) .022  1.2  .069 0 unknown .0081 .92 .021  0 error (1) .41 40 3.4 0 error (1) .42 38 3.7 0 true 6.1 340 48 2 unknown 3.9  66 46   0 error (1) .022 4.8 .12  0 error (1) .028 4.9 .17  0 error (1) .044 4.7 .11  0 error (1) .018 4.8 .13  0 unknown .072 13 .54 0 error (1) .055 7.3 .42 0 unknown .057 7.1 .63 0 true 23   580 240 2 error (1) .024 5.3 .22 0 error (1) .049 5.3 .16 0
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .15  25 1.3  2 timeout 900   3600 10000 0 error (42) .021  1.3  .038 0 unknown .011  1.0  .025  0 error (1) .44 38 3.9 0 error (1) .40 40 4.2 0 true 3.1 270 26 2 unknown 1.9  56 21   0 error (1) .044 4.9 .089 0 error (1) .021 4.9 .077 0 error (1) .044 4.8 .13  0 error (1) .022 4.8 .11  0 unknown .082 14 .44 0 error (1) .071 7.1 .30 0 unknown .055 7.3 .50 0 true 6.0 320 48 2 error (1) .027 5.4 .20 0 error (1) .042 5.3 .27 0
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true .25  40 2.3  2 timeout 900   3800 13000 0 error (42) .020  1.5  .041 0 unknown .0077 .98 .015  0 error (1) .43 37 4.3 0 error (1) .42 40 3.8 0 true 3.4 280 31 2 unknown 1.2  58 12   0 error (1) .044 4.9 .16  0 error (1) .020 4.7 .13  0 error (1) .018 4.7 .14  0 error (1) .021 4.8 .11  0 unknown .058 13 .66 0 error (1) .062 7.3 .32 0 unknown .085 7.3 .56 0 true 6.6 340 55 2 error (1) .027 5.5 .21 0 error (1) .049 5.4 .18 0
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true .24  40 2.3  2 timeout 900   3800 14000 0 error (42) .021  1.2  .043 0 unknown .0097 1.1  .018  0 error (1) .42 38 3.7 0 error (1) .42 37 3.8 0 true 3.6 280 31 2 unknown 2.5  56 34   0 error (1) .021 4.9 .10  0 error (1) .017 4.7 .14  0 error (1) .045 4.8 .13  0 error (1) .020 4.7 .14  0 unknown .058 14 .72 0 error (1) .067 7.4 .34 0 unknown .075 7.3 .58 0 true 7.2 340 54 2 error (1) .026 5.4 .17 0 error (1) .039 5.4 .22 0
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c error (5) .51  31 7.0  0 false(termination) 49   3800 330 1 error (42) .010  1.4  .064 0 unknown .0089 .92 .021  0 error (1) .42 37 4.2 0 error (1) .42 37 3.6 0 false(termination) 29   900 220 1 unknown 490    110 6600   0 error (1) .022 4.8 .13  0 error (1) .021 4.8 .082 0 error (1) .046 4.8 .16  0 error (1) .021 4.7 .10  0 unknown .075 14 .37 0 error (1) .057 7.4 .33 0 unknown .083 7.1 .47 0 false(termination) 18   650 130 1 error (1) .050 5.4 .19 0 error (1) .055 5.4 .15 0
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c error (5) .42  29 4.3  0 false(termination) 12   880 82 1 error (42) .019  1.3  .045 0 unknown .010  1.0  .031  0 error (1) .43 37 3.2 0 error (1) .46 40 3.8 0 false(termination) 6.7 430 54 1 unknown 180    63 2200   0 error (1) .034 4.8 .14  0 error (1) .030 4.7 .14  0 error (1) .044 4.8 .13  0 error (1) .045 4.8 .15  0 unknown .053 14 .47 0 error (1) .069 7.2 .32 0 unknown .072 7.1 .62 0 false(termination) 8.5 480 65 1 error (1) .042 5.4 .21 0 error (1) .041 5.3 .16 0
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c error (5) 49     380 530    0 timeout 900   3700 11000 0 error (42) .018  .95 .038 0 unknown .0074 1.1  .020  0 error (1) .42 40 3.9 0 error (1) .40 40 4.2 0 true 570   4200 7100 2 unknown 19    77 220   0 error (1) .031 4.9 .13  0 error (1) .032 4.7 .14  0 error (1) .018 4.7 .13  0 error (1) .046 4.8 .14  0 unknown .066 13 .45 0 error (1) .055 7.2 .42 0 unknown .058 7.1 .60 0 true 36   880 320 2 error (1) .045 5.2 .16 0 error (1) .026 5.4 .16 0
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c timeout 900     590 8600    0 timeout 900   3500 11000 0 error (42) .010  1.2  .049 0 unknown .0091 .88 .020  0 error (1) .41 40 3.9 0 error (1) .39 37 4.0 0 timeout 910   3700 10000 0 unknown 130    480 1600   0 error (1) .031 4.8 .14  0 error (1) .035 4.7 .12  0 error (1) .043 4.8 .15  0 error (1) .034 4.9 .13  0 unknown .080 13 .56 0 error (1) .057 7.5 .39 0 unknown .083 7.2 .61 0 true 36   940 370 2 error (1) .026 5.4 .20 0 error (1) .025 5.4 .21 0
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c timeout 900     380 6400    0 timeout 900   3900 11000 0 error (42) .013  1.1  .044 0 unknown .0083 .87 .025  0 error (1) .42 40 4.2 0 error (1) .43 40 3.6 0 false(termination) 3.6 280 30 1 unknown 2.4  64 33   0 error (1) .042 4.8 .11  0 error (1) .021 4.7 .14  0 error (1) .043 4.8 .15  0 error (1) .022 4.8 .14  0 unknown .078 13 .39 0 error (1) .069 7.1 .32 0 unknown .082 7.0 .54 0 false(termination) 11   550 89 1 error (1) .042 5.5 .19 0 error (1) .050 5.3 .23 0
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c timeout 900     390 7100    0 timeout 900   3900 10000 0 error (42) .012  1.2  .051 0 unknown .0089 1.0  .022  0 error (1) .43 37 3.7 0 error (1) .41 40 3.6 0 false(termination) 3.8 280 34 1 unknown 2.6  73 31   0 error (1) .020 4.7 .13  0 error (1) .021 4.8 .12  0 error (1) .044 4.8 .13  0 error (1) .032 4.8 .16  0 unknown .081 13 .40 0 error (1) .042 7.4 .37 0 unknown .054 7.0 .61 0 false(termination) 11   540 89 1 error (1) .051 5.4 .16 0 error (1) .026 5.5 .19 0
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c timeout 900     370 5600    0 timeout 900   3600 13000 0 error (42) .019  1.4  .042 0 unknown .0081 1.0  .030  0 error (1) .43 38 3.9 0 error (1) .42 37 3.5 0 false(termination) 4.2 280 33 1 unknown 2.9  83 37   0 error (1) .018 4.8 .15  0 error (1) .044 4.9 .10  0 error (1) .034 4.7 .14  0 error (1) .045 4.8 .11  0 unknown .082 13 .34 0 error (1) .045 7.2 .35 0 unknown .057 7.2 .55 0 false(termination) 12   880 86 1 error (1) .044 5.3 .16 0 error (1) .050 5.5 .18 0
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c timeout 900     500 5700    0 timeout 900   3800 9500 0 error (42) .015  1.2  .048 0 unknown .010  1.0  .018  0 error (1) .42 38 3.8 0 error (1) .43 40 4.0 0 false(termination) 5.8 440 46 1 unknown 3.2  94 43   0 error (1) .044 4.8 .12  0 error (1) .022 4.9 .14  0 error (1) .018 4.7 .11  0 error (1) .043 4.8 .11  0 unknown .083 13 .31 0 error (1) .070 7.2 .25 0 unknown .10  7.2 .47 0 false(termination) 23   1500 140 1 error (1) .023 5.4 .24 0 error (1) .048 5.3 .14 0
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c timeout 900     350 6800    0 timeout 900   3000 11000 0 error (42) .018  1.3  .047 0 unknown .010  .73 .022  0 error (1) .41 38 3.9 0 error (1) .41 40 4.6 0 false(termination) 4.7 290 39 1 unknown .86 56 9.7 0 error (1) .022 4.7 .13  0 error (1) .044 4.8 .11  0 error (1) .044 4.8 .12  0 error (1) .023 4.8 .13  0 unknown .083 13 .32 0 error (1) .066 7.3 .35 0 unknown .082 7.2 .50 0 false(termination) 14   860 110 1 error (1) .026 5.3 .16 0 error (1) .043 5.3 .16 0
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c timeout 900     470 6300    0 timeout 900   3800 10000 0 error (42) .015  1.4  .046 0 unknown .0091 .90 .020  0 error (1) .41 38 3.8 0 error (1) .42 38 3.9 0 false(termination) 4.7 300 36 1 unknown 3.5  100 44   0 error (1) .039 4.9 .14  0 error (1) .039 4.9 .11  0 error (1) .019 4.8 .15  0 error (1) .019 4.8 .17  0 unknown .060 14 .41 0 error (1) .065 7.3 .32 0 unknown .078 7.2 .52 0 false(termination) 37   2800 210 1 error (1) .046 5.4 .22 0 error (1) .043 5.3 .15 0
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c timeout 900     410 6500    0 timeout 900   3600 11000 0 error (42) .013  1.1  .040 0 unknown .0077 .92 .023  0 error (1) .45 40 4.1 0 error (1) .39 37 3.9 0 false(termination) 6.2 410 53 1 unknown .88 56 8.9 0 error (1) .021 4.8 .16  0 error (1) .030 4.9 .15  0 error (1) .021 4.9 .13  0 error (1) .034 4.8 .16  0 unknown .079 13 .39 0 error (1) .069 7.2 .33 0 unknown .055 7.2 .60 0 false(termination) 18   1500 130 1 error (1) .050 5.3 .15 0 error (1) .044 5.4 .20 0
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c timeout 900     440 6000    0 timeout 900   3600 11000 0 error (42) .019  1.1  .043 0 unknown .0045 .89 .016  0 error (1) .44 40 3.7 0 error (1) .40 37 3.7 0 false(termination) 4.6 300 40 1 unknown 3.9  120 48   0 error (1) .023 4.8 .13  0 error (1) .021 4.7 .12  0 error (1) .018 4.8 .15  0 error (1) .020 4.8 .11  0 unknown .055 14 .44 0 error (1) .069 7.2 .32 0 unknown .077 7.2 .51 0 false(termination) 68   4700 410 1 error (1) .025 5.3 .22 0 error (1) .042 5.4 .18 0
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c timeout 900     370 10000    0 false(termination) 140   5600 930 1 error (42) .013  1.1  .053 0 unknown .0093 .79 .017  0 error (1) .40 37 3.6 0 error (1) .41 40 3.8 0 false(termination) 3.1 270 28 1 unknown 1.5  56 21   0 error (1) .022 4.7 .14  0 error (1) .019 4.8 .11  0 error (1) .042 4.7 .15  0 error (1) .022 4.8 .12  0 unknown .078 13 .41 0 error (1) .063 7.3 .35 0 unknown .078 7.2 .52 0 false(termination) 6.2 320 54 1 error (1) .042 5.4 .17 0 error (1) .051 5.5 .17 0
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c timeout 900     540 8000    0 false(termination) 240   5900 1500 1 error (42) .018  1.0  .044 0 unknown .0089 .70 .023  0 error (1) .39 38 4.1 0 error (1) .43 38 3.8 0 false(termination) 3.6 280 27 1 unknown 1.7  55 22   0 error (1) .018 4.8 .17  0 error (1) .041 4.8 .11  0 error (1) .044 4.8 .11  0 error (1) .045 4.8 .092 0 unknown .062 13 .33 0 error (1) .060 7.4 .41 0 unknown .073 7.2 .60 0 false(termination) 6.4 330 50 1 error (1) .026 5.4 .15 0 error (1) .053 5.3 .13 0
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c timeout 900     360 9200    0 false(termination) 710   9600 5000 1 error (42) .022  1.1  .044 0 unknown .010  .72 .020  0 error (1) .40 40 4.0 0 error (1) .42 38 3.7 0 false(termination) 3.3 280 31 1 unknown 1.8  56 21   0 error (1) .033 4.8 .14  0 error (1) .044 4.8 .12  0 error (1) .020 4.8 .14  0 error (1) .045 4.8 .10  0 unknown .059 14 .34 0 error (1) .057 7.4 .36 0 unknown .085 7.3 .60 0 false(termination) 7.7 380 59 1 error (1) .051 5.4 .17 0 error (1) .042 5.4 .22 0
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c timeout 900     290 7200    0 timeout 910   8700 9100 0 error (42) .013  1.1  .059 0 unknown .0091 .81 .022  0 error (1) .45 40 4.2 0 error (1) .40 37 3.6 0 false(termination) 3.5 280 35 1 unknown 2.0  55 24   0 error (1) .031 4.7 .13  0 error (1) .022 4.8 .15  0 error (1) .021 4.8 .096 0 error (1) .045 4.9 .12  0 unknown .076 14 .39 0 error (1) .041 7.4 .40 0 unknown .080 7.2 .58 0 false(termination) 7.7 440 55 1 error (1) .026 5.4 .24 0 error (1) .051 5.3 .16 0
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c timeout 900     390 7300    0 timeout 900   2600 11000 0 error (42) .013  1.3  .036 0 unknown .010  .92 .014  0 error (1) .42 37 4.0 0 error (1) .43 37 3.8 0 false(termination) 4.0 280 31 1 unknown 2.2  57 29   0 error (1) .045 4.8 .11  0 error (1) .017 4.7 .15  0 error (1) .023 4.8 .18  0 error (1) .020 4.9 .093 0 unknown .053 14 .47 0 error (1) .069 7.4 .36 0 unknown .083 7.2 .48 0 false(termination) 9.2 500 69 1 error (1) .025 5.4 .16 0 error (1) .024 5.3 .23 0
ssh-simplified/s3_clnt_3.cil_true-unreach-call_true-termination.c error (5) 41     240 520    0 timeout 900   3800 11000 0 error (42) .013  1.3  .055 0 unknown .010  .78 .017  0 error (1) .40 37 4.0 0 error (1) .43 40 3.6 0 timeout 900   5200 11000 0 unknown 95    370 1100   0 error (1) .021 4.9 .13  0 error (1) .022 4.8 .13  0 error (1) .022 4.8 .15  0 error (1) .021 4.8 .13  0 unknown .085 13 .44 0 error (1) .038 7.3 .41 0 unknown .085 7.2 .56 0 true 81   1000 890 2 error (1) .049 5.3 .15 0 error (1) .024 5.4 .28 0
loops/for_infinite_loop_1_true-unreach-call_false-termination.i error (5) .28  29 2.9  0 false(termination) 5.5 450 40 1 error (42) .012  .95 .052 0 unknown .0088 1.0  .031  0 error (1) .44 40 4.1 0 error (1) .41 38 3.6 0 unknown 4.0 300 36 0 unknown 1.2  56 13   0 error (1) .022 4.8 .12  0 error (1) .020 4.7 .10  0 error (1) .045 4.8 .096 0 error (1) .023 4.7 .14  0 unknown .12  41 1.4  0 error (1) .062 7.2 .34 0 unknown .054 7.1 .58 0 false(termination) 7.6 370 55 1 error (1) .050 5.4 .18 0 error (1) .051 5.3 .15 0
loops/for_infinite_loop_2_true-unreach-call_false-termination.i error (5) .25  29 3.2  0 false(termination) 5.9 380 44 1 error (42) .012  1.5  .050 0 unknown .0093 .94 .024  0 error (1) .43 40 4.0 0 error (1) .42 40 4.2 0 unknown 4.3 300 34 0 unknown 1.2  56 13   0 error (1) .021 4.9 .16  0 error (1) .040 4.9 .11  0 error (1) .030 4.8 .20  0 error (1) .021 4.8 .11  0 unknown .12  41 1.5  0 error (1) .069 7.2 .32 0 unknown .080 7.2 .48 0 false(termination) 6.5 350 53 1 error (1) .024 5.4 .23 0 error (1) .024 5.4 .19 0
loops/n.c11_true-unreach-call_false-termination.i error (5) .27  29 2.6  0 error (1) 5.2 390 40 0 error (42) .021  1.2  .060 0 unknown .0095 .89 .029  0 error (1) .43 39 3.6 0 error (1) .39 37 4.1 0 unknown 570   4100 7800 0 unknown 59    28 750   0 error (1) .031 4.8 .13  0 error (1) .030 4.8 .18  0 error (1) .021 4.8 .14  0 error (1) .040 4.8 .13  0 unknown .093 35 .49 0 error (1) .069 7.6 .33 0 unknown .056 7.2 .56 0 false(termination) 30   470 330 1 error (1) .024 5.4 .18 0 error (1) .022 5.2 .19 0
loops/nec11_false-unreach-call_false-termination.i error (5) .26  28 3.2  0 error (1) 10   620 82 0 error (42) .022  1.4  .062 0 unknown .0091 .79 .021  0 error (1) .40 40 3.6 0 error (1) .42 38 3.8 0 unknown 660   4300 8800 0 unknown .82 56 9.8 0 error (1) .022 4.8 .096 0 error (1) .043 4.9 .12  0 error (1) .018 4.9 .19  0 error (1) .020 4.8 .11  0 unknown .069 35 .59 0 error (1) .043 7.5 .36 0 unknown .054 7.2 .61 0 false(termination) 6.5 320 60 1 error (1) .051 5.3 .17 0 error (1) .024 5.5 .21 0
loops/sum03_true-unreach-call_false-termination.i false(termination) .18  25 1.8  1 false(termination) 7.2 520 54 1 error (42) .021  1.1  .035 0 unknown .0071 .92 .032  0 error (1) .40 37 3.4 0 error (1) .41 40 3.8 0 unknown 8.7 480 70 0 unknown 58    28 720   0 error (1) .020 4.8 .17  0 error (1) .031 4.7 .13  0 error (1) .027 4.9 .14  0 error (1) .021 4.8 .15  0 unknown .066 35 .69 0 error (1) .060 7.2 .42 0 unknown .074 7.0 .55 0 unknown 74   1000 740 0 error (1) .053 5.3 .15 0 error (1) .029 5.3 .17 0
loops/trex04_true-unreach-call_false-termination.i error (5) .28  25 3.0  0 false(termination) 24   1900 160 1 error (42) .021  1.1  .054 0 unknown .010  .95 .017  0 error (1) .40 40 4.0 0 error (1) .39 37 3.9 0 false(termination) 3.3 270 25 1 unknown 1.3  56 13   0 error (1) .018 4.8 .19  0 error (1) .020 4.8 .12  0 error (1) .021 4.8 .10  0 error (1) .043 4.8 .12  0 unknown .070 34 .76 0 error (1) .042 7.5 .40 0 unknown .056 7.1 .53 0 false(termination) 9.6 380 74 1 error (1) .050 5.4 .18 0 error (1) .051 5.3 .16 0
loops/while_infinite_loop_1_true-unreach-call_false-termination.i false(termination) .11  22 .87 1 false(termination) 2.7 240 25 1 error (42) .021  1.3  .043 0 unknown .0078 .89 .024  0 error (1) .42 37 4.5 0 error (1) .41 40 3.4 0 false(termination) 2.7 270 24 1 unknown 1.2  55 12   0 error (1) .030 4.8 .19  0 error (1) .022 4.8 .15  0 error (1) .015 4.8 .11  0 error (1) .021 4.8 .13  0 unknown .15  41 1.1  0 error (1) .062 7.6 .31 0 unknown .082 7.2 .49 0 false(termination) 5.4 340 41 1 error (1) .026 5.4 .21 0 error (1) .052 5.4 .19 0
loops/while_infinite_loop_2_true-unreach-call_false-termination.i false(termination) .12  22 .92 1 false(termination) 2.9 230 25 1 error (42) .012  1.1  .043 0 unknown .0088 .77 .021  0 error (1) .42 40 4.1 0 error (1) .42 37 3.6 0 false(termination) 2.7 270 23 1 unknown 1.2  56 13   0 error (1) .022 4.8 .13  0 error (1) .018 4.8 .16  0 error (1) .044 4.8 .11  0 error (1) .019 4.8 .17  0 unknown .14  41 1.4  0 error (1) .064 7.3 .33 0 unknown .055 7.1 .54 0 false(termination) 6.0 330 44 1 error (1) .053 5.4 .15 0 error (1) .047 5.3 .15 0
loops/while_infinite_loop_3_true-unreach-call_false-termination.i false(termination) .11  22 .91 1 false(termination) 2.8 240 24 1 error (42) .018  1.4  .048 0 unknown .0092 .96 .022  0 error (1) .42 40 3.7 0 error (1) .43 40 3.8 0 false(termination) 2.7 260 22 1 unknown 1.2  55 14   0 error (1) .018 4.8 .16  0 error (1) .044 4.8 .15  0 error (1) .042 4.7 .14  0 error (1) .045 4.9 .14  0 unknown .15  41 1.2  0 error (1) .063 7.1 .35 0 unknown .053 7.2 .47 0 false(termination) 5.6 320 49 1 error (1) .028 5.5 .19 0 error (1) .025 5.3 .20 0
loops/array_false-unreach-call_true-termination.i true .11  23 .98 2 true 3.4 260 26 2 error (42) .022  1.3  .034 0 unknown .0090 1.0  .027  0 error (1) .41 39 3.9 0 error (1) .41 40 3.9 0 timeout 900   4400 11000 0 unknown 1.4  55 17   0 error (1) .018 4.8 .11  0 error (1) .030 4.9 .11  0 error (1) .019 4.8 .14  0 error (1) .045 4.8 .12  0 true .36  46 3.9  2 error (1) .066 7.4 .37 0 unknown .053 7.2 .59 0 true 10   510 70 2 error (1) .052 5.5 .15 0 error (1) .052 5.3 .19 0
loops/array_true-unreach-call_true-termination.i true .12  23 .82 2 true 3.7 270 28 2 error (42) .012  1.1  .061 0 unknown .0088 .99 .029  0 error (1) .43 40 3.9 0 error (1) .44 40 4.2 0 timeout 910   4500 13000 0 unknown 1.2  55 14   0 error (1) .019 4.8 .17  0 error (1) .021 4.9 .085 0 error (1) .042 4.7 .12  0 error (1) .019 4.8 .16  0 true .39  46 3.9  2 error (1) .044 7.3 .35 0 unknown .084 7.2 .50 0 true 8.6 480 68 2 error (1) .050 5.4 .19 0 error (1) .025 5.4 .16 0
loops/count_up_down_false-unreach-call_true-termination.i true .10  24 1.1  2 true 6.3 490 46 2 error (42) .021  1.2  .042 0 unknown .0089 .91 .018  0 error (1) .41 37 3.8 0 error (1) .38 37 4.1 0 true 4.5 300 40 2 unknown .80 56 9.5 0 error (1) .020 4.8 .12  0 error (1) .022 4.8 .15  0 error (1) .022 4.8 .13  0 error (1) .044 4.9 .095 0 unknown .092 34 .51 0 error (1) .039 7.3 .45 0 unknown .057 7.2 .60 0 unknown 53   570 580 0 error (1) .050 5.5 .18 0 error (1) .043 5.5 .20 0
loops/count_up_down_true-unreach-call_true-termination.i true .10  26 1.2  2 true 6.3 490 50 2 error (42) .022  1.5  .048 0 unknown .0074 .81 .019  0 error (1) .41 38 3.7 0 error (1) .41 38 3.4 0 true 5.4 320 37 2 unknown 69    29 880   0 error (1) .020 4.7 .16  0 error (1) .021 4.7 .12  0 error (1) .044 4.8 .12  0 error (1) .019 4.8 .14  0 unknown .091 34 .53 0 error (1) .068 7.3 .33 0 unknown .053 7.3 .55 0 unknown 54   570 630 0 error (1) .025 5.4 .15 0 error (1) .053 5.3 .17 0
loops/eureka_05_true-unreach-call_true-termination.i true .37  28 3.8  2 timeout 900   11000 5900 0 error (42) .013  1.2  .045 0 unknown .0099 .85 .025  0 error (1) .40 38 3.3 0 error (1) .43 40 3.5 0 timeout 900   4100 13000 0 unknown 3.5  58 42   0 error (1) .019 4.8 .17  0 error (1) .033 4.8 .12  0 error (1) .036 4.8 .12  0 error (1) .015 4.8 .071 0 unknown .15  41 1.3  0 error (1) .070 7.3 .30 0 unknown .080 7.2 .53 0 true 23   790 230 2 error (1) .050 5.3 .16 0 error (1) .026 5.4 .20 0
loops/for_bounded_loop1_false-unreach-call_true-termination.i true .15  25 1.5  2 true 12   750 82 2 error (42) .012  1.1  .070 0 unknown .0088 .92 .026  0 error (1) .40 40 3.9 0 error (1) .42 41 4.3 0 true 7.2 480 56 2 unknown 1.3  56 16   0 error (1) .031 4.8 .15  0 error (1) .033 4.8 .17  0 error (1) .044 4.9 .14  0 error (1) .021 4.8 .14  0 unknown .15  41 1.1  0 error (1) .070 7.6 .31 0 unknown .085 7.1 .48 0 true 7.3 360 56 2 error (1) .026 5.2 .21 0 error (1) .026 5.5 .23 0
loops/insertion_sort_false-unreach-call_true-termination.i error (5) .75  34 9.1  0 error (1) 9.6 720 83 0 error (42) .016  1.1  .058 0 unknown .0090 1.1  .018  0 error (1) .41 37 3.5 0 error (1) .44 40 4.2 0 timeout 900   4400 11000 0 unknown 3.9  56 51   0 error (1) .043 4.8 .12  0 error (1) .020 4.7 .15  0 error (1) .026 4.9 .14  0 error (1) .021 4.7 .13  0 unknown .095 34 .51 0 error (1) .044 7.3 .44 0 unknown .078 7.2 .56 0 true 16   560 140 2 error (1) .024 5.4 .21 0 error (1) .053 5.4 .17 0
loops/insertion_sort_true-unreach-call_true-termination.i error (5) .60  33 8.2  0 error (1) 9.3 690 69 0 error (42) .015  1.0  .048 0 unknown .0085 .92 .018  0 error (1) .41 40 4.5 0 error (1) .44 40 4.1 0 timeout 900   4400 11000 0 unknown 890    120 10000   0 error (1) .042 4.8 .092 0 error (1) .032 4.8 .16  0 error (1) .019 4.8 .14  0 error (1) .022 4.8 .15  0 unknown .095 35 .65 0 error (1) .067 7.4 .30 0 unknown .072 7.3 .59 0 true 15   480 140 2 error (1) .051 5.4 .14 0 error (1) .027 5.3 .21 0
loops/invert_string_false-unreach-call_true-termination.i true .30  29 3.5  2 timeout 900   3500 13000 0 error (42) .015  1.4  .048 0 unknown .0089 .93 .025  0 error (1) .41 37 4.1 0 error (1) .40 38 4.0 0 timeout 900   4500 11000 0 unknown 2.0  56 21   0 error (1) .018 4.9 .17  0 error (1) .019 4.7 .17  0 error (1) .042 4.7 .14  0 error (1) .022 4.8 .15  0 unknown .074 34 .59 0 error (1) .069 7.3 .27 0 unknown .054 7.2 .51 0 true 9.9 500 78 2 error (1) .042 5.4 .18 0 error (1) .051 5.3 .16 0
loops/invert_string_true-unreach-call_true-termination.i true .22  30 2.8  2 error (1) 28   3600 210 0 error (42) .012  1.2  .041 0 unknown .0089 .93 .028  0 error (1) .41 37 3.5 0 error (1) .40 37 3.7 0 timeout 900   4500 13000 0 unknown 3.4  56 41   0 error (1) .021 4.9 .086 0 error (1) .015 4.8 .11  0 error (1) .044 4.8 .11  0 error (1) .045 4.8 .14  0 unknown .097 35 .60 0 error (1) .070 7.0 .33 0 unknown .055 7.3 .57 0 true 14   490 130 2 error (1) .027 5.3 .17 0 error (1) .028 5.4 .18 0
loops/matrix_false-unreach-call_true-termination.i true 1.4   39 14    2 error (1) 3.2 260 28 0 error (42) .021  1.2  .046 0 unknown .0099 .75 .016  0 error (1) .40 37 3.4 0 error (1) .42 37 3.5 0 timeout 910   4600 13000 0 unknown 1.5  57 17   0 error (1) .017 4.7 .17  0 error (1) .044 4.8 .14  0 error (1) .033 4.7 .14  0 error (1) .024 4.9 .14  0 unknown .037 10 .43 0 error (1) .071 7.3 .27 0 unknown .056 7.2 .51 0 unknown 66   590 690 0 error (1) .026 5.4 .18 0 error (1) .043 5.3 .20 0
loops/matrix_true-unreach-call_true-termination.i true .20  25 1.7  2 true 3.7 340 31 2 error (42) .021  1.3  .056 0 unknown .0070 1.0  .023  0 error (1) .42 37 4.0 0 error (1) .46 40 4.0 0 timeout 900   4000 13000 0 unknown 1.2  56 13   0 error (1) .021 4.7 .11  0 error (1) .020 4.8 .14  0 error (1) .045 4.7 .090 0 error (1) .019 4.7 .12  0 unknown .068 12 .26 0 error (1) .066 7.4 .32 0 unknown .10  7.1 .46 0 true 27   570 240 2 error (1) .051 5.4 .15 0 error (1) .027 5.3 .17 0
loops/n.c40_true-unreach-call_true-termination.i true .14  24 1.0  2 error (1) 55   3700 470 0 error (42) .020  1.3  .048 0 unknown .0095 .88 .017  0 error (1) .40 38 3.9 0 error (1) .42 40 3.8 0 true 3.4 280 29 2 unknown 1.2  56 13   0 error (1) .045 4.8 .14  0 error (1) .044 4.7 .12  0 error (1) .045 4.8 .12  0 error (1) .021 4.8 .12  0 unknown .12  41 1.6  0 error (1) .045 7.4 .36 0 unknown .083 7.2 .53 0 true 160   690 1800 2 error (1) .051 5.4 .16 0 error (1) .048 5.5 .16 0
loops/nec20_false-unreach-call_true-termination.i true .55  56 5.6  2 true 16   1300 130 2 error (42) .012  1.4  .047 0 unknown .0098 .92 .019  0 error (1) .44 40 4.2 0 error (1) .42 37 3.7 0 true 6.0 350 49 2 unknown 1.4  56 18   0 error (1) .043 4.8 .094 0 error (1) .033 4.8 .10  0 error (1) .019 4.7 .17  0 error (1) .020 4.8 .15  0 unknown .085 35 .49 0 error (1) .071 7.4 .32 0 unknown .054 7.1 .52 0 true 6.6 340 53 2 error (1) .025 5.3 .18 0 error (1) .051 5.4 .12 0
loops/nec40_true-unreach-call_true-termination.i true .13  24 1.0  2 error (1) 43   2500 370 0 error (42) .022  1.4  .041 0 unknown .0073 .88 .025  0 error (1) .42 38 3.3 0 error (1) .41 37 3.7 0 true 3.3 280 26 2 unknown 1.2  56 12   0 error (1) .039 4.8 .12  0 error (1) .030 4.8 .15  0 error (1) .019 4.8 .15  0 error (1) .044 4.7 .14  0 unknown .14  41 1.5  0 error (1) .066 7.3 .33 0 unknown .050 7.3 .55 0 true 160   550 2200 2 error (1) .052 5.5 .14 0 error (1) .049 5.2 .21 0
loops/string_false-unreach-call_true-termination.i error (5) .83  34 11    0 error (1) 19   1900 130 0 error (42) .023  1.4  .045 0 unknown .0096 .76 .015  0 error (1) .43 40 3.9 0 error (1) .39 38 3.8 0 timeout 920   4500 11000 0 unknown 4.0  56 45   0 error (1) .019 4.8 .14  0 error (1) .043 4.9 .083 0 error (1) .033 4.8 .11  0 error (1) .045 4.8 .11  0 unknown .076 13 .19 0 error (1) .072 7.3 .30 0 unknown .055 7.3 .57 0 true 23   660 210 2 error (1) .019 5.2 .16 0 error (1) .054 5.4 .15 0
loops/string_true-unreach-call_true-termination.i error (5) .68  33 7.9  0 timeout 900   8900 9200 0 error (42) .012  1.3  .045 0 unknown .010  1.0  .030  0 error (1) .41 37 3.9 0 error (1) .39 37 3.7 0 timeout 910   4200 12000 0 unknown 1.3  55 14   0 error (1) .019 4.7 .15  0 error (1) .047 4.8 .13  0 error (1) .035 4.8 .15  0 error (1) .043 4.8 .13  0 unknown .074 35 .68 0 error (1) .068 7.4 .36 0 unknown .078 7.2 .55 0 true 22   830 180 2 error (1) .048 5.4 .16 0 error (1) .052 5.3 .17 0
loops/sum01_bug02_false-unreach-call_true-termination.i error (5) 6.9   44 89    0 true 15   1300 110 2 error (42) .021  .96 .037 0 unknown .0088 .98 .030  0 error (1) .42 37 3.6 0 error (1) .42 40 4.6 0 true 13   580 96 2 unknown 3.9  56 45   0 error (1) .021 4.9 .12  0 error (1) .026 4.8 .13  0 error (1) .044 4.8 .087 0 error (1) .045 4.8 .11  0 unknown .080 34 .66 0 error (1) .069 7.4 .33 0 unknown .082 7.1 .50 0 true 7.0 340 60 2 error (1) .056 5.6 .14 0 error (1) .051 5.5 .15 0
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i error (5) .65  34 7.4  0 true 9.8 770 67 2 error (42) .012  1.3  .042 0 unknown .0093 1.0  .026  0 error (1) .43 38 3.7 0 error (1) .43 38 3.6 0 true 8.2 460 59 2 unknown 2.8  55 33   0 error (1) .027 4.9 .16  0 error (1) .034 4.8 .14  0 error (1) .034 4.7 .11  0 error (1) .020 4.7 .15  0 unknown .082 34 .70 0 error (1) .064 7.3 .31 0 unknown .058 7.4 .52 0 true 7.2 380 55 2 error (1) .051 5.5 .16 0 error (1) .026 5.4 .18 0
loops/sum01_false-unreach-call_true-termination.i error (5) .38  32 4.7  0 true 9.9 770 69 2 error (42) .011  .96 .055 0 unknown .0086 .88 .025  0 error (1) .43 37 3.7 0 error (1) .41 37 4.2 0 true 17   590 130 2 unknown 5.9  56 74   0 error (1) .021 4.8 .093 0 error (1) .020 4.8 .15  0 error (1) .030 4.7 .16  0 error (1) .024 4.9 .14  0 unknown .095 34 .49 0 error (1) .068 7.4 .30 0 unknown .078 7.2 .55 0 true 7.6 370 63 2 error (1) .045 5.4 .21 0 error (1) .053 5.4 .15 0
loops/sum01_true-unreach-call_true-termination.i true .15  26 1.6  2 true 7.5 520 60 2 error (42) .018  1.3  .046 0 unknown .0078 .79 .021  0 error (1) .48 40 3.4 0 error (1) .41 38 3.4 0 true 4.0 290 37 2 unknown 64    42 900   0 error (1) .044 4.8 .11  0 error (1) .021 4.9 .12  0 error (1) .040 4.8 .13  0 error (1) .044 4.9 .12  0 unknown .15  41 1.2  0 error (1) .059 7.1 .34 0 unknown .081 7.0 .57 0 true 6.6 320 52 2 error (1) .028 5.3 .18 0 error (1) .026 5.3 .26 0
loops/sum03_false-unreach-call_true-termination.i false(termination) .13  23 .84 -16 true 11   770 81 2 error (42) .013  1.1  .051 0 unknown .0097 .93 .022  0 error (1) .41 37 4.0 0 error (1) .39 37 3.7 0 true 5.1 320 44 2 unknown 5.9  56 69   0 error (1) .020 4.8 .16  0 error (1) .041 4.8 .12  0 error (1) .021 4.7 .14  0 error (1) .044 4.8 .10  0 unknown .092 35 .58 0 error (1) .068 7.3 .31 0 unknown .084 7.2 .48 0 timeout 900   810 9800 0 error (1) .023 5.4 .21 0 error (1) .048 5.4 .15 0
loops/sum04_false-unreach-call_true-termination.i true .13  23 1.0  2 true 7.9 500 53 2 error (42) .013  1.0  .045 0 unknown .0091 1.0  .016  0 error (1) .40 38 3.6 0 error (1) .45 40 3.8 0 true 11   470 91 2 unknown 4.8  56 60   0 error (1) .018 4.8 .18  0 error (1) .044 4.8 .13  0 error (1) .018 4.8 .20  0 error (1) .044 4.8 .14  0 unknown .15  41 1.2  0 error (1) .047 7.3 .26 0 unknown .057 7.3 .54 0 true 8.1 350 56 2 error (1) .053 5.5 .18 0 error (1) .024 5.3 .18 0
loops/sum04_true-unreach-call_true-termination.i true .15  26 1.2  2 true 4.8 430 39 2 error (42) .012  1.1  .041 0 unknown .0085 1.0  .027  0 error (1) .43 37 3.5 0 error (1) .42 40 3.5 0 true 9.0 440 69 2 unknown 4.6  56 57   0 error (1) .020 4.8 .13  0 error (1) .019 4.8 .11  0 error (1) .024 4.8 .15  0 error (1) .022 4.9 .15  0 unknown .15  41 1.2  0 error (1) .068 7.0 .33 0 unknown .058 7.1 .59 0 true 6.5 340 51 2 error (1) .051 5.3 .18 0 error (1) .024 5.3 .19 0
loops/terminator_01_false-unreach-call_true-termination.i false(termination) .096 23 .98 -16 true 4.6 340 35 2 error (42) .012  .99 .053 0 unknown .010  .88 .020  0 error (1) .43 40 4.2 0 error (1) .40 37 4.2 0 true 4.4 290 40 2 unknown .80 56 8.4 0 error (1) .020 4.8 .12  0 error (1) .019 4.8 .15  0 error (1) .020 4.7 .13  0 error (1) .041 4.8 .14  0 unknown .12  41 1.2  0 error (1) .069 7.6 .32 0 unknown .083 7.0 .52 0 true 8.5 460 61 2 error (1) .024 5.3 .21 0 error (1) .050 5.4 .17 0
loops/terminator_02_false-unreach-call_true-termination.i false(termination) .13  23 1.1  -16 true 22   1400 150 2 error (42) .021  1.4  .055 0 unknown .0064 .92 .029  0 error (1) .39 37 4.3 0 error (1) .43 40 3.6 0 true 5.7 330 42 2 unknown .82 56 9.2 0 error (1) .022 4.8 .079 0 error (1) .021 4.8 .14  0 error (1) .031 4.8 .098 0 error (1) .040 4.8 .11  0 unknown .066 35 .79 0 error (1) .044 7.4 .36 0 unknown .054 7.2 .48 0 true 9.8 490 72 2 error (1) .048 5.4 .16 0 error (1) .051 5.4 .14 0
loops/terminator_02_true-unreach-call_true-termination.i true .13  23 1.0  2 true 3.2 240 24 2 error (42) .012  1.4  .052 0 unknown .0092 1.1  .025  0 error (1) .43 38 3.7 0 error (1) .42 37 3.9 0 true 2.8 270 23 2 unknown 1.3  55 13   0 error (1) .021 4.8 .16  0 error (1) .033 4.7 .11  0 error (1) .020 4.9 .14  0 error (1) .029 4.7 .085 0 unknown .097 34 .60 0 error (1) .068 7.2 .31 0 unknown .081 7.1 .46 0 true 6.5 330 54 2 error (1) .052 5.5 .16 0 error (1) .042 5.5 .21 0
loops/terminator_03_false-unreach-call_true-termination.i error (5) .19  29 2.0  0 true 5.2 360 37 2 error (42) .015  1.3  .049 0 unknown .0089 .89 .021  0 error (1) .45 40 3.8 0 error (1) .43 39 3.8 0 unknown 3.2 280 28 0 unknown .82 56 9.0 0 error (1) .020 4.9 .14  0 error (1) .041 4.7 .12  0 error (1) .021 4.9 .16  0 error (1) .044 4.7 .14  0 unknown .14  41 1.5  0 error (1) .064 7.3 .29 0 unknown .056 7.4 .59 0 true 6.3 330 53 2 error (1) .050 5.3 .15 0 error (1) .050 5.3 .16 0
loops/terminator_03_true-unreach-call_true-termination.i true .10  23 .89 2 true 5.8 370 40 2 error (42) .016  1.4  .049 0 unknown .0093 .89 .017  0 error (1) .40 40 3.6 0 error (1) .44 38 3.9 0 unknown 3.4 270 31 0 unknown 1.2  56 13   0 error (1) .018 4.8 .20  0 error (1) .022 4.8 .084 0 error (1) .044 4.8 .11  0 error (1) .044 4.8 .13  0 unknown .14  41 1.6  0 error (1) .040 7.3 .40 0 unknown .081 7.1 .51 0 true 18   380 180 2 error (1) .027 5.4 .21 0 error (1) .027 5.4 .23 0
loops/trex01_false-unreach-call_true-termination.i error (5) .35  32 4.2  0 true 54   4200 330 2 error (42) .013  1.3  .046 0 unknown .0087 1.1  .027  0 error (1) .41 37 3.9 0 error (1) .39 38 3.6 0 true 12   480 100 2 unknown .84 57 9.9 0 error (1) .020 4.9 .12  0 error (1) .019 4.8 .14  0 error (1) .041 4.8 .13  0 error (1) .021 4.8 .13  0 unknown .039 13 .32 0 error (1) .069 7.4 .34 0 unknown .082 7.2 .49 0 true 21   570 210 2 error (1) .028 5.3 .18 0 error (1) .051 5.5 .18 0
loops/trex01_true-unreach-call_true-termination.i error (5) .79  33 9.9  0 true 79   5800 570 2 error (42) .021  1.3  .039 0 unknown .010  .77 .018  0 error (1) .45 40 3.4 0 error (1) .41 40 3.6 0 true 13   510 100 2 unknown 560    150 5700   0 error (1) .030 4.8 .12  0 error (1) .026 4.8 .17  0 error (1) .041 4.8 .11  0 error (1) .022 4.9 .13  0 unknown .072 13 .29 0 error (1) .071 7.2 .31 0 unknown .054 7.2 .54 0 true 100   750 1100 2 error (1) .046 5.4 .16 0 error (1) .042 5.3 .17 0
loops/trex02_false-unreach-call_true-termination.i true .11  22 .84 2 true 9.3 800 61 2 error (42) .013  .96 .032 0 unknown .0098 .90 .021  0 error (1) .42 40 3.7 0 error (1) .42 40 3.6 0 true 3.5 270 28 2 unknown .83 56 7.8 0 error (1) .031 4.8 .14  0 error (1) .023 4.8 .13  0 error (1) .021 4.7 .14  0 error (1) .045 4.9 .13  0 unknown .076 35 .70 0 error (1) .063 7.2 .30 0 unknown .057 7.2 .56 0 true 6.3 330 52 2 error (1) .024 5.1 .19 0 error (1) .054 5.3 .14 0
loops/trex02_true-unreach-call_true-termination.i true .12  24 .70 2 true 8.8 810 54 2 error (42) .014  1.3  .039 0 unknown .0099 .72 .018  0 error (1) .41 38 3.6 0 error (1) .41 38 4.0 0 true 3.5 270 33 2 unknown 1.3  56 13   0 error (1) .019 4.8 .12  0 error (1) .020 4.7 .14  0 error (1) .030 4.7 .15  0 error (1) .021 4.7 .11  0 unknown .064 35 .70 0 error (1) .062 7.3 .30 0 unknown .083 7.1 .56 0 true 6.1 320 49 2 error (1) .029 5.5 .19 0 error (1) .051 5.3 .17 0
loops/trex03_false-unreach-call_true-termination.i true .15  26 1.5  2 true 82   6400 490 2 error (42) .011  1.1  .040 0 unknown .0093 .89 .020  0 error (1) .44 38 3.6 0 error (1) .41 38 4.1 0 true 7.4 430 53 2 unknown .83 56 8.4 0 error (1) .042 4.7 .12  0 error (1) .045 4.8 .12  0 error (1) .044 4.8 .082 0 error (1) .021 4.8 .13  0 unknown .094 35 .48 0 error (1) .067 7.1 .33 0 unknown .080 7.2 .49 0 unknown 41   540 480 0 error (1) .026 5.5 .21 0 error (1) .053 5.5 .21 0
loops/trex03_true-unreach-call_true-termination.i true .17  28 1.7  2 true 190   8800 950 2 error (42) .022  1.5  .040 0 unknown .0081 .78 .031  0 error (1) .42 38 3.9 0 error (1) .41 40 4.0 0 true 7.3 440 57 2 unknown 1.4  56 16   0 error (1) .044 4.8 .12  0 error (1) .022 4.8 .11  0 error (1) .021 4.8 .12  0 error (1) .022 4.9 .15  0 unknown .094 35 .58 0 error (1) .065 7.2 .30 0 unknown .083 7.2 .53 0 unknown 42   550 440 0 error (1) .051 5.4 .16 0 error (1) .025 5.3 .17 0
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i error (5) .084 23 .90 0 error (1) 4.6 330 38 0 error (42) .020  1.3  .056 0 unknown .0087 .88 .027  0 error (1) .44 40 4.0 0 error (1) .40 37 3.6 0 true 3.1 290 27 2 unknown 1.3  57 15   0 error (1) .035 4.8 .16  0 error (1) .037 4.8 .12  0 error (1) .021 4.9 .16  0 error (1) .022 4.8 .090 0 unknown .16  41 1.4  0 error (1) .071 7.3 .29 0 unknown .054 7.2 .50 0 true 7.9 470 68 2 error (1) .051 5.3 .15 0 error (1) .053 5.3 .15 0
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i error (5) .43  32 4.2  0 timeout 900   3600 13000 0 error (42) .013  1.1  .041 0 unknown .0072 1.0  .033  0 error (1) .42 37 3.7 0 error (1) .40 38 3.8 0 timeout 900   4600 11000 0 unknown 7.2  56 82   0 error (1) .021 4.7 .11  0 error (1) .022 4.8 .13  0 error (1) .021 4.9 .12  0 error (1) .044 4.8 .15  0 unknown .075 35 .71 0 error (1) .042 7.2 .40 0 unknown .073 7.2 .59 0 true 36   690 360 2 error (1) .022 5.4 .15 0 error (1) .047 5.4 .14 0
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i error (5) 2.1   46 24    0 error (1) 14   1200 130 0 error (42) .012  1.1  .065 0 unknown .0073 .88 .018  0 error (1) .42 40 3.5 0 error (1) .41 40 3.7 0 timeout 900   4400 12000 0 unknown 1.2  57 16   0 error (1) .033 4.8 .13  0 error (1) .030 4.8 .12  0 error (1) .033 4.7 .16  0 error (1) .018 4.7 .11  0 unknown .065 35 .76 0 error (1) .046 7.2 .37 0 unknown .081 7.3 .56 0 unknown 17   790 130 0 error (1) .050 5.3 .16 0 error (1) .051 5.3 .16 0
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i error (5) .11  23 .77 0 error (1) 3.5 270 29 0 error (42) .020  1.1  .040 0 unknown .0091 1.1  .023  0 error (1) .39 38 3.8 0 error (1) .40 37 3.7 0 true 3.1 290 26 2 unknown 1.8  55 22   0 error (1) .045 4.8 .11  0 error (1) .036 4.7 .13  0 error (1) .043 4.8 .12  0 error (1) .020 4.8 .15  0 unknown .13  41 1.3  0 error (1) .042 7.1 .39 0 unknown .083 7.2 .48 0 true 8.2 460 64 2 error (1) .026 5.3 .21 0 error (1) .050 5.4 .16 0
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i error (5) .46  31 4.6  0 timeout 900   3500 12000 0 error (42) .022  1.4  .051 0 unknown .0087 .88 .029  0 error (1) .42 40 3.9 0 error (1) .41 39 3.6 0 timeout 900   4400 13000 0 unknown 2.1  56 28   0 error (1) .018 4.7 .17  0 error (1) .030 4.8 .10  0 error (1) .044 4.8 .12  0 error (1) .044 4.8 .13  0 unknown .097 35 .56 0 error (1) .041 7.2 .43 0 unknown .055 7.2 .57 0 true 16   580 140 2 error (1) .046 5.5 .13 0 error (1) .051 5.4 .12 0
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(termination) .11  22 .88 -16 true 2.2 220 17 2 error (42) .0065 1.8  .055 0 unknown .0091 .92 .017  0 error (1) .40 37 3.5 0 error (1) .43 40 3.9 0 true 2.6 270 23 2 unknown .82 56 8.4 0 error (1) .020 4.7 .13  0 error (1) .019 4.9 .18  0 error (1) .018 4.8 .15  0 error (1) .021 4.8 .10  0 unknown .13  41 1.5  0 error (1) .039 7.3 .45 0 unknown .091 17   1.4  0 true 5.5 320 42 2 error (1) .051 5.3 .19 0 error (1) .045 5.2 .20 0
loop-acceleration/array_false-unreach-call1_true-termination.i true 1.2   97 13    2 true 6.4 500 54 2 error (42) .022  1.4  .047 0 unknown .0089 .92 .024  0 error (1) .43 38 3.2 0 error (1) .45 40 3.8 0 timeout 900   4500 11000 0 unknown 890    290 9200   0 error (1) .021 4.7 .12  0 error (1) .020 4.8 .13  0 error (1) .056 4.8 .16  0 error (1) .044 4.8 .14  0 unknown .13  40 1.3  0 error (1) .070 7.1 .31 0 unknown .072 7.3 .67 0 true 7.2 350 49 2 error (1) .044 5.4 .20 0 error (1) .027 5.3 .16 0
loop-acceleration/array_false-unreach-call2_true-termination.i true 1.7   160 17    2 true 9.8 770 78 2 error (42) .012  1.1  .054 0 unknown .0043 .90 .016  0 error (1) .41 40 3.9 0 error (1) .44 40 3.8 0 timeout 900   4400 12000 0 unknown 900    160 9400   0 error (1) .019 4.7 .18  0 error (1) .021 4.8 .14  0 error (1) .044 4.8 .12  0 error (1) .044 4.8 .13  0 unknown .12  41 1.2  0 error (1) .070 7.2 .31 0 unknown .055 7.2 .55 0 true 6.6 340 50 2 error (1) .050 5.3 .16 0 error (1) .058 5.3 .11 0
loop-acceleration/array_false-unreach-call3_true-termination.i true .92  79 12    2 true 15   930 93 2 error (42) .022  1.2  .057 0 unknown .0099 .85 .018  0 error (1) .42 40 4.1 0 error (1) .42 40 3.7 0 timeout 900   4500 10000 0 unknown 900    190 10000   0 error (1) .042 4.8 .095 0 error (1) .039 4.8 .15  0 error (1) .019 4.8 .16  0 error (1) .026 4.7 .077 0 unknown .14  41 1.5  0 error (1) .042 7.2 .42 0 unknown .055 7.2 .54 0 timeout 900   1200 12000 0 error (1) .025 5.4 .18 0 error (1) .052 5.4 .17 0
loop-acceleration/array_true-unreach-call1_true-termination.i true 1.2   97 15    2 true 7.7 490 58 2 error (42) .016  1.1  .040 0 unknown .010  .77 .013  0 error (1) .42 38 4.4 0 error (1) .40 37 3.2 0 timeout 900   4500 11000 0 unknown 1.2  56 15   0 error (1) .031 4.8 .10  0 error (1) .030 4.7 .16  0 error (1) .020 4.7 .17  0 error (1) .019 4.8 .082 0 unknown .15  40 1.2  0 error (1) .070 7.1 .35 0 unknown .060 7.1 .50 0 true 6.1 330 49 2 error (1) .028 5.4 .11 0 error (1) .049 5.3 .17 0
loop-acceleration/array_true-unreach-call2_true-termination.i true 1.8   160 18    2 true 10   760 81 2 error (42) .021  1.4  .040 0 unknown .0098 .73 .020  0 error (1) .43 37 4.2 0 error (1) .45 40 3.7 0 timeout 900   4500 11000 0 unknown 900    240 11000   0 error (1) .032 4.8 .13  0 error (1) .030 4.8 .11  0 error (1) .019 4.8 .15  0 error (1) .044 4.8 .099 0 unknown .15  41 1.1  0 error (1) .068 7.4 .33 0 unknown .077 7.1 .54 0 true 5.9 330 50 2 error (1) .052 5.5 .18 0 error (1) .025 5.3 .15 0
loop-acceleration/array_true-unreach-call3_true-termination.i true 1.0   79 11    2 true 14   800 110 2 error (42) .013  1.3  .055 0 unknown .010  .94 .020  0 error (1) .40 37 3.7 0 error (1) .43 37 3.8 0 timeout 900   4500 12000 0 unknown 890    180 8100   0 error (1) .044 4.8 .13  0 error (1) .020 4.7 .13  0 error (1) .042 4.8 .15  0 error (1) .021 4.9 .14  0 unknown .15  41 1.1  0 error (1) .060 7.1 .37 0 unknown .056 7.1 .55 0 timeout 900   1400 11000 0 error (1) .051 5.5 .18 0 error (1) .026 5.5 .18 0
loop-acceleration/array_true-unreach-call4_true-termination.i error (5) 1.7   81 15    0 error (1) 16   830 130 0 error (42) .021  1.3  .046 0 unknown .0090 .85 .028  0 error (1) .43 37 3.8 0 error (1) .41 40 4.0 0 timeout 900   4300 8700 0 unknown 890    250 11000   0 error (1) .042 4.8 .14  0 error (1) .021 4.8 .16  0 error (1) .021 4.7 .14  0 error (1) .020 4.8 .19  0 unknown .15  41 1.2  0 error (1) .041 7.4 .43 0 unknown .057 7.2 .65 0 timeout 900   1300 14000 0 error (1) .051 5.4 .16 0 error (1) .051 5.4 .15 0
loop-acceleration/diamond_true-unreach-call1_true-termination.i true .11  23 .91 2 error (1) 2.1 220 17 0 error (42) .016  1.2  .040 0 unknown .0089 1.0  .028  0 error (1) .39 39 3.6 0 error (1) .40 40 4.6 0 true 81   4000 900 2 unknown 120    55 1600   0 error (1) .019 4.8 .13  0 error (1) .043 4.8 .17  0 error (1) .045 4.9 .11  0 error (1) .021 4.8 .14  0 unknown .082 35 .62 0 error (1) .068 7.5 .34 0 unknown .053 7.3 .65 0 unknown 56   540 730 0 error (1) .051 5.3 .15 0 error (1) .051 5.4 .18 0
loop-acceleration/functions_false-unreach-call1_true-termination.i true .11  23 .94 2 error (1) 2.7 230 25 0 error (42) .019  1.6  .041 0 unknown .0088 1.0  .018  0 error (1) .41 40 4.1 0 error (1) .42 41 3.8 0 true 10   460 70 2 unknown 56    30 690   0 error (1) .021 4.9 .12  0 error (1) .020 4.8 .15  0 error (1) .018 4.7 .16  0 error (1) .019 4.8 .20  0 unknown .14  41 1.4  0 error (1) .066 7.3 .34 0 unknown .075 7.2 .53 0 unknown 69   830 770 0 error (1) .045 5.4 .18 0 error (1) .051 5.3 .19 0
loop-acceleration/functions_true-unreach-call1_true-termination.i true .11  24 .88 2 error (1) 2.7 240 27 0 error (42) .017  1.1  .036 0 unknown .010  1.1  .021  0 error (1) .40 38 3.3 0 error (1) .43 40 3.8 0 true 8.6 460 67 2 unknown 55    28 650   0 error (1) .019 4.8 .16  0 error (1) .044 4.8 .12  0 error (1) .018 4.8 .17  0 error (1) .020 4.8 .13  0 unknown .12  41 1.6  0 error (1) .040 7.4 .45 0 unknown .072 7.1 .58 0 unknown 67   840 600 0 error (1) .023 5.5 .22 0 error (1) .051 5.2 .14 0
loop-acceleration/multivar_false-unreach-call1_true-termination.i true .16  26 1.3  2 true 4.9 430 37 2 error (42) .017  1.1  .036 0 unknown .010  .93 .023  0 error (1) .43 37 3.6 0 error (1) .42 40 4.3 0 true 4.1 290 34 2 unknown .83 56 8.4 0 error (1) .019 4.8 .14  0 error (1) .042 4.7 .14  0 error (1) .030 4.8 .091 0 error (1) .044 4.7 .12  0 unknown .067 35 .60 0 error (1) .071 7.3 .34 0 unknown .054 7.3 .52 0 unknown 64   590 680 0 error (1) .032 5.5 .21 0 error (1) .048 5.4 .18 0
loop-acceleration/multivar_true-unreach-call1_true-termination.i true .15  26 1.2  2 true 4.8 370 39 2 error (42) .022  1.1  .029 0 unknown .0087 .76 .029  0 error (1) .42 37 4.3 0 error (1) .40 38 4.0 0 true 4.6 290 36 2 unknown 62    36 920   0 error (1) .041 4.8 .10  0 error (1) .017 4.8 .20  0 error (1) .044 4.7 .10  0 error (1) .021 4.8 .14  0 unknown .070 34 .52 0 error (1) .068 7.2 .32 0 unknown .052 7.1 .58 0 unknown 61   560 660 0 error (1) .053 5.4 .14 0 error (1) .041 5.3 .17 0
loop-acceleration/simple_false-unreach-call2_true-termination.i true .11  23 1.3  2 error (1) 2.2 190 21 0 error (42) .021  1.1  .047 0 unknown .0089 .92 .033  0 error (1) .42 37 4.2 0 error (1) .39 38 4.1 0 true 2.9 270 26 2 unknown .83 55 8.3 0 error (1) .044 4.7 .10  0 error (1) .026 4.7 .15  0 error (1) .019 4.8 .13  0 error (1) .044 4.8 .14  0 unknown .13  41 1.1  0 error (1) .061 7.2 .41 0 unknown .055 7.1 .53 0 unknown 51   550 640 0 error (1) .050 5.4 .15 0 error (1) .051 5.4 .15 0
loop-acceleration/simple_false-unreach-call3_true-termination.i true .14  23 .92 2 error (1) 2.0 220 16 0 error (42) .021  1.0  .041 0 unknown .010  .75 .017  0 error (1) .40 37 3.7 0 error (1) .42 38 3.2 0 true 3.9 280 34 2 unknown .81 55 8.7 0 error (1) .046 4.8 .11  0 error (1) .018 4.8 .072 0 error (1) .030 4.8 .11  0 error (1) .044 4.7 .13  0 unknown .15  41 1.3  0 error (1) .043 7.3 .39 0 unknown .076 7.3 .57 0 unknown 61   550 780 0 error (1) .051 5.3 .16 0 error (1) .031 5.4 .20 0
loop-acceleration/simple_true-unreach-call2_true-termination.i true .10  23 1.1  2 error (1) 1.8 190 14 0 error (42) .021  1.2  .055 0 unknown .0089 1.0  .024  0 error (1) .43 40 3.5 0 error (1) .41 38 3.6 0 true 2.9 280 29 2 unknown 1.2  56 14   0 error (1) .019 4.8 .15  0 error (1) .031 4.9 .11  0 error (1) .049 4.9 .11  0 error (1) .018 4.8 .14  0 unknown .15  41 1.3  0 error (1) .043 7.5 .35 0 unknown .082 7.3 .48 0 unknown 50   530 540 0 error (1) .054 5.4 .18 0 error (1) .019 5.3 .16 0
loop-acceleration/simple_true-unreach-call3_true-termination.i true .12  23 1.1  2 error (1) 2.2 220 21 0 error (42) .015  1.5  .034 0 unknown .010  1.1  .022  0 error (1) .41 37 3.6 0 error (1) .40 37 3.3 0 true 3.8 270 33 2 unknown 56    30 870   0 error (1) .022 4.9 .15  0 error (1) .045 4.8 .11  0 error (1) .018 4.8 .16  0 error (1) .030 4.7 .12  0 unknown .067 35 .60 0 error (1) .071 7.3 .28 0 unknown .081 7.3 .54 0 unknown 62   590 710 0 error (1) .049 5.4 .21 0 error (1) .024 5.4 .19 0
loop-acceleration/underapprox_false-unreach-call1_true-termination.i true .12  24 1.0  2 true 7.1 490 50 2 error (42) .012  1.2  .045 0 unknown .0092 .92 .018  0 error (1) .41 40 3.9 0 error (1) .38 38 3.7 0 true 8.1 440 72 2 unknown 3.8  56 42   0 error (1) .043 4.9 .13  0 error (1) .018 4.8 .15  0 error (1) .044 4.8 .098 0 error (1) .030 4.8 .11  0 unknown .13  41 1.3  0 error (1) .069 7.4 .33 0 unknown .074 7.2 .58 0 unknown 62   1000 630 0 error (1) .047 5.4 .14 0 error (1) .026 5.4 .24 0
loop-acceleration/underapprox_false-unreach-call2_true-termination.i false(termination) .12  23 1.0  -16 true 6.3 500 47 2 error (42) .012  1.4  .042 0 unknown .0090 .85 .029  0 error (1) .43 38 3.9 0 error (1) .41 40 4.7 0 true 7.7 450 69 2 unknown 3.8  55 43   0 error (1) .031 4.9 .11  0 error (1) .022 4.8 .20  0 error (1) .044 4.8 .12  0 error (1) .038 4.8 .12  0 unknown .14  41 1.6  0 error (1) .046 7.5 .37 0 unknown .081 7.3 .51 0 unknown 69   820 720 0 error (1) .046 5.3 .19 0 error (1) .024 5.4 .25 0
loop-acceleration/underapprox_true-unreach-call1_true-termination.i true .11  24 1.3  2 error (1) 3.1 280 27 0 error (42) .013  1.1  .042 0 unknown .0090 1.0  .027  0 error (1) .45 40 3.8 0 error (1) .41 37 3.7 0 true 9.2 470 70 2 unknown 3.6  56 50   0 error (1) .044 4.8 .12  0 error (1) .019 4.8 .11  0 error (1) .018 4.7 .16  0 error (1) .019 4.9 .14  0 unknown .14  41 1.3  0 error (1) .069 7.3 .28 0 unknown .057 7.2 .53 0 unknown 61   1000 680 0 error (1) .051 5.4 .17 0 error (1) .028 5.4 .18 0
loop-acceleration/underapprox_true-unreach-call2_true-termination.i true .11  26 1.4  2 true 6.8 500 52 2 error (42) .019  1.1  .046 0 unknown .010  .88 .018  0 error (1) .42 39 4.1 0 error (1) .42 40 4.4 0 true 8.7 450 71 2 unknown 1.2  56 13   0 error (1) .031 4.7 .16  0 error (1) .023 4.8 .15  0 error (1) .033 4.8 .12  0 error (1) .019 4.8 .13  0 unknown .12  41 1.4  0 error (1) .068 7.3 .31 0 unknown .081 7.1 .50 0 unknown 69   870 800 0 error (1) .055 5.3 .18 0 error (1) .049 5.5 .16 0
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i error (5) .45  32 4.9  0 false(termination) 80   5600 480 1 error (42) .012  1.1  .066 0 unknown .0074 .82 .022  0 error (1) .43 40 4.4 0 error (1) .43 40 3.7 0 false(termination) 11   470 79 1 unknown 900    120 13000   0 error (1) .021 4.8 .11  0 error (1) .020 4.8 .17  0 error (1) .039 4.8 .10  0 error (1) .020 4.7 .11  0 unknown .072 12 .26 0 error (1) .041 7.4 .40 0 unknown .075 7.2 .53 0 false(termination) 6.4 340 49 1 error (1) .051 5.4 .17 0 error (1) .051 5.4 .15 0
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i true .22  25 2.4  2 true 78   5100 780 2 error (42) .014  1.4  .049 0 unknown .0073 .88 .013  0 error (1) .40 37 3.7 0 error (1) .41 38 4.2 0 true 6.5 450 48 2 unknown 900    75 11000   0 error (1) .030 4.7 .14  0 error (1) .030 4.9 .11  0 error (1) .044 4.7 .15  0 error (1) .033 4.8 .18  0 unknown .063 12 .29 0 error (1) .063 7.3 .32 0 unknown .054 7.3 .65 0 true 6.7 340 47 2 error (1) .052 5.5 .13 0 error (1) .052 5.3 .17 0
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i true .098 23 1.1  2 true 11   760 70 2 error (42) .021  1.5  .040 0 unknown .011  .88 .025  0 error (1) .41 40 3.9 0 error (1) .43 38 3.8 0 true 5.5 340 49 2 unknown 88    66 1400   0 error (1) .019 4.8 .15  0 error (1) .020 4.8 .16  0 error (1) .033 4.8 .11  0 error (1) .021 4.8 .14  0 unknown .048 13 .28 0 error (1) .065 7.4 .42 0 unknown .082 7.2 .54 0 true 7.2 350 57 2 error (1) .027 5.4 .18 0 error (1) .026 5.3 .15 0
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i true .31  27 3.1  2 error (1) 7.6 660 62 0 error (42) .021  1.4  .049 0 unknown .0042 .92 .013  0 error (1) .42 40 4.2 0 error (1) .42 40 4.4 0 true 26   960 200 2 unknown 890    61 12000   0 error (1) .020 4.8 .17  0 error (1) .019 4.7 .13  0 error (1) .044 4.8 .15  0 error (1) .021 4.7 .11  0 unknown .046 13 .33 0 error (1) .070 7.3 .31 0 unknown .058 7.3 .56 0 true 8.0 390 65 2 error (1) .027 5.4 .18 0 error (1) .025 5.3 .16 0
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i true .16  26 1.1  2 timeout 900   3500 13000 0 error (42) .019  1.1  .038 0 unknown .0087 .89 .023  0 error (1) .42 40 4.0 0 error (1) .41 38 3.8 0 true 8.9 460 64 2 unknown 890    62 12000   0 error (1) .044 4.8 .11  0 error (1) .022 4.8 .13  0 error (1) .021 4.8 .13  0 error (1) .044 4.8 .11  0 unknown .066 12 .22 0 error (1) .070 7.5 .34 0 unknown .084 7.0 .48 0 true 7.2 370 52 2 error (1) .053 5.4 .13 0 error (1) .026 5.4 .18 0
loop-invgen/down_true-unreach-call_true-termination.i true .34  26 3.8  2 true 9.2 530 71 2 error (42) .017  1.0  .050 0 unknown .0075 .91 .018  0 error (1) .42 38 3.6 0 error (1) .39 37 3.6 0 true 6.2 390 50 2 unknown 120    65 1300   0 error (1) .019 4.9 .15  0 error (1) .020 4.8 .16  0 error (1) .044 4.9 .14  0 error (1) .020 4.8 .082 0 unknown .15  41 1.3  0 error (1) .044 7.4 .36 0 unknown .076 7.2 .51 0 true 7.0 350 61 2 error (1) .027 5.4 .17 0 error (1) .024 5.4 .16 0
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i true .50  33 5.2  2 true 64   3900 460 2 error (42) .012  .97 .052 0 unknown .0058 .79 .012  0 error (1) .43 37 3.9 0 error (1) .41 38 3.3 0 timeout 900   4400 11000 0 unknown 92    52 1200   0 error (1) .044 4.7 .14  0 error (1) .022 4.8 .15  0 error (1) .021 4.8 .12  0 error (1) .046 4.7 .12  0 unknown .12  41 1.4  0 error (1) .070 7.4 .31 0 unknown .082 7.2 .50 0 true 7.9 430 68 2 error (1) .046 5.2 .21 0 error (1) .050 5.5 .17 0
loop-invgen/half_2_true-unreach-call_true-termination.i true .26  26 2.6  2 true 30   1500 210 2 error (42) .022  1.5  .043 0 unknown .0089 .77 .022  0 error (1) .41 40 4.1 0 error (1) .43 38 3.8 0 true 8.3 480 67 2 unknown 160    69 1900   0 error (1) .036 4.8 .10  0 error (1) .046 4.7 .089 0 error (1) .022 4.8 .14  0 error (1) .021 4.8 .12  0 unknown .14  41 1.4  0 error (1) .047 7.3 .47 0 unknown .076 7.1 .57 0 true 7.6 420 61 2 error (1) .024 5.4 .18 0 error (1) .032 5.5 .20 0
loop-invgen/heapsort_true-unreach-call_true-termination.i true .59  33 6.5  2 error (1) 1.7 170 16 0 error (42) .016  1.3  .043 0 unknown .0073 .92 .018  0 error (1) .39 38 3.7 0 error (1) .44 38 4.3 0 true 37   1400 310 2 unknown 890    530 7900   0 error (1) .041 4.7 .12  0 error (1) .048 5.0 .11  0 error (1) .023 4.8 .15  0 error (1) .044 4.8 .14  0 unknown .14  41 1.4  0 error (1) .066 7.4 .32 0 unknown .074 7.1 .54 0 true 45   780 510 2 error (1) .048 5.4 .14 0 error (1) .043 5.3 .18 0
loop-invgen/id_build_true-unreach-call_true-termination.i true .15  24 1.2  2 error (1) 9.3 690 70 0 error (42) .014  1.3  .046 0 unknown .010  .76 .020  0 error (1) .42 37 3.6 0 error (1) .42 37 3.2 0 true 14   580 110 2 unknown 900    2700 11000   0 error (1) .022 4.8 .14  0 error (1) .019 4.8 .18  0 error (1) .019 4.7 .13  0 error (1) .020 4.8 .12  0 unknown .15  41 1.3  0 error (1) .068 7.3 .30 0 unknown .083 7.3 .51 0 true 780   2600 8100 2 error (1) .027 5.3 .12 0 error (1) .027 5.3 .17 0
loop-invgen/id_trans_false-unreach-call_true-termination.i true .15  24 1.1  2 true 17   1300 140 2 error (42) .0062 1.2  .062 0 unknown .0046 1.1  .020  0 error (1) .43 40 4.1 0 error (1) .41 37 3.8 0 true 31   1600 250 2 unknown .88 56 10   0 error (1) .021 4.8 .15  0 error (1) .021 4.8 .15  0 error (1) .024 4.9 .14  0 error (1) .018 4.8 .17  0 unknown .14  41 1.3  0 error (1) .039 7.1 .46 0 unknown .069 7.2 .48 0 true 21   970 200 2 error (1) .049 5.3 .17 0 error (1) .051 5.4 .14 0
loop-invgen/large_const_true-unreach-call_true-termination.i true .21  25 2.0  2 error (1) 1.7 170 16 0 error (42) .020  1.3  .032 0 unknown .0096 1.0  .022  0 error (1) .40 38 3.8 0 error (1) .44 40 4.2 0 true 6.8 450 53 2 unknown 1.6  56 20   0 error (1) .042 4.8 .12  0 error (1) .038 4.8 .11  0 error (1) .021 4.7 .090 0 error (1) .044 4.7 .11  0 unknown .14  40 1.5  0 error (1) .068 7.2 .30 0 unknown .083 7.2 .51 0 true 7.5 410 63 2 error (1) .051 5.4 .18 0 error (1) .051 5.4 .19 0
loop-invgen/nest-if3_true-unreach-call_true-termination.i true .34  26 3.6  2 true 42   4000 270 2 error (42) .012  1.4  .047 0 unknown .0088 .81 .018  0 error (1) .45 40 3.7 0 error (1) .43 40 3.8 0 true 8.1 460 60 2 unknown 900    310 7100   0 error (1) .021 4.8 .14  0 error (1) .020 4.7 .11  0 error (1) .044 4.8 .13  0 error (1) .044 4.7 .11  0 unknown .15  41 1.2  0 error (1) .061 7.3 .41 0 unknown .075 7.0 .56 0 true 8.6 450 62 2 error (1) .025 5.5 .25 0 error (1) .054 5.5 .18 0
loop-invgen/nested6_true-unreach-call_true-termination.i true .40  28 5.2  2 error (1) 26   2300 200 0 error (42) .022  1.5  .036 0 unknown .0081 .93 .032  0 error (1) .41 38 4.2 0 error (1) .40 38 3.5 0 true 20   640 160 2 unknown 900    2000 7600   0 error (1) .018 4.8 .17  0 error (1) .035 4.8 .14  0 error (1) .021 4.8 .12  0 error (1) .044 4.8 .16  0 unknown .068 13 .25 0 error (1) .059 7.3 .39 0 unknown .078 7.2 .56 0 true 11   490 89 2 error (1) .024 5.4 .22 0 error (1) .028 5.4 .18 0
loop-invgen/nested9_true-unreach-call_true-termination.i timeout 900     310 11000    0 timeout 900   5100 12000 0 error (42) .021  1.2  .053 0 unknown .0088 .78 .016  0 error (1) .43 40 4.2 0 error (1) .41 37 3.3 0 true 12   480 110 2 unknown 900    4200 9200   0 error (1) .022 4.9 .14  0 error (1) .019 4.8 .15  0 error (1) .044 4.8 .11  0 error (1) .019 4.8 .17  0 unknown .041 11 .39 0 error (1) .069 7.5 .33 0 unknown .072 7.2 .51 0 true 59   1900 750 2 error (1) .051 5.4 .18 0 error (1) .049 5.3 .20 0
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i true .17  24 1.5  2 timeout 900   3700 9900 0 error (42) .013  1.2  .057 0 unknown .0078 1.0  .026  0 error (1) .44 41 3.5 0 error (1) .42 40 3.9 0 true 11   570 81 2 unknown 230    82 3100   0 error (1) .030 4.7 .11  0 error (1) .017 4.8 .21  0 error (1) .030 4.7 .14  0 error (1) .021 4.8 .12  0 unknown .043 12 .35 0 error (1) .042 7.3 .43 0 unknown .076 7.2 .58 0 true 8.2 380 57 2 error (1) .051 5.4 .17 0 error (1) .052 5.4 .15 0
loop-invgen/seq_true-unreach-call_true-termination.i true .30  27 3.1  2 true 70   3700 700 2 error (42) .021  1.2  .039 0 unknown .010  .98 .021  0 error (1) .43 39 3.7 0 error (1) .42 37 3.7 0 true 8.4 480 62 2 unknown 900    74 11000   0 error (1) .021 4.8 .11  0 error (1) .020 4.8 .15  0 error (1) .022 4.8 .11  0 error (1) .018 4.8 .13  0 unknown .15  40 1.2  0 error (1) .045 7.4 .32 0 unknown .086 7.1 .49 0 true 11   420 92 2 error (1) .051 5.5 .18 0 error (1) .045 5.3 .18 0
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i false(termination) .12  23 .90 -16 error (1) 65   1900 380 0 error (42) .021  1.3  .048 0 unknown .0038 .66 .018  0 error (1) .43 38 3.8 0 error (1) .40 40 4.3 0 timeout 900   4000 11000 0 unknown 900    15000 11000   0 error (1) .040 4.9 .090 0 error (1) .030 4.7 .16  0 error (1) .032 4.8 .12  0 error (1) .019 4.8 .19  0 unknown .043 13 .31 0 error (1) .043 7.2 .38 0 unknown .084 7.2 .44 0 true 6.0 320 50 2 error (1) .033 5.3 .19 0 error (1) .027 5.4 .20 0
loop-invgen/up_true-unreach-call_true-termination.i true .23  29 2.1  2 true 14   1100 100 2 error (42) .022  1.2  .044 0 unknown .0094 .92 .026  0 error (1) .43 40 3.4 0 error (1) .43 40 4.3 0 true 6.3 390 51 2 unknown 100    69 1300   0 error (1) .018 4.7 .13  0 error (1) .031 4.7 .13  0 error (1) .041 4.8 .14  0 error (1) .042 4.8 .15  0 unknown .15  41 1.4  0 error (1) .042 7.3 .36 0 unknown .059 7.2 .55 0 true 6.8 350 58 2 error (1) .051 5.5 .17 0 error (1) .050 5.4 .14 0
loop-lit/afnp2014_true-unreach-call_true-termination.c.i true .23  25 2.2  2 true 11   750 79 2 error (42) .012  1.1  .039 0 unknown .0061 .82 .022  0 error (1) .40 37 3.5 0 error (1) .43 40 3.4 0 timeout 900   4500 9200 0 unknown 85    60 1100   0 error (1) .018 4.7 .16  0 error (1) .040 4.8 .11  0 error (1) .019 4.8 .17  0 error (1) .048 5.0 .15  0 unknown .13  41 1.5  0 error (1) .067 7.5 .37 0 unknown .081 7.2 .53 0 true 6.2 330 52 2 error (1) .024 5.4 .20 0 error (1) .043 5.5 .26 0
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i true .23  25 2.1  2 true 63   4000 590 2 error (42) .018  1.2  .035 0 unknown .0061 1.0  .033  0 error (1) .42 38 3.4 0 error (1) .40 37 3.8 0 true 4.9 310 40 2 unknown 890    37 13000   0 error (1) .020 4.7 .19  0 error (1) .019 4.9 .086 0 error (1) .020 4.8 .14  0 error (1) .018 4.8 .18  0 unknown .13  41 1.2  0 error (1) .067 7.3 .33 0 unknown .057 7.3 .56 0 true 6.5 330 54 2 error (1) .026 5.4 .18 0 error (1) .054 5.4 .17 0
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i true .14  23 1.3  2 true 4.9 400 36 2 error (42) .022  1.1  .040 0 unknown .0086 .95 .020  0 error (1) .41 39 3.6 0 error (1) .41 37 3.9 0 true 5.9 320 47 2 unknown 2.6  56 35   0 error (1) .044 4.8 .11  0 error (1) .032 4.8 .10  0 error (1) .019 4.8 .12  0 error (1) .022 4.9 .13  0 unknown .15  41 1.1  0 error (1) .044 7.3 .37 0 unknown .083 7.2 .50 0 true 6.7 340 48 2 error (1) .053 5.5 .17 0 error (1) .051 5.4 .19 0
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i true .22  25 2.1  2 true 11   770 92 2 error (42) .014  1.2  .042 0 unknown .0083 1.1  .022  0 error (1) .43 40 3.7 0 error (1) .41 37 4.0 0 true 4.4 300 37 2 unknown 100    49 1400   0 error (1) .020 4.7 .13  0 error (1) .020 4.7 .14  0 error (1) .030 4.7 .11  0 error (1) .021 4.8 .049 0 unknown .12  40 1.2  0 error (1) .061 7.4 .34 0 unknown .055 7.2 .51 0 true 6.9 350 56 2 error (1) .050 5.3 .15 0 error (1) .024 5.3 .19 0
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i true .21  26 2.4  2 true 8.7 580 62 2 error (42) .013  1.2  .043 0 unknown .0093 .92 .017  0 error (1) .41 37 3.8 0 error (1) .38 37 4.0 0 timeout 900   4100 6500 0 unknown 1.2  55 13   0 error (1) .044 4.8 .10  0 error (1) .020 4.7 .10  0 error (1) .018 4.8 .18  0 error (1) .034 4.7 .17  0 unknown .14  41 1.3  0 error (1) .068 7.2 .33 0 unknown .083 7.2 .54 0 true 9.1 470 68 2 error (1) .047 5.3 .17 0 error (1) .050 5.4 .18 0
loop-lit/css2003_true-unreach-call_true-termination.c.i timeout 900     250 9000    0 true 84   3600 870 2 error (42) .021  1.3  .041 0 unknown .0074 .88 .016  0 error (1) .44 41 4.3 0 error (1) .40 37 3.8 0 true 6.6 380 58 2 unknown 74    47 890   0 error (1) .040 4.8 .11  0 error (1) .031 4.7 .12  0 error (1) .021 4.8 .13  0 error (1) .021 4.8 .11  0 unknown .15  41 1.3  0 error (1) .070 7.2 .29 0 unknown .054 7.1 .58 0 true 6.5 330 49 2 error (1) .044 5.4 .19 0 error (1) .049 5.2 .14 0
loop-lit/gj2007_true-unreach-call_true-termination.c.i true .16  23 1.1  2 true 7.3 410 50 2 error (42) .012  1.3  .045 0 unknown .0071 .92 .028  0 error (1) .43 37 4.5 0 error (1) .40 37 3.9 0 timeout 900   4300 9700 0 unknown 70    50 1000   0 error (1) .041 4.9 .13  0 error (1) .041 4.8 .11  0 error (1) .030 4.8 .19  0 error (1) .046 4.9 .10  0 unknown .15  41 1.3  0 error (1) .066 7.2 .29 0 unknown .079 7.2 .50 0 true 7.1 340 51 2 error (1) .051 5.4 .16 0 error (1) .025 5.5 .20 0
loop-lit/gj2007b_true-unreach-call_true-termination.c.i true .19  24 1.8  2 true 21   1600 140 2 error (42) .014  1.2  .039 0 unknown .0088 .85 .019  0 error (1) .40 37 3.4 0 error (1) .41 38 3.4 0 true 4.2 280 35 2 unknown 95    42 1200   0 error (1) .022 4.8 .13  0 error (1) .020 4.8 .17  0 error (1) .033 4.8 .14  0 error (1) .037 4.8 .17  0 unknown .14  41 1.6  0 error (1) .066 7.2 .29 0 unknown .081 7.3 .50 0 true 7.7 360 61 2 error (1) .052 5.4 .15 0 error (1) .053 5.4 .15 0
loop-lit/gr2006_true-unreach-call_true-termination.c.i error (5) .45  31 4.9  0 true 8.0 500 59 2 error (42) .018  1.4  .034 0 unknown .0088 .90 .016  0 error (1) .40 37 3.9 0 error (1) .44 38 3.6 0 timeout 900   4000 10000 0 unknown 64    54 870   0 error (1) .019 4.7 .14  0 error (1) .042 4.9 .15  0 error (1) .017 4.8 .14  0 error (1) .044 4.7 .12  0 unknown .12  41 1.3  0 error (1) .066 7.3 .28 0 unknown .081 7.2 .51 0 true 7.8 450 67 2 error (1) .051 5.5 .16 0 error (1) .042 5.4 .20 0
loop-lit/gsv2008_true-unreach-call_true-termination.c.i error (5) .86  39 8.8  0 true 17   1400 120 2 error (42) .022  1.1  .038 0 unknown .0098 1.0  .027  0 error (1) .44 38 3.4 0 error (1) .41 37 3.7 0 unknown 11   590 85 0 unknown 120    51 1600   0 error (1) .021 4.8 .14  0 error (1) .018 4.7 .15  0 error (1) .045 4.7 .093 0 error (1) .038 4.9 .13  0 unknown .15  41 1.3  0 error (1) .069 7.3 .33 0 unknown .081 7.2 .49 0 true 7.9 330 70 2 error (1) .051 5.4 .17 0 error (1) .028 5.4 .18 0
loop-lit/hhk2008_true-unreach-call_true-termination.c.i true .22  24 2.3  2 true 7.6 520 51 2 error (42) .021  1.2  .043 0 unknown .0044 1.1  .017  0 error (1) .43 38 3.8 0 error (1) .41 37 4.2 0 true 4.2 290 32 2 unknown 900    42 10000   0 error (1) .032 4.9 .12  0 error (1) .027 4.9 .14  0 error (1) .044 4.8 .11  0 error (1) .021 4.8 .14  0 unknown .12  40 1.1  0 error (1) .046 7.5 .39 0 unknown .080 7.2 .43 0 true 6.1 330 53 2 error (1) .041 5.4 .19 0 error (1) .053 5.4 .16 0
loop-lit/jm2006_true-unreach-call_true-termination.c.i true .19  25 2.3  2 true 6.4 460 47 2 error (42) .015  1.3  .044 0 unknown .0089 .89 .021  0 error (1) .43 40 4.2 0 error (1) .43 40 4.2 0 true 5.5 350 47 2 unknown 95    34 1100   0 error (1) .019 4.7 .14  0 error (1) .041 4.9 .14  0 error (1) .022 4.9 .11  0 error (1) .043 4.8 .11  0 unknown .12  41 1.3  0 error (1) .068 7.3 .31 0 unknown .073 7.2 .52 0 true 7.5 400 58 2 error (1) .044 5.3 .19 0 error (1) .051 5.4 .17 0
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i true .29  28 2.8  2 true 13   820 100 2 error (42) .013  1.2  .039 0 unknown .0098 1.0  .021  0 error (1) .42 40 4.2 0 error (1) .40 38 4.1 0 true 4.8 290 37 2 unknown 96    40 1200   0 error (1) .045 4.7 .098 0 error (1) .044 4.9 .15  0 error (1) .020 4.7 .15  0 error (1) .020 4.8 .12  0 unknown .14  40 1.3  0 error (1) .069 7.2 .33 0 unknown .082 7.2 .59 0 true 8.3 440 62 2 error (1) .052 5.3 .13 0 error (1) .025 5.4 .15 0
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i true .27  26 2.8  2 error (1) 2.5 230 22 0 error (42) .021  1.2  .043 0 unknown .0030 1.0  .031  0 error (1) .40 37 3.3 0 error (1) .42 40 3.9 0 true 13   640 110 2 unknown 890    70 10000   0 error (1) .021 4.9 .090 0 error (1) .023 4.9 .14  0 error (1) .022 4.8 .13  0 error (1) .043 4.8 .13  0 unknown .073 34 .61 0 error (1) .070 7.5 .33 0 unknown .081 7.0 .46 0 true 10   500 79 2 error (1) .024 5.4 .28 0 error (1) .050 5.2 .14 0
loop-lit/gcnr2008_false-unreach-call_false-termination.i error (5) 1.5   46 17    0 timeout 900   3700 13000 0 error (42) .014  1.1  .036 0 unknown .0088 .65 .018  0 error (1) .45 40 3.8 0 error (1) .44 40 3.7 0 unknown 13   630 90 0 unknown .82 57 9.3 0 error (1) .022 4.9 .13  0 error (1) .020 4.7 .20  0 error (1) .023 4.9 .12  0 error (1) .020 5.0 .18  0 unknown .14  41 1.7  0 error (1) .070 7.4 .35 0 unknown .084 7.1 .46 0 false(termination) 27   520 270 1 error (1) .057 5.4 .16 0 error (1) .028 5.5 .18 0
loop-new/count_by_1_true-unreach-call_true-termination.i true .14  23 1.1  2 true 4.7 340 33 2 error (42) .020  1.2  .051 0 unknown .0099 .72 .022  0 error (1) .42 37 3.9 0 error (1) .41 40 4.0 0 timeout 900   4400 9400 0 unknown 1.2  55 13   0 error (1) .044 4.8 .11  0 error (1) .034 4.8 .12  0 error (1) .044 4.9 .098 0 error (1) .018 4.8 .15  0 unknown .13  41 1.3  0 error (1) .058 7.1 .34 0 unknown .056 7.2 .50 0 true 6.3 320 51 2 error (1) .052 5.4 .13 0 error (1) .050 5.5 .22 0
loop-new/count_by_1_variant_true-unreach-call_true-termination.i true .13  25 1.2  2 true 5.2 410 42 2 error (42) .017  1.2  .039 0 unknown .0087 1.0  .023  0 error (1) .43 37 3.9 0 error (1) .41 40 4.3 0 timeout 900   4300 9600 0 unknown 59    36 760   0 error (1) .019 4.8 .15  0 error (1) .021 4.8 .16  0 error (1) .018 4.7 .16  0 error (1) .039 4.9 .16  0 unknown .15  40 1.2  0 error (1) .057 7.2 .36 0 unknown .073 7.2 .53 0 true 6.5 330 48 2 error (1) .045 5.5 .19 0 error (1) .049 5.3 .19 0
loop-new/count_by_2_true-unreach-call_true-termination.i true .15  23 1.1  2 true 3.8 330 29 2 error (42) .019  1.2  .045 0 unknown .0070 .85 .015  0 error (1) .41 37 4.2 0 error (1) .40 39 4.1 0 timeout 900   4400 9100 0 unknown 57    30 690   0 error (1) .019 4.8 .16  0 error (1) .020 4.7 .12  0 error (1) .043 4.7 .12  0 error (1) .020 4.8 .15  0 unknown .15  41 1.2  0 error (1) .061 7.4 .35 0 unknown .074 7.2 .55 0 true 5.9 320 49 2 error (1) .048 5.4 .20 0 error (1) .027 5.4 .13 0
loop-new/count_by_k_true-unreach-call_true-termination.i error (5) .15  24 1.5  0 true 6.1 450 46 2 error (42) .019  1.1  .048 0 unknown .0095 .88 .021  0 error (1) .41 37 4.2 0 error (1) .44 40 3.9 0 unknown 3.3 280 32 0 unknown 77    35 1100   0 error (1) .044 4.8 .11  0 error (1) .042 4.9 .15  0 error (1) .044 4.9 .12  0 error (1) .046 4.8 .11  0 unknown .14  41 1.4  0 error (1) .062 7.3 .36 0 unknown .060 7.1 .55 0 true 32   440 420 2 error (1) .040 5.3 .15 0 error (1) .032 5.4 .18 0
loop-new/count_by_nondet_true-unreach-call_true-termination.i true .19  25 1.7  2 true 9.4 760 76 2 error (42) .021  1.4  .044 0 unknown .0068 .65 .018  0 error (1) .43 40 3.7 0 error (1) .40 37 3.6 0 true 4.7 300 37 2 unknown 900    160 9800   0 error (1) .022 4.8 .12  0 error (1) .020 4.8 .13  0 error (1) .031 4.8 .15  0 error (1) .038 4.9 .13  0 unknown .15  41 1.3  0 error (1) .070 7.2 .26 0 unknown .082 7.3 .48 0 true 19   400 220 2 error (1) .051 5.4 .16 0 error (1) .052 5.5 .18 0
loop-new/gauss_sum_true-unreach-call_true-termination.i true .16  26 1.5  2 true 23   2300 170 2 error (42) .017  1.1  .046 0 unknown .0080 .93 .025  0 error (1) .42 37 3.7 0 error (1) .41 37 4.1 0 true 4.5 300 41 2 unknown 70    51 1000   0 error (1) .018 4.8 .16  0 error (1) .025 4.8 .21  0 error (1) .020 4.7 .13  0 error (1) .019 4.7 .10  0 unknown .15  41 1.2  0 error (1) .069 7.1 .29 0 unknown .073 7.2 .43 0 true 6.2 330 52 2 error (1) .051 5.4 .16 0 error (1) .052 5.3 .15 0
loop-new/half_true-unreach-call_true-termination.i true .20  25 1.9  2 true 22   1800 140 2 error (42) .022  1.3  .040 0 unknown .0090 1.0  .028  0 error (1) .43 40 4.0 0 error (1) .42 37 4.0 0 true 80   3900 710 2 unknown 76    53 940   0 error (1) .021 4.8 .091 0 error (1) .020 4.8 .16  0 error (1) .019 4.7 .18  0 error (1) .018 4.9 .20  0 unknown .14  41 1.5  0 error (1) .069 7.6 .30 0 unknown .087 7.4 .46 0 true 7.1 340 61 2 error (1) .025 5.4 .20 0 error (1) .051 5.3 .18 0
loop-new/nested_true-unreach-call_true-termination.i true .27  26 3.3  2 true 31   3000 240 2 error (42) .022  1.1  .051 0 unknown .0044 1.0  .018  0 error (1) .44 39 4.1 0 error (1) .46 37 4.3 0 true 65   2500 610 2 unknown 900    640 6700   0 error (1) .019 4.7 .17  0 error (1) .022 4.7 .078 0 error (1) .031 4.8 .11  0 error (1) .043 4.8 .13  0 unknown .15  41 1.2  0 error (1) .044 7.2 .32 0 unknown .055 7.2 .59 0 true 7.9 440 58 2 error (1) .052 5.5 .19 0 error (1) .029 5.4 .20 0
product-lines/elevator_spec13_productSimulator_true-unreach-call_true-termination.cil.c error (5) 74     7000 610    0 timeout 900   3700 11000 0 error (42) .022  1.2  .034 0 unknown .011  1.0  .022  0 error (1) .41 37 3.5 0 error (1) .40 37 3.5 0 timeout 960   11000 5200 0 unknown 890    1100 10000   0 error (1) .044 4.8 .11  0 error (1) .022 4.8 .096 0 error (1) .036 4.8 .11  0 error (1) .045 4.8 .12  0 unknown .092 14 1.0  0 error (1) .061 7.5 .35 0 unknown .083 7.3 .74 0 timeout 910   13000 5500 0 error (1) .050 5.5 .23 0 error (1) .025 5.3 .19 0
product-lines/elevator_spec14_product03_true-unreach-call_true-termination.cil.c true 7.4   570 76    2 timeout 900   3700 11000 0 error (42) .021  1.2  .039 0 unknown .0090 .89 .016  0 error (1) .44 38 3.7 0 error (1) .44 41 4.0 0 timeout 900   4200 9600 0 unknown 56    130 780   0 error (1) .023 4.7 .14  0 error (1) .045 4.7 .14  0 error (1) .017 4.7 .17  0 error (1) .018 4.8 .12  0 unknown .075 14 1.0  0 error (1) .041 7.2 .40 0 unknown .065 7.3 .71 0 true 98   4800 760 2 error (1) .028 5.4 .19 0 error (1) .022 5.4 .26 0
product-lines/elevator_spec14_product11_true-unreach-call_true-termination.cil.c true 8.5   660 93    2 timeout 900   3500 11000 0 error (42) .012  1.3  .039 0 unknown .0089 .77 .027  0 error (1) .41 40 4.0 0 error (1) .42 37 4.1 0 timeout 910   4200 11000 0 unknown 61    150 840   0 error (1) .043 4.8 .13  0 error (1) .029 4.7 .092 0 error (1) .031 4.7 .14  0 error (1) .020 4.8 .17  0 unknown .085 14 .78 0 error (1) .066 7.1 .31 0 unknown .064 7.2 .62 0 timeout 910   13000 5500 0 error (1) .049 5.4 .16 0 error (1) .044 5.5 .23 0
product-lines/elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 7.6   640 82    2 timeout 900   3700 14000 0 error (42) .021  1.1  .049 0 unknown .0093 1.0  .022  0 error (1) .44 40 4.0 0 error (1) .45 41 3.9 0 timeout 910   3900 12000 0 unknown 61    150 890   0 error (1) .019 4.8 .16  0 error (1) .019 4.8 .13  0 error (1) .045 4.8 .13  0 error (1) .022 4.9 .15  0 unknown .10  14 .86 0 error (1) .066 7.4 .34 0 unknown .079 7.2 .59 0 true 110   5600 790 2 error (1) .046 5.4 .15 0 error (1) .028 5.3 .17 0
product-lines/elevator_spec14_product20_false-unreach-call_true-termination.cil.c false(termination) 5.7   1100 48    -16 timeout 900   3500 13000 0 error (42) .020  1.3  .042 0 unknown .010  .98 .030  0 error (1) .41 37 3.8 0 error (1) .41 37 3.4 0 timeout 900   3900 10000 0 unknown 1.2  56 11   0 error (1) .021 4.8 .14  0 error (1) .019 4.7 .16  0 error (1) .044 4.7 .10  0 error (1) .019 4.9 .21  0 unknown .082 14 .77 0 error (1) .068 7.4 .31 0 unknown .082 7.3 .65 0 true 76   3000 640 2 error (1) .050 5.3 .13 0 error (1) .051 5.4 .16 0
product-lines/elevator_spec14_product23_true-unreach-call_true-termination.cil.c true 8.5   1000 90    2 timeout 900   3500 11000 0 error (42) .021  1.5  .049 0 unknown .010  .72 .018  0 error (1) .43 37 3.4 0 error (1) .43 37 4.3 0 timeout 910   4200 12000 0 unknown 170    270 2100   0 error (1) .044 4.8 .13  0 error (1) .022 4.8 .14  0 error (1) .039 4.8 .11  0 error (1) .021 4.7 .14  0 unknown .080 14 .85 0 error (1) .066 7.2 .35 0 unknown .093 7.1 .65 0 timeout 910   13000 5500 0 error (1) .027 5.4 .20 0 error (1) .025 5.5 .19 0
product-lines/elevator_spec14_product24_false-unreach-call_true-termination.cil.c false(termination) 9.7   1900 92    -16 timeout 900   3700 12000 0 error (42) .012  1.1  .048 0 unknown .0043 .92 .017  0 error (1) .40 38 3.8 0 error (1) .45 40 4.0 0 timeout 910   4100 9700 0 unknown 1.2  57 15   0 error (1) .031 4.8 .16  0 error (1) .021 4.8 .086 0 error (1) .039 4.8 .15  0 error (1) .045 4.8 .12  0 unknown .10  14 .75 0 error (1) .069 7.3 .29 0 unknown .091 7.2 .58 0 true 66   4000 670 2 error (1) .025 5.4 .21 0 error (1) .051 5.4 .17 0
product-lines/elevator_spec14_product27_true-unreach-call_true-termination.cil.c true 8.2   690 89    2 timeout 900   5100 11000 0 error (42) .018  1.2  .039 0 unknown .0092 .87 .020  0 error (1) .42 40 3.6 0 error (1) .40 40 3.8 0 timeout 910   3900 9900 0 unknown 65    170 760   0 error (1) .044 4.8 .13  0 error (1) .023 4.8 .14  0 error (1) .021 4.8 .10  0 error (1) .019 4.7 .15  0 unknown .080 14 .85 0 error (1) .066 7.6 .33 0 unknown .064 7.2 .59 0 true 140   6600 930 2 error (1) .040 5.3 .22 0 error (1) .025 5.4 .21 0
product-lines/elevator_spec14_product28_false-unreach-call_true-termination.cil.c false(termination) 5.8   1200 52    -16 timeout 900   3700 11000 0 error (42) .012  1.2  .041 0 unknown .0097 1.0  .018  0 error (1) .43 37 4.0 0 error (1) .44 40 3.8 0 timeout 910   4000 13000 0 unknown 1.2  57 15   0 error (1) .021 4.8 .11  0 error (1) .030 4.8 .12  0 error (1) .020 4.8 .11  0 error (1) .033 4.8 .16  0 unknown .077 14 .99 0 error (1) .069 7.3 .32 0 unknown .089 7.1 .61 0 true 71   3000 570 2 error (1) .028 5.4 .18 0 error (1) .038 5.2 .14 0
product-lines/elevator_spec14_product31_true-unreach-call_true-termination.cil.c true 8.9   1000 100    2 timeout 900   3500 10000 0 error (42) .013  1.4  .042 0 unknown .0092 1.1  .022  0 error (1) .40 38 3.4 0 error (1) .40 38 3.8 0 timeout 910   4200 11000 0 unknown 180    290 2200   0 error (1) .030 4.8 .11  0 error (1) .036 4.8 .12  0 error (1) .018 4.7 .15  0 error (1) .022 4.8 .12  0 unknown .083 14 .81 0 error (1) .060 7.5 .37 0 unknown .090 7.3 .68 0 true 160   6900 1200 2 error (1) .026 5.2 .18 0 error (1) .050 5.4 .19 0
product-lines/elevator_spec14_product32_false-unreach-call_true-termination.cil.c false(termination) 10     2000 98    -16 timeout 900   3700 12000 0 error (42) .021  1.1  .049 0 unknown .0092 .96 .016  0 error (1) .42 37 3.5 0 error (1) .43 40 4.2 0 timeout 900   3900 9400 0 unknown 1.2  56 14   0 error (1) .044 4.7 .11  0 error (1) .022 4.7 .085 0 error (1) .042 4.7 .14  0 error (1) .044 4.8 .12  0 unknown .086 14 .72 0 error (1) .068 7.2 .35 0 unknown .091 7.3 .63 0 true 87   4500 650 2 error (1) .051 5.4 .19 0 error (1) .027 5.4 .17 0
product-lines/elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c true 59     6600 490    2 timeout 900   3700 12000 0 error (42) .019  1.3  .043 0 unknown .0099 .63 .019  0 error (1) .40 38 3.5 0 error (1) .41 38 4.0 0 timeout 910   4400 12000 0 unknown 50    300 730   0 error (1) .040 4.8 .14  0 error (1) .018 4.7 .18  0 error (1) .021 4.8 .11  0 error (1) .022 4.8 .13  0 unknown .095 14 .92 0 error (1) .043 7.4 .41 0 unknown .063 7.3 .64 0 true 260   7100 2200 2 error (1) .051 5.4 .16 0 error (1) .026 5.3 .18 0
product-lines/elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 8.0   330 94    2 timeout 900   3700 10000 0 error (42) .021  1.1  .054 0 unknown .010  .94 .020  0 error (1) .42 40 3.8 0 error (1) .39 38 3.4 0 timeout 910   3500 13000 0 unknown 54    130 640   0 error (1) .019 4.8 .14  0 error (1) .043 4.8 .12  0 error (1) .023 4.9 .18  0 error (1) .019 4.8 .087 0 unknown .084 14 .83 0 error (1) .069 7.5 .33 0 unknown .088 7.3 .53 0 timeout 910   14000 4300 0 error (1) .025 5.3 .24 0 error (1) .024 5.3 .19 0
product-lines/elevator_spec1_product03_true-unreach-call_true-termination.cil.c true 10     370 110    2 timeout 900   3700 11000 0 error (42) .021  1.0  .042 0 unknown .0033 .92 .023  0 error (1) .41 38 3.6 0 error (1) .43 39 3.4 0 timeout 910   4100 13000 0 unknown 58    140 630   0 error (1) .024 4.9 .14  0 error (1) .028 4.9 .17  0 error (1) .044 4.9 .12  0 error (1) .022 4.8 .11  0 unknown .084 14 .77 0 error (1) .063 7.2 .36 0 unknown .064 7.3 .68 0 true 550   9500 3600 2 error (1) .051 5.4 .16 0 error (1) .040 5.4 .24 0
product-lines/elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 8.1   340 90    2 timeout 900   3700 11000 0 error (42) .021  1.2  .043 0 unknown .0092 .92 .026  0 error (1) .42 38 4.3 0 error (1) .40 38 4.0 0 timeout 910   3000 11000 0 unknown 57    140 890   0 error (1) .045 4.8 .12  0 error (1) .022 4.8 .11  0 error (1) .044 4.8 .13  0 error (1) .018 4.8 .18  0 unknown .10  14 .80 0 error (1) .033 7.3 .43 0 unknown .089 7.3 .69 0 timeout 900   13000 4800 0 error (1) .024 5.5 .15 0