Tool ESBMC ESBMC version 2.0.0 64-bit x86_64 linux
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]
OS 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-16 17:45:19 CET [[ 2016-01-17 00:36:28 CET ]] [[ 2016-01-17 00:39:38 CET ]]
Run set sv-comp16.Loops
Options [[ -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 ]]
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
loops/array_false-unreach-call.i 23     10     600 4.9 2.9 240 10   6.0 320
loops/bubble_sort_false-unreach-call.i 170     160     15000
loops/count_up_down_false-unreach-call_true-termination.i 4.5   10     230 91   81   1400 14   8.0 370
loops/eureka_01_false-unreach-call.i 800     710     4100 91   74   970 13   7.7 350
loops/for_bounded_loop1_false-unreach-call_true-termination.i 100     76     1300
loops/insertion_sort_false-unreach-call.i 890     900     800
loops/invert_string_false-unreach-call.i 130     66     4400
loops/linear_search_false-unreach-call.i 19     10     600 9.5 5.2 400 11   5.8 340
loops/ludcmp_false-unreach-call.i 120     120     8800
loops/matrix_false-unreach-call_true-termination.i 900     900     9700
loops/n.c24_false-unreach-call.i 340     340     15000
loops/nec11_false-unreach-call.i 4.1   10     220 4.9 2.9 230 10   5.7 330
loops/nec20_false-unreach-call.i 5.3   10     250 91   62   1500 11   6.5 320
loops/s3_false-unreach-call.i 470     400     4300 7.8 4.4 280 16   9.1 340
loops/string_false-unreach-call.i 20     17     660 8.1 4.6 360 12   7.2 320
loops/sum01_bug02_false-unreach-call_true-termination.i 16     10     560
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i 15     10     490
loops/sum01_false-unreach-call_true-termination.i 15     10     480
loops/sum03_false-unreach-call_true-termination.i 12     10     400
loops/sum04_false-unreach-call_true-termination.i 5.0   10     240 5.5 3.2 240 12   7.7 330
loops/sum_array_false-unreach-call.i 120     69     4000
loops/terminator_01_false-unreach-call_false-termination.i 4.1   10     220 4.9 2.9 230 11   6.5 340
loops/terminator_02_false-unreach-call_true-termination.i 4.7   11     230 5.0 2.9 240 12   6.8 360
loops/terminator_03_false-unreach-call_true-termination.i 16     10     540 4.8 2.8 230 14   7.4 350
loops/trex01_false-unreach-call_true-termination.i 5.5   11     220 5.4 3.1 240 13   8.4 340
loops/trex02_false-unreach-call_true-termination.i 4.5   11     220 4.8 2.9 230 12   7.7 330
loops/trex03_false-unreach-call_true-termination.i 21     11     550 5.4 3.1 240 9.8 5.7 320
loops/verisec_NetBSD-libc__loop_false-unreach-call.i 7.0   11     280 91   68   1300 10   6.1 330
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.i 68     63     1400 91   70   1200 11   6.3 330
loops/vogal_false-unreach-call.i 110     71     3000
loops/while_infinite_loop_4_false-unreach-call_true-termination.i 5.5   10     290
loops/array_true-unreach-call.i .11  .13  13
loops/bubble_sort_true-unreach-call.i 890     900     5800
loops/count_up_down_true-unreach-call_true-termination.i 16     10     560
loops/eureka_01_true-unreach-call.i 1.2   1.2   57
loops/eureka_05_true-unreach-call.i .57  .59  43
loops/for_infinite_loop_1_true-unreach-call_false-termination.i .081 .091 13
loops/for_infinite_loop_2_true-unreach-call_false-termination.i 87     50     4300
loops/insertion_sort_true-unreach-call.i 890     900     940
loops/invert_string_true-unreach-call.i .074 .084 13
loops/linear_sea.ch_true-unreach-call.i .82  .83  15
loops/lu.cmp_true-unreach-call.i 60     60     8800
loops/matrix_true-unreach-call_true-termination.i .47  .48  38
loops/n.c11_true-unreach-call.i .17  .19  14
loops/n.c40_true-unreach-call.i .10  .11  13
loops/nec40_true-unreach-call.i .076 .088 13
loops/string_true-unreach-call.i .71  .73  22
loops/sum01_true-unreach-call_true-termination.i 17     10     520
loops/sum03_true-unreach-call_false-termination.i .082 .092 13
loops/sum04_true-unreach-call_true-termination.i .082 .094 13
loops/sum_array_true-unreach-call.i 890     900     100
loops/terminator_02_true-unreach-call_true-termination.i 1.4   1.4   75
loops/terminator_03_true-unreach-call_true-termination.i 20     16     500
loops/trex01_true-unreach-call.i 120     61     2800
loops/trex02_true-unreach-call_true-termination.i 76     61     3900
loops/trex03_true-unreach-call.i 40     17     780
loops/trex04_true-unreach-call_false-termination.i 44     10     840
loops/veris.c_NetBSD-libc__loop_true-unreach-call.i .31  .32  43
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.i 25     25     970
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i .19  .20  14
loops/vogal_true-unreach-call.i 5.5   5.5   120
loops/while_infinite_loop_1_true-unreach-call_false-termination.i 11     10     380
loops/while_infinite_loop_2_true-unreach-call_false-termination.i .057 .064 13
loops/while_infinite_loop_3_true-unreach-call_false-termination.i 14     10     690
loop-acceleration/array_false-unreach-call1.i 86     61     1100
loop-acceleration/array_false-unreach-call2.i 96     61     3800
loop-acceleration/array_false-unreach-call3.i .12  .13  13
loop-acceleration/const_false-unreach-call1.i 87     50     4000
loop-acceleration/diamond_false-unreach-call1.i 73     51     3800
loop-acceleration/functions_false-unreach-call1.i 89     50     4200
loop-acceleration/multivar_false-unreach-call1.i 3.9   10     220 4.9 2.9 230 11   6.2 310
loop-acceleration/nested_false-unreach-call1.i .29  .30  19
loop-acceleration/phases_false-unreach-call1.i .084 .097 13
loop-acceleration/phases_false-unreach-call2.i 20     27     520 4.9 3.0 230 11   6.5 320
loop-acceleration/simple_false-unreach-call1.i 79     50     3900
loop-acceleration/simple_false-unreach-call2.i 4.0   10     220 4.3 2.6 230 10   6.9 320
loop-acceleration/simple_false-unreach-call3.i 4.0   10     220 4.6 2.8 230 11   6.6 320
loop-acceleration/simple_false-unreach-call4.i 81     50     3900
loop-acceleration/underapprox_false-unreach-call1.i 4.9   10     230 5.4 3.2 240 11   6.3 310
loop-acceleration/underapprox_false-unreach-call2.i 4.8   10     230 5.6 3.2 250 10   6.4 310
loop-acceleration/array_true-unreach-call1.i 85     61     1000
loop-acceleration/array_true-unreach-call2.i 95     61     3900
loop-acceleration/array_true-unreach-call3.i .12  .13  13
loop-acceleration/array_true-unreach-call4.i .085 .094 13
loop-acceleration/const_true-unreach-call1.i .066 .073 13
loop-acceleration/diamond_true-unreach-call1.i .55  .56  13
loop-acceleration/diamond_true-unreach-call2.i 5.1   5.1   49
loop-acceleration/functions_true-unreach-call1.i .068 .077 13
loop-acceleration/multivar_true-unreach-call1.i .085 .094 13
loop-acceleration/nested_true-unreach-call1.i 130     71     4500
loop-acceleration/overflow_true-unreach-call1.i .065 .072 12
loop-acceleration/phases_true-unreach-call1.i .10  .11  12
loop-acceleration/phases_true-unreach-call2.i 21     13     540
loop-acceleration/simple_true-unreach-call1.i .081 .092 13
loop-acceleration/simple_true-unreach-call2.i 9.5   10     430
loop-acceleration/simple_true-unreach-call3.i .11  .12  13
loop-acceleration/simple_true-unreach-call4.i .10  .12  13
loop-acceleration/underapprox_true-unreach-call1.i .062 .072 13
loop-acceleration/underapprox_true-unreach-call2.i .062 .071 13
loop-invgen/id_trans_false-unreach-call.i 140     71     4800
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call.i 100     100     100
loop-invgen/NetBSD_loop_true-unreach-call.i .29  .29  28
loop-invgen/SpamAssassin-loop_true-unreach-call.i 37     37     15000
loop-invgen/apache-escape-absolute_true-unreach-call.i 890     900     540
loop-invgen/apache-get-tag_true-unreach-call.i 800     480     7100
loop-invgen/down_true-unreach-call.i .48  .50  37
loop-invgen/fragtest_simple_true-unreach-call.i .40  .42  44
loop-invgen/half_2_true-unreach-call.i 1.0   1.1   39
loop-invgen/heapsort_true-unreach-call.i 45     44     15000
loop-invgen/id_build_true-unreach-call.i 14     14     2300
loop-invgen/large_const_true-unreach-call.i 1.5   1.5   64
loop-invgen/nest-if3_true-unreach-call.i 890     900     7000
loop-invgen/nested6_true-unreach-call.i 92     92     15000
loop-invgen/nested9_true-unreach-call.i 50     50     15000
loop-invgen/sendmail-close-angle_true-unreach-call.i 1.4   1.4   100
loop-invgen/seq_true-unreach-call.i 5.5   5.6   45
loop-invgen/string_concat-noarr_true-unreach-call.i 110     83     3800
loop-invgen/up_true-unreach-call.i .35  .36  33
loop-lit/afnp2014_true-unreach-call.c.i .17  .18  13
loop-lit/bhmr2007_true-unreach-call.c.i 21     13     500
loop-lit/cggmp2005_true-unreach-call.c.i .10  .12  13
loop-lit/cggmp2005_variant_true-unreach-call.c.i 20     10     530
loop-lit/cggmp2005b_true-unreach-call.c.i .46  .47  38
loop-lit/css2003_true-unreach-call.c.i .15  .16  19
loop-lit/ddlm2013_true-unreach-call.c.i 6.8   6.8   23
loop-lit/gj2007_true-unreach-call.c.i .096 .11  13
loop-lit/gj2007b_true-unreach-call.c.i .14  .15  18
loop-lit/gr2006_true-unreach-call.c.i .074 .084 13
loop-lit/gsv2008_true-unreach-call.c.i 14     10     470
loop-lit/hhk2008_true-unreach-call.c.i 15     10     510
loop-lit/jm2006_true-unreach-call.c.i 74     60     3700
loop-lit/jm2006_variant_true-unreach-call.c.i 80     60     3700
loop-lit/mcmillan2006_true-unreach-call.c.i 890     900     56
loop-new/count_by_1_true-unreach-call.i 81     60     3800
loop-new/count_by_1_variant_true-unreach-call.i .097 .11  13
loop-new/count_by_2_true-unreach-call.i 80     50     3900
loop-new/count_by_k_true-unreach-call.i 13     11     460
loop-new/count_by_nondet_true-unreach-call.i 1.1   1.1   67
loop-new/gauss_sum_true-unreach-call.i 13     10     470
loop-new/half_true-unreach-call.i 15     10     490
loop-new/nested_true-unreach-call.i 8.8   8.8   1100
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
total tasks 141 13000    12000    250000 141 550   410   11000   141 270   160   7600  
    correct results 72 420    450    21000 17 93   54   4300   17 190   110   5600  
        correct true 55 250    250    15000 0 0   0   0   17 0   0   0  
        correct false 17 170    200    5900 17 93   54   4300   0 190   110   5600  
    incorrect results 4 800    480    7200 0 0   0   0   0 0   0   0  
        incorrect true 3 .50 .53 45 0 0   0   0   0 0   0   0  
        incorrect false 1 800    480    7100 0 0   0   0   0 0   0   0  
score (141 tasks, max score: 234) 15
Run set sv-comp16.Loops