Tool CPAchecker 1.4-svn 18373
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-04 20:04:07 CET [[ 2016-01-15 08:41:31 CET ]] [[ 2016-01-15 22:05:37 CET ]]
Run set sv-comp16.Loops
Options -sv-comp16--refsel -disable-java-assertions -heap 12500m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-refsel.2016-01-04_2004.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-refsel.2016-01-04_2004.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) 4.7 2.2 250 wit false(reach) 4.5 2.6 240 false(reach) 11 7.8 330
loops/bubble_sort_false-unreach-call.i false(reach) 8.9 3.3 430 wit false(reach) 12   6.3 440 error 12 6.9 320
loops/count_up_down_false-unreach-call_true-termination.i false(reach) 3.9 1.8 230 wit false(reach) 5.2 2.9 240 false(reach) 12 6.8 320
loops/eureka_01_false-unreach-call.i timeout 900   890   800 wit - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(reach) 4.7 2.1 240 wit false(reach) 4.9 2.8 240 false(reach) 13 7.4 330
loops/insertion_sort_false-unreach-call.i error 4.3 2.0 230 wit - -
loops/invert_string_false-unreach-call.i error 14   7.5 470 wit - -
loops/linear_search_false-unreach-call.i false(reach) 6.1 2.6 260 wit false(reach) 5.7 3.3 330 error 48 38   480
loops/ludcmp_false-unreach-call.i witness timeout 41   37   1400 wit timeout 91   87   780 timeout 82 51   7000
loops/matrix_false-unreach-call_true-termination.i false(reach) 11   4.7 430 wit false(reach) 16   13   890 false(reach) 14 7.7 360
loops/n.c24_false-unreach-call.i timeout 900   830   4800 wit - -
loops/nec11_false-unreach-call.i false(reach) 3.9 1.8 240 wit false(reach) 4.4 2.5 240 false(reach) 12 7.0 340
loops/nec20_false-unreach-call.i false(reach) 3.6 1.6 230 wit false(reach) 5.0 2.9 250 false(reach) 12 6.7 340
loops/s3_false-unreach-call.i timeout 900   850   1400 wit - -
loops/string_false-unreach-call.i false(reach) 5.0 2.1 280 wit false(reach) 7.0 4.0 360 false(reach) 29 17   370
loops/sum01_bug02_false-unreach-call_true-termination.i false(reach) 6.5 2.9 270 wit false(reach) 5.9 3.4 260 false(reach) 15 9.1 350
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(reach) 4.3 2.0 250 wit false(reach) 5.3 3.1 240 false(reach) 15 9.0 350
loops/sum01_false-unreach-call_true-termination.i false(reach) 7.8 3.4 340 wit false(reach) 5.3 3.1 240 false(reach) 18 10   340
loops/sum03_false-unreach-call_true-termination.i false(reach) 5.5 2.1 280 wit false(reach) 7.2 4.2 340 false(reach) 34 19   570
loops/sum04_false-unreach-call_true-termination.i false(reach) 4.0 1.7 230 wit false(reach) 4.4 2.6 240 false(reach) 15 12   350
loops/sum_array_false-unreach-call.i false(reach) 4.7 2.3 260 wit false(reach) 7.0 4.3 380 false(reach) 15 8.0 330
loops/terminator_01_false-unreach-call_false-termination.i false(reach) 3.9 1.9 230 wit false(reach) 4.6 2.7 230 false(reach) 11 7.1 330
loops/terminator_02_false-unreach-call_true-termination.i false(reach) 3.3 1.5 230 wit false(reach) 4.8 2.8 230 false(reach) 13 8.1 340
loops/terminator_03_false-unreach-call_true-termination.i false(reach) 4.3 1.9 240 wit false(reach) 4.8 2.7 240 false(reach) 13 7.5 350
loops/trex01_false-unreach-call_true-termination.i false(reach) 4.0 1.8 230 wit false(reach) 5.1 2.9 240 false(reach) 12 6.7 340
loops/trex02_false-unreach-call_true-termination.i false(reach) 4.0 1.8 230 wit false(reach) 4.6 2.6 230 false(reach) 11 5.8 330
loops/trex03_false-unreach-call_true-termination.i false(reach) 4.5 2.0 240 wit false(reach) 5.0 2.9 240 false(reach) 12 7.1 330
loops/verisec_NetBSD-libc__loop_false-unreach-call.i false(reach) 4.2 1.9 240 wit false(reach) 4.7 2.8 230 false(reach) 15 8.5 340
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.i false(reach) 4.5 1.9 250 wit false(reach) 6.9 3.9 330 false(reach) 27 15   490
loops/vogal_false-unreach-call.i false(reach) 9.9 3.5 450 wit false(reach) 8.9 5.0 370 timeout 91 66   1400
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(reach) 3.9 1.8 230 wit false(reach) 4.3 2.6 220 false(reach) 12 7.4 330
loops/array_true-unreach-call.i true 3.3 1.6 220 wit - -
loops/bubble_sort_true-unreach-call.i true 19   4.9 650 wit - -
loops/count_up_down_true-unreach-call_true-termination.i timeout 900   880   840 wit - -
loops/eureka_01_true-unreach-call.i true 5.7 2.3 280 wit - -
loops/eureka_05_true-unreach-call.i true 4.7 2.0 230 wit - -
loops/for_infinite_loop_1_true-unreach-call_false-termination.i timeout 900   860   4600 wit - -
loops/for_infinite_loop_2_true-unreach-call_false-termination.i timeout 900   850   4600 wit - -
loops/insertion_sort_true-unreach-call.i error 4.3 2.0 240 wit - -
loops/invert_string_true-unreach-call.i error 4.8 2.3 240 wit - -
loops/linear_sea.ch_true-unreach-call.i false(reach) 11   3.9 470 wit - -
loops/lu.cmp_true-unreach-call.i true 5.2 2.1 250 wit - -
loops/matrix_true-unreach-call_true-termination.i timeout 900   880   1700 wit - -
loops/n.c11_true-unreach-call.i true 3.7 1.7 210 wit - -
loops/n.c40_true-unreach-call.i true 4.3 2.1 220 wit - -
loops/nec40_true-unreach-call.i true 3.6 1.7 220 wit - -
loops/string_true-unreach-call.i true 4.6 1.9 250 wit - -
loops/sum01_true-unreach-call_true-termination.i timeout 900   860   1200 wit - -
loops/sum03_true-unreach-call_false-termination.i timeout 900   860   4600 wit - -
loops/sum04_true-unreach-call_true-termination.i true 3.7 1.7 210 wit - -
loops/sum_array_true-unreach-call.i timeout 900   850   900 wit - -
loops/terminator_02_true-unreach-call_true-termination.i true 3.9 1.9 210 wit - -
loops/terminator_03_true-unreach-call_true-termination.i true 4.0 1.8 220 wit - -
loops/trex01_true-unreach-call.i true 24   11   730 wit - -
loops/trex02_true-unreach-call_true-termination.i true 3.6 1.7 210 wit - -
loops/trex03_true-unreach-call.i true 4.2 1.9 220 wit - -
loops/trex04_true-unreach-call_false-termination.i true 4.4 1.9 220 wit - -
loops/veris.c_NetBSD-libc__loop_true-unreach-call.i true 4.5 2.3 220 wit - -
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.i true 9.6 3.6 360 wit - -
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i true 3.4 1.5 220 wit - -
loops/vogal_true-unreach-call.i timeout 900   870   10000 wit - -
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true 3.4 1.6 210 wit - -
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 3.5 1.6 210 wit - -
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true 3.5 1.6 210 wit - -
loop-acceleration/array_false-unreach-call1.i timeout 900   860   5700 wit - -
loop-acceleration/array_false-unreach-call2.i timeout 900   880   4300 wit - -
loop-acceleration/array_false-unreach-call3.i timeout 900   870   810 wit - -
loop-acceleration/const_false-unreach-call1.i false(reach) 200   160   5000 wit false(reach) 74   41   1700 timeout 91 59   4500
loop-acceleration/diamond_false-unreach-call1.i false(reach) 140   110   790 wit false(reach) 10   5.7 410 timeout 90 61   3200
loop-acceleration/functions_false-unreach-call1.i timeout 900   860   4600 wit - -
loop-acceleration/multivar_false-unreach-call1.i false(reach) 3.9 1.8 230 wit false(reach) 4.7 2.7 230 false(reach) 13 6.9 330
loop-acceleration/nested_false-unreach-call1.i timeout 900   850   4600 wit - -
loop-acceleration/phases_false-unreach-call1.i timeout 900   850   4600 wit - -
loop-acceleration/phases_false-unreach-call2.i false(reach) 4.0 1.9 240 wit false(reach) 5.1 2.9 240 false(reach) 11 7.6 350
loop-acceleration/simple_false-unreach-call1.i timeout 900   860   4400 wit - -
loop-acceleration/simple_false-unreach-call2.i false(reach) 3.8 1.7 230 wit false(reach) 4.5 2.6 230 false(reach) 11 6.3 340
loop-acceleration/simple_false-unreach-call3.i false(reach) 3.9 1.8 230 wit false(reach) 3.9 2.3 220 false(reach) 11 8.5 320
loop-acceleration/simple_false-unreach-call4.i timeout 900   850   4500 wit - -
loop-acceleration/underapprox_false-unreach-call1.i false(reach) 4.4 1.9 240 wit false(reach) 4.9 2.9 240 false(reach) 17 9.2 380
loop-acceleration/underapprox_false-unreach-call2.i false(reach) 4.2 1.9 240 wit false(reach) 4.7 2.8 230 false(reach) 17 9.5 370
loop-acceleration/array_true-unreach-call1.i true 39   34   500 wit - -
loop-acceleration/array_true-unreach-call2.i timeout 900   880   4300 wit - -
loop-acceleration/array_true-unreach-call3.i timeout 900   860   890 wit - -
loop-acceleration/array_true-unreach-call4.i timeout 900   880   890 wit - -
loop-acceleration/const_true-unreach-call1.i true 7.6 2.9 490 wit - -
loop-acceleration/diamond_true-unreach-call1.i true 390   370   800 wit - -
loop-acceleration/diamond_true-unreach-call2.i true 7.9 4.1 280 wit - -
loop-acceleration/functions_true-unreach-call1.i timeout 900   860   4600 wit - -
loop-acceleration/multivar_true-unreach-call1.i true 3.6 1.7 210 wit - -
loop-acceleration/nested_true-unreach-call1.i timeout 900   860   4500 wit - -
loop-acceleration/overflow_true-unreach-call1.i timeout 900   860   4500 wit - -
loop-acceleration/phases_true-unreach-call1.i timeout 900   860   4600 wit - -
loop-acceleration/phases_true-unreach-call2.i true 3.8 1.9 220 wit - -
loop-acceleration/simple_true-unreach-call1.i timeout 900   850   4600 wit - -
loop-acceleration/simple_true-unreach-call2.i true 2.9 1.4 210 wit - -
loop-acceleration/simple_true-unreach-call3.i timeout 900   870   860 wit - -
loop-acceleration/simple_true-unreach-call4.i timeout 900   850   4600 wit - -
loop-acceleration/underapprox_true-unreach-call1.i true 3.4 1.6 200 wit - -
loop-acceleration/underapprox_true-unreach-call2.i true 3.6 1.7 210 wit - -
loop-invgen/id_trans_false-unreach-call.i false(reach) 4.0 1.7 240 wit false(reach) 4.8 2.7 250 false(reach) 12 6.9 340
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call.i timeout 900   890   820 wit - -
loop-invgen/NetBSD_loop_true-unreach-call.i timeout 900   890   770 wit - -
loop-invgen/SpamAssassin-loop_true-unreach-call.i timeout 900   860   840 wit - -
loop-invgen/apache-escape-absolute_true-unreach-call.i timeout 900   880   820 wit - -
loop-invgen/apache-get-tag_true-unreach-call.i timeout 900   880   930 wit - -
loop-invgen/down_true-unreach-call.i timeout 900   870   820 wit - -
loop-invgen/fragtest_simple_true-unreach-call.i timeout 900   860   4600 wit - -
loop-invgen/half_2_true-unreach-call.i timeout 900   870   860 wit - -
loop-invgen/heapsort_true-unreach-call.i timeout 900   880   830 wit - -
loop-invgen/id_build_true-unreach-call.i timeout 900   870   820 wit - -
loop-invgen/large_const_true-unreach-call.i true 12   4.6 440 wit - -
loop-invgen/nest-if3_true-unreach-call.i timeout 900   880   850 wit - -
loop-invgen/nested6_true-unreach-call.i timeout 900   880   860 wit - -
loop-invgen/nested9_true-unreach-call.i timeout 900   880   940 wit - -
loop-invgen/sendmail-close-angle_true-unreach-call.i timeout 900   870   820 wit - -
loop-invgen/seq_true-unreach-call.i timeout 900   850   1800 wit - -
loop-invgen/string_concat-noarr_true-unreach-call.i timeout 900   860   1400 wit - -
loop-invgen/up_true-unreach-call.i timeout 900   850   1600 wit - -
loop-lit/afnp2014_true-unreach-call.c.i timeout 900   870   850 wit - -
loop-lit/bhmr2007_true-unreach-call.c.i timeout 900   840   4000 wit - -
loop-lit/cggmp2005_true-unreach-call.c.i true 3.1 1.4 210 wit - -
loop-lit/cggmp2005_variant_true-unreach-call.c.i timeout 900   890   790 wit - -
loop-lit/cggmp2005b_true-unreach-call.c.i true 5.7 2.2 260 wit - -
loop-lit/css2003_true-unreach-call.c.i timeout 900   880   1100 wit - -
loop-lit/ddlm2013_true-unreach-call.c.i timeout 900   860   810 wit - -
loop-lit/gj2007_true-unreach-call.c.i true 5.2 2.0 240 wit - -
loop-lit/gj2007b_true-unreach-call.c.i timeout 900   850   1300 wit - -
loop-lit/gr2006_true-unreach-call.c.i true 5.5 2.1 250 wit - -
loop-lit/gsv2008_true-unreach-call.c.i timeout 900   890   800 wit - -
loop-lit/hhk2008_true-unreach-call.c.i timeout 900   880   820 wit - -
loop-lit/jm2006_true-unreach-call.c.i true 3.8 1.7 230 wit - -
loop-lit/jm2006_variant_true-unreach-call.c.i timeout 900   870   880 wit - -
loop-lit/mcmillan2006_true-unreach-call.c.i false(reach) 6.6 3.0 290 wit - -
loop-new/count_by_1_true-unreach-call.i timeout 900   850   4600 wit - -
loop-new/count_by_1_variant_true-unreach-call.i timeout 900   850   4700 wit - -
loop-new/count_by_2_true-unreach-call.i timeout 900   860   4500 wit - -
loop-new/count_by_k_true-unreach-call.i timeout 900   870   770 wit - -
loop-new/count_by_nondet_true-unreach-call.i timeout 900   880   870 wit - -
loop-new/gauss_sum_true-unreach-call.i timeout 900   870   840 wit - -
loop-new/half_true-unreach-call.i timeout 900   860   1300 wit - -
loop-new/nested_true-unreach-call.i timeout 900   860   850 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 58000 55000   180000 141 360   240   12000   141 840   540   27000  
    correct results 71 1100 830   25000 34 270   160   11000   29 760   490   20000  
        correct true 37 630 480   11000 0 0   0   0   0 0   0   0  
        correct false 34 490 340   14000 34 270   160   11000   29 760   490   20000  
    incorrect results 2 17 6.8 760 0 0   0   0   0 0   0   0  
        incorrect true 0
        incorrect false 2 17 6.8 760 0 0   0   0   0 0   0   0  
score (141 tasks, max score: 234) 76
Run set sv-comp16.Loops