Tool symbiotic 3.0.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-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-07 09:04:54 CET [[ 2016-01-15 09:39:10 CET ]] [[ 2016-01-15 22:39:28 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/symbiotic3.2016-01-07_0904.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/symbiotic3.2016-01-07_0904.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 witness unconfirmed 18     18     6.5 wit true 4.7 2.7 230 unknown 9.4   7.2   320  
loops/bubble_sort_false-unreach-call.i false(reach) 18     18     33   wit false(reach) 15   8.0 490 unknown 9.4   5.5   300  
loops/count_up_down_false-unreach-call_true-termination.i false(reach) .21  .23  6.7 wit false(reach) 4.8 3.1 230 unknown 9.8   6.0   320  
loops/eureka_01_false-unreach-call.i witness timeout 790     790     11   wit timeout 90   76   800 unknown 9.7   7.1   300  
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(reach) 18     18     6.6 wit false(reach) 5.5 3.1 250 unknown 8.9   5.2   300  
loops/insertion_sort_false-unreach-call.i unknown .11  .13  7.1 wit - -
loops/invert_string_false-unreach-call.i unknown .23  .26  6.9 wit - -
loops/linear_search_false-unreach-call.i unknown .14  .18  7.0 wit - -
loops/ludcmp_false-unreach-call.i witness timeout 18     18     6.7 wit timeout 91   88   780 unknown 9.4   6.0   310  
loops/matrix_false-unreach-call_true-termination.i unknown .16  .19  7.0 wit - -
loops/n.c24_false-unreach-call.i timeout 900     900     23   wit - -
loops/nec11_false-unreach-call.i false(reach) .13  .16  6.6 wit false(reach) 4.7 2.7 230 unknown 9.1   5.8   320  
loops/nec20_false-unreach-call.i false(reach) .14  .17  6.8 wit false(reach) 5.7 3.3 250 unknown 8.4   5.1   310  
loops/s3_false-unreach-call.i unknown .85  1.0   20   wit - -
loops/string_false-unreach-call.i false(reach) 140     140     7.1 wit false(reach) 8.0 4.5 350 unknown 9.3   6.5   310  
loops/sum01_bug02_false-unreach-call_true-termination.i false(reach) 120     120     6.7 wit false(reach) 8.8 5.0 380 unknown 8.6   5.0   330  
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(reach) 36     36     6.8 wit false(reach) 5.2 3.1 240 unknown 9.4   5.5   310  
loops/sum01_false-unreach-call_true-termination.i false(reach) 190     190     6.7 wit false(reach) 12   6.8 450 unknown 9.3   5.4   310  
loops/sum03_false-unreach-call_true-termination.i false(reach) 19     19     6.7 wit false(reach) 7.0 4.0 350 unknown 9.3   6.3   320  
loops/sum04_false-unreach-call_true-termination.i false(reach) 18     18     6.7 wit false(reach) 4.9 2.8 240 unknown 10     5.8   330  
loops/sum_array_false-unreach-call.i unknown .24  .26  7.0 wit - -
loops/terminator_01_false-unreach-call_false-termination.i false(reach) .22  .25  8.2 wit false(reach) 4.4 2.7 230 unknown 9.0   5.3   310  
loops/terminator_02_false-unreach-call_true-termination.i false(reach) .21  .24  6.6 wit false(reach) 4.9 2.8 240 unknown 9.1   5.2   330  
loops/terminator_03_false-unreach-call_true-termination.i false(reach) .14  .16  7.1 wit false(reach) 4.8 2.7 250 unknown 8.7   5.7   300  
loops/trex01_false-unreach-call_true-termination.i false(reach) 18     18     6.7 wit false(reach) 4.2 2.4 230 unknown 11     7.3   310  
loops/trex02_false-unreach-call_true-termination.i false(reach) .23  .25  6.7 wit false(reach) 4.6 2.7 230 unknown 8.4   5.0   310  
loops/trex03_false-unreach-call_true-termination.i false(reach) .16  .19  8.0 wit false(reach) 4.9 3.0 230 unknown 8.7   5.1   330  
loops/verisec_NetBSD-libc__loop_false-unreach-call.i false(reach) 18     18     6.7 wit false(reach) 4.7 2.8 240 unknown 10     6.8   330  
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.i false(reach) 260     260     7.8 wit false(reach) 6.9 3.9 340 unknown 9.7   5.4   310  
loops/vogal_false-unreach-call.i false(reach) 77     77     6.9 wit false(reach) 10   6.5 400 unknown 9.0   5.7   300  
loops/while_infinite_loop_4_false-unreach-call_true-termination.i witness unconfirmed .10  .12  6.6 wit true 4.1 2.4 210 unknown 8.9   5.2   310  
loops/array_true-unreach-call.i true 18     18     7.0 wit - -
loops/bubble_sort_true-unreach-call.i true .093 .12  6.0 wit - -
loops/count_up_down_true-unreach-call_true-termination.i timeout 900     910     1500   wit - -
loops/eureka_01_true-unreach-call.i true 7.6   7.6   5.7 wit - -
loops/eureka_05_true-unreach-call.i true 18     18     5.8 wit - -
loops/for_infinite_loop_1_true-unreach-call_false-termination.i timeout 900     900     5.8 wit - -
loops/for_infinite_loop_2_true-unreach-call_false-termination.i timeout 900     900     5.9 wit - -
loops/insertion_sort_true-unreach-call.i unknown .22  .24  7.0 wit - -
loops/invert_string_true-unreach-call.i unknown .11  .12  5.7 wit - -
loops/linear_sea.ch_true-unreach-call.i unknown 18     18     7.2 wit - -
loops/lu.cmp_true-unreach-call.i true 18     18     6.4 wit - -
loops/matrix_true-unreach-call_true-termination.i true 35     35     7.3 wit - -
loops/n.c11_true-unreach-call.i timeout 900     900     6.5 wit - -
loops/n.c40_true-unreach-call.i true .16  .19  5.8 wit - -
loops/nec40_true-unreach-call.i true .15  .18  6.0 wit - -
loops/string_true-unreach-call.i timeout 900     900     7.7 wit - -
loops/sum01_true-unreach-call_true-termination.i timeout 900     900     25   wit - -
loops/sum03_true-unreach-call_false-termination.i true 28     28     380   wit - -
loops/sum04_true-unreach-call_true-termination.i true 18     18     5.8 wit - -
loops/sum_array_true-unreach-call.i unknown .20  .23  7.1 wit - -
loops/terminator_02_true-unreach-call_true-termination.i true 18     18     7.2 wit - -
loops/terminator_03_true-unreach-call_true-termination.i timeout 900     900     27   wit - -
loops/trex01_true-unreach-call.i timeout 900     900     8.8 wit - -
loops/trex02_true-unreach-call_true-termination.i true .11  .13  7.0 wit - -
loops/trex03_true-unreach-call.i timeout 900     900     300   wit - -
loops/trex04_true-unreach-call_false-termination.i timeout 900     910     1000   wit - -
loops/veris.c_NetBSD-libc__loop_true-unreach-call.i true 18     18     5.7 wit - -
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.i true .10  .12  5.9 wit - -
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i true .18  .21  6.1 wit - -
loops/vogal_true-unreach-call.i timeout 900     900     7.7 wit - -
loops/while_infinite_loop_1_true-unreach-call_false-termination.i timeout 900     900     5.8 wit - -
loops/while_infinite_loop_2_true-unreach-call_false-termination.i timeout 900     900     5.8 wit - -
loops/while_infinite_loop_3_true-unreach-call_false-termination.i timeout 900     900     5.9 wit - -
loop-acceleration/array_false-unreach-call1.i witness timeout 18     18     6.8 wit timeout 91   82   3300 unknown 9.5   6.0   310  
loop-acceleration/array_false-unreach-call2.i witness invalid (out of memory) 18     18     8.2 wit out of memory 75   61   7000 unknown 9.1   5.1   320  
loop-acceleration/array_false-unreach-call3.i timeout 900     900     7.3 wit - -
loop-acceleration/const_false-unreach-call1.i false(reach) 18     18     6.6 wit false(reach) 44   26   1500 unknown 8.9   5.2   310  
loop-acceleration/diamond_false-unreach-call1.i witness timeout 18     18     6.9 wit timeout 92   76   1600 unknown 11     5.8   330  
loop-acceleration/functions_false-unreach-call1.i witness timeout .18  .20  6.6 wit timeout 91   82   770 unknown 10     6.0   330  
loop-acceleration/multivar_false-unreach-call1.i false(reach) 18     18     6.6 wit false(reach) 4.7 2.8 220 unknown 9.2   5.7   320  
loop-acceleration/nested_false-unreach-call1.i timeout 870     930     15000   wit - -
loop-acceleration/phases_false-unreach-call1.i witness timeout 630     690     15000   wit timeout 91   81   1600 unknown 8.9   5.3   320  
loop-acceleration/phases_false-unreach-call2.i false(reach) 18     18     6.7 wit false(reach) 4.4 2.5 240 unknown 9.6   6.6   310  
loop-acceleration/simple_false-unreach-call1.i witness timeout .11  .13  6.8 wit timeout 91   79   3700 unknown 9.1   7.0   300  
loop-acceleration/simple_false-unreach-call2.i false(reach) .21  .23  6.7 wit false(reach) 3.9 2.3 230 unknown 8.6   5.2   320  
loop-acceleration/simple_false-unreach-call3.i witness timeout .18  .21  6.6 wit timeout 91   78   1400 unknown 10     6.2   330  
loop-acceleration/simple_false-unreach-call4.i witness timeout .11  .14  6.6 wit timeout 90   81   770 unknown 9.7   5.8   310  
loop-acceleration/underapprox_false-unreach-call1.i witness unconfirmed 18     18     7.9 wit true 4.2 2.5 210 unknown 9.7   6.1   310  
loop-acceleration/underapprox_false-unreach-call2.i witness unconfirmed .12  .14  6.6 wit true 4.3 2.5 210 unknown 9.5   6.3   320  
loop-acceleration/array_true-unreach-call1.i true 18     18     5.9 wit - -
loop-acceleration/array_true-unreach-call2.i true 18     18     7.0 wit - -
loop-acceleration/array_true-unreach-call3.i unknown 120     120     120   wit - -
loop-acceleration/array_true-unreach-call4.i true 120     120     110   wit - -
loop-acceleration/const_true-unreach-call1.i true 18     18     5.8 wit - -
loop-acceleration/diamond_true-unreach-call1.i true 36     36     7.4 wit - -
loop-acceleration/diamond_true-unreach-call2.i true .19  .22  6.2 wit - -
loop-acceleration/functions_true-unreach-call1.i true .067 .082 5.7 wit - -
loop-acceleration/multivar_true-unreach-call1.i true 87     90     160   wit - -
loop-acceleration/nested_true-unreach-call1.i timeout 880     930     15000   wit - -
loop-acceleration/overflow_true-unreach-call1.i true .098 .12  5.7 wit - -
loop-acceleration/phases_true-unreach-call1.i true 610     670     15000   wit - -
loop-acceleration/phases_true-unreach-call2.i timeout 900     910     9200   wit - -
loop-acceleration/simple_true-unreach-call1.i true .16  .18  5.6 wit - -
loop-acceleration/simple_true-unreach-call2.i true .17  .20  6.0 wit - -
loop-acceleration/simple_true-unreach-call3.i timeout 900     900     9.5 wit - -
loop-acceleration/simple_true-unreach-call4.i true .17  .19  5.7 wit - -
loop-acceleration/underapprox_true-unreach-call1.i true 18     18     5.6 wit - -
loop-acceleration/underapprox_true-unreach-call2.i true .095 .11  5.6 wit - -
loop-invgen/id_trans_false-unreach-call.i witness unconfirmed .18  .21  7.2 wit unknown 3.3 2.0 150 error (1) .024 .029 5.2
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call.i timeout 900     900     9.6 wit - -
loop-invgen/NetBSD_loop_true-unreach-call.i timeout 900     900     8.2 wit - -
loop-invgen/SpamAssassin-loop_true-unreach-call.i timeout 900     900     8.3 wit - -
loop-invgen/apache-escape-absolute_true-unreach-call.i timeout 900     900     8.2 wit - -
loop-invgen/apache-get-tag_true-unreach-call.i timeout 900     900     7.8 wit - -
loop-invgen/down_true-unreach-call.i timeout 900     900     22   wit - -
loop-invgen/fragtest_simple_true-unreach-call.i timeout 900     900     35   wit - -
loop-invgen/half_2_true-unreach-call.i unknown 36     36     7.3 wit - -
loop-invgen/heapsort_true-unreach-call.i false(reach) 18     18     7.4 wit - -
loop-invgen/id_build_true-unreach-call.i timeout 900     900     8.9 wit - -
loop-invgen/large_const_true-unreach-call.i unknown 35     35     7.2 wit - -
loop-invgen/nest-if3_true-unreach-call.i timeout 900     900     270   wit - -
loop-invgen/nested6_true-unreach-call.i timeout 900     900     10   wit - -
loop-invgen/nested9_true-unreach-call.i timeout 900     900     36   wit - -
loop-invgen/sendmail-close-angle_true-unreach-call.i timeout 900     900     9.9 wit - -
loop-invgen/seq_true-unreach-call.i timeout 900     930     270   wit - -
loop-invgen/string_concat-noarr_true-unreach-call.i timeout 900     900     220   wit - -
loop-invgen/up_true-unreach-call.i timeout 900     900     8.4 wit - -
loop-lit/afnp2014_true-unreach-call.c.i timeout 900     900     6.7 wit - -
loop-lit/bhmr2007_true-unreach-call.c.i timeout 900     910     290   wit - -
loop-lit/cggmp2005_true-unreach-call.c.i true 18     18     5.8 wit - -
loop-lit/cggmp2005_variant_true-unreach-call.c.i timeout 900     900     12   wit - -
loop-lit/cggmp2005b_true-unreach-call.c.i true 18     18     5.4 wit - -
loop-lit/css2003_true-unreach-call.c.i true 55     56     690   wit - -
loop-lit/ddlm2013_true-unreach-call.c.i timeout 900     900     140   wit - -
loop-lit/gj2007_true-unreach-call.c.i true 17     17     5.9 wit - -
loop-lit/gj2007b_true-unreach-call.c.i timeout 900     900     240   wit - -
loop-lit/gr2006_true-unreach-call.c.i true 18     18     5.8 wit - -
loop-lit/gsv2008_true-unreach-call.c.i timeout 900     900     22   wit - -
loop-lit/hhk2008_true-unreach-call.c.i timeout 900     900     17   wit - -
loop-lit/jm2006_true-unreach-call.c.i timeout 900     920     1200   wit - -
loop-lit/jm2006_variant_true-unreach-call.c.i timeout 900     920     1900   wit - -
loop-lit/mcmillan2006_true-unreach-call.c.i unknown .12  .15  7.1 wit - -
loop-new/count_by_1_true-unreach-call.i true .077 .098 5.7 wit - -
loop-new/count_by_1_variant_true-unreach-call.i true 22     22     360   wit - -
loop-new/count_by_2_true-unreach-call.i true .085 .10  5.7 wit - -
loop-new/count_by_k_true-unreach-call.i timeout 900     900     79   wit - -
loop-new/count_by_nondet_true-unreach-call.i timeout 900     900     19   wit - -
loop-new/gauss_sum_true-unreach-call.i timeout 900     900     76   wit - -
loop-new/half_true-unreach-call.i timeout 900     900     7.8 wit - -
loop-new/nested_true-unreach-call.i timeout 900     900     7.7 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 80000   141 1100   900   31000   141 350   220   12000  
    correct results 62 2200 2300 17000   24 190   110   8000   0 220   140   7500  
        correct true 38 1300 1300 17000   0 0   0   0   0 0   0   0  
        correct false 24 990 990 190   24 190   110   8000   0 220   140   7500  
    incorrect results 1 18 18 7.4 0 0   0   0   0 0   0   0  
        incorrect true 0
        incorrect false 1 18 18 7.4 0 0   0   0   0 0   0   0  
score (141 tasks, max score: 234) 84
Run set sv-comp16.Loops