Tool CPAchecker 1.4-svcomp16c
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 06:25:51 CET [[ 2016-01-15 08:31:02 CET ]] [[ 2016-01-15 21:59:57 CET ]]
Run set sv-comp16.Loops
Options -sv-comp16-bam -disable-java-assertions -heap 10000m -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-bam.2016-01-04_0625.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-bam.2016-01-04_0625.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.3 2.0 240 wit false(reach) 4.5 2.6 240 false(reach) 12 7.1 350
loops/bubble_sort_false-unreach-call.i false(reach) 6.8 2.4 370 wit false(reach) 13   7.2 500 error 10 6.3 320
loops/count_up_down_false-unreach-call_true-termination.i false(reach) 3.8 1.9 230 wit false(reach) 5.0 2.9 240 false(reach) 12 7.5 330
loops/eureka_01_false-unreach-call.i timeout 900   860   920 wit - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(reach) 3.8 1.7 240 wit false(reach) 5.2 3.0 230 false(reach) 12 7.2 340
loops/insertion_sort_false-unreach-call.i timeout 900   890   850 wit - -
loops/invert_string_false-unreach-call.i timeout 900   890   1200 wit - -
loops/linear_search_false-unreach-call.i witness unconfirmed 6.4 2.7 330 wit true 23   12   610 timeout 91 81   480
loops/ludcmp_false-unreach-call.i witness timeout 490   480   1200 wit timeout 91   87   860 timeout 80 51   7000
loops/matrix_false-unreach-call_true-termination.i false(reach) 18   14   870 wit false(reach) 22   18   880 false(reach) 16 10   350
loops/n.c24_false-unreach-call.i out of memory 740   690   15000 wit - -
loops/nec11_false-unreach-call.i false(reach) 3.3 1.6 230 wit false(reach) 4.3 2.4 230 false(reach) 12 7.1 340
loops/nec20_false-unreach-call.i witness timeout 3.8 1.7 230 wit timeout 90   72   3000 true 23 14   470
loops/s3_false-unreach-call.i false(reach) 21   7.7 820 wit false(reach) 14   7.7 490 true 26 17   470
loops/string_false-unreach-call.i timeout 900   860   1100 wit - -
loops/sum01_bug02_false-unreach-call_true-termination.i false(reach) 7.2 2.8 350 wit false(reach) 6.0 3.4 260 false(reach) 16 9.0 350
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(reach) 5.3 2.3 250 wit false(reach) 5.0 2.9 240 false(reach) 14 8.1 330
loops/sum01_false-unreach-call_true-termination.i false(reach) 7.6 2.9 420 wit false(reach) 6.1 3.4 270 false(reach) 18 10   360
loops/sum03_false-unreach-call_true-termination.i false(reach) 7.5 2.6 390 wit true 5.2 3.0 230 false(reach) 32 17   550
loops/sum04_false-unreach-call_true-termination.i false(reach) 4.7 2.1 240 wit false(reach) 5.5 3.4 240 false(reach) 16 8.9 360
loops/sum_array_false-unreach-call.i false(reach) 6.4 3.3 290 wit false(reach) 7.5 4.2 390 false(reach) 14 7.5 340
loops/terminator_01_false-unreach-call_false-termination.i false(reach) 4.0 1.9 230 wit false(reach) 4.8 2.8 230 false(reach) 14 7.7 330
loops/terminator_02_false-unreach-call_true-termination.i false(reach) 3.4 1.6 230 wit false(reach) 4.9 2.8 240 false(reach) 11 9.1 310
loops/terminator_03_false-unreach-call_true-termination.i false(reach) 3.5 1.6 230 wit true 4.6 2.7 220 false(reach) 13 7.9 340
loops/trex01_false-unreach-call_true-termination.i false(reach) 4.2 1.9 230 wit false(reach) 5.0 2.9 230 false(reach) 12 7.2 330
loops/trex02_false-unreach-call_true-termination.i false(reach) 3.9 1.8 230 wit false(reach) 4.7 2.8 230 false(reach) 11 6.6 330
loops/trex03_false-unreach-call_true-termination.i false(reach) 3.8 1.7 230 wit true 7.4 4.3 280 false(reach) 13 8.1 330
loops/verisec_NetBSD-libc__loop_false-unreach-call.i false(reach) 3.3 1.6 240 wit false(reach) 5.2 3.0 240 true 12 7.0 340
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.i false(reach) 5.3 2.1 330 wit false(reach) 7.0 4.1 340 false(reach) 31 17   520
loops/vogal_false-unreach-call.i timeout 900   870   1000 wit - -
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(reach) 3.8 1.8 220 wit false(reach) 4.7 3.0 230 false(reach) 11 9.7 330
loops/array_true-unreach-call.i true 3.9 1.9 230 wit - -
loops/bubble_sort_true-unreach-call.i true 3.4 1.6 230 wit - -
loops/count_up_down_true-unreach-call_true-termination.i timeout 900   850   1500 wit - -
loops/eureka_01_true-unreach-call.i true 19   5.5 710 wit - -
loops/eureka_05_true-unreach-call.i true 6.3 2.4 270 wit - -
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true 3.7 1.7 210 wit - -
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true 3.1 1.5 220 wit - -
loops/insertion_sort_true-unreach-call.i timeout 900   890   850 wit - -
loops/invert_string_true-unreach-call.i true 10   6.2 300 wit - -
loops/linear_sea.ch_true-unreach-call.i false(reach) 4.6 2.1 230 wit - -
loops/lu.cmp_true-unreach-call.i true 10   4.8 620 wit - -
loops/matrix_true-unreach-call_true-termination.i true 12   9.2 420 wit - -
loops/n.c11_true-unreach-call.i true 3.3 1.6 220 wit - -
loops/n.c40_true-unreach-call.i true 4.2 2.1 240 wit - -
loops/nec40_true-unreach-call.i true 4.4 2.2 230 wit - -
loops/string_true-unreach-call.i true 3.3 1.5 220 wit - -
loops/sum01_true-unreach-call_true-termination.i timeout 900   860   1100 wit - -
loops/sum03_true-unreach-call_false-termination.i timeout 900   860   1000 wit - -
loops/sum04_true-unreach-call_true-termination.i true 3.9 1.9 220 wit - -
loops/sum_array_true-unreach-call.i timeout 900   890   1000 wit - -
loops/terminator_02_true-unreach-call_true-termination.i true 3.8 1.7 220 wit - -
loops/terminator_03_true-unreach-call_true-termination.i true 3.1 1.4 210 wit - -
loops/trex01_true-unreach-call.i timeout 900   860   1100 wit - -
loops/trex02_true-unreach-call_true-termination.i true 3.7 1.7 220 wit - -
loops/trex03_true-unreach-call.i true 3.7 1.7 220 wit - -
loops/trex04_true-unreach-call_false-termination.i true 3.9 1.8 220 wit - -
loops/veris.c_NetBSD-libc__loop_true-unreach-call.i true 3.4 1.6 240 wit - -
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.i true 3.4 1.6 220 wit - -
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i true 3.0 1.4 210 wit - -
loops/vogal_true-unreach-call.i timeout 900   870   1000 wit - -
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true 3.0 1.4 220 wit - -
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 3.8 1.7 220 wit - -
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true 3.0 1.4 220 wit - -
loop-acceleration/array_false-unreach-call1.i timeout 900   890   4400 wit - -
loop-acceleration/array_false-unreach-call2.i timeout 900   880   14000 wit - -
loop-acceleration/array_false-unreach-call3.i false(reach) 34   12   880 wit false(reach) 35   21   920 timeout 91 59   4000
loop-acceleration/const_false-unreach-call1.i false(reach) 60   20   1200 wit false(reach) 66   37   1800 timeout 92 57   5400
loop-acceleration/diamond_false-unreach-call1.i false(reach) 9.2 3.0 400 wit false(reach) 8.7 4.8 400 timeout 90 62   3500
loop-acceleration/functions_false-unreach-call1.i timeout 900   850   1600 wit - -
loop-acceleration/multivar_false-unreach-call1.i false(reach) 3.8 1.7 230 wit false(reach) 4.6 2.7 230 false(reach) 11 7.3 320
loop-acceleration/nested_false-unreach-call1.i timeout 900   880   860 wit - -
loop-acceleration/phases_false-unreach-call1.i timeout 900   880   820 wit - -
loop-acceleration/phases_false-unreach-call2.i false(reach) 3.3 1.5 230 wit false(reach) 4.7 2.7 240 false(reach) 13 8.1 340
loop-acceleration/simple_false-unreach-call1.i timeout 900   880   800 wit - -
loop-acceleration/simple_false-unreach-call2.i false(reach) 3.2 1.5 230 wit false(reach) 4.5 2.7 230 false(reach) 12 7.2 330
loop-acceleration/simple_false-unreach-call3.i false(reach) 3.3 1.6 220 wit false(reach) 4.1 2.4 220 false(reach) 12 6.7 340
loop-acceleration/simple_false-unreach-call4.i timeout 900   880   810 wit - -
loop-acceleration/underapprox_false-unreach-call1.i false(reach) 4.7 2.0 230 wit false(reach) 5.4 3.1 230 false(reach) 17 9.4 370
loop-acceleration/underapprox_false-unreach-call2.i false(reach) 4.6 2.0 240 wit false(reach) 5.3 3.0 240 false(reach) 19 11   370
loop-acceleration/array_true-unreach-call1.i true 28   11   830 wit - -
loop-acceleration/array_true-unreach-call2.i timeout 900   880   13000 wit - -
loop-acceleration/array_true-unreach-call3.i true 26   9.6 800 wit - -
loop-acceleration/array_true-unreach-call4.i true 37   12   1600 wit - -
loop-acceleration/const_true-unreach-call1.i true 17   5.9 570 wit - -
loop-acceleration/diamond_true-unreach-call1.i true 20   12   680 wit - -
loop-acceleration/diamond_true-unreach-call2.i true 17   5.5 470 wit - -
loop-acceleration/functions_true-unreach-call1.i timeout 900   850   1300 wit - -
loop-acceleration/multivar_true-unreach-call1.i true 3.8 1.8 220 wit - -
loop-acceleration/nested_true-unreach-call1.i timeout 900   870   900 wit - -
loop-acceleration/overflow_true-unreach-call1.i timeout 900   880   810 wit - -
loop-acceleration/phases_true-unreach-call1.i timeout 900   870   830 wit - -
loop-acceleration/phases_true-unreach-call2.i true 3.3 1.6 220 wit - -
loop-acceleration/simple_true-unreach-call1.i timeout 900   880   790 wit - -
loop-acceleration/simple_true-unreach-call2.i true 3.1 1.5 220 wit - -
loop-acceleration/simple_true-unreach-call3.i timeout 900   860   970 wit - -
loop-acceleration/simple_true-unreach-call4.i true 3.0 1.4 220 wit - -
loop-acceleration/underapprox_true-unreach-call1.i true 5.1 2.1 240 wit - -
loop-acceleration/underapprox_true-unreach-call2.i true 4.0 1.8 220 wit - -
loop-invgen/id_trans_false-unreach-call.i false(reach) 4.2 1.9 230 wit false(reach) 4.4 2.6 240 false(reach) 12 6.7 330
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call.i timeout 900   890   810 wit - -
loop-invgen/NetBSD_loop_true-unreach-call.i timeout 900   870   1000 wit - -
loop-invgen/SpamAssassin-loop_true-unreach-call.i timeout 900   760   5600 wit - -
loop-invgen/apache-escape-absolute_true-unreach-call.i timeout 900   880   1200 wit - -
loop-invgen/apache-get-tag_true-unreach-call.i timeout 900   860   1100 wit - -
loop-invgen/down_true-unreach-call.i timeout 900   860   950 wit - -
loop-invgen/fragtest_simple_true-unreach-call.i timeout 900   850   3800 wit - -
loop-invgen/half_2_true-unreach-call.i timeout 900   870   880 wit - -
loop-invgen/heapsort_true-unreach-call.i true 510   500   820 wit - -
loop-invgen/id_build_true-unreach-call.i timeout 900   860   860 wit - -
loop-invgen/large_const_true-unreach-call.i true 4.5 2.0 250 wit - -
loop-invgen/nest-if3_true-unreach-call.i timeout 900   890   520 wit - -
loop-invgen/nested6_true-unreach-call.i timeout 900   880   890 wit - -
loop-invgen/nested9_true-unreach-call.i timeout 900   880   840 wit - -
loop-invgen/sendmail-close-angle_true-unreach-call.i timeout 900   840   1900 wit - -
loop-invgen/seq_true-unreach-call.i timeout 900   850   2600 wit - -
loop-invgen/string_concat-noarr_true-unreach-call.i timeout 900   860   1000 wit - -
loop-invgen/up_true-unreach-call.i timeout 900   840   2900 wit - -
loop-lit/afnp2014_true-unreach-call.c.i true 24   7.3 800 wit - -
loop-lit/bhmr2007_true-unreach-call.c.i timeout 900   890   800 wit - -
loop-lit/cggmp2005_true-unreach-call.c.i true 3.3 1.5 220 wit - -
loop-lit/cggmp2005_variant_true-unreach-call.c.i timeout 900   890   820 wit - -
loop-lit/cggmp2005b_true-unreach-call.c.i true 7.6 2.8 370 wit - -
loop-lit/css2003_true-unreach-call.c.i timeout 900   870   1200 wit - -
loop-lit/ddlm2013_true-unreach-call.c.i timeout 900   870   1000 wit - -
loop-lit/gj2007_true-unreach-call.c.i true 4.9 2.1 250 wit - -
loop-lit/gj2007b_true-unreach-call.c.i timeout 900   870   1000 wit - -
loop-lit/gr2006_true-unreach-call.c.i timeout 900   860   1000 wit - -
loop-lit/gsv2008_true-unreach-call.c.i timeout 900   890   820 wit - -
loop-lit/hhk2008_true-unreach-call.c.i timeout 900   870   830 wit - -
loop-lit/jm2006_true-unreach-call.c.i true 3.3 1.6 220 wit - -
loop-lit/jm2006_variant_true-unreach-call.c.i timeout 900   860   1500 wit - -
loop-lit/mcmillan2006_true-unreach-call.c.i false(reach) 5.9 2.4 350 wit - -
loop-new/count_by_1_true-unreach-call.i timeout 900   880   790 wit - -
loop-new/count_by_1_variant_true-unreach-call.i timeout 900   870   910 wit - -
loop-new/count_by_2_true-unreach-call.i timeout 900   880   780 wit - -
loop-new/count_by_k_true-unreach-call.i timeout 900   860   770 wit - -
loop-new/count_by_nondet_true-unreach-call.i timeout 900   860   1100 wit - -
loop-new/gauss_sum_true-unreach-call.i timeout 900   860   1000 wit - -
loop-new/half_true-unreach-call.i timeout 900   850   1600 wit - -
loop-new/nested_true-unreach-call.i timeout 900   880   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 56000 53000   140000 141 500   350   16000   141 900   580   31000  
    correct results 76 1100 760   27000 32 300   170   11000   28 710   440   23000  
        correct true 44 860 650   16000 3 0   0   0   2 0   0   0  
        correct false 32 270 110   11000 29 300   170   11000   26 710   440   23000  
    incorrect results 2 11 4.5 580 0 0   0   0   0 0   0   0  
        incorrect true 0
        incorrect false 2 11 4.5 580 0 0   0   0   0 0   0   0  
score (141 tasks, max score: 234) 88
Run set sv-comp16.Loops