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