Tool CBMC
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-22-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-03 00:42:25 CET [[ 2016-01-15 08:22:02 CET ]] [[ 2016-01-15 21:54:19 CET ]]
Run set sv-comp16.Loops
Options --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-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 .11  .12  24 5.2 3.0 240 12 7.7 330
loops/bubble_sort_false-unreach-call.i 1.9   1.9   130 15   7.8 490 11 6.3 320
loops/count_up_down_false-unreach-call_true-termination.i .11  .12  24 4.8 2.8 240 11 6.7 340
loops/eureka_01_false-unreach-call.i .40  .41  29 90   76   1100 18 11   390
loops/for_bounded_loop1_false-unreach-call_true-termination.i .12  .13  24 5.2 3.1 240 12 7.4 340
loops/insertion_sort_false-unreach-call.i 3.3   3.4   270 90   76   1500 24 13   460
loops/invert_string_false-unreach-call.i .60  .62  39 90   74   1600 15 8.2 360
loops/linear_search_false-unreach-call.i .86  .88  28 4.0 2.3 170 29 20   500
loops/ludcmp_false-unreach-call.i 2.3   2.3   170 13   7.3 550 71 50   7000
loops/matrix_false-unreach-call_true-termination.i .19  .20  26 91   79   810 15 8.0 340
loops/n.c24_false-unreach-call.i 310     310     15000
loops/nec11_false-unreach-call.i .17  .18  24 4.7 2.8 240 12 8.0 320
loops/nec20_false-unreach-call.i .38  .40  40 44   37   880 12 8.0 330
loops/s3_false-unreach-call.i 27     27     1100 10   5.5 320 91 81   470
loops/string_false-unreach-call.i .31  .32  25 8.8 4.9 390 29 16   370
loops/sum01_bug02_false-unreach-call_true-termination.i .45  .46  24 6.4 3.6 350 17 9.7 340
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i .17  .18  24 5.8 3.3 250 15 9.6 330
loops/sum01_false-unreach-call_true-termination.i .38  .39  24 7.2 4.1 360 15 8.4 340
loops/sum03_false-unreach-call_true-termination.i .47  .48  24 8.0 4.5 340 22 14   500
loops/sum04_false-unreach-call_true-termination.i .38  .39  24 5.5 3.2 240 13 9.1 330
loops/sum_array_false-unreach-call.i .14  .15  25 90   74   3800 14 7.9 340
loops/terminator_01_false-unreach-call_false-termination.i .16  .17  24 4.1 2.4 220 12 8.2 340
loops/terminator_02_false-unreach-call_true-termination.i .12  .13  24 4.8 2.8 230 13 7.7 350
loops/terminator_03_false-unreach-call_true-termination.i .14  .15  24 4.2 2.4 230 13 7.6 330
loops/trex01_false-unreach-call_true-termination.i .14  .15  24 5.2 3.1 240 12 7.3 340
loops/trex02_false-unreach-call_true-termination.i .091 .098 24 4.6 2.7 230 11 8.2 330
loops/trex03_false-unreach-call_true-termination.i .18  .19  24 5.5 3.2 240 12 6.7 340
loops/verisec_NetBSD-libc__loop_false-unreach-call.i .22  .23  24 4.4 2.6 220 15 8.9 360
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.i .35  .36  27 4.0 2.3 180 26 14   510
loops/vogal_false-unreach-call.i .56  .57  31 91   82   770 91 57   1500
loops/while_infinite_loop_4_false-unreach-call_true-termination.i .16  .17  24 4.6 2.7 220 11 7.8 330
loops/array_true-unreach-call.i 1.1   1.1   24
loops/bubble_sort_true-unreach-call.i 850     850     1400
loops/count_up_down_true-unreach-call_true-termination.i 3.2   3.2   46
loops/eureka_01_true-unreach-call.i 1.3   1.3   26
loops/eureka_05_true-unreach-call.i 1.0   1.0   24
loops/for_infinite_loop_1_true-unreach-call_false-termination.i 1.2   1.2   24
loops/for_infinite_loop_2_true-unreach-call_false-termination.i .93  .96  24
loops/insertion_sort_true-unreach-call.i 850     850     3800
loops/invert_string_true-unreach-call.i .96  1.0   24
loops/linear_sea.ch_true-unreach-call.i 8.7   8.7   130
loops/lu.cmp_true-unreach-call.i 1.6   1.6   25
loops/matrix_true-unreach-call_true-termination.i 1.2   1.2   26
loops/n.c11_true-unreach-call.i 5.3   5.3   29
loops/n.c40_true-unreach-call.i .93  .95  24
loops/nec40_true-unreach-call.i 1.1   1.1   24
loops/string_true-unreach-call.i 3.5   3.5   180
loops/sum01_true-unreach-call_true-termination.i 2.0   2.0   38
loops/sum03_true-unreach-call_false-termination.i 1.2   1.2   24
loops/sum04_true-unreach-call_true-termination.i 1.1   1.1   24
loops/sum_array_true-unreach-call.i 120     120     14000
loops/terminator_02_true-unreach-call_true-termination.i 4.4   4.4   150
loops/terminator_03_true-unreach-call_true-termination.i 6.4   6.4   57
loops/trex01_true-unreach-call.i 6.8   6.8   200
loops/trex02_true-unreach-call_true-termination.i 4.8   4.8   100
loops/trex03_true-unreach-call.i 9.4   9.5   230
loops/trex04_true-unreach-call_false-termination.i 5.4   5.4   58
loops/veris.c_NetBSD-libc__loop_true-unreach-call.i 4.8   4.9   31
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.i 850     850     170
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i 1.6   1.6   25
loops/vogal_true-unreach-call.i 6.3   6.3   160
loops/while_infinite_loop_1_true-unreach-call_false-termination.i 1.0   1.1   24
loops/while_infinite_loop_2_true-unreach-call_false-termination.i 1.2   1.2   24
loops/while_infinite_loop_3_true-unreach-call_false-termination.i .96  .99  24
loop-acceleration/array_false-unreach-call1.i 2.3   2.3   450
loop-acceleration/array_false-unreach-call2.i 1.9   1.9   460
loop-acceleration/array_false-unreach-call3.i 1.4   1.4   33
loop-acceleration/const_false-unreach-call1.i 1.1   1.2   24
loop-acceleration/diamond_false-unreach-call1.i 1.6   1.6   44 13   7.0 500 91 68   3800
loop-acceleration/functions_false-unreach-call1.i 1.2   1.2   24
loop-acceleration/multivar_false-unreach-call1.i .16  .17  24 4.6 2.7 230 11 6.3 330
loop-acceleration/nested_false-unreach-call1.i 1.4   1.4   25
loop-acceleration/phases_false-unreach-call1.i 1.2   1.2   24
loop-acceleration/phases_false-unreach-call2.i .14  .16  24 4.7 2.8 230 12 7.3 350
loop-acceleration/simple_false-unreach-call1.i 1.2   1.2   24
loop-acceleration/simple_false-unreach-call2.i .16  .17  24 4.5 2.7 230 11 6.2 340
loop-acceleration/simple_false-unreach-call3.i .12  .13  24 4.8 2.8 230 12 6.4 340
loop-acceleration/simple_false-unreach-call4.i 1.2   1.2   24
loop-acceleration/underapprox_false-unreach-call1.i .31  .32  24 5.4 3.2 240 18 9.9 380
loop-acceleration/underapprox_false-unreach-call2.i .44  .45  24 5.6 3.2 240 18 13   390
loop-acceleration/array_true-unreach-call1.i 2.2   2.2   450
loop-acceleration/array_true-unreach-call2.i 2.3   2.3   460
loop-acceleration/array_true-unreach-call3.i 1.4   1.4   33
loop-acceleration/array_true-unreach-call4.i 1.3   1.4   34
loop-acceleration/const_true-unreach-call1.i .96  .99  24
loop-acceleration/diamond_true-unreach-call1.i 4.7   4.8   91
loop-acceleration/diamond_true-unreach-call2.i 16     16     600
loop-acceleration/functions_true-unreach-call1.i 1.2   1.2   24
loop-acceleration/multivar_true-unreach-call1.i 5.2   5.3   71
loop-acceleration/nested_true-unreach-call1.i 1.3   1.3   25
loop-acceleration/overflow_true-unreach-call1.i .82  .85  24
loop-acceleration/phases_true-unreach-call1.i 1.1   1.2   24
loop-acceleration/phases_true-unreach-call2.i 130     130     930
loop-acceleration/simple_true-unreach-call1.i 1.1   1.2   24
loop-acceleration/simple_true-unreach-call2.i 3.7   3.8   48
loop-acceleration/simple_true-unreach-call3.i 1.4   1.4   29
loop-acceleration/simple_true-unreach-call4.i .99  1.0   24
loop-acceleration/underapprox_true-unreach-call1.i 1.1   1.1   24
loop-acceleration/underapprox_true-unreach-call2.i 1.0   1.1   24
loop-invgen/id_trans_false-unreach-call.i .13  .14  24 5.1 3.0 240 10 5.8 340
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call.i 850     850     620
loop-invgen/NetBSD_loop_true-unreach-call.i 4.1   4.1   52
loop-invgen/SpamAssassin-loop_true-unreach-call.i 850     850     670
loop-invgen/apache-escape-absolute_true-unreach-call.i 850     850     180
loop-invgen/apache-get-tag_true-unreach-call.i 850     850     2700
loop-invgen/down_true-unreach-call.i 5.6   5.7   91
loop-invgen/fragtest_simple_true-unreach-call.i 7.3   7.3   130
loop-invgen/half_2_true-unreach-call.i 7.4   7.4   100
loop-invgen/heapsort_true-unreach-call.i 850     850     1900
loop-invgen/id_build_true-unreach-call.i 57     57     380
loop-invgen/large_const_true-unreach-call.i 6.8   6.9   180
loop-invgen/nest-if3_true-unreach-call.i 850     850     5200
loop-invgen/nested6_true-unreach-call.i 850     850     970
loop-invgen/nested9_true-unreach-call.i 850     850     740
loop-invgen/sendmail-close-angle_true-unreach-call.i 20     20     220
loop-invgen/seq_true-unreach-call.i 410     410     320
loop-invgen/string_concat-noarr_true-unreach-call.i 850     850     8200
loop-invgen/up_true-unreach-call.i 5.1   5.1   70
loop-lit/afnp2014_true-unreach-call.c.i 2.1   2.1   40
loop-lit/bhmr2007_true-unreach-call.c.i 850     850     320
loop-lit/cggmp2005_true-unreach-call.c.i 1.0   1.1   24
loop-lit/cggmp2005_variant_true-unreach-call.c.i 5.5   5.5   75
loop-lit/cggmp2005b_true-unreach-call.c.i .98  1.0   24
loop-lit/css2003_true-unreach-call.c.i 2.3   2.4   71
loop-lit/ddlm2013_true-unreach-call.c.i 4.5   4.6   150
loop-lit/gj2007_true-unreach-call.c.i 1.1   1.1   24
loop-lit/gj2007b_true-unreach-call.c.i 2.9   3.0   56
loop-lit/gr2006_true-unreach-call.c.i 1.2   1.2   24
loop-lit/gsv2008_true-unreach-call.c.i 14     14     65
loop-lit/hhk2008_true-unreach-call.c.i 850     850     250
loop-lit/jm2006_true-unreach-call.c.i 4.1   4.2   61
loop-lit/jm2006_variant_true-unreach-call.c.i 4.2   4.2   64
loop-lit/mcmillan2006_true-unreach-call.c.i 180     180     14000
loop-new/count_by_1_true-unreach-call.i 1.1   1.2   24
loop-new/count_by_1_variant_true-unreach-call.i 1.0   1.1   24
loop-new/count_by_2_true-unreach-call.i 1.1   1.2   24
loop-new/count_by_k_true-unreach-call.i 3.0   3.1   62
loop-new/count_by_nondet_true-unreach-call.i 2.0   2.0   67
loop-new/gauss_sum_true-unreach-call.i 2.4   2.4   38
loop-new/half_true-unreach-call.i 2.5   2.6   36
loop-new/nested_true-unreach-call.i 850     850     12000
../../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 14000 14000 93000 141 780   610   19000   141 860   570   25000  
    correct results 126 14000 14000 76000 26 650   500   17000   32 560   350   15000  
        correct true 93 14000 14000 75000 0 0   0   0   0 0   0   0  
        correct false 33 12 13 1100 26 650   500   17000   32 560   350   15000  
    incorrect results 9 13 13 1100 0 0   0   0   0 0   0   0  
        incorrect true 9 13 13 1100 0 0   0   0   0 0   0   0  
        incorrect false 0
score (141 tasks, max score: 234) -69
Run set sv-comp16.Loops