Tool 2LS 0.3.4 BLAST 2.7.3 CBMC CPAchecker 1.4-svcomp16c CPAchecker 1.4-svn 18373 CPAchecker 1.4-svcomp16c ESBMC ESBMC version 2.0.0 64-bit x86_64 linux DepthK ESBMC+DepthK version 2.1 Forest svc_16_20151108 impara 0.45 CPAchecker 1.4-svn 18356M SeaHorn-F16 0.1.0 skink SMACK+Corral 1.5.2 symbiotic 3.0.1 ULTIMATE Automizer cfb9fd9e ULTIMATE Kojak fd30d3d8 VVT prerelease
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24] [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23] [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24]
OS Linux 4.2.0-22-generic Linux 4.2.0-23-generic Linux 4.2.0-22-generic Linux 4.2.0-23-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135149 MB
Date of execution 2016-01-02 22:42:27 CET [[ 2016-01-15 08:01:51 CET ]] [[ 2016-01-15 21:37:22 CET ]] 2016-01-03 17:36:26 CET [[ 2016-01-15 08:15:11 CET ]] [[ 2016-01-15 21:49:51 CET ]] 2016-01-03 00:42:25 CET [[ 2016-01-15 08:22:02 CET ]] [[ 2016-01-15 21:54:19 CET ]] 2016-01-04 06:25:51 CET [[ 2016-01-15 08:31:02 CET ]] [[ 2016-01-15 21:59:57 CET ]] 2016-01-04 01:42:53 CET [[ 2016-01-15 08:36:34 CET ]] [[ 2016-01-15 22:02:40 CET ]] 2016-01-04 20:04:07 CET [[ 2016-01-15 08:41:31 CET ]] [[ 2016-01-15 22:05:37 CET ]] 2016-01-04 13:17:38 CET [[ 2016-01-15 08:48:20 CET ]] [[ 2016-01-15 22:10:37 CET ]] 2016-01-16 17:45:19 CET [[ 2016-01-17 00:36:28 CET ]] [[ 2016-01-17 00:39:38 CET ]] 2016-01-05 14:06:34 CET [[ 2016-01-15 09:00:06 CET ]] [[ 2016-01-15 22:17:52 CET ]] 2016-01-09 23:49:59 CET [[ 2016-01-15 09:05:13 CET ]] [[ 2016-01-15 22:20:31 CET ]] 2016-01-13 07:41:14 CET [[ 2016-01-15 09:11:00 CET ]] [[ 2016-01-15 22:23:23 CET ]] 2016-01-10 22:01:17 CET [[ 2016-01-15 09:16:15 CET ]] [[ 2016-01-15 22:26:01 CET ]] 2016-01-11 21:35:00 [[ 2016-01-15 18:20:27 CET ]] [[ 2016-01-15 22:30:28 CET ]] 2016-01-15 22:52:00 CET [[ 2016-01-16 00:34:30 CET ]] [[ 2016-01-16 00:56:26 CET ]] 2016-01-07 09:05:16 CET [[ 2016-01-15 09:34:34 CET ]] [[ 2016-01-15 22:36:10 CET ]] 2016-01-07 09:04:54 CET [[ 2016-01-15 09:39:10 CET ]] [[ 2016-01-15 22:39:28 CET ]] 2016-01-14 23:51:13 CET [[ 2016-01-15 09:43:48 CET ]] [[ 2016-01-15 22:41:15 CET ]] 2016-01-08 15:10:30 CET [[ 2016-01-15 09:49:48 CET ]] [[ 2016-01-15 22:43:29 CET ]] 2016-01-17 23:14:00 CET [[ 2016-01-18 06:54:01 CET ]] [[ 2016-01-18 07:05:55 CET ]]
Run set 2ls.sv-comp16.Loops blast.sv-comp16.Loops cbmc.sv-comp16.Loops cpa-bam.sv-comp16.Loops cpa-kind.sv-comp16.Loops cpa-refsel.sv-comp16.Loops cpa-seq.sv-comp16.Loops esbmc.sv-comp16.Loops esbmcdepthk.sv-comp16.Loops forest.sv-comp16.Loops impara.sv-comp16.Loops lpi.sv-comp16.Loops seahorn.sv-comp16.Loops skink.sv-comp16.Loops smack.sv-comp16.Loops symbiotic3.sv-comp16.Loops uautomizer.sv-comp16.Loops ukojak.sv-comp16.Loops vvt.sv-comp16.Loops
Options --k-induction --competition-mode --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/2ls.2016-01-02_2242.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/2ls.2016-01-02_2242.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -alias empty -enable-recursion -noprofile -cref -sv-comp -lattice -include-lattice symb -nosserr -svcomp-witness error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/blast.2016-01-03_1736.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/blast.2016-01-03_1736.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16-bam -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-bam.2016-01-04_0625.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-bam.2016-01-04_0625.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16--k-induction -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-kind.2016-01-04_0142.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-kind.2016-01-04_0142.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16--refsel -disable-java-assertions -heap 12500m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-refsel.2016-01-04_2004.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-refsel.2016-01-04_2004.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16 -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-seq.2016-01-04_1317.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-seq.2016-01-04_1317.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/esbmc.2016-01-16_1745.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/esbmc.2016-01-16_1745.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/esbmcdepthk.2016-01-05_1406.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/esbmcdepthk.2016-01-05_1406.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -svcomp [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/forest.2016-01-09_2349.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/forest.2016-01-09_2349.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] --eager --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/impara.2016-01-13_0741.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/impara.2016-01-13_0741.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -lpi-svcomp16 -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/lpi.2016-01-10_2201.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/lpi.2016-01-10_2201.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] --cex=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/seahorn.2016-01-11_2135.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/seahorn.2016-01-11_2135.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/skink.2016-01-15_2252.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/skink.2016-01-15_2252.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -w error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/smack.2016-01-07_0905.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/smack.2016-01-07_0905.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/symbiotic3.2016-01-07_0904.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/symbiotic3.2016-01-07_0904.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/uautomizer.2016-01-14_2351.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/uautomizer.2016-01-14_2351.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/ukojak.2016-01-08_1510.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/ukojak.2016-01-08_1510.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/vvt.2016-01-17_2314.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/vvt.2016-01-17_2314.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/ status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB)
loops/array_false-unreach-call.i false(reach) .099 24 false(reach) .54  24   false(reach) .11  24 false(reach) 4.3 240 false(reach) 5.7 360 false(reach) 4.7 250 false(reach) 3.8 210 false(reach) 23     600 false(reach) 3.3  160 unknown .48  38   false(reach) .12  25 false(reach) 6.7 310 false(reach) .21 37 witness unconfirmed 11   470 false(reach) 3.1 73 witness unconfirmed 18     6.5 false(reach) 9.1 330 false(reach) 9.1 320 witness unconfirmed .12  14  
loops/bubble_sort_false-unreach-call.i false(reach) .74  94 exception (gremlins) .034 24   witness unconfirmed 1.9   130 false(reach) 6.8 370 false(reach) 17   500 false(reach) 8.9 430 false(reach) 110   3200 out of memory 170     15000 false(reach) 9.8  230 unknown .17  4.8 invalid output .70  31 false(reach) 14   430 error (245) .53 56 unknown 54   1300 witness unconfirmed 4.6 91 false(reach) 18     33   error 9.6 340 error 8.7 320 unknown 13     51  
loops/count_up_down_false-unreach-call_true-termination.i false(reach) .10  23 false(reach) .072 18   false(reach) .11  24 false(reach) 3.8 230 false(reach) 4.9 320 false(reach) 3.9 230 false(reach) 3.1 210 witness timeout 4.5   230 false(reach) 3.1  160 unknown .27  7.4 false(reach) .11  23 false(reach) 4.6 310 false(reach) .27 37 witness timeout 8.3 330 false(reach) 3.3 75 false(reach) .21  6.7 false(reach) 7.8 310 false(reach) 9.2 330 witness unconfirmed .16  12  
loops/eureka_01_false-unreach-call.i witness timeout 1.8   60 witness timeout 5.3   39   false(reach) .40  29 timeout 900   920 timeout 900   5900 timeout 900   800 timeout 900   4900 witness timeout 800     4100 witness timeout 4.2  170 unknown .51  38   false(reach) 240     54 timeout 900   7200 witness timeout .67 63 unknown 14   640 false(reach) 3.8 91 witness timeout 790     11   false(reach) 120   1000 timeout 130   1800 unknown .069 9.5
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(reach) .32  26 false(reach) .96  28   false(reach) .12  24 false(reach) 3.8 240 false(reach) 6.8 350 false(reach) 4.7 240 false(reach) 6.6 410 error (1) 100     1300 false(reach) 3.4  170 unknown .55  38   false(reach) .17  23 false(reach) 6.3 320 false(reach) .29 40 witness timeout 10   450 false(reach) 3.2 78 false(reach) 18     6.6 false(reach) 9.8 320 false(reach) 11   340 witness unconfirmed .13  16  
loops/insertion_sort_false-unreach-call.i witness timeout 520     7700 witness timeout 4.0   26   false(reach) 3.3   270 timeout 900   850 exception 58   1900 error 4.3 230 exception 57   1700 unknown 890     800 witness timeout 620    310 true .65  39   witness timeout 180     150 exception 26   650 witness timeout .52 49 unknown 11   450 false(reach) 3.9 81 unknown .11  7.1 false(reach) 86   940 false(reach) 33   570 true 15     62  
loops/invert_string_false-unreach-call.i false(reach) 1.3   52 false(reach) 1.3   28   false(reach) .60  39 timeout 900   1200 false(reach) 25   890 error 14   470 false(reach) 24   870 error (1) 130     4400 witness timeout 4.4  160 true .88  38   false(reach) .71  26 false(reach) 16   450 witness timeout .32 43 witness timeout 14   710 false(reach) 3.5 80 unknown .23  6.9 false(reach) 19   370 false(reach) 15   470 witness unconfirmed .25  17  
loops/linear_search_false-unreach-call.i false(reach) 1.9   79 witness unconfirmed .13  20   witness invalid (exception) .86  28 witness unconfirmed 6.4 330 unknown 6.2 380 false(reach) 6.1 260 unknown 10   430 false(reach) 19     600 false(reach) 3.3  170 unknown .58  38   witness unconfirmed 5.3   38 unknown 6.2 320 false(reach) .30 40 unknown 7.8 330 false(reach) 24   100 unknown .14  7.0 error 190   430 error 770   650 unknown .068 11  
loops/ludcmp_false-unreach-call.i timeout 900     4200 witness unconfirmed 1.9   33   witness unconfirmed 2.3   170 witness timeout 490   1200 timeout 900   4100 witness timeout 41   1400 witness timeout 39   1300 error (1) 120     8800 unknown .25 23 witness timeout 1.1   41   witness unconfirmed 6.7   990 timeout 910   6200 witness unconfirmed .30 33 unknown 3.3 180 witness timeout 98   580 witness timeout 18     6.7 error 43   7100 error 55   7100 unknown .075 12  
loops/matrix_false-unreach-call_true-termination.i false(reach) 140     2500 exception (gremlins) .031 9.3 false(reach) .19  26 false(reach) 18   870 false(reach) 57   3700 false(reach) 11   430 false(reach) 150   2600 unknown 900     9700 witness timeout 3.7  170 unknown .51  38   false(reach) .32  24 false(reach) 15   670 witness timeout .47 48 unknown 8.1 340 false(reach) 3.4 76 unknown .16  7.0 false(reach) 9.5 330 false(reach) 12   330 witness unconfirmed .27  17  
loops/n.c24_false-unreach-call.i timeout 900     1800 timeout 670     230   out of memory 310     15000 out of memory 740   15000 timeout 900   4700 timeout 900   4800 timeout 900   4700 out of memory 340     15000 true .65 26 true .91  39   timeout 900     140 timeout 900   5800 timeout 900    680 unknown 9.7 440 true 880   4000 timeout 900     23   timeout 900   1200 timeout 59   1400 unknown .092 10  
loops/nec11_false-unreach-call.i false(reach) .11  23 false(reach) .071 18   false(reach) .17  24 false(reach) 3.3 230 false(reach) 5.9 330 false(reach) 3.9 240 false(reach) 3.7 210 false(reach) 4.1   220 false(reach) 2.6  160 false(reach) .73  38   false(reach) .10  23 false(reach) 5.2 310 witness unconfirmed .27 34 witness unconfirmed 8.3 340 false(reach) 3.2 77 false(reach) .13  6.6 false(reach) 9.0 340 false(reach) 8.8 320 witness unconfirmed .11  14  
loops/nec20_false-unreach-call.i false(reach) 1.5   73 false(reach) .29  24   false(reach) .38  40 witness timeout 3.8 230 false(reach) 6.6 360 false(reach) 3.6 230 false(reach) 3.2 210 witness timeout 5.3   250 false(reach) 3.0  160 unknown .62  38   false(reach) .38  49 false(reach) 6.5 340 false(reach) .28 37 unknown 45   1100 false(reach) 3.4 78 false(reach) .14  6.8 false(reach) 8.1 320 false(reach) 9.1 330 timeout 900     490  
loops/s3_false-unreach-call.i witness unconfirmed 560     1100 witness unconfirmed 19     48   witness invalid (assertion) 27     1100 false(reach) 21   820 out of memory 110   15000 timeout 900   1400 out of memory 210   15000 witness unconfirmed 470     4300 unknown 890    3400 unknown .29  5.7 error (8) 7.1   33 out of memory 96   15000 false(reach) 3.1  75 unknown 11   460 witness unconfirmed 16   200 unknown .85  20   unknown 270   930 timeout 39   710 unknown .15  17  
loops/string_false-unreach-call.i false(reach) 3.2   65 false(reach) 1.4   28   false(reach) .31  25 timeout 900   1100 witness unconfirmed 140   4100 false(reach) 5.0 280 false(reach) 5.2 240 false(reach) 20     660 false(reach) 5.0  170 true .63  38   false(reach) .52  25 witness unconfirmed 48   1100 false(reach) .33 47 unknown 8.7 370 false(reach) 3.6 83 false(reach) 140     7.1 false(reach) 22   400 false(reach) 23   380 unknown .12  9.4
loops/sum01_bug02_false-unreach-call_true-termination.i false(reach) 1.3   41 false(reach) 26     46   false(reach) .45  24 false(reach) 7.2 350 false(reach) 8.9 400 false(reach) 6.5 270 false(reach) 9.8 430 error (1) 16     560 false(reach) 5.1  160 false(reach) 3.1   38   false(reach) .59  23 false(reach) 7.1 330 false(reach) .49 42 witness timeout 16   760 false(reach) 3.4 75 false(reach) 120     6.7 false(reach) 16   480 false(reach) 16   430 witness unconfirmed .17  22  
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(reach) .56  31 false(reach) 12     34   false(reach) .17  24 false(reach) 5.3 250 false(reach) 6.2 350 false(reach) 4.3 250 false(reach) 7.7 410 error (1) 15     490 false(reach) 4.5  170 false(reach) 2.2   41   false(reach) .21  23 false(reach) 6.3 320 false(reach) .37 41 witness timeout 14   590 false(reach) 3.3 75 false(reach) 36     6.8 false(reach) 11   360 false(reach) 9.9 330 witness unconfirmed .15  20  
loops/sum01_false-unreach-call_true-termination.i false(reach) 1.2   37 false(reach) 44     46   false(reach) .38  24 false(reach) 7.6 420 false(reach) 9.6 430 false(reach) 7.8 340 false(reach) 10   430 error (1) 15     480 false(reach) 6.3  160 unknown .57  38   false(reach) .42  23 false(reach) 8.1 340 false(reach) .51 42 witness timeout 23   880 false(reach) 3.3 83 false(reach) 190     6.7 false(reach) 18   470 false(reach) 15   340 witness unconfirmed .22  27  
loops/sum03_false-unreach-call_true-termination.i false(reach) .81  36 false(reach) 4.6   37   false(reach) .47  24 false(reach) 7.5 390 false(reach) 12   490 false(reach) 5.5 280 false(reach) 5.9 240 error (1) 12     400 witness timeout 3.4  160 unknown .45  38   false(reach) .25  23 false(reach) 10   360 false(reach) .49 42 witness unconfirmed 55   1300 false(reach) 3.6 78 false(reach) 19     6.7 false(reach) 19   470 false(reach) 25   510 witness unconfirmed .23  28  
loops/sum04_false-unreach-call_true-termination.i false(reach) .91  36 false(reach) 1.1   27   false(reach) .38  24 false(reach) 4.7 240 false(reach) 8.1 390 false(reach) 4.0 230 false(reach) 4.0 210 false(reach) 5.0   240 false(reach) 5.5  170 false(reach) .64  38   false(reach) .15  27 false(reach) 7.1 330 witness unconfirmed .26 34 witness unconfirmed 18   750 witness unconfirmed 2.8 74 false(reach) 18     6.7 false(reach) 10   330 false(reach) 11   320 unknown .064 8.1
loops/sum_array_false-unreach-call.i false(reach) .57  47 false(reach) .72  29   false(reach) .14  25 false(reach) 6.4 290 false(reach) 22   1000 false(reach) 4.7 260 false(reach) 24   980 error (1) 120     4000 witness timeout 3.7  160 unknown .64  36   false(reach) .34  24 false(reach) 13   390 witness timeout .45 51 witness timeout 13   670 false(reach) 3.5 76 unknown .24  7.0 false(reach) 9.7 330 false(reach) 23   330 witness unconfirmed .18  21  
loops/terminator_01_false-unreach-call_false-termination.i false(reach) .15  23 false(reach) .12  15   false(reach) .16  24 false(reach) 4.0 230 false(reach) 5.6 330 false(reach) 3.9 230 false(reach) 3.7 210 false(reach) 4.1   220 false(reach) 3.0  160 false(reach) .54  38   false(reach) .10  23 false(reach) 5.5 320 witness unconfirmed .16 34 witness unconfirmed 8.9 320 false(reach) 2.8 74 false(reach) .22  8.2 false(reach) 8.7 320 false(reach) 9.4 340 witness unconfirmed .097 14  
loops/terminator_02_false-unreach-call_true-termination.i false(reach) .11  23 false(reach) .093 15   false(reach) .12  24 false(reach) 3.4 230 false(reach) 5.7 340 false(reach) 3.3 230 false(reach) 3.6 210 false(reach) 4.7   230 false(reach) 3.0  160 true .61  38   false(reach) .084 23 false(reach) 4.7 320 false(reach) .22 39 witness unconfirmed 10   340 false(reach) 3.0 73 false(reach) .21  6.6 false(reach) 8.2 330 false(reach) 8.7 320 witness unconfirmed .11  14  
loops/terminator_03_false-unreach-call_true-termination.i false(reach) .083 23 false(reach) .22  21   false(reach) .14  24 false(reach) 3.5 230 false(reach) 6.1 340 false(reach) 4.3 240 false(reach) 7.5 390 false(reach) 16     540 false(reach) 2.9  160 error (139) .92  38   false(reach) .093 23 false(reach) 4.9 320 false(reach) .30 39 witness unconfirmed 9.4 390 false(reach) 2.5 72 false(reach) .14  7.1 false(reach) 9.0 330 false(reach) 9.1 320 witness unconfirmed .10  14  
loops/trex01_false-unreach-call_true-termination.i false(reach) .12  24 false(reach) .12  20   false(reach) .14  24 false(reach) 4.2 230 false(reach) 6.3 340 false(reach) 4.0 230 false(reach) 3.2 210 false(reach) 5.5   220 false(reach) 3.1  160 true .63  39   false(reach) .13  25 false(reach) 5.3 320 witness timeout .22 28 unknown 5.3 260 false(reach) 3.3 79 false(reach) 18     6.7 false(reach) 9.7 350 false(reach) 8.3 330 witness unconfirmed .14  17  
loops/trex02_false-unreach-call_true-termination.i false(reach) .10  23 false(reach) .088 19   false(reach) .091 24 false(reach) 3.9 230 false(reach) 5.8 340 false(reach) 4.0 230 false(reach) 3.8 210 false(reach) 4.5   220 false(reach) 3.0  160 false(reach) .59  38   false(reach) .10  25 false(reach) 4.8 310 false(reach) .29 39 witness unconfirmed 8.1 320 false(reach) 3.1 77 false(reach) .23  6.7 false(reach) 9.1 330 false(reach) 8.7 320 witness unconfirmed .11  16  
loops/trex03_false-unreach-call_true-termination.i false(reach) .11  23 false(reach) .075 18   false(reach) .18  24 false(reach) 3.8 230 false(reach) 5.0 340 false(reach) 4.5 240 false(reach) 7.4 390 false(reach) 21     550 witness timeout 3.2  170 true .52  38   false(reach) .084 23 false(reach) 5.3 320 false(reach) .32 39 witness unconfirmed 9.7 410 false(reach) 3.2 79 false(reach) .16  8.0 false(reach) 9.4 330 false(reach) 9.2 330 witness unconfirmed .16  15  
loops/verisec_NetBSD-libc__loop_false-unreach-call.i false(reach) .14  25 false(reach) .33  28   false(reach) .22  24 false(reach) 3.3 240 unknown 4.7 330 false(reach) 4.2 240 false(reach) 3.9 210 witness timeout 7.0   280 witness timeout 3.6  170 true .55  38   false(reach) .11  23 unknown 5.0 330 false(reach) .28 39 unknown 7.1 310 false(reach) 3.3 76 false(reach) 18     6.7 false(reach) 11   340 false(reach) 9.9 320 unknown .077 13  
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.i witness timeout .66  37 false(reach) 33     42   false(reach) .35  27 false(reach) 5.3 330 false(reach) 38   930 false(reach) 4.5 250 false(reach) 4.5 220 witness timeout 68     1400 witness timeout 4.7  170 unknown .15  4.6 false(reach) 1.6   26 false(reach) 27   750 false(reach) .54 52 unknown 11   420 false(reach) 3.6 80 false(reach) 260     7.8 false(reach) 16   480 false(reach) 13   340 unknown .062 7.7
loops/vogal_false-unreach-call.i witness timeout 39     270 timeout 680     200   witness timeout .56  31 timeout 900   1000 false(reach) 63   1500 false(reach) 9.9 450 false(reach) 8.2 310 error (1) 110     3000 witness timeout 5.5  170 true .58  38   false(reach) 12     27 false(reach) 45   950 witness timeout 1.1  53 unknown 10   460 witness unconfirmed 4.4 130 false(reach) 77     6.9 error 170   1700 witness timeout 54   940 unknown .079 8.2
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(reach) .11  23 false(reach) .11  17   false(reach) .16  24 false(reach) 3.8 220 false(reach) 4.7 330 false(reach) 3.9 230 false(reach) 3.6 210 error (1) 5.5   290 false(reach) 2.9  160 error (139) 20     910   false(reach) .12  23 false(reach) 5.2 310 witness unconfirmed .28 35 witness unconfirmed 7.4 320 false(reach) 3.2 75 witness unconfirmed .10  6.6 false(reach) 8.4 320 false(reach) 8.6 320 witness unconfirmed .14  14  
loops/array_true-unreach-call.i true .18  24 true .61  26   true 1.1   24 true 3.9 230 true 4.6 260 true 3.3 220 true 7.2 380 true .11  13 true .43 21 true .57  39   true .17  23 true 5.2 240 true .20 30 true 12   510 true 2.6 64 true 18     7.0 true 9.4 330 true 9.3 330 unknown .10  13  
loops/bubble_sort_true-unreach-call.i true .11  23 true .020 14   true 850     1400 true 3.4 230 true 4.3 230 true 19   650 true 93   2300 unknown 890     5800 true 2.6  98 unknown .59  39   true .14  23 true 3.9 230 true .24 25 unknown 6.1 290 true 3.0 78 true .093 6.0 true 9.0 330 true 11   340 unknown .064 8.1
loops/count_up_down_true-unreach-call_true-termination.i timeout 900     1300 false(reach) .084 18   true 3.2   46 timeout 900   1500 timeout 900   7900 timeout 900   840 timeout 900   6000 error (1) 16     560 unknown 51    23 true .53  38   timeout 900     61 unknown 5.1 310 true .17 30 true 11   420 true 880   1200 timeout 900     1500   timeout 900   500 timeout 140   570 true 43     91  
loops/eureka_01_true-unreach-call.i true 35     260 timeout 880     540   true 1.3   26 true 19   710 timeout 900   5300 true 5.7 280 true 5.3 240 true 1.2   57 true .43 24 true 1.7   39   true 290     61 timeout 900   5200 timeout 900    220 unknown 13   560 timeout 880   660 true 7.6   5.7 timeout 900   1800 timeout 98   1800 unknown .051 7.7
loops/eureka_05_true-unreach-call.i true 6.5   110 false(reach) 7.8   38   true 1.0   24 true 6.3 270 timeout 900   4800 true 4.7 230 true 3.9 190 true .57  43 true 1.4  22 error (134) .85  38   segmentation fault .42  33 true 210   4100 killed by signal 9 240    15000 unknown 6.8 310 true 3.1 81 true 18     5.8 true 35   590 true 97   1300 unknown .29  17  
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true .10  23 true .023 13   true 1.2   24 true 3.7 210 true 3.7 250 timeout 900   4600 true 93   3600 true .081 13 true .38 21 true .79  38   true .13  23 true 3.8 220 true .24 27 unknown 11   370 true 2.8 76 timeout 900     5.8 true 8.4 320 true 8.1 330 unknown .089 13  
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true .13  23 true .041 16   true .93  24 true 3.1 220 true 4.5 250 timeout 900   4600 true 93   3600 error (1) 87     4300 unknown 31    22 true 20     43   true .14  23 true 4.4 220 true .19 28 unknown 9.2 360 true 2.8 74 timeout 900     5.9 true 8.6 320 true 8.5 320 unknown .095 15  
loops/insertion_sort_true-unreach-call.i timeout 900     6100 false(reach) 3.7   27   true 850     3800 timeout 900   850 timeout 900   4000 error 4.3 240 timeout 900   4000 unknown 890     940 unknown 890    570 true 200     41   timeout 900     1100 timeout 900   5500 false(reach) .51 49 unknown 10   450 timeout 880   240 unknown .22  7.0 error 160   940 timeout 79   1200 true 2.8   49  
loops/invert_string_true-unreach-call.i true 2.0   52 false(reach) 2.4   37   true .96  24 true 10   300 true 64   1200 error 4.8 240 true 61   1300 true .074 13 true 2.0  22 true 3.0   38   true 1.4   24 true 17   490 true 5.5  43 unknown 30   940 true 3.1 73 unknown .11  5.7 true 130   1300 timeout 68   660 unknown .10  11  
loops/linear_sea.ch_true-unreach-call.i timeout 900     5400 false(reach) .058 19   true 8.7   130 false(reach) 4.6 230 unknown 6.7 380 false(reach) 11   470 unknown 100   3500 true .82  15 true .55 23 true .61  38   timeout 900     180 unknown 5.4 330 false(reach) .29 40 unknown 8.0 330 true 880   180 unknown 18     7.2 error 42   460 timeout 720   770 unknown .079 7.6
loops/lu.cmp_true-unreach-call.i true 15     4000 true 67     70   true 1.6   25 true 10   620 true 17   620 true 5.2 250 true 4.5 210 true 60     8800 unknown .17 23 unknown .71  7.6 out of memory 190     15000 true 31   800 true .30 39 unknown 3.9 180 true 310   1100 true 18     6.4 error 65   6900 error 47   7100 unknown .060 12  
loops/matrix_true-unreach-call_true-termination.i true .19  26 exception (gremlins) .015 7.6 true 1.2   26 true 12   420 true 22   810 timeout 900   1700 true 28   870 true .47  38 true .43 22 true 1.8   39   true .33  26 true 7.5 340 true .26 30 unknown 8.8 320 true 2.8 67 true 35     7.3 true 12   370 true 14   350 unknown .085 14  
loops/n.c11_true-unreach-call.i timeout 900     1600 true .70  28   true 5.3   29 true 3.3 220 true 4.4 250 true 3.7 210 true 2.8 190 true .17  14 true .37 22 true .57  38   timeout 900     510 true 5.2 240 true .37 37 true 27   770 true 890   620 timeout 900     6.5 true 10   330 true 11   340 true .42  37  
loops/n.c40_true-unreach-call.i true .12  27 false(reach) .25  25   true .93  24 true 4.2 240 true 4.2 240 true 4.3 220 true 5.9 370 true .10  13 true .35 21 true .79  38   true .078 23 true 3.8 230 true .27 34 unknown 9.2 360 true 3.1 75 true .16  5.8 true 390   890 true 410   1800 unknown 1.1   37  
loops/nec40_true-unreach-call.i true .15  29 false(reach) .28  24   true 1.1   24 true 4.4 230 true 4.3 250 true 3.6 220 true 5.7 360 true .076 13 true .39 21 true .56  38   true .094 23 true 4.0 230 true .23 34 false(reach) 9.5 380 true 3.1 86 true .15  6.0 true 400   530 true 410   1700 unknown 1.1   39  
loops/string_true-unreach-call.i true .13  24 true .70  25   true 3.5   180 true 3.3 220 true 8.4 370 true 4.6 250 true 4.4 220 true .71  22 true .48 23 true .60  38   true 53     31 true 7.7 320 true .33 38 unknown 49   1100 true 3.1 79 timeout 900     7.7 true 20   430 true 8.6 320 true 1.1   34  
loops/sum01_true-unreach-call_true-termination.i timeout 900     1500 timeout 630     200   true 2.0   38 timeout 900   1100 timeout 900   6100 timeout 900   1200 timeout 900   5000 error (1) 17     520 unknown 37    24 false(reach) 1.9   38   timeout 900     40 true 7.9 330 true .36 34 true 14   460 true 880   790 timeout 900     25   timeout 900   1200 true 11   330 true 57     110  
loops/sum03_true-unreach-call_false-termination.i timeout 900     320 true .21  24   true 1.2   24 timeout 900   1000 true 4.5 250 timeout 900   4600 true 160   3600 true .082 13 true .29 21 true .57  38   timeout 900     29 true 4.3 230 true .25 33 true 12   440 true 250   390 true 28     380   timeout 900   1200 true 9.0 320 true .82  40  
loops/sum04_true-unreach-call_true-termination.i true .99  40 true 1.0   28   true 1.1   24 true 3.9 220 true 6.0 280 true 3.7 210 true 3.2 180 true .082 13 true 2.2  22 unknown .49  38   true .096 23 true 5.5 300 true .22 30 true 19   800 true 2.5 64 true 18     5.8 true 12   340 true 13   350 unknown .066 7.9
loops/sum_array_true-unreach-call.i timeout 900     8700 false(reach) .73  29   true 120     14000 timeout 900   1000 timeout 900   5200 timeout 900   900 false(reach) 310   4700 unknown 890     100 true 13    64 true .61  38   timeout 900     180 timeout 900   6400 false(reach) .38 51 unknown 88   1300 true 880   480 unknown .20  7.1 timeout 900   1600 timeout 770   1100 true 5.0   65  
loops/terminator_02_true-unreach-call_true-termination.i true .11  23 true 1.2   31   true 4.4   150 true 3.8 220 true 4.0 250 true 3.9 210 true 6.6 350 true 1.4   75 true .52 27 true .60  38   true .14  23 true 4.0 230 true .32 36 true 11   450 true 2.9 71 true 18     7.2 true 9.5 340 true 8.3 330 unknown .12  16  
loops/terminator_03_true-unreach-call_true-termination.i true .10  23 true .45  29   true 6.4   57 true 3.1 210 true 5.1 250 true 4.0 220 true 7.0 370 error (1) 20     500 unknown 88    39 true .61  38   true .11  23 true 4.1 230 true .26 36 true 11   440 true 2.9 76 timeout 900     27   true 9.9 360 true 9.0 330 true .24  23  
loops/trex01_true-unreach-call.i true 15     190 true 1.5   26   true 6.8   200 timeout 900   1100 true 6.5 360 true 24   730 true 160   2300 error (1) 120     2800 true .63 29 unknown .32  7.6 timeout 900     35 true 5.3 300 true .28 38 unknown 5.3 280 true 3.0 78 timeout 900     8.8 true 9.6 330 true 9.3 330 true .40  39  
loops/trex02_true-unreach-call_true-termination.i true .10  23 true .10  21   true 4.8   100 true 3.7 220 true 4.5 250 true 3.6 210 true 6.8 380 error (1) 76     3900 unknown 100    45 true .51  39   true .085 23 true 4.8 230 true .30 36 unknown 39   1100 true 2.8 71 true .11  7.0 true 9.2 330 true 8.6 330 true .18  22  
loops/trex03_true-unreach-call.i true .12  23 false(reach) .13  21   true 9.4   230 true 3.7 220 true 5.5 260 true 4.2 220 true 7.8 380 error (1) 40     780 unknown 250    69 true .70  39   true .13  23 unknown 5.2 310 true .40 37 unknown 25   940 true 880   470 timeout 900     300   true 8.8 320 true 9.2 320 true 1.1   40  
loops/trex04_true-unreach-call_false-termination.i true .15  23 true .56  29   true 5.4   58 true 3.9 220 true 5.3 260 true 4.4 220 true 6.3 370 error (1) 44     840 unknown 890    140 unknown .94  40   true .18  23 true 4.4 240 true .35 36 unknown 21   870 true 2.9 74 timeout 900     1000   true 9.2 330 true 9.5 330 unknown .094 13  
loops/veris.c_NetBSD-libc__loop_true-unreach-call.i true .15  23 true .26  20   true 4.8   31 true 3.4 240 true 4.1 240 true 4.5 220 true 6.6 370 true .31  43 true .54 22 true .53  38   true .15  23 timeout 900   4100 false(reach) .29 39 unknown 8.2 320 true 3.0 74 true 18     5.7 true 12   330 true 10   320 unknown .066 9.5
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.i true .13  23 true .033 19   true 850     170 true 3.4 220 true 4.0 240 true 9.6 360 true 93   3600 true 25     970 true .85 32 unknown .16  4.5 true .097 23 true 4.1 230 true .26 25 unknown 9.2 420 true 3.0 73 true .10  5.9 true 8.4 330 true 9.5 320 unknown .061 8.0
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i true .11  23 true .26  24   true 1.6   25 true 3.0 210 true 5.0 250 true 3.4 220 true 5.9 370 true .19  14 true .48 22 true 2.4   38   true .11  23 true 5.6 300 true .19 30 unknown 10   360 true 2.8 73 true .18  6.1 true 9.8 320 true 10   340 unknown .093 13  
loops/vogal_true-unreach-call.i true 9.3   130 timeout 690     360   true 6.3   160 timeout 900   1000 true 91   2000 timeout 900   10000 true 160   4000 true 5.5   120 true .82 29 true .69  39   true 130     32 true 46   1100 timeout 900    250 unknown 10   470 true 6.2 89 timeout 900     7.7 true 110   2400 timeout 79   1000 unknown .065 8.8
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true .11  23 true .027 14   true 1.0   24 true 3.0 220 true 4.4 240 true 3.4 210 true 3.2 180 error (1) 11     380 unknown 30    22 timeout 900     150   true .14  22 true 3.7 220 true .18 24 true 8.1 330 true 2.8 69 timeout 900     5.8 true 8.3 320 true 9.5 330 unknown .088 13  
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true .10  23 true .038 15   true 1.2   24 true 3.8 220 true 4.5 240 true 3.5 210 true 2.6 180 true .057 13 true .43 21 unknown 16     38   true .11  22 true 3.8 230 true .16 28 true 7.7 330 true 2.8 73 timeout 900     5.8 true 9.2 340 true 8.9 320 unknown .12  13  
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true .10  23 true .039 14   true .96  24 true 3.0 220 true 3.8 250 true 3.5 210 true 3.1 190 error (1) 14     690 unknown 29    22 true 16     38   true .13  22 true 3.7 230 true .18 29 true 8.1 320 true 2.9 73 timeout 900     5.9 true 8.8 330 true 8.9 340 true .19  24  
loop-acceleration/array_false-unreach-call1.i timeout 900     1200 timeout 710     230   true 2.3   450 timeout 900   4400 timeout 900   11000 timeout 900   5700 timeout 900   5300 error (1) 86     1100 unknown 210    69 witness timeout .70  41   timeout 900     59 timeout 900   4600 timeout 900    11000 unknown 46   1000 witness unconfirmed 19   280 witness timeout 18     6.8 timeout 900   1100 timeout 53   1500 out of memory 320     15000  
loop-acceleration/array_false-unreach-call2.i timeout 900     1500 timeout 860     370   true 1.9   460 timeout 900   14000 timeout 900   9900 timeout 900   4300 timeout 900   6300 error (1) 96     3800 unknown 200    69 witness invalid (out of memory) .64  39   timeout 900     29 timeout 900   4500 witness timeout .26 35 unknown 64   920 witness unconfirmed 190   2100 witness invalid (out of memory) 18     8.2 timeout 900   1600 timeout 55   860 timeout 900     130  
loop-acceleration/array_false-unreach-call3.i timeout 900     6800 timeout 780     330   true 1.4   33 false(reach) 34   880 timeout 900   7000 timeout 900   810 false(reach) 44   790 true .12  13 true .46 22 unknown .47  38   timeout 900     110 false(reach) 700   4000 witness timeout 220    630 unknown 53   1100 true 880   690 timeout 900     7.3 timeout 900   1100 timeout 54   1000 out of memory 130     15000  
loop-acceleration/const_false-unreach-call1.i timeout 900     1400 timeout 700     200   true 1.1   24 false(reach) 60   1200 timeout 900   12000 false(reach) 200   5000 timeout 900   4800 error (1) 87     4000 unknown 31    22 false(reach) .52  38   false(reach) 860     52 timeout 900   4100 false(reach) 660    200 unknown 31   970 witness unconfirmed 5.0 140 false(reach) 18     6.6 timeout 900   990 timeout 44   730 timeout 900     240  
loop-acceleration/diamond_false-unreach-call1.i false(reach) 1.3   37 witness timeout 60     47   false(reach) 1.6   44 false(reach) 9.2 400 false(reach) 31   1900 false(reach) 140   790 false(reach) 19   1200 error (1) 73     3800 false(reach) 23    160 true .59  38   false(reach) 4.8   24 false(reach) 49   1300 false(reach) 620    290 unknown 37   1000 false(reach) 360   140 witness timeout 18     6.9 false(reach) 210   730 timeout 20   480 witness unconfirmed .69  30  
loop-acceleration/functions_false-unreach-call1.i timeout 900     1600 timeout 740     170   true 1.2   24 timeout 900   1600 timeout 900   12000 timeout 900   4600 timeout 900   5500 error (1) 89     4200 unknown 31    22 unknown 1.2   38   timeout 900     31 timeout 900   3900 timeout 900    250 unknown 42   1100 error (1) 880   1000 witness timeout .18  6.6 timeout 900   1400 timeout 44   940 unknown 650     260  
loop-acceleration/multivar_false-unreach-call1.i false(reach) .10  23 false(reach) .099 20   false(reach) .16  24 false(reach) 3.8 230 false(reach) 4.8 330 false(reach) 3.9 230 false(reach) 3.0 210 false(reach) 3.9   220 false(reach) 3.0  160 true .51  38   false(reach) .14  23 false(reach) 5.1 310 witness unconfirmed .25 34 witness unconfirmed 8.2 320 false(reach) 3.2 78 false(reach) 18     6.6 false(reach) 9.3 330 false(reach) 8.8 330 witness unconfirmed .12  16  
loop-acceleration/nested_false-unreach-call1.i timeout 900     8600 timeout 640     240   true 1.4   25 timeout 900   860 timeout 900   4000 timeout 900   4600 timeout 900   3600 true .29  19 true .38 21 unknown 4.4   38   timeout 900     36 timeout 900   4200 witness timeout .20 34 unknown 71   940 out of memory 530   15000 timeout 870     15000   timeout 900   2100 timeout 44   640 unknown 520     210  
loop-acceleration/phases_false-unreach-call1.i timeout 900     1300 exception (gremlins) .087 19   true 1.2   24 timeout 900   820 timeout 900   6100 timeout 900   4600 timeout 900   4500 true .084 13 true .43 21 unknown .75  7.5 timeout 900     27 timeout 900   3900 timeout 900    260 unknown 130   1300 error (1) 880   330 witness timeout 630     15000   timeout 900   1400 timeout 900   4200 timeout 900     260  
loop-acceleration/phases_false-unreach-call2.i false(reach) .14  25 false(reach) .087 18   false(reach) .14  24 false(reach) 3.3 230 false(reach) 5.1 330 false(reach) 4.0 240 false(reach) 3.3 210 false(reach) 20     520 false(reach) 2.9  160 unknown .55  38   false(reach) .084 25 false(reach) 4.9 310 witness unconfirmed .30 36 witness unconfirmed 8.7 320 true 880   93 false(reach) 18     6.7 false(reach) 9.7 320 false(reach) 10   350 unknown .067 9.2
loop-acceleration/simple_false-unreach-call1.i timeout 900     1200 timeout 870     160   true 1.2   24 timeout 900   800 timeout 900   8600 timeout 900   4400 timeout 900   5100 error (1) 79     3900 unknown 30    22 witness timeout .91  39   timeout 900     30 timeout 900   3900 witness timeout .20 35 unknown 30   930 out of memory 670   15000 witness timeout .11  6.8 timeout 900   1000 timeout 43   1100 unknown 640     260  
loop-acceleration/simple_false-unreach-call2.i false(reach) .12  23 false(reach) .089 18   false(reach) .16  24 false(reach) 3.2 230 false(reach) 4.7 320 false(reach) 3.8 230 false(reach) 3.2 200 false(reach) 4.0   220 false(reach) 3.1  160 false(reach) 1.3   38   false(reach) .15  23 false(reach) 5.1 310 witness unconfirmed .27 27 witness unconfirmed 9.0 320 false(reach) 3.2 76 false(reach) .21  6.7 false(reach) 8.8 320 false(reach) 8.9 320 timeout 900     240  
loop-acceleration/simple_false-unreach-call3.i false(reach) .10  23 false(reach) .068 16   false(reach) .12  24 false(reach) 3.3 220 false(reach) 4.8 330 false(reach) 3.9 230 false(reach) 3.7 210 false(reach) 4.0   220 false(reach) 3.0  160 false(reach) .44  38   false(reach) .086 25 false(reach) 5.9 330 witness timeout .27 35 witness timeout 7.8 320 false(reach) 3.1 76 witness timeout .18  6.6 false(reach) 8.8 320 false(reach) 9.5 330 witness unconfirmed .093 13  
loop-acceleration/simple_false-unreach-call4.i timeout 900     1000 exception (gremlins) 1.0   42   true 1.2   24 timeout 900   810 timeout 900   8300 timeout 900   4500 timeout 900   5900 error (1) 81     3900 unknown 30    26 witness timeout .77  38   timeout 900     26 timeout 900   4000 witness timeout .19 35 unknown 28   900 out of memory 660   15000 witness timeout .11  6.6 timeout 900   1200 timeout 37   1100 unknown 520     210  
loop-acceleration/underapprox_false-unreach-call1.i false(reach) .33  30 false(reach) 1.4   27   false(reach) .31  24 false(reach) 4.7 230 false(reach) 7.1 350 false(reach) 4.4 240 false(reach) 3.2 210 false(reach) 4.9   230 false(reach) 3.2  160 false(reach) .56  38   false(reach) .11  23 false(reach) 5.7 330 witness unconfirmed .21 34 witness unconfirmed 12   520 witness unconfirmed 3.1 73 witness unconfirmed 18     7.9 false(reach) 11   340 false(reach) 11   340 witness unconfirmed .094 16  
loop-acceleration/underapprox_false-unreach-call2.i false(reach) .41  29 false(reach) .75  27   false(reach) .44  24 false(reach) 4.6 240 false(reach) 5.8 350 false(reach) 4.2 240 false(reach) 4.1 210 false(reach) 4.8   230 false(reach) 3.2  160 false(reach) .55  38   false(reach) .089 23 false(reach) 5.8 320 witness unconfirmed .19 34 witness unconfirmed 13   510 witness unconfirmed 3.0 75 witness unconfirmed .12  6.6 false(reach) 10   330 false(reach) 11   340 witness unconfirmed .10  17  
loop-acceleration/array_true-unreach-call1.i true 47     700 timeout 700     230   true 2.2   450 true 28   830 true 3.8 250 true 39   500 true 100   690 error (1) 85     1000 unknown 200    69 true .65  38   timeout 900     100 true 4.0 230 true .30 37 true 9.4 370 true 5.1 180 true 18     5.9 timeout 900   1600 timeout 55   740 out of memory 320     15000  
loop-acceleration/array_true-unreach-call2.i timeout 900     15000 timeout 860     370   true 2.3   460 timeout 900   13000 timeout 900   10000 timeout 900   4300 timeout 900   6300 error (1) 95     3900 unknown 200    69 error (134) 5.0   39   timeout 900     29 timeout 900   4600 true .20 30 unknown 62   910 true 37   1900 true 18     7.0 timeout 900   930 timeout 54   1200 timeout 900     130  
loop-acceleration/array_true-unreach-call3.i true .41  54 true .27  24   true 1.4   33 true 26   800 true 4.7 250 timeout 900   890 true 18   1200 true .12  13 true .45 22 true .67  38   timeout 900     1600 true 4.7 230 true .54 38 true 10   420 true 880   710 unknown 120     120   true 9.3 320 true 8.8 320 out of memory 120     15000  
loop-acceleration/array_true-unreach-call4.i timeout 900     6900 timeout 780     330   true 1.3   34 true 37   1600 timeout 900   6600 timeout 900   890 true 12   700 true .085 13 true .45 22 unknown .62  38   timeout 900     110 timeout 900   4000 timeout 900    280 unknown 36   1100 true 880   1000 true 120     110   timeout 900   1100 timeout 51   940 out of memory 130     15000  
loop-acceleration/const_true-unreach-call1.i true .24  25 true .18  23   true .96  24 true 17   570 true 3.8 250 true 7.6 490 true 12   1200 true .066 13 true .43 21 true .60  38   true 850     28 true 3.8 220 true .26 37 true 8.6 320 true 3.4 85 true 18     5.8 timeout 900   1100 timeout 43   900 true .16  23  
loop-acceleration/diamond_true-unreach-call1.i true 1.1   37 false(reach) 56     48   true 4.7   91 true 20   680 true 29   2400 true 390   800 true 49   2900 true .55  13 true .80 25 true 98     43   true 8.2   26 unknown 88   2400 timeout 900    220 unknown 25   880 true 880   200 true 36     7.4 true 710   1400 timeout 21   450 unknown 3.5   27  
loop-acceleration/diamond_true-unreach-call2.i true .27  29 false(reach) 97     45   true 16     600 true 17   470 true 14   560 true 7.9 280 true 17   580 true 5.1   49 true .73 55 unknown .61  38   true .55  23 timeout 900   4400 true 5.8  58 unknown 30   940 true 3.7 100 true .19  6.2 true 26   460 timeout 25   470 timeout 900     840  
loop-acceleration/functions_true-unreach-call1.i timeout 900     1600 timeout 770     160   true 1.2   24 timeout 900   1300 timeout 900   8900 timeout 900   4600 timeout 900   5500 true .068 13 true .39 21 true 1.1   38   timeout 900     30 true 4.2 230 true .27 36 unknown 44   1100 true 880   1100 true .067 5.7 timeout 900   880 timeout 43   760 unknown 500     210  
loop-acceleration/multivar_true-unreach-call1.i timeout 900     1400 true .15  20   true 5.2   71 true 3.8 220 true 4.7 260 true 3.6 210 true 7.5 380 true .085 13 true .44 21 true .61  38   true .076 23 true 4.2 230 true .21 25 true 9.5 350 true 880   1000 true 87     160   true 9.4 340 true 8.4 320 true .22  33  
loop-acceleration/nested_true-unreach-call1.i true .14  25 timeout 650     240   true 1.3   25 timeout 900   900 true 5.0 240 timeout 900   4500 true 160   3500 error (1) 130     4500 true .70 21 unknown 4.4   38   timeout 900     35 true 6.2 310 true .23 31 unknown 38   830 out of memory 520   15000 timeout 880     15000   timeout 900   2400 timeout 42   880 unknown 610     260  
loop-acceleration/overflow_true-unreach-call1.i timeout 900     1200 true .16  20   true .82  24 timeout 900   810 timeout 900   8600 timeout 900   4500 timeout 900   5700 true .065 12 true .34 21 true 4.7   38   timeout 900     27 true 3.8 230 true .19 30 true 8.2 320 true 890   900 true .098 5.7 timeout 900   990 timeout 43   740 timeout 900     170  
loop-acceleration/phases_true-unreach-call1.i timeout 900     1300 exception (gremlins) .15  20   true 1.1   24 timeout 900   830 timeout 900   6000 timeout 900   4600 timeout 900   4500 true .10  12 true .36 21 true 11     38   timeout 900     27 timeout 900   3900 timeout 900    260 unknown 140   1000 true 880   330 true 610     15000   timeout 900   1900 timeout 900   4200 timeout 900     250  
loop-acceleration/phases_true-unreach-call2.i true .13  26 false(reach) .55  23   true 130     930 true 3.3 220 true 4.6 240 true 3.8 220 true 6.2 360 error (1) 21     540 unknown 890    480 true 47     38   timeout 900     150 unknown 6.2 320 false(reach) .28 40 unknown 8.9 350 true 880   140 timeout 900     9200   true 11   350 true 16   330 unknown .098 11  
loop-acceleration/simple_true-unreach-call1.i timeout 900     1400 timeout 870     160   true 1.1   24 timeout 900   790 timeout 900   8700 timeout 900   4600 timeout 900   5600 true .081 13 true .38 21 true 2.2   38   timeout 900     27 true 4.0 230 true .19 30 unknown 26   840 out of memory 670   15000 true .16  5.6 timeout 900   2000 timeout 39   620 unknown 540     210  
loop-acceleration/simple_true-unreach-call2.i true .079 23 exception (gremlins) .11  20   true 3.7   48 true 3.1 220 true 4.5 240 true 2.9 210 true 5.6 340 error (1) 9.5   430 unknown 58    30 true 2.5   38   true .13  22 true 3.8 230 true .18 30 true 7.7 320 true 2.4 69 true .17  6.0 true 9.8 330 true 9.0 330 unknown .088 11  
loop-acceleration/simple_true-unreach-call3.i timeout 900     1000 false(reach) .10  20   true 1.4   29 timeout 900   970 timeout 900   5700 timeout 900   860 timeout 900   4500 true .11  13 true .49 21 true 12     38   true .10  23 true 4.0 230 true .23 25 true 10   410 true 880   450 timeout 900     9.5 timeout 900   1900 true 9.9 330 timeout 900     360  
loop-acceleration/simple_true-unreach-call4.i true .10  23 exception (gremlins) 1.7   48   true .99  24 true 3.0 220 true 4.6 250 timeout 900   4600 true 150   3600 true .10  13 true .41 21 true 13     38   timeout 900     29 true 3.9 220 true .22 30 unknown 28   850 out of memory 650   15000 true .17  5.7 timeout 900   820 true 8.8 330 unknown 510     210  
loop-acceleration/underapprox_true-unreach-call1.i true .47  29 true .58  27   true 1.1   24 true 5.1 240 true 5.8 280 true 3.4 200 true 2.7 180 true .062 13 true .39 21 true .68  38   true .15  23 true 6.2 340 true .24 30 true 13   630 true 2.7 64 true 18     5.6 true 13   380 timeout 900   400 unknown .13  15  
loop-acceleration/underapprox_true-unreach-call2.i true .13  24 true .25  20   true 1.0   24 true 4.0 220 true 3.8 250 true 3.6 210 true 2.7 180 true .062 13 true 1.6  22 unknown .52  38   true .10  23 true 4.8 230 true .24 30 true 9.0 350 true 2.6 66 true .095 5.6 true 11   340 true 12   330 unknown .082 15  
loop-invgen/id_trans_false-unreach-call.i false(reach) .12  24 exception (gremlins) .41  28   false(reach) .13  24 false(reach) 4.2 230 false(reach) 5.3 340 false(reach) 4.0 240 false(reach) 7.3 390 error (1) 140     4800 false(reach) 3.2  160 true 2.7   38   false(reach) .20  27 false(reach) 5.5 320 false(reach) .35 40 witness timeout 14   490 false(reach) 3.1 79 witness unconfirmed .18  7.2 false(reach) 10   350 false(reach) 10   320 witness unconfirmed .13  14  
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call.i timeout 900     570 true 13     42   true 850     620 timeout 900   810 timeout 900   4600 timeout 900   820 timeout 900   4100 true 100     100 true 6.3  30 true 22     39   timeout 900     270 true 180   3800 true .46 40 true 16   740 true 39   160 timeout 900     9.6 timeout 900   1600 true 13   350 timeout 900     650  
loop-invgen/NetBSD_loop_true-unreach-call.i true .26  25 true .66  26   true 4.1   52 timeout 900   1000 timeout 900   6600 timeout 900   770 timeout 900   4800 true .29  28 true .50 22 true 3.0   38   timeout 900     45 true 12   430 true .27 37 true 15   610 true 880   670 timeout 900     8.2 true 12   360 true 11   350 true .35  40  
loop-invgen/SpamAssassin-loop_true-unreach-call.i true .55  31 true 260     130   true 850     670 timeout 900   5600 timeout 900   4200 timeout 900   840 true 380   4100 out of memory 37     15000 unknown 900    1500 unknown .57  38   timeout 900     160 timeout 900   4500 true .48 51 unknown 180   1700 true 880   450 timeout 900     8.3 true 12   330 true 28   730 true 4.3   54  
loop-invgen/apache-escape-absolute_true-unreach-call.i true 2.7   48 true 37     51   true 850     180 timeout 900   1200 timeout 900   4500 timeout 900   820 true 340   4300 unknown 890     540 true 690    80 unknown .59  39   true .74  23 true 15   420 true .80 58 unknown 93   1300 true 880   330 timeout 900     8.2 true 13   330 true 26   460 true 2.4   51  
loop-invgen/apache-get-tag_true-unreach-call.i true 1.4   33 true 7.0   38   true 850     2700 timeout 900   1100 true 21   610 timeout 900   930 true 19   540 false(reach) 800     7100 unknown 890    63 true .62  38   true .43  23 true 7.9 340 true .42 47 unknown 22   920 true 880   360 timeout 900     7.8 true 12   360 true 14   450 true .81  45  
loop-invgen/down_true-unreach-call.i timeout 900     1600 timeout 710     180   true 5.6   91 timeout 900   950 timeout 900   7500 timeout 900   820 timeout 900   5300 true .48  37 true .51 24 unknown .43  38   timeout 900     280 true 20   500 true .32 37 unknown 61   1200 true 880   390 timeout 900     22   timeout 900   1800 timeout 59   1300 true .66  47  
loop-invgen/fragtest_simple_true-unreach-call.i timeout 900     3100 timeout 740     170   true 7.3   130 timeout 900   3800 timeout 900   6800 timeout 900   4600 timeout 900   5300 true .40  44 true .49 24 unknown .50  38   timeout 900     100 true 43   1100 true .34 43 unknown 92   1200 true 880   470 timeout 900     35   timeout 900   1700 timeout 53   790 true 2.8   45  
loop-invgen/half_2_true-unreach-call.i timeout 900     1900 exception (gremlins) .11  22   true 7.4   100 timeout 900   880 timeout 900   5800 timeout 900   860 timeout 900   5000 true 1.0   39 true .68 26 true .18  7.6 timeout 900     320 timeout 900   4300 false(reach) .32 40 unknown 49   1200 true 690   280 unknown 36     7.3 timeout 900   1700 timeout 50   690 timeout 900     240  
loop-invgen/heapsort_true-unreach-call.i timeout 900     1500 exception (gremlins) .18  29   true 850     1900 true 510   820 timeout 900   4300 timeout 900   830 timeout 900   3000 out of memory 45     15000 true 600    1400 true .78  39   timeout 900     7000 timeout 900   4600 true 1.3  72 unknown 110   1400 true 880   400 false(reach) 18     7.4 error 16   390 timeout 77   1200 true 1.9   47  
loop-invgen/id_build_true-unreach-call.i true .28  26 true .56  29   true 57     380 timeout 900   860 true 5.7 280 timeout 900   820 true 8.5 380 true 14     2300 true 1.0  110 true .55  38   true .44  23 true 5.3 230 true .28 38 unknown 300   1800 true 890   570 timeout 900     8.9 true 9.1 340 true 11   360 true .39  43  
loop-invgen/large_const_true-unreach-call.i true .37  28 exception (gremlins) 120     55   true 6.8   180 true 4.5 250 true 6.3 270 true 12   440 true 6.7 380 true 1.5   64 true .68 28 error (134) 2.5   39   true .31  25 true 5.7 310 true 160    140 true 17   740 true 2.6 75 unknown 35     7.2 true 11   340 true 12   360 unknown .12  14  
loop-invgen/nest-if3_true-unreach-call.i true 1.4   41 false(reach) .53  25   true 850     5200 timeout 900   520 timeout 900   4300 timeout 900   850 timeout 900   3800 unknown 890     7000 true 38    190 true .54  38   timeout 900     6800 true 16   440 true .39 41 unknown 70   1500 true 880   340 timeout 900     270   true 8.8 350 true 11   320 true 1.3   50  
loop-invgen/nested6_true-unreach-call.i timeout 900     1300 true 200     53   true 850     970 timeout 900   890 timeout 900   4500 timeout 900   860 timeout 900   3500 out of memory 92     15000 unknown 890    330 true 2.3   38   timeout 900     10000 true 59   1400 true .53 49 unknown 58   1300 true 880   320 timeout 900     10   true 13   370 true 24   470 true 30     69  
loop-invgen/nested9_true-unreach-call.i timeout 900     360 true .68  26   true 850     740 timeout 900   840 timeout 900   4400 timeout 900   940 timeout 900   4300 out of memory 50     15000 true 3.8  780 true .65  38   timeout 900     360 true 37   930 true 900    910 unknown 93   1400 true 880   480 timeout 900     36   timeout 900   2100 timeout 99   1600 true 61     94  
loop-invgen/sendmail-close-angle_true-unreach-call.i timeout 900     2100 exception (gremlins) 11     44   true 20     220 timeout 900   1900 timeout 900   7500 timeout 900   820 timeout 900   4800 true 1.4   100 true .79 23 true .75  39   timeout 900     510 true 24   650 true .32 39 unknown 28   940 true 880   390 timeout 900     9.9 timeout 900   1000 true 25   590 true 1.6   43  
loop-invgen/seq_true-unreach-call.i timeout 900     1100 timeout 740     160   true 410     320 timeout 900   2600 timeout 900   5900 timeout 900   1800 timeout 900   4900 true 5.5   45 true 1.3  25 unknown .61  38   timeout 900     240 true 110   4000 true .31 37 unknown 68   1200 true 880   320 timeout 900     270   timeout 900   1500 timeout 58   670 timeout 900     170  
loop-invgen/string_concat-noarr_true-unreach-call.i true .14  24 timeout 810     190   true 850     8200 timeout 900   1000 timeout 900   9400 timeout 900   1400 timeout 900   4900 error (1) 110     3800 true 15    130 unknown .57  38   timeout 900     190 true 13   370 true .36 40 unknown 82   1200 true 880   680 timeout 900     220   true 520   1300 timeout 58   1000 timeout 900     200  
loop-invgen/up_true-unreach-call.i timeout 900     1900 timeout 720     180   true 5.1   70 timeout 900   2900 timeout 900   7600 timeout 900   1600 timeout 900   5400 true .35  33 true .49 22 false(reach) .54  38   timeout 900     330 true 41   920 true .31 38 unknown 60   1100 true 880   530 timeout 900     8.4 timeout 900   1900 timeout 53   780 true 8.9   56  
loop-lit/afnp2014_true-unreach-call.c.i timeout 900     2000 true 1.4   27   true 2.1   40 true 24   800 true 63   3900 timeout 900   850 true 16   1200 true .17  13 true .54 22 true 1.2   38   timeout 900     60 true 6.5 320 true .29 37 unknown 28   790 true 880   810 timeout 900     6.7 true 10   330 timeout 57   940 true .48  40  
loop-lit/bhmr2007_true-unreach-call.c.i timeout 900     320 false(reach) .074 20   true 850     320 timeout 900   800 timeout 900   4000 timeout 900   4000 timeout 900   3900 error (1) 21     500 unknown 890    38 false(reach) 1.7   39   timeout 900     45 true 26   950 true .35 39 unknown 59   1100 true 880   120 timeout 900     290   timeout 900   2000 true 9.5 320 timeout 900     210  
loop-lit/cggmp2005_true-unreach-call.c.i true .38  28 true .45  26   true 1.0   24 true 3.3 220 true 5.3 260 true 3.1 210 true 2.7 180 true .10  13 true .92 21 true .59  38   true .083 23 true 4.4 230 true .42 38 true 12   500 true 2.9 73 true 18     5.8 true 10   330 true 9.9 320 unknown .11  14  
loop-lit/cggmp2005_variant_true-unreach-call.c.i timeout 900     1700 false(reach) .13  19   true 5.5   75 timeout 900   820 timeout 900   10000 timeout 900   790 timeout 900   6400 error (1) 20     530 unknown 58    32 unknown .51  38   timeout 900     70 true 9.4 380 true .32 34 true 10   440 true 430   630 timeout 900     12   timeout 900   1500 true 9.7 320 true 56     150  
loop-lit/cggmp2005b_true-unreach-call.c.i true 1.5   44 true .84  25   true .98  24 true 7.6 370 true 4.7 260 true 5.7 260 true 4.1 260 true .46  38 true .41 21 true .57  38   true 52     24 true 4.5 230 true .33 35 unknown 62   1400 true 92   1800 true 18     5.4 timeout 900   940 true 10   340 unknown .10  15  
loop-lit/css2003_true-unreach-call.c.i true .74  32 false(reach) .13  19   true 2.3   71 timeout 900   1200 true 5.1 260 timeout 900   1100 true 6.0 360 true .15  19 true .48 22 false(reach) 15     39   timeout 900     39 true 4.4 230 true .33 37 true 13   600 true 710   510 true 55     690   timeout 900   1400 true 8.3 330 true .59  43  
loop-lit/ddlm2013_true-unreach-call.c.i timeout 900     1900 false(reach) 34     35   true 4.5   150 timeout 900   1000 timeout 900   9800 timeout 900   810 timeout 900   5200 true 6.8   23 true .63 49 true .50  38   true .23  25 timeout 900   5400 true .39 39 unknown 220   1700 true 880   300 timeout 900     140   timeout 900   1000 timeout 41   660 timeout 900     190  
loop-lit/gj2007_true-unreach-call.c.i true 7.2   96 timeout 860     300   true 1.1   24 true 4.9 250 true 11   480 true 5.2 240 true 3.9 220 true .096 13 true 30    22 true 1.1   38   true 9.0   23 true 36   900 true .20 30 unknown 150   1000 true 310   260 true 17     5.9 true 310   1600 timeout 55   1100 unknown 3.4   49  
loop-lit/gj2007b_true-unreach-call.c.i timeout 900     1100 true 2.5   33   true 2.9   56 timeout 900   1000 timeout 900   5200 timeout 900   1300 timeout 900   4600 true .14  18 true .55 22 true .60  38   timeout 900     210 true 5.6 300 true .32 38 unknown 44   1000 true 880   330 timeout 900     240   true 12   360 true 11   330 true 1.0   44  
loop-lit/gr2006_true-unreach-call.c.i true 12     140 timeout 770     170   true 1.2   24 timeout 900   1000 true 33   1100 true 5.5 250 true 5.4 240 true .074 13 true 31    22 true .54  38   true 9.8   23 true 32   960 true 670    430 unknown 160   1300 true 630   430 true 18     5.8 true 83   1100 timeout 59   1400 unknown 6.6   49  
loop-lit/gsv2008_true-unreach-call.c.i timeout 900     630 true .40  24   true 14     65 timeout 900   820 timeout 900   3700 timeout 900   800 timeout 900   4100 error (1) 14     470 unknown 83    43 true .65  38   timeout 900     110 true 4.0 230 true .28 37 true 9.8 400 true 880   380 timeout 900     22   true 8.9 340 true 9.9 320 true .25  33  
loop-lit/hhk2008_true-unreach-call.c.i timeout 900     370 false(reach) .11  21   true 850     250 timeout 900   830 timeout 900   4700 timeout 900   820 timeout 900   3400 error (1) 15     510 unknown 790    48 unknown .47  38   timeout 900     70 true 24   830 true .31 35 true 11   430 true 150   340 timeout 900     17   timeout 900   1100 true 8.8 320 timeout 900     400  
loop-lit/jm2006_true-unreach-call.c.i timeout 900     1300 exception (gremlins) 2.6   46   true 4.1   61 true 3.3 220 timeout 900   8800 true 3.8 230 true 310   5200 error (1) 74     3700 unknown 60    27 unknown .59  38   timeout 900     66 true 16   580 true .27 35 true 11   430 true 880   1000 timeout 900     1200   timeout 900   810 true 11   360 true .69  38  
loop-lit/jm2006_variant_true-unreach-call.c.i timeout 900     1500 true 34     44   true 4.2   64 timeout 900   1500 timeout 900   12000 timeout 900   880 timeout 900   5700 error (1) 80     3700 unknown 71    29 true 1.1   38   timeout 900     64 true 31   850 true .32 35 true 12   480 true 370   580 timeout 900     1900   timeout 900   800 true 13   330 timeout 900     440  
loop-lit/mcmillan2006_true-unreach-call.c.i killed by signal 9 810     15000 false(reach) .70  29   true 180     14000 false(reach) 5.9 350 unknown 13   540 false(reach) 6.6 290 timeout 900   2300 unknown 890     56 true 720    90 error (139) .020 3.4 timeout 900     410 unknown 9.2 360 false(reach) .29 40 unknown 7.8 320 true 880   340 unknown .12  7.1 timeout 900   1800 timeout 88   1000 unknown .087 12  
loop-new/count_by_1_true-unreach-call.i true .16  24 true .26  21   true 1.1   24 timeout 900   790 true 3.8 240 timeout 900   4600 true 150   3500 error (1) 81     3800 unknown 30    22 unknown .52  38   timeout 900     28 true 3.6 230 true .20 30 true 8.9 330 true 2.6 64 true .077 5.7 timeout 900   970 timeout 51   800 true .26  37  
loop-new/count_by_1_variant_true-unreach-call.i true .26  25 true .22  25   true 1.0   24 timeout 900   910 true 3.8 240 timeout 900   4700 true 160   3600 true .097 13 true .42 21 true 2.5   39   timeout 900     28 true 4.7 220 true .39 37 true 9.6 370 true 58   180 true 22     360   timeout 900   2000 timeout 56   1000 true 19     59  
loop-new/count_by_2_true-unreach-call.i timeout 900     1000 exception (gremlins) 400     160   true 1.1   24 timeout 900   780 timeout 900   8900 timeout 900   4500 timeout 900   6000 error (1) 80     3900 unknown 29    22 true 2.5   38   timeout 900     28 true 4.5 230 true .18 30 unknown 28   790 true 2.7 65 true .085 5.7 timeout 900   1300 timeout 45   860 timeout 900     250  
loop-new/count_by_k_true-unreach-call.i timeout 900     1000 false(reach) .072 17   true 3.0   62 timeout 900   770 timeout 900   7600 timeout 900   770 timeout 900   4600 error (1) 13     460 unknown 40    29 true 2.8   38   timeout 900     130 timeout 900   3900 timeout 900    440 unknown 36   960 true 480   280 timeout 900     79   timeout 900   2500 timeout 38   850 timeout 900     310  
loop-new/count_by_nondet_true-unreach-call.i timeout 900     1300 timeout 700     180   true 2.0   67 timeout 900   1100 timeout 900   4200 timeout 900   870 timeout 900   3700 true 1.1   67 true .42 42 true .61  38   timeout 900     190 timeout 900   4700 true .31 37 unknown 64   1100 true 76   170 timeout 900     19   timeout 900   1700 timeout 59   1500 true .37  40  
loop-new/gauss_sum_true-unreach-call.i timeout 900     1400 false(reach) .12  19   true 2.4   38 timeout 900   1000 true 77   2800 timeout 900   840 true 77   2000 error (1) 13     470 unknown 42    26 unknown .59  38   timeout 900     66 unknown 6.2 320 false(reach) .28 37 unknown 10   330 true 880   320 timeout 900     76   timeout 900   1100 error 8.9 330 timeout 900     370  
loop-new/half_true-unreach-call.i timeout 900     1600 exception (gremlins) 2.9   28   true 2.5   36 timeout 900   1600 timeout 900   7700 timeout 900   1300 timeout 900   5000 error (1) 15     490 unknown 37    23 true .62  38   timeout 900     34 timeout 900   4100 true .73 40 unknown 54   1200 true 880   250 timeout 900     7.8 timeout 900   900 timeout 51   930 timeout 900     100  
loop-new/nested_true-unreach-call.i timeout 900     2400 false(reach) .12  22   true 850     12000 timeout 900   850 timeout 900   4200 timeout 900   850 timeout 900   4100 true 8.8   1100 true 7.5  100 true .54  38   timeout 900     130 true 43   920 true .56 40 unknown 62   1200 true 880   570 timeout 900     7.7 true 31   660 timeout 81   750 timeout 900     160  
../../sv-benchmarks/c/ status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB)
total tasks 141 48000 150000 141 21000 9600 141 14000 93000 141 56000 140000 141 49000 430000 141 58000 180000 141 45000 330000 141 13000    250000 141 13000   18000 141 1500   6100 141 57000 52000 141 26000 200000 141 13000   36000 141 4600   99000 141 51000 140000 141 48000 80000   141 50000 130000 141 9700 110000 141 27000 87000
    correct results 84 320 10000 70 770 1900 126 14000 76000 76 1100 27000 81 1000 45000 71 1100 25000 90 3600 90000 72 420    21000 90 2300   8700 73 500   2800 74 2500 1900 103 2300 56000 98 3100   5400 32 370   15000 118 41000 35000 62 2200 17000   82 3900 39000 83 1900 33000 36 310 1800
        correct true 52 160 6900 42 640 1200 93 14000 75000 44 860 16000 50 630 27000 37 630 11000 56 3100 73000 55 250    15000 64 2200   4400 62 490   2400 40 1400 990 71 1300 40000 78 1800   4200 32 370   15000 88 40000 32000 38 1300 17000   49 3100 25000 52 1500 22000 36 310 1800
        correct false 32 160 3600 28 130 710 33 12 1100 32 270 11000 31 410 19000 34 490 14000 34 510 17000 17 170    5900 26 120   4300 11 11   420 34 1100 900 32 1000 17000 20 1300   1300 0 30 470 2400 24 990 190   33 750 13000 31 380 11000 0
    incorrect results 0 23 200 600 9 13 1100 2 11 580 0 2 17 760 1 310 4700 4 800    7200 4 1.9 90 16 28   620 0 0 8 2.6 340 1 9.5 380 3 2600 4800 1 18 7.4 0 0 1 15 62
        incorrect true 0 0 9 13 1100 0 0 0 0 3 .50 45 4 1.9 90 12 9.7 460 0 0 0 0 3 2600 4800 0 0 0 1 15 62
        incorrect false 0 23 200 600 0 2 11 580 0 2 17 760 1 310 4700 1 800    7100 0 4 19   150 0 0 8 2.6 340 1 9.5 380 0 1 18 7.4 0 0 0
score (141 tasks, max score: 234) 136 -256 -69 88 131 76 130 15 26 -313 114 174 48 48 110 84 131 135 40
Run set 2ls.sv-comp16.Loops blast.sv-comp16.Loops cbmc.sv-comp16.Loops cpa-bam.sv-comp16.Loops cpa-kind.sv-comp16.Loops cpa-refsel.sv-comp16.Loops cpa-seq.sv-comp16.Loops esbmc.sv-comp16.Loops esbmcdepthk.sv-comp16.Loops forest.sv-comp16.Loops impara.sv-comp16.Loops lpi.sv-comp16.Loops seahorn.sv-comp16.Loops skink.sv-comp16.Loops smack.sv-comp16.Loops symbiotic3.sv-comp16.Loops uautomizer.sv-comp16.Loops ukojak.sv-comp16.Loops vvt.sv-comp16.Loops