Tool impara 0.45
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-13 07:41:14 CET [[ 2016-01-15 09:11:00 CET ]] [[ 2016-01-15 22:23:23 CET ]]
Run set sv-comp16.Loops
Options --eager --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/impara.2016-01-13_0741.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/impara.2016-01-13_0741.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) .12  .12  25 wit false(reach) 4.8 2.8 240 false(reach) 11 6.6 330
loops/bubble_sort_false-unreach-call.i invalid output .70  .71  31 wit - -
loops/count_up_down_false-unreach-call_true-termination.i false(reach) .11  .11  23 wit false(reach) 4.7 2.8 220 false(reach) 11 6.6 350
loops/eureka_01_false-unreach-call.i false(reach) 240     240     54 wit timeout 90   75   930 false(reach) 39 26   840
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(reach) .17  .17  23 wit false(reach) 5.5 3.2 240 false(reach) 11 7.2 320
loops/insertion_sort_false-unreach-call.i witness timeout 180     180     150 wit timeout 90   75   1500 timeout 92 64   1500
loops/invert_string_false-unreach-call.i false(reach) .71  .71  26 wit false(reach) 7.2 4.0 370 false(reach) 14 8.5 350
loops/linear_search_false-unreach-call.i witness unconfirmed 5.3   5.3   38 wit true 5.9 3.3 250 error 32 23   500
loops/ludcmp_false-unreach-call.i witness unconfirmed 6.7   6.7   990 wit true 23   12   910 timeout 58 39   7000
loops/matrix_false-unreach-call_true-termination.i false(reach) .32  .32  24 wit timeout 90   77   1400 false(reach) 13 7.0 340
loops/n.c24_false-unreach-call.i timeout 900     900     140 wit - -
loops/nec11_false-unreach-call.i false(reach) .10  .11  23 wit false(reach) 4.1 2.4 230 false(reach) 13 7.2 340
loops/nec20_false-unreach-call.i false(reach) .38  .38  49 wit false(reach) 43   36   870 false(reach) 12 7.4 330
loops/s3_false-unreach-call.i error (8) 7.1   7.1   33 wit - -
loops/string_false-unreach-call.i false(reach) .52  .52  25 wit false(reach) 6.8 3.9 360 false(reach) 28 16   370
loops/sum01_bug02_false-unreach-call_true-termination.i false(reach) .59  .59  23 wit false(reach) 6.0 3.5 250 false(reach) 15 8.3 340
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(reach) .21  .21  23 wit false(reach) 5.5 3.2 240 false(reach) 13 7.4 320
loops/sum01_false-unreach-call_true-termination.i false(reach) .42  .42  23 wit false(reach) 7.7 4.3 350 false(reach) 26 18   470
loops/sum03_false-unreach-call_true-termination.i false(reach) .25  .25  23 wit false(reach) 7.0 3.9 370 false(reach) 27 17   490
loops/sum04_false-unreach-call_true-termination.i false(reach) .15  .15  27 wit false(reach) 5.4 3.2 240 false(reach) 15 9.9 340
loops/sum_array_false-unreach-call.i false(reach) .34  .34  24 wit timeout 90   76   1500 false(reach) 13 7.6 350
loops/terminator_01_false-unreach-call_false-termination.i false(reach) .10  .11  23 wit false(reach) 4.6 2.7 230 false(reach) 12 7.3 330
loops/terminator_02_false-unreach-call_true-termination.i false(reach) .084 .088 23 wit false(reach) 4.4 2.6 240 false(reach) 11 6.5 320
loops/terminator_03_false-unreach-call_true-termination.i false(reach) .093 .094 23 wit false(reach) 4.7 2.8 230 false(reach) 12 7.6 340
loops/trex01_false-unreach-call_true-termination.i false(reach) .13  .13  25 wit false(reach) 5.0 2.9 240 false(reach) 12 6.3 330
loops/trex02_false-unreach-call_true-termination.i false(reach) .10  .11  25 wit false(reach) 4.0 2.4 230 false(reach) 11 6.7 340
loops/trex03_false-unreach-call_true-termination.i false(reach) .084 .091 23 wit false(reach) 5.3 3.0 230 false(reach) 12 7.3 320
loops/verisec_NetBSD-libc__loop_false-unreach-call.i false(reach) .11  .12  23 wit true 5.3 3.1 230 false(reach) 14 7.8 350
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.i false(reach) 1.6   1.6   26 wit false(reach) 7.1 3.9 340 false(reach) 25 14   490
loops/vogal_false-unreach-call.i false(reach) 12     12     27 wit false(reach) 11   6.4 430 timeout 91 74   1200
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(reach) .12  .12  23 wit false(reach) 4.6 2.7 230 false(reach) 11 7.0 330
loops/array_true-unreach-call.i true .17  .17  23 wit - -
loops/bubble_sort_true-unreach-call.i true .14  .14  23 wit - -
loops/count_up_down_true-unreach-call_true-termination.i timeout 900     900     61 wit - -
loops/eureka_01_true-unreach-call.i true 290     290     61 wit - -
loops/eureka_05_true-unreach-call.i segmentation fault .42  .42  33 wit - -
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true .13  .13  23 wit - -
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true .14  .14  23 wit - -
loops/insertion_sort_true-unreach-call.i timeout 900     900     1100 wit - -
loops/invert_string_true-unreach-call.i true 1.4   1.4   24 wit - -
loops/linear_sea.ch_true-unreach-call.i timeout 900     900     180 wit - -
loops/lu.cmp_true-unreach-call.i out of memory 190     190     15000 wit - -
loops/matrix_true-unreach-call_true-termination.i true .33  .33  26 wit - -
loops/n.c11_true-unreach-call.i timeout 900     900     510 wit - -
loops/n.c40_true-unreach-call.i true .078 .081 23 wit - -
loops/nec40_true-unreach-call.i true .094 .098 23 wit - -
loops/string_true-unreach-call.i true 53     53     31 wit - -
loops/sum01_true-unreach-call_true-termination.i timeout 900     900     40 wit - -
loops/sum03_true-unreach-call_false-termination.i timeout 900     900     29 wit - -
loops/sum04_true-unreach-call_true-termination.i true .096 .10  23 wit - -
loops/sum_array_true-unreach-call.i timeout 900     900     180 wit - -
loops/terminator_02_true-unreach-call_true-termination.i true .14  .14  23 wit - -
loops/terminator_03_true-unreach-call_true-termination.i true .11  .12  23 wit - -
loops/trex01_true-unreach-call.i timeout 900     900     35 wit - -
loops/trex02_true-unreach-call_true-termination.i true .085 .089 23 wit - -
loops/trex03_true-unreach-call.i true .13  .13  23 wit - -
loops/trex04_true-unreach-call_false-termination.i true .18  .18  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 .097 .10  23 wit - -
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i true .11  .12  23 wit - -
loops/vogal_true-unreach-call.i true 130     130     32 wit - -
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true .14  .14  22 wit - -
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true .11  .12  22 wit - -
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true .13  .14  22 wit - -
loop-acceleration/array_false-unreach-call1.i timeout 900     900     59 wit - -
loop-acceleration/array_false-unreach-call2.i timeout 900     900     29 wit - -
loop-acceleration/array_false-unreach-call3.i timeout 900     900     110 wit - -
loop-acceleration/const_false-unreach-call1.i false(reach) 860     860     52 wit false(reach) 61   36   1700 timeout 91 56   4400
loop-acceleration/diamond_false-unreach-call1.i false(reach) 4.8   4.8   24 wit false(reach) 8.7 4.8 390 timeout 90 68   1400
loop-acceleration/functions_false-unreach-call1.i timeout 900     900     31 wit - -
loop-acceleration/multivar_false-unreach-call1.i false(reach) .14  .14  23 wit false(reach) 4.8 2.9 230 false(reach) 11 7.8 320
loop-acceleration/nested_false-unreach-call1.i timeout 900     900     36 wit - -
loop-acceleration/phases_false-unreach-call1.i timeout 900     900     27 wit - -
loop-acceleration/phases_false-unreach-call2.i false(reach) .084 .088 25 wit false(reach) 4.8 2.8 230 false(reach) 11 6.4 330
loop-acceleration/simple_false-unreach-call1.i timeout 900     900     30 wit - -
loop-acceleration/simple_false-unreach-call2.i false(reach) .15  .15  23 wit false(reach) 4.4 2.6 230 false(reach) 12 8.3 340
loop-acceleration/simple_false-unreach-call3.i false(reach) .086 .089 25 wit false(reach) 4.6 2.8 230 false(reach) 11 7.6 340
loop-acceleration/simple_false-unreach-call4.i timeout 900     900     26 wit - -
loop-acceleration/underapprox_false-unreach-call1.i false(reach) .11  .12  23 wit false(reach) 5.5 3.2 240 false(reach) 16 9.0 370
loop-acceleration/underapprox_false-unreach-call2.i false(reach) .089 .094 23 wit false(reach) 5.3 3.1 240 false(reach) 16 9.5 380
loop-acceleration/array_true-unreach-call1.i timeout 900     900     100 wit - -
loop-acceleration/array_true-unreach-call2.i timeout 900     900     29 wit - -
loop-acceleration/array_true-unreach-call3.i timeout 900     900     1600 wit - -
loop-acceleration/array_true-unreach-call4.i timeout 900     900     110 wit - -
loop-acceleration/const_true-unreach-call1.i true 850     850     28 wit - -
loop-acceleration/diamond_true-unreach-call1.i true 8.2   8.2   26 wit - -
loop-acceleration/diamond_true-unreach-call2.i true .55  .55  23 wit - -
loop-acceleration/functions_true-unreach-call1.i timeout 900     900     30 wit - -
loop-acceleration/multivar_true-unreach-call1.i true .076 .079 23 wit - -
loop-acceleration/nested_true-unreach-call1.i timeout 900     900     35 wit - -
loop-acceleration/overflow_true-unreach-call1.i timeout 900     900     27 wit - -
loop-acceleration/phases_true-unreach-call1.i timeout 900     900     27 wit - -
loop-acceleration/phases_true-unreach-call2.i timeout 900     900     150 wit - -
loop-acceleration/simple_true-unreach-call1.i timeout 900     900     27 wit - -
loop-acceleration/simple_true-unreach-call2.i true .13  .14  22 wit - -
loop-acceleration/simple_true-unreach-call3.i true .10  .10  23 wit - -
loop-acceleration/simple_true-unreach-call4.i timeout 900     900     29 wit - -
loop-acceleration/underapprox_true-unreach-call1.i true .15  .15  23 wit - -
loop-acceleration/underapprox_true-unreach-call2.i true .10  .11  23 wit - -
loop-invgen/id_trans_false-unreach-call.i false(reach) .20  .20  27 wit false(reach) 4.9 2.9 240 true 12 6.6 340
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call.i timeout 900     900     270 wit - -
loop-invgen/NetBSD_loop_true-unreach-call.i timeout 900     900     45 wit - -
loop-invgen/SpamAssassin-loop_true-unreach-call.i timeout 900     900     160 wit - -
loop-invgen/apache-escape-absolute_true-unreach-call.i true .74  .74  23 wit - -
loop-invgen/apache-get-tag_true-unreach-call.i true .43  .44  23 wit - -
loop-invgen/down_true-unreach-call.i timeout 900     900     280 wit - -
loop-invgen/fragtest_simple_true-unreach-call.i timeout 900     900     100 wit - -
loop-invgen/half_2_true-unreach-call.i timeout 900     900     320 wit - -
loop-invgen/heapsort_true-unreach-call.i timeout 900     900     7000 wit - -
loop-invgen/id_build_true-unreach-call.i true .44  .44  23 wit - -
loop-invgen/large_const_true-unreach-call.i true .31  .32  25 wit - -
loop-invgen/nest-if3_true-unreach-call.i timeout 900     900     6800 wit - -
loop-invgen/nested6_true-unreach-call.i timeout 900     900     10000 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     510 wit - -
loop-invgen/seq_true-unreach-call.i timeout 900     900     240 wit - -
loop-invgen/string_concat-noarr_true-unreach-call.i timeout 900     900     190 wit - -
loop-invgen/up_true-unreach-call.i timeout 900     900     330 wit - -
loop-lit/afnp2014_true-unreach-call.c.i timeout 900     900     60 wit - -
loop-lit/bhmr2007_true-unreach-call.c.i timeout 900     900     45 wit - -
loop-lit/cggmp2005_true-unreach-call.c.i true .083 .086 23 wit - -
loop-lit/cggmp2005_variant_true-unreach-call.c.i timeout 900     900     70 wit - -
loop-lit/cggmp2005b_true-unreach-call.c.i true 52     52     24 wit - -
loop-lit/css2003_true-unreach-call.c.i timeout 900     900     39 wit - -
loop-lit/ddlm2013_true-unreach-call.c.i true .23  .23  25 wit - -
loop-lit/gj2007_true-unreach-call.c.i true 9.0   9.0   23 wit - -
loop-lit/gj2007b_true-unreach-call.c.i timeout 900     900     210 wit - -
loop-lit/gr2006_true-unreach-call.c.i true 9.8   9.8   23 wit - -
loop-lit/gsv2008_true-unreach-call.c.i timeout 900     900     110 wit - -
loop-lit/hhk2008_true-unreach-call.c.i timeout 900     900     70 wit - -
loop-lit/jm2006_true-unreach-call.c.i timeout 900     900     66 wit - -
loop-lit/jm2006_variant_true-unreach-call.c.i timeout 900     900     64 wit - -
loop-lit/mcmillan2006_true-unreach-call.c.i timeout 900     900     410 wit - -
loop-new/count_by_1_true-unreach-call.i timeout 900     900     28 wit - -
loop-new/count_by_1_variant_true-unreach-call.i timeout 900     900     28 wit - -
loop-new/count_by_2_true-unreach-call.i timeout 900     900     28 wit - -
loop-new/count_by_k_true-unreach-call.i timeout 900     900     130 wit - -
loop-new/count_by_nondet_true-unreach-call.i timeout 900     900     190 wit - -
loop-new/gauss_sum_true-unreach-call.i timeout 900     900     66 wit - -
loop-new/half_true-unreach-call.i timeout 900     900     34 wit - -
loop-new/nested_true-unreach-call.i timeout 900     900     130 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 57000 57000 52000 141 660   480   17000   141 920   610   28000  
    correct results 74 2500 2500 1900 31 540   390   14000   31 740   480   19000  
        correct true 40 1400 1400 990 1 0   0   0   1 0   0   0  
        correct false 34 1100 1100 900 30 540   390   14000   30 740   480   19000  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (141 tasks, max score: 234) 114
Run set sv-comp16.Loops