Tool 2LS 0.3.4
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-02 22:42:27 CET [[ 2016-01-15 08:01:51 CET ]] [[ 2016-01-15 21:37:22 CET ]]
Run set 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 ]]
../../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) .099 .10  24 wit false(reach) 5.4 3.1 250 false(reach) 11 7.5 340
loops/bubble_sort_false-unreach-call.i false(reach) .74  .74  94 wit false(reach) 17   9.1 580 error 12 8.1 330
loops/count_up_down_false-unreach-call_true-termination.i false(reach) .10  .11  23 wit false(reach) 4.8 2.8 240 false(reach) 11 6.4 340
loops/eureka_01_false-unreach-call.i witness timeout 1.8   1.8   60 wit timeout 91   79   1400 true 14 7.8 360
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(reach) .32  .32  26 wit false(reach) 4.8 2.8 230 false(reach) 13 7.9 350
loops/insertion_sort_false-unreach-call.i witness timeout 520     520     7700 wit timeout 90   73   1500 timeout 91 65   1700
loops/invert_string_false-unreach-call.i false(reach) 1.3   1.3   52 wit timeout 90   75   1500 false(reach) 21 12   480
loops/linear_search_false-unreach-call.i false(reach) 1.9   1.9   79 wit true 11   5.9 400 false(reach) 75 66   380
loops/ludcmp_false-unreach-call.i timeout 900     900     4200 wit - -
loops/matrix_false-unreach-call_true-termination.i false(reach) 140     140     2500 wit timeout 91   83   1300 false(reach) 13 7.2 340
loops/n.c24_false-unreach-call.i timeout 900     900     1800 wit - -
loops/nec11_false-unreach-call.i false(reach) .11  .11  23 wit false(reach) 4.3 2.4 240 false(reach) 12 6.6 350
loops/nec20_false-unreach-call.i false(reach) 1.5   1.5   73 wit false(reach) 4.7 2.7 250 false(reach) 12 6.8 340
loops/s3_false-unreach-call.i witness unconfirmed 560     560     1100 wit true 10   5.4 430 true 19 10   380
loops/string_false-unreach-call.i false(reach) 3.2   3.2   65 wit false(reach) 6.9 4.0 360 false(reach) 29 18   420
loops/sum01_bug02_false-unreach-call_true-termination.i false(reach) 1.3   1.3   41 wit timeout 90   76   1900 false(reach) 14 8.9 330
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(reach) .56  .56  31 wit timeout 90   76   1600 false(reach) 13 7.7 330
loops/sum01_false-unreach-call_true-termination.i false(reach) 1.2   1.2   37 wit timeout 90   76   1600 false(reach) 16 8.8 350
loops/sum03_false-unreach-call_true-termination.i false(reach) .81  .81  36 wit false(reach) 6.2 3.5 340 false(reach) 20 11   460
loops/sum04_false-unreach-call_true-termination.i false(reach) .91  .92  36 wit false(reach) 5.1 3.0 230 false(reach) 13 11   330
loops/sum_array_false-unreach-call.i false(reach) .57  .57  47 wit false(reach) 9.4 5.6 410 false(reach) 13 7.7 330
loops/terminator_01_false-unreach-call_false-termination.i false(reach) .15  .15  23 wit false(reach) 4.7 2.7 230 false(reach) 11 8.1 320
loops/terminator_02_false-unreach-call_true-termination.i false(reach) .11  .12  23 wit false(reach) 5.1 2.9 230 false(reach) 12 6.4 360
loops/terminator_03_false-unreach-call_true-termination.i false(reach) .083 .084 23 wit false(reach) 4.6 2.7 230 false(reach) 12 7.7 360
loops/trex01_false-unreach-call_true-termination.i false(reach) .12  .12  24 wit false(reach) 6.9 3.8 340 false(reach) 12 6.9 340
loops/trex02_false-unreach-call_true-termination.i false(reach) .10  .10  23 wit false(reach) 4.3 2.5 240 false(reach) 11 6.2 350
loops/trex03_false-unreach-call_true-termination.i false(reach) .11  .11  23 wit false(reach) 5.4 3.1 240 false(reach) 12 6.8 350
loops/verisec_NetBSD-libc__loop_false-unreach-call.i false(reach) .14  .14  25 wit false(reach) 4.7 2.8 230 false(reach) 13 7.4 340
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.i witness timeout .66  .67  37 wit timeout 91   79   1400 true 11 6.0 330
loops/vogal_false-unreach-call.i witness timeout 39     39     270 wit timeout 90   77   1400 timeout 91 75   1100
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(reach) .11  .11  23 wit false(reach) 4.4 2.6 220 false(reach) 11 6.2 320
loops/array_true-unreach-call.i true .18  .18  24 wit - -
loops/bubble_sort_true-unreach-call.i true .11  .11  23 wit - -
loops/count_up_down_true-unreach-call_true-termination.i timeout 900     900     1300 wit - -
loops/eureka_01_true-unreach-call.i true 35     35     260 wit - -
loops/eureka_05_true-unreach-call.i true 6.5   6.5   110 wit - -
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true .10  .11  23 wit - -
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true .13  .13  23 wit - -
loops/insertion_sort_true-unreach-call.i timeout 900     900     6100 wit - -
loops/invert_string_true-unreach-call.i true 2.0   2.0   52 wit - -
loops/linear_sea.ch_true-unreach-call.i timeout 900     900     5400 wit - -
loops/lu.cmp_true-unreach-call.i true 15     15     4000 wit - -
loops/matrix_true-unreach-call_true-termination.i true .19  .20  26 wit - -
loops/n.c11_true-unreach-call.i timeout 900     900     1600 wit - -
loops/n.c40_true-unreach-call.i true .12  .12  27 wit - -
loops/nec40_true-unreach-call.i true .15  .16  29 wit - -
loops/string_true-unreach-call.i true .13  .13  24 wit - -
loops/sum01_true-unreach-call_true-termination.i timeout 900     900     1500 wit - -
loops/sum03_true-unreach-call_false-termination.i timeout 900     900     320 wit - -
loops/sum04_true-unreach-call_true-termination.i true .99  1.0   40 wit - -
loops/sum_array_true-unreach-call.i timeout 900     900     8700 wit - -
loops/terminator_02_true-unreach-call_true-termination.i true .11  .11  23 wit - -
loops/terminator_03_true-unreach-call_true-termination.i true .10  .10  23 wit - -
loops/trex01_true-unreach-call.i true 15     15     190 wit - -
loops/trex02_true-unreach-call_true-termination.i true .10  .11  23 wit - -
loops/trex03_true-unreach-call.i true .12  .13  23 wit - -
loops/trex04_true-unreach-call_false-termination.i true .15  .15  23 wit - -
loops/veris.c_NetBSD-libc__loop_true-unreach-call.i true .15  .15  23 wit - -
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.i true .13  .13  23 wit - -
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i true .11  .11  23 wit - -
loops/vogal_true-unreach-call.i true 9.3   9.3   130 wit - -
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true .11  .11  23 wit - -
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true .10  .10  23 wit - -
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true .10  .11  23 wit - -
loop-acceleration/array_false-unreach-call1.i timeout 900     900     1200 wit - -
loop-acceleration/array_false-unreach-call2.i timeout 900     900     1500 wit - -
loop-acceleration/array_false-unreach-call3.i timeout 900     900     6800 wit - -
loop-acceleration/const_false-unreach-call1.i timeout 900     900     1400 wit - -
loop-acceleration/diamond_false-unreach-call1.i false(reach) 1.3   1.3   37 wit false(reach) 7.8 4.3 370 timeout 90 63   4000
loop-acceleration/functions_false-unreach-call1.i timeout 900     900     1600 wit - -
loop-acceleration/multivar_false-unreach-call1.i false(reach) .10  .11  23 wit false(reach) 5.0 2.8 240 false(reach) 11 7.2 350
loop-acceleration/nested_false-unreach-call1.i timeout 900     900     8600 wit - -
loop-acceleration/phases_false-unreach-call1.i timeout 900     900     1300 wit - -
loop-acceleration/phases_false-unreach-call2.i false(reach) .14  .14  25 wit false(reach) 4.5 2.7 230 false(reach) 11 6.5 340
loop-acceleration/simple_false-unreach-call1.i timeout 900     900     1200 wit - -
loop-acceleration/simple_false-unreach-call2.i false(reach) .12  .12  23 wit false(reach) 4.5 2.7 220 false(reach) 10 5.8 340
loop-acceleration/simple_false-unreach-call3.i false(reach) .10  .10  23 wit false(reach) 4.5 2.6 230 false(reach) 12 6.8 340
loop-acceleration/simple_false-unreach-call4.i timeout 900     900     1000 wit - -
loop-acceleration/underapprox_false-unreach-call1.i false(reach) .33  .34  30 wit false(reach) 4.6 2.7 250 false(reach) 15 8.7 380
loop-acceleration/underapprox_false-unreach-call2.i false(reach) .41  .41  29 wit false(reach) 4.6 2.8 230 false(reach) 17 9.6 380
loop-acceleration/array_true-unreach-call1.i true 47     47     700 wit - -
loop-acceleration/array_true-unreach-call2.i timeout 900     900     15000 wit - -
loop-acceleration/array_true-unreach-call3.i true .41  .42  54 wit - -
loop-acceleration/array_true-unreach-call4.i timeout 900     900     6900 wit - -
loop-acceleration/const_true-unreach-call1.i true .24  .25  25 wit - -
loop-acceleration/diamond_true-unreach-call1.i true 1.1   1.1   37 wit - -
loop-acceleration/diamond_true-unreach-call2.i true .27  .28  29 wit - -
loop-acceleration/functions_true-unreach-call1.i timeout 900     900     1600 wit - -
loop-acceleration/multivar_true-unreach-call1.i timeout 900     900     1400 wit - -
loop-acceleration/nested_true-unreach-call1.i true .14  .14  25 wit - -
loop-acceleration/overflow_true-unreach-call1.i timeout 900     900     1200 wit - -
loop-acceleration/phases_true-unreach-call1.i timeout 900     900     1300 wit - -
loop-acceleration/phases_true-unreach-call2.i true .13  .14  26 wit - -
loop-acceleration/simple_true-unreach-call1.i timeout 900     900     1400 wit - -
loop-acceleration/simple_true-unreach-call2.i true .079 .083 23 wit - -
loop-acceleration/simple_true-unreach-call3.i timeout 900     900     1000 wit - -
loop-acceleration/simple_true-unreach-call4.i true .10  .11  23 wit - -
loop-acceleration/underapprox_true-unreach-call1.i true .47  .47  29 wit - -
loop-acceleration/underapprox_true-unreach-call2.i true .13  .14  24 wit - -
loop-invgen/id_trans_false-unreach-call.i false(reach) .12  .13  24 wit false(reach) 4.7 2.7 250 false(reach) 11 6.1 330
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call.i timeout 900     900     570 wit - -
loop-invgen/NetBSD_loop_true-unreach-call.i true .26  .26  25 wit - -
loop-invgen/SpamAssassin-loop_true-unreach-call.i true .55  .55  31 wit - -
loop-invgen/apache-escape-absolute_true-unreach-call.i true 2.7   2.7   48 wit - -
loop-invgen/apache-get-tag_true-unreach-call.i true 1.4   1.5   33 wit - -
loop-invgen/down_true-unreach-call.i timeout 900     900     1600 wit - -
loop-invgen/fragtest_simple_true-unreach-call.i timeout 900     900     3100 wit - -
loop-invgen/half_2_true-unreach-call.i timeout 900     900     1900 wit - -
loop-invgen/heapsort_true-unreach-call.i timeout 900     900     1500 wit - -
loop-invgen/id_build_true-unreach-call.i true .28  .29  26 wit - -
loop-invgen/large_const_true-unreach-call.i true .37  .37  28 wit - -
loop-invgen/nest-if3_true-unreach-call.i true 1.4   1.4   41 wit - -
loop-invgen/nested6_true-unreach-call.i timeout 900     900     1300 wit - -
loop-invgen/nested9_true-unreach-call.i timeout 900     900     360 wit - -
loop-invgen/sendmail-close-angle_true-unreach-call.i timeout 900     900     2100 wit - -
loop-invgen/seq_true-unreach-call.i timeout 900     900     1100 wit - -
loop-invgen/string_concat-noarr_true-unreach-call.i true .14  .14  24 wit - -
loop-invgen/up_true-unreach-call.i timeout 900     900     1900 wit - -
loop-lit/afnp2014_true-unreach-call.c.i timeout 900     900     2000 wit - -
loop-lit/bhmr2007_true-unreach-call.c.i timeout 900     900     320 wit - -
loop-lit/cggmp2005_true-unreach-call.c.i true .38  .38  28 wit - -
loop-lit/cggmp2005_variant_true-unreach-call.c.i timeout 900     900     1700 wit - -
loop-lit/cggmp2005b_true-unreach-call.c.i true 1.5   1.5   44 wit - -
loop-lit/css2003_true-unreach-call.c.i true .74  .74  32 wit - -
loop-lit/ddlm2013_true-unreach-call.c.i timeout 900     900     1900 wit - -
loop-lit/gj2007_true-unreach-call.c.i true 7.2   7.2   96 wit - -
loop-lit/gj2007b_true-unreach-call.c.i timeout 900     900     1100 wit - -
loop-lit/gr2006_true-unreach-call.c.i true 12     12     140 wit - -
loop-lit/gsv2008_true-unreach-call.c.i timeout 900     900     630 wit - -
loop-lit/hhk2008_true-unreach-call.c.i timeout 900     900     370 wit - -
loop-lit/jm2006_true-unreach-call.c.i timeout 900     900     1300 wit - -
loop-lit/jm2006_variant_true-unreach-call.c.i timeout 900     900     1500 wit - -
loop-lit/mcmillan2006_true-unreach-call.c.i killed by signal 9 810     810     15000 wit - -
loop-new/count_by_1_true-unreach-call.i true .16  .16  24 wit - -
loop-new/count_by_1_variant_true-unreach-call.i true .26  .26  25 wit - -
loop-new/count_by_2_true-unreach-call.i timeout 900     900     1000 wit - -
loop-new/count_by_k_true-unreach-call.i timeout 900     900     1000 wit - -
loop-new/count_by_nondet_true-unreach-call.i timeout 900     900     1300 wit - -
loop-new/gauss_sum_true-unreach-call.i timeout 900     900     1400 wit - -
loop-new/half_true-unreach-call.i timeout 900     900     1600 wit - -
loop-new/nested_true-unreach-call.i timeout 900     900     2400 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 48000 48000 150000 141 980   790   21000   141 800   540   19000  
    correct results 84 320 320 10000 27 610   480   15000   30 570   370   15000  
        correct true 52 160 170 6900 1 0   0   0   0 0   0   0  
        correct false 32 160 160 3600 26 610   480   15000   30 570   370   15000  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (141 tasks, max score: 234) 136
Run set sv-comp16.Loops