Tool Forest svc_16_20151108
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]
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-09 23:49:59 CET [[ 2016-01-15 09:05:13 CET ]] [[ 2016-01-15 22:20:31 CET ]]
Run set sv-comp16.Loops
Options -svcomp [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/forest.2016-01-09_2349.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/forest.2016-01-09_2349.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 unknown .48  .54  38   wit - -
loops/bubble_sort_false-unreach-call.i unknown .17  .24  4.8 wit - -
loops/count_up_down_false-unreach-call_true-termination.i unknown .27  .37  7.4 wit - -
loops/eureka_01_false-unreach-call.i unknown .51  .59  38   wit - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i unknown .55  .65  38   wit - -
loops/insertion_sort_false-unreach-call.i true .65  .75  39   wit - -
loops/invert_string_false-unreach-call.i true .88  1.0   38   wit - -
loops/linear_search_false-unreach-call.i unknown .58  .66  38   wit - -
loops/ludcmp_false-unreach-call.i witness timeout 1.1   1.2   41   wit timeout 91   87   780 timeout 56   38   7000
loops/matrix_false-unreach-call_true-termination.i unknown .51  .58  38   wit - -
loops/n.c24_false-unreach-call.i true .91  1.1   39   wit - -
loops/nec11_false-unreach-call.i false(reach) .73  .87  38   wit false(reach) 4.5 2.6 240 true 9.5 6.4 330
loops/nec20_false-unreach-call.i unknown .62  .71  38   wit - -
loops/s3_false-unreach-call.i unknown .29  .37  5.7 wit - -
loops/string_false-unreach-call.i true .63  .76  38   wit - -
loops/sum01_bug02_false-unreach-call_true-termination.i false(reach) 3.1   3.7   38   wit false(reach) 21   11   750 true 10   6.0 340
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(reach) 2.2   2.7   41   wit false(reach) 18   9.7 620 true 10   7.6 320
loops/sum01_false-unreach-call_true-termination.i unknown .57  .66  38   wit - -
loops/sum03_false-unreach-call_true-termination.i unknown .45  .53  38   wit - -
loops/sum04_false-unreach-call_true-termination.i false(reach) .64  .73  38   wit false(reach) 5.0 2.9 230 true 11   7.6 320
loops/sum_array_false-unreach-call.i unknown .64  .72  36   wit - -
loops/terminator_01_false-unreach-call_false-termination.i false(reach) .54  .64  38   wit false(reach) 4.6 2.7 220 true 11   6.1 340
loops/terminator_02_false-unreach-call_true-termination.i true .61  .70  38   wit - -
loops/terminator_03_false-unreach-call_true-termination.i error (139) .92  1.1   38   wit - -
loops/trex01_false-unreach-call_true-termination.i true .63  .74  39   wit - -
loops/trex02_false-unreach-call_true-termination.i false(reach) .59  .71  38   wit false(reach) 4.5 2.7 230 true 11   7.3 320
loops/trex03_false-unreach-call_true-termination.i true .52  .61  38   wit - -
loops/verisec_NetBSD-libc__loop_false-unreach-call.i true .55  .64  38   wit - -
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.i unknown .15  .22  4.6 wit - -
loops/vogal_false-unreach-call.i true .58  .66  38   wit - -
loops/while_infinite_loop_4_false-unreach-call_true-termination.i error (139) 20     16     910   wit - -
loops/array_true-unreach-call.i true .57  .66  39   wit - -
loops/bubble_sort_true-unreach-call.i unknown .59  .66  39   wit - -
loops/count_up_down_true-unreach-call_true-termination.i true .53  .61  38   wit - -
loops/eureka_01_true-unreach-call.i true 1.7   1.9   39   wit - -
loops/eureka_05_true-unreach-call.i error (134) .85  1.0   38   wit - -
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true .79  .94  38   wit - -
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true 20     21     43   wit - -
loops/insertion_sort_true-unreach-call.i true 200     210     41   wit - -
loops/invert_string_true-unreach-call.i true 3.0   3.4   38   wit - -
loops/linear_sea.ch_true-unreach-call.i true .61  .70  38   wit - -
loops/lu.cmp_true-unreach-call.i unknown .71  .80  7.6 wit - -
loops/matrix_true-unreach-call_true-termination.i true 1.8   2.2   39   wit - -
loops/n.c11_true-unreach-call.i true .57  .67  38   wit - -
loops/n.c40_true-unreach-call.i true .79  .95  38   wit - -
loops/nec40_true-unreach-call.i true .56  .66  38   wit - -
loops/string_true-unreach-call.i true .60  .69  38   wit - -
loops/sum01_true-unreach-call_true-termination.i false(reach) 1.9   2.3   38   wit - -
loops/sum03_true-unreach-call_false-termination.i true .57  .67  38   wit - -
loops/sum04_true-unreach-call_true-termination.i unknown .49  .57  38   wit - -
loops/sum_array_true-unreach-call.i true .61  .70  38   wit - -
loops/terminator_02_true-unreach-call_true-termination.i true .60  .70  38   wit - -
loops/terminator_03_true-unreach-call_true-termination.i true .61  .72  38   wit - -
loops/trex01_true-unreach-call.i unknown .32  .41  7.6 wit - -
loops/trex02_true-unreach-call_true-termination.i true .51  .62  39   wit - -
loops/trex03_true-unreach-call.i true .70  .81  39   wit - -
loops/trex04_true-unreach-call_false-termination.i unknown .94  1.0   40   wit - -
loops/veris.c_NetBSD-libc__loop_true-unreach-call.i true .53  .62  38   wit - -
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.i unknown .16  .23  4.5 wit - -
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i true 2.4   2.9   38   wit - -
loops/vogal_true-unreach-call.i true .69  .81  39   wit - -
loops/while_infinite_loop_1_true-unreach-call_false-termination.i timeout 900     930     150   wit - -
loops/while_infinite_loop_2_true-unreach-call_false-termination.i unknown 16     16     38   wit - -
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true 16     16     38   wit - -
loop-acceleration/array_false-unreach-call1.i witness timeout .70  .83  41   wit timeout 91   83   3500 true 12   6.6 360
loop-acceleration/array_false-unreach-call2.i witness invalid (out of memory) .64  .73  39   wit out of memory 63   52   7000 true 10   5.8 320
loop-acceleration/array_false-unreach-call3.i unknown .47  .55  38   wit - -
loop-acceleration/const_false-unreach-call1.i false(reach) .52  .60  38   wit false(reach) 42   24   1500 true 10   7.1 320
loop-acceleration/diamond_false-unreach-call1.i true .59  .70  38   wit - -
loop-acceleration/functions_false-unreach-call1.i unknown 1.2   1.3   38   wit - -
loop-acceleration/multivar_false-unreach-call1.i true .51  .60  38   wit - -
loop-acceleration/nested_false-unreach-call1.i unknown 4.4   4.4   38   wit - -
loop-acceleration/phases_false-unreach-call1.i unknown .75  .84  7.5 wit - -
loop-acceleration/phases_false-unreach-call2.i unknown .55  .64  38   wit - -
loop-acceleration/simple_false-unreach-call1.i witness timeout .91  1.0   39   wit timeout 91   78   3800 true 9.8 6.8 310
loop-acceleration/simple_false-unreach-call2.i false(reach) 1.3   1.4   38   wit false(reach) 4.7 2.8 220 true 10   5.7 330
loop-acceleration/simple_false-unreach-call3.i false(reach) .44  .52  38   wit false(reach) 4.7 2.8 220 true 10   6.9 320
loop-acceleration/simple_false-unreach-call4.i witness timeout .77  .85  38   wit timeout 91   81   1400 true 10   6.9 310
loop-acceleration/underapprox_false-unreach-call1.i false(reach) .56  .66  38   wit false(reach) 4.8 2.8 240 true 11   7.1 320
loop-acceleration/underapprox_false-unreach-call2.i false(reach) .55  .64  38   wit false(reach) 5.0 3.0 240 true 12   6.8 330
loop-acceleration/array_true-unreach-call1.i true .65  .74  38   wit - -
loop-acceleration/array_true-unreach-call2.i error (134) 5.0   5.4   39   wit - -
loop-acceleration/array_true-unreach-call3.i true .67  .78  38   wit - -
loop-acceleration/array_true-unreach-call4.i unknown .62  .71  38   wit - -
loop-acceleration/const_true-unreach-call1.i true .60  .71  38   wit - -
loop-acceleration/diamond_true-unreach-call1.i true 98     110     43   wit - -
loop-acceleration/diamond_true-unreach-call2.i unknown .61  .70  38   wit - -
loop-acceleration/functions_true-unreach-call1.i true 1.1   1.2   38   wit - -
loop-acceleration/multivar_true-unreach-call1.i true .61  .70  38   wit - -
loop-acceleration/nested_true-unreach-call1.i unknown 4.4   4.4   38   wit - -
loop-acceleration/overflow_true-unreach-call1.i true 4.7   4.8   38   wit - -
loop-acceleration/phases_true-unreach-call1.i true 11     12     38   wit - -
loop-acceleration/phases_true-unreach-call2.i true 47     57     38   wit - -
loop-acceleration/simple_true-unreach-call1.i true 2.2   2.6   38   wit - -
loop-acceleration/simple_true-unreach-call2.i true 2.5   2.9   38   wit - -
loop-acceleration/simple_true-unreach-call3.i true 12     13     38   wit - -
loop-acceleration/simple_true-unreach-call4.i true 13     14     38   wit - -
loop-acceleration/underapprox_true-unreach-call1.i true .68  .81  38   wit - -
loop-acceleration/underapprox_true-unreach-call2.i unknown .52  .61  38   wit - -
loop-invgen/id_trans_false-unreach-call.i true 2.7   3.3   38   wit - -
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call.i true 22     24     39   wit - -
loop-invgen/NetBSD_loop_true-unreach-call.i true 3.0   3.5   38   wit - -
loop-invgen/SpamAssassin-loop_true-unreach-call.i unknown .57  .66  38   wit - -
loop-invgen/apache-escape-absolute_true-unreach-call.i unknown .59  .68  39   wit - -
loop-invgen/apache-get-tag_true-unreach-call.i true .62  .71  38   wit - -
loop-invgen/down_true-unreach-call.i unknown .43  .51  38   wit - -
loop-invgen/fragtest_simple_true-unreach-call.i unknown .50  .58  38   wit - -
loop-invgen/half_2_true-unreach-call.i true .18  .26  7.6 wit - -
loop-invgen/heapsort_true-unreach-call.i true .78  .92  39   wit - -
loop-invgen/id_build_true-unreach-call.i true .55  .65  38   wit - -
loop-invgen/large_const_true-unreach-call.i error (134) 2.5   3.0   39   wit - -
loop-invgen/nest-if3_true-unreach-call.i true .54  .63  38   wit - -
loop-invgen/nested6_true-unreach-call.i true 2.3   2.8   38   wit - -
loop-invgen/nested9_true-unreach-call.i true .65  .76  38   wit - -
loop-invgen/sendmail-close-angle_true-unreach-call.i true .75  .89  39   wit - -
loop-invgen/seq_true-unreach-call.i unknown .61  .71  38   wit - -
loop-invgen/string_concat-noarr_true-unreach-call.i unknown .57  .66  38   wit - -
loop-invgen/up_true-unreach-call.i false(reach) .54  .63  38   wit - -
loop-lit/afnp2014_true-unreach-call.c.i true 1.2   1.4   38   wit - -
loop-lit/bhmr2007_true-unreach-call.c.i false(reach) 1.7   2.0   39   wit - -
loop-lit/cggmp2005_true-unreach-call.c.i true .59  .70  38   wit - -
loop-lit/cggmp2005_variant_true-unreach-call.c.i unknown .51  .58  38   wit - -
loop-lit/cggmp2005b_true-unreach-call.c.i true .57  .67  38   wit - -
loop-lit/css2003_true-unreach-call.c.i false(reach) 15     16     39   wit - -
loop-lit/ddlm2013_true-unreach-call.c.i true .50  .58  38   wit - -
loop-lit/gj2007_true-unreach-call.c.i true 1.1   1.4   38   wit - -
loop-lit/gj2007b_true-unreach-call.c.i true .60  .69  38   wit - -
loop-lit/gr2006_true-unreach-call.c.i true .54  .65  38   wit - -
loop-lit/gsv2008_true-unreach-call.c.i true .65  .75  38   wit - -
loop-lit/hhk2008_true-unreach-call.c.i unknown .47  .54  38   wit - -
loop-lit/jm2006_true-unreach-call.c.i unknown .59  .67  38   wit - -
loop-lit/jm2006_variant_true-unreach-call.c.i true 1.1   1.3   38   wit - -
loop-lit/mcmillan2006_true-unreach-call.c.i error (139) .020 .026 3.4 wit - -
loop-new/count_by_1_true-unreach-call.i unknown .52  .60  38   wit - -
loop-new/count_by_1_variant_true-unreach-call.i true 2.5   2.9   39   wit - -
loop-new/count_by_2_true-unreach-call.i true 2.5   3.0   38   wit - -
loop-new/count_by_k_true-unreach-call.i true 2.8   3.4   38   wit - -
loop-new/count_by_nondet_true-unreach-call.i true .61  .73  38   wit - -
loop-new/gauss_sum_true-unreach-call.i unknown .59  .68  38   wit - -
loop-new/half_true-unreach-call.i true .62  .71  38   wit - -
loop-new/nested_true-unreach-call.i true .54  .64  38   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 1500   1600 6100 141 550   450   21000   141 210   140   12000  
    correct results 73 500   560 2800 11 120   67   4700   11 120   75   3600  
        correct true 62 490   540 2400 0 0   0   0   11 0   0   0  
        correct false 11 11   13 420 11 120   67   4700   0 120   75   3600  
    incorrect results 16 28   33 620 0 0   0   0   0 0   0   0  
        incorrect true 12 9.7 12 460 0 0   0   0   0 0   0   0  
        incorrect false 4 19   21 150 0 0   0   0   0 0   0   0  
score (141 tasks, max score: 234) -313
Run set sv-comp16.Loops