Tool DepthK ESBMC+DepthK version 2.1
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-05 14:06:34 CET [[ 2016-01-15 09:00:06 CET ]] [[ 2016-01-15 22:17:52 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/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 ]]
../../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) 3.3  1.8  160 wit false(reach) 5.0 2.9 240 true 10   6.2 330
loops/bubble_sort_false-unreach-call.i false(reach) 9.8  7.9  230 wit false(reach) 16   8.8 520 error 11   6.4 320
loops/count_up_down_false-unreach-call_true-termination.i false(reach) 3.1  1.6  160 wit false(reach) 5.0 2.9 230 true 11   6.1 310
loops/eureka_01_false-unreach-call.i witness timeout 4.2  2.6  170 wit timeout 90   73   1400 true 12   6.8 330
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(reach) 3.4  2.0  170 wit false(reach) 5.8 3.4 240 true 12   6.7 350
loops/insertion_sort_false-unreach-call.i witness timeout 620    620    310 wit timeout 90   73   1000 true 10   5.8 340
loops/invert_string_false-unreach-call.i witness timeout 4.4  2.8  160 wit timeout 91   71   1200 true 12   7.3 350
loops/linear_search_false-unreach-call.i false(reach) 3.3  1.9  170 wit false(reach) 9.4 5.4 390 true 14   7.7 350
loops/ludcmp_false-unreach-call.i unknown .25 .27 23 wit - -
loops/matrix_false-unreach-call_true-termination.i witness timeout 3.7  2.1  170 wit timeout 90   78   850 true 11   7.0 320
loops/n.c24_false-unreach-call.i true .65 .69 26 wit - -
loops/nec11_false-unreach-call.i false(reach) 2.6  1.3  160 wit false(reach) 4.7 2.7 220 true 9.8 6.5 330
loops/nec20_false-unreach-call.i false(reach) 3.0  1.7  160 wit false(reach) 58   35   1700 true 10   6.0 340
loops/s3_false-unreach-call.i unknown 890    900    3400 wit - -
loops/string_false-unreach-call.i false(reach) 5.0  3.5  170 wit false(reach) 12   6.7 470 true 11   6.7 340
loops/sum01_bug02_false-unreach-call_true-termination.i false(reach) 5.1  3.6  160 wit false(reach) 7.0 4.0 350 true 9.5 6.4 320
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(reach) 4.5  3.0  170 wit false(reach) 6.1 3.5 260 true 11   6.6 320
loops/sum01_false-unreach-call_true-termination.i false(reach) 6.3  4.9  160 wit false(reach) 7.3 4.1 340 true 11   6.3 330
loops/sum03_false-unreach-call_true-termination.i witness timeout 3.4  1.7  160 wit timeout 91   71   3800 true 11   6.2 330
loops/sum04_false-unreach-call_true-termination.i false(reach) 5.5  4.0  170 wit false(reach) 6.0 3.5 260 true 10   7.0 320
loops/sum_array_false-unreach-call.i witness timeout 3.7  2.1  160 wit timeout 90   75   1300 true 10   6.5 330
loops/terminator_01_false-unreach-call_false-termination.i false(reach) 3.0  1.6  160 wit false(reach) 4.7 2.8 230 true 11   7.8 320
loops/terminator_02_false-unreach-call_true-termination.i false(reach) 3.0  1.5  160 wit false(reach) 5.1 3.0 230 true 11   7.8 310
loops/terminator_03_false-unreach-call_true-termination.i false(reach) 2.9  1.5  160 wit false(reach) 4.7 2.8 230 true 9.5 5.7 330
loops/trex01_false-unreach-call_true-termination.i false(reach) 3.1  1.5  160 wit false(reach) 5.2 3.0 240 true 11   6.3 330
loops/trex02_false-unreach-call_true-termination.i false(reach) 3.0  1.6  160 wit false(reach) 4.7 2.9 230 true 12   7.4 330
loops/trex03_false-unreach-call_true-termination.i witness timeout 3.2  1.6  170 wit timeout 90   65   2700 true 12   7.1 340
loops/verisec_NetBSD-libc__loop_false-unreach-call.i witness timeout 3.6  1.9  170 wit timeout 91   70   1200 true 11   7.7 330
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.i witness timeout 4.7  3.2  170 wit timeout 91   72   1300 true 9.8 5.9 330
loops/vogal_false-unreach-call.i witness timeout 5.5  4.0  170 wit timeout 91   78   4800 true 13   7.2 330
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(reach) 2.9  1.5  160 wit false(reach) 4.6 2.7 230 true 11   7.3 330
loops/array_true-unreach-call.i true .43 .46 21 wit - -
loops/bubble_sort_true-unreach-call.i true 2.6  2.6  98 wit - -
loops/count_up_down_true-unreach-call_true-termination.i unknown 51    52    23 wit - -
loops/eureka_01_true-unreach-call.i true .43 .45 24 wit - -
loops/eureka_05_true-unreach-call.i true 1.4  1.5  22 wit - -
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true .38 .40 21 wit - -
loops/for_infinite_loop_2_true-unreach-call_false-termination.i unknown 31    32    22 wit - -
loops/insertion_sort_true-unreach-call.i unknown 890    900    570 wit - -
loops/invert_string_true-unreach-call.i true 2.0  2.0  22 wit - -
loops/linear_sea.ch_true-unreach-call.i true .55 .58 23 wit - -
loops/lu.cmp_true-unreach-call.i unknown .17 .20 23 wit - -
loops/matrix_true-unreach-call_true-termination.i true .43 .46 22 wit - -
loops/n.c11_true-unreach-call.i true .37 .40 22 wit - -
loops/n.c40_true-unreach-call.i true .35 .38 21 wit - -
loops/nec40_true-unreach-call.i true .39 .42 21 wit - -
loops/string_true-unreach-call.i true .48 .51 23 wit - -
loops/sum01_true-unreach-call_true-termination.i unknown 37    38    24 wit - -
loops/sum03_true-unreach-call_false-termination.i true .29 .33 21 wit - -
loops/sum04_true-unreach-call_true-termination.i true 2.2  2.3  22 wit - -
loops/sum_array_true-unreach-call.i true 13    13    64 wit - -
loops/terminator_02_true-unreach-call_true-termination.i true .52 .54 27 wit - -
loops/terminator_03_true-unreach-call_true-termination.i unknown 88    89    39 wit - -
loops/trex01_true-unreach-call.i true .63 .66 29 wit - -
loops/trex02_true-unreach-call_true-termination.i unknown 100    110    45 wit - -
loops/trex03_true-unreach-call.i unknown 250    260    69 wit - -
loops/trex04_true-unreach-call_false-termination.i unknown 890    900    140 wit - -
loops/veris.c_NetBSD-libc__loop_true-unreach-call.i true .54 .57 22 wit - -
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.i true .85 .87 32 wit - -
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i true .48 .51 22 wit - -
loops/vogal_true-unreach-call.i true .82 .86 29 wit - -
loops/while_infinite_loop_1_true-unreach-call_false-termination.i unknown 30    31    22 wit - -
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true .43 .47 21 wit - -
loops/while_infinite_loop_3_true-unreach-call_false-termination.i unknown 29    30    22 wit - -
loop-acceleration/array_false-unreach-call1.i unknown 210    210    69 wit - -
loop-acceleration/array_false-unreach-call2.i unknown 200    200    69 wit - -
loop-acceleration/array_false-unreach-call3.i true .46 .49 22 wit - -
loop-acceleration/const_false-unreach-call1.i unknown 31    32    22 wit - -
loop-acceleration/diamond_false-unreach-call1.i false(reach) 23    23    160 wit false(reach) 9.4 5.3 380 true 10   6.3 330
loop-acceleration/functions_false-unreach-call1.i unknown 31    32    22 wit - -
loop-acceleration/multivar_false-unreach-call1.i false(reach) 3.0  1.5  160 wit false(reach) 5.1 3.0 230 true 9.3 5.4 320
loop-acceleration/nested_false-unreach-call1.i true .38 .41 21 wit - -
loop-acceleration/phases_false-unreach-call1.i true .43 .46 21 wit - -
loop-acceleration/phases_false-unreach-call2.i false(reach) 2.9  1.5  160 wit false(reach) 4.9 3.1 230 true 11   6.2 340
loop-acceleration/simple_false-unreach-call1.i unknown 30    31    22 wit - -
loop-acceleration/simple_false-unreach-call2.i false(reach) 3.1  1.5  160 wit false(reach) 4.5 2.7 230 true 11   5.9 320
loop-acceleration/simple_false-unreach-call3.i false(reach) 3.0  1.5  160 wit false(reach) 4.6 2.8 230 true 11   5.8 310
loop-acceleration/simple_false-unreach-call4.i unknown 30    32    26 wit - -
loop-acceleration/underapprox_false-unreach-call1.i false(reach) 3.2  1.7  160 wit false(reach) 5.0 2.9 240 true 11   5.9 310
loop-acceleration/underapprox_false-unreach-call2.i false(reach) 3.2  1.7  160 wit false(reach) 5.5 3.2 240 true 10   6.8 310
loop-acceleration/array_true-unreach-call1.i unknown 200    200    69 wit - -
loop-acceleration/array_true-unreach-call2.i unknown 200    200    69 wit - -
loop-acceleration/array_true-unreach-call3.i true .45 .48 22 wit - -
loop-acceleration/array_true-unreach-call4.i true .45 .48 22 wit - -
loop-acceleration/const_true-unreach-call1.i true .43 .47 21 wit - -
loop-acceleration/diamond_true-unreach-call1.i true .80 .84 25 wit - -
loop-acceleration/diamond_true-unreach-call2.i true .73 .77 55 wit - -
loop-acceleration/functions_true-unreach-call1.i true .39 .43 21 wit - -
loop-acceleration/multivar_true-unreach-call1.i true .44 .47 21 wit - -
loop-acceleration/nested_true-unreach-call1.i true .70 .74 21 wit - -
loop-acceleration/overflow_true-unreach-call1.i true .34 .37 21 wit - -
loop-acceleration/phases_true-unreach-call1.i true .36 .38 21 wit - -
loop-acceleration/phases_true-unreach-call2.i unknown 890    900    480 wit - -
loop-acceleration/simple_true-unreach-call1.i true .38 .41 21 wit - -
loop-acceleration/simple_true-unreach-call2.i unknown 58    59    30 wit - -
loop-acceleration/simple_true-unreach-call3.i true .49 .52 21 wit - -
loop-acceleration/simple_true-unreach-call4.i true .41 .44 21 wit - -
loop-acceleration/underapprox_true-unreach-call1.i true .39 .42 21 wit - -
loop-acceleration/underapprox_true-unreach-call2.i true 1.6  1.7  22 wit - -
loop-invgen/id_trans_false-unreach-call.i false(reach) 3.2  1.6  160 wit false(reach) 17   10   560 true 12   6.9 350
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call.i true 6.3  6.4  30 wit - -
loop-invgen/NetBSD_loop_true-unreach-call.i true .50 .54 22 wit - -
loop-invgen/SpamAssassin-loop_true-unreach-call.i unknown 900    900    1500 wit - -
loop-invgen/apache-escape-absolute_true-unreach-call.i true 690    690    80 wit - -
loop-invgen/apache-get-tag_true-unreach-call.i unknown 890    900    63 wit - -
loop-invgen/down_true-unreach-call.i true .51 .54 24 wit - -
loop-invgen/fragtest_simple_true-unreach-call.i true .49 .52 24 wit - -
loop-invgen/half_2_true-unreach-call.i true .68 .72 26 wit - -
loop-invgen/heapsort_true-unreach-call.i true 600    600    1400 wit - -
loop-invgen/id_build_true-unreach-call.i true 1.0  1.0  110 wit - -
loop-invgen/large_const_true-unreach-call.i true .68 .71 28 wit - -
loop-invgen/nest-if3_true-unreach-call.i true 38    38    190 wit - -
loop-invgen/nested6_true-unreach-call.i unknown 890    900    330 wit - -
loop-invgen/nested9_true-unreach-call.i true 3.8  3.9  780 wit - -
loop-invgen/sendmail-close-angle_true-unreach-call.i true .79 .82 23 wit - -
loop-invgen/seq_true-unreach-call.i true 1.3  1.3  25 wit - -
loop-invgen/string_concat-noarr_true-unreach-call.i true 15    15    130 wit - -
loop-invgen/up_true-unreach-call.i true .49 .51 22 wit - -
loop-lit/afnp2014_true-unreach-call.c.i true .54 .58 22 wit - -
loop-lit/bhmr2007_true-unreach-call.c.i unknown 890    900    38 wit - -
loop-lit/cggmp2005_true-unreach-call.c.i true .92 .97 21 wit - -
loop-lit/cggmp2005_variant_true-unreach-call.c.i unknown 58    59    32 wit - -
loop-lit/cggmp2005b_true-unreach-call.c.i true .41 .45 21 wit - -
loop-lit/css2003_true-unreach-call.c.i true .48 .51 22 wit - -
loop-lit/ddlm2013_true-unreach-call.c.i true .63 .66 49 wit - -
loop-lit/gj2007_true-unreach-call.c.i true 30    31    22 wit - -
loop-lit/gj2007b_true-unreach-call.c.i true .55 .58 22 wit - -
loop-lit/gr2006_true-unreach-call.c.i true 31    32    22 wit - -
loop-lit/gsv2008_true-unreach-call.c.i unknown 83    84    43 wit - -
loop-lit/hhk2008_true-unreach-call.c.i unknown 790    790    48 wit - -
loop-lit/jm2006_true-unreach-call.c.i unknown 60    62    27 wit - -
loop-lit/jm2006_variant_true-unreach-call.c.i unknown 71    72    29 wit - -
loop-lit/mcmillan2006_true-unreach-call.c.i true 720    720    90 wit - -
loop-new/count_by_1_true-unreach-call.i unknown 30    31    22 wit - -
loop-new/count_by_1_variant_true-unreach-call.i true .42 .46 21 wit - -
loop-new/count_by_2_true-unreach-call.i unknown 29    31    22 wit - -
loop-new/count_by_k_true-unreach-call.i unknown 40    41    29 wit - -
loop-new/count_by_nondet_true-unreach-call.i true .42 .44 42 wit - -
loop-new/gauss_sum_true-unreach-call.i unknown 42    43    26 wit - -
loop-new/half_true-unreach-call.i unknown 37    38    23 wit - -
loop-new/nested_true-unreach-call.i true 7.5  7.6  100 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   13000   18000 141 1100   860   28000   141 390   240   12000  
    correct results 90 2300   2300   8700 26 230   130   9000   25 280   170   8500  
        correct true 64 2200   2200   4400 0 0   0   0   25 0   0   0  
        correct false 26 120   80   4300 26 230   130   9000   0 280   170   8500  
    incorrect results 4 1.9 2.1 90 0 0   0   0   0 0   0   0  
        incorrect true 4 1.9 2.1 90 0 0   0   0   0 0   0   0  
        incorrect false 0
score (141 tasks, max score: 234) 26
Run set sv-comp16.Loops