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 13:17:38 CET [[ 2016-01-15 08:48:20 CET ]] [[ 2016-01-15 22:10:37 CET ]]
Run set sv-comp16.Loops
Options -sv-comp16 -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-seq.2016-01-04_1317.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-seq.2016-01-04_1317.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) 3.8 1.8 210 wit true 5.6 3.3 230 false(reach) 13 7.2 350
loops/bubble_sort_false-unreach-call.i false(reach) 110   81   3200 wit false(reach) 13   7.0 480 error 11 6.2 310
loops/count_up_down_false-unreach-call_true-termination.i false(reach) 3.1 1.4 210 wit false(reach) 4.7 2.7 230 false(reach) 12 11   340
loops/eureka_01_false-unreach-call.i timeout 900   720   4900 wit - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(reach) 6.6 2.7 410 wit false(reach) 5.0 2.9 230 false(reach) 12 7.1 330
loops/insertion_sort_false-unreach-call.i exception 57   19   1700 wit - -
loops/invert_string_false-unreach-call.i false(reach) 24   7.1 870 wit false(reach) 7.5 4.3 360 false(reach) 15 8.1 340
loops/linear_search_false-unreach-call.i unknown 10   3.5 430 wit - -
loops/ludcmp_false-unreach-call.i witness timeout 39   35   1300 wit timeout 91   87   830 timeout 60 40   7000
loops/matrix_false-unreach-call_true-termination.i false(reach) 150   100   2600 wit false(reach) 30   26   850 false(reach) 15 7.9 360
loops/n.c24_false-unreach-call.i timeout 900   690   4700 wit - -
loops/nec11_false-unreach-call.i false(reach) 3.7 1.7 210 wit false(reach) 4.6 2.7 230 false(reach) 11 6.3 330
loops/nec20_false-unreach-call.i false(reach) 3.2 1.5 210 wit false(reach) 5.3 3.2 240 false(reach) 12 10   330
loops/s3_false-unreach-call.i out of memory 210   130   15000 wit - -
loops/string_false-unreach-call.i false(reach) 5.2 2.2 240 wit false(reach) 7.9 4.6 350 false(reach) 29 17   390
loops/sum01_bug02_false-unreach-call_true-termination.i false(reach) 9.8 3.2 430 wit false(reach) 5.7 3.2 250 false(reach) 17 11   340
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(reach) 7.7 2.6 410 wit false(reach) 5.5 3.2 240 false(reach) 16 12   330
loops/sum01_false-unreach-call_true-termination.i false(reach) 10   3.3 430 wit false(reach) 7.0 4.0 340 false(reach) 17 9.1 370
loops/sum03_false-unreach-call_true-termination.i false(reach) 5.9 2.2 240 wit false(reach) 7.8 4.4 340 false(reach) 32 18   560
loops/sum04_false-unreach-call_true-termination.i false(reach) 4.0 1.8 210 wit false(reach) 5.9 3.4 250 false(reach) 15 9.1 340
loops/sum_array_false-unreach-call.i false(reach) 24   7.1 980 wit false(reach) 7.1 4.1 380 false(reach) 15 8.3 350
loops/terminator_01_false-unreach-call_false-termination.i false(reach) 3.7 1.7 210 wit false(reach) 4.6 2.7 230 false(reach) 12 8.4 320
loops/terminator_02_false-unreach-call_true-termination.i false(reach) 3.6 1.7 210 wit false(reach) 4.9 2.8 230 false(reach) 12 6.9 330
loops/terminator_03_false-unreach-call_true-termination.i false(reach) 7.5 2.8 390 wit false(reach) 4.8 2.8 230 false(reach) 13 8.1 350
loops/trex01_false-unreach-call_true-termination.i false(reach) 3.2 1.5 210 wit false(reach) 5.0 2.9 240 false(reach) 12 7.4 330
loops/trex02_false-unreach-call_true-termination.i false(reach) 3.8 1.8 210 wit false(reach) 4.6 2.7 230 false(reach) 13 7.2 350
loops/trex03_false-unreach-call_true-termination.i false(reach) 7.4 2.8 390 wit false(reach) 5.1 3.0 240 false(reach) 14 11   360
loops/verisec_NetBSD-libc__loop_false-unreach-call.i false(reach) 3.9 1.7 210 wit false(reach) 4.6 2.7 230 false(reach) 16 12   380
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.i false(reach) 4.5 2.0 220 wit false(reach) 6.9 3.9 330 false(reach) 26 14   500
loops/vogal_false-unreach-call.i false(reach) 8.2 2.9 310 wit false(reach) 9.4 5.3 410 timeout 91 70   1700
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(reach) 3.6 1.7 210 wit false(reach) 4.5 2.6 230 false(reach) 12 8.1 330
loops/array_true-unreach-call.i true 7.2 2.8 380 wit - -
loops/bubble_sort_true-unreach-call.i true 93   84   2300 wit - -
loops/count_up_down_true-unreach-call_true-termination.i timeout 900   710   6000 wit - -
loops/eureka_01_true-unreach-call.i true 5.3 2.0 240 wit - -
loops/eureka_05_true-unreach-call.i true 3.9 1.6 190 wit - -
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true 93   85   3600 wit - -
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true 93   84   3600 wit - -
loops/insertion_sort_true-unreach-call.i timeout 900   720   4000 wit - -
loops/invert_string_true-unreach-call.i true 61   13   1300 wit - -
loops/linear_sea.ch_true-unreach-call.i unknown 100   86   3500 wit - -
loops/lu.cmp_true-unreach-call.i true 4.5 1.8 210 wit - -
loops/matrix_true-unreach-call_true-termination.i true 28   7.3 870 wit - -
loops/n.c11_true-unreach-call.i true 2.8 1.3 190 wit - -
loops/n.c40_true-unreach-call.i true 5.9 2.2 370 wit - -
loops/nec40_true-unreach-call.i true 5.7 2.2 360 wit - -
loops/string_true-unreach-call.i true 4.4 1.7 220 wit - -
loops/sum01_true-unreach-call_true-termination.i timeout 900   700   5000 wit - -
loops/sum03_true-unreach-call_false-termination.i true 160   130   3600 wit - -
loops/sum04_true-unreach-call_true-termination.i true 3.2 1.5 180 wit - -
loops/sum_array_true-unreach-call.i false(reach) 310   140   4700 wit - -
loops/terminator_02_true-unreach-call_true-termination.i true 6.6 2.6 350 wit - -
loops/terminator_03_true-unreach-call_true-termination.i true 7.0 2.5 370 wit - -
loops/trex01_true-unreach-call.i true 160   140   2300 wit - -
loops/trex02_true-unreach-call_true-termination.i true 6.8 2.5 380 wit - -
loops/trex03_true-unreach-call.i true 7.8 2.7 380 wit - -
loops/trex04_true-unreach-call_false-termination.i true 6.3 2.3 370 wit - -
loops/veris.c_NetBSD-libc__loop_true-unreach-call.i true 6.6 2.6 370 wit - -
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.i true 93   81   3600 wit - -
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i true 5.9 2.2 370 wit - -
loops/vogal_true-unreach-call.i true 160   84   4000 wit - -
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true 3.2 1.5 180 wit - -
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 2.6 1.2 180 wit - -
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true 3.1 1.4 190 wit - -
loop-acceleration/array_false-unreach-call1.i timeout 900   710   5300 wit - -
loop-acceleration/array_false-unreach-call2.i timeout 900   680   6300 wit - -
loop-acceleration/array_false-unreach-call3.i false(reach) 44   28   790 wit false(reach) 40   24   930 timeout 91 58   3900
loop-acceleration/const_false-unreach-call1.i timeout 900   690   4800 wit - -
loop-acceleration/diamond_false-unreach-call1.i false(reach) 19   8.8 1200 wit false(reach) 9.5 5.2 380 timeout 91 67   3200
loop-acceleration/functions_false-unreach-call1.i timeout 900   710   5500 wit - -
loop-acceleration/multivar_false-unreach-call1.i false(reach) 3.0 1.4 210 wit false(reach) 5.1 2.9 240 false(reach) 12 6.7 360
loop-acceleration/nested_false-unreach-call1.i timeout 900   700   3600 wit - -
loop-acceleration/phases_false-unreach-call1.i timeout 900   720   4500 wit - -
loop-acceleration/phases_false-unreach-call2.i false(reach) 3.3 1.4 210 wit false(reach) 4.6 2.7 220 false(reach) 13 7.6 350
loop-acceleration/simple_false-unreach-call1.i timeout 900   700   5100 wit - -
loop-acceleration/simple_false-unreach-call2.i false(reach) 3.2 1.4 200 wit false(reach) 4.6 2.7 220 false(reach) 13 8.2 350
loop-acceleration/simple_false-unreach-call3.i false(reach) 3.7 1.7 210 wit false(reach) 4.5 2.7 220 false(reach) 13 7.2 350
loop-acceleration/simple_false-unreach-call4.i timeout 900   710   5900 wit - -
loop-acceleration/underapprox_false-unreach-call1.i false(reach) 3.2 1.5 210 wit false(reach) 5.5 3.2 240 false(reach) 16 9.0 370
loop-acceleration/underapprox_false-unreach-call2.i false(reach) 4.1 1.8 210 wit false(reach) 5.5 3.2 240 false(reach) 17 11   390
loop-acceleration/array_true-unreach-call1.i true 100   90   690 wit - -
loop-acceleration/array_true-unreach-call2.i timeout 900   680   6300 wit - -
loop-acceleration/array_true-unreach-call3.i true 18   6.6 1200 wit - -
loop-acceleration/array_true-unreach-call4.i true 12   5.8 700 wit - -
loop-acceleration/const_true-unreach-call1.i true 12   5.8 1200 wit - -
loop-acceleration/diamond_true-unreach-call1.i true 49   17   2900 wit - -
loop-acceleration/diamond_true-unreach-call2.i true 17   4.4 580 wit - -
loop-acceleration/functions_true-unreach-call1.i timeout 900   710   5500 wit - -
loop-acceleration/multivar_true-unreach-call1.i true 7.5 2.6 380 wit - -
loop-acceleration/nested_true-unreach-call1.i true 160   140   3500 wit - -
loop-acceleration/overflow_true-unreach-call1.i timeout 900   710   5700 wit - -
loop-acceleration/phases_true-unreach-call1.i timeout 900   720   4500 wit - -
loop-acceleration/phases_true-unreach-call2.i true 6.2 2.4 360 wit - -
loop-acceleration/simple_true-unreach-call1.i timeout 900   700   5600 wit - -
loop-acceleration/simple_true-unreach-call2.i true 5.6 2.2 340 wit - -
loop-acceleration/simple_true-unreach-call3.i timeout 900   710   4500 wit - -
loop-acceleration/simple_true-unreach-call4.i true 150   140   3600 wit - -
loop-acceleration/underapprox_true-unreach-call1.i true 2.7 1.2 180 wit - -
loop-acceleration/underapprox_true-unreach-call2.i true 2.7 1.3 180 wit - -
loop-invgen/id_trans_false-unreach-call.i false(reach) 7.3 2.9 390 wit false(reach) 5.1 3.0 230 false(reach) 12 8.4 320
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call.i timeout 900   730   4100 wit - -
loop-invgen/NetBSD_loop_true-unreach-call.i timeout 900   710   4800 wit - -
loop-invgen/SpamAssassin-loop_true-unreach-call.i true 380   170   4100 wit - -
loop-invgen/apache-escape-absolute_true-unreach-call.i true 340   150   4300 wit - -
loop-invgen/apache-get-tag_true-unreach-call.i true 19   4.4 540 wit - -
loop-invgen/down_true-unreach-call.i timeout 900   710   5300 wit - -
loop-invgen/fragtest_simple_true-unreach-call.i timeout 900   670   5300 wit - -
loop-invgen/half_2_true-unreach-call.i timeout 900   690   5000 wit - -
loop-invgen/heapsort_true-unreach-call.i timeout 900   700   3000 wit - -
loop-invgen/id_build_true-unreach-call.i true 8.5 3.0 380 wit - -
loop-invgen/large_const_true-unreach-call.i true 6.7 2.4 380 wit - -
loop-invgen/nest-if3_true-unreach-call.i timeout 900   710   3800 wit - -
loop-invgen/nested6_true-unreach-call.i timeout 900   680   3500 wit - -
loop-invgen/nested9_true-unreach-call.i timeout 900   720   4300 wit - -
loop-invgen/sendmail-close-angle_true-unreach-call.i timeout 900   710   4800 wit - -
loop-invgen/seq_true-unreach-call.i timeout 900   700   4900 wit - -
loop-invgen/string_concat-noarr_true-unreach-call.i timeout 900   700   4900 wit - -
loop-invgen/up_true-unreach-call.i timeout 900   700   5400 wit - -
loop-lit/afnp2014_true-unreach-call.c.i true 16   8.3 1200 wit - -
loop-lit/bhmr2007_true-unreach-call.c.i timeout 900   730   3900 wit - -
loop-lit/cggmp2005_true-unreach-call.c.i true 2.7 1.3 180 wit - -
loop-lit/cggmp2005_variant_true-unreach-call.c.i timeout 900   730   6400 wit - -
loop-lit/cggmp2005b_true-unreach-call.c.i true 4.1 1.6 260 wit - -
loop-lit/css2003_true-unreach-call.c.i true 6.0 2.2 360 wit - -
loop-lit/ddlm2013_true-unreach-call.c.i timeout 900   710   5200 wit - -
loop-lit/gj2007_true-unreach-call.c.i true 3.9 1.5 220 wit - -
loop-lit/gj2007b_true-unreach-call.c.i timeout 900   720   4600 wit - -
loop-lit/gr2006_true-unreach-call.c.i true 5.4 2.0 240 wit - -
loop-lit/gsv2008_true-unreach-call.c.i timeout 900   730   4100 wit - -
loop-lit/hhk2008_true-unreach-call.c.i timeout 900   720   3400 wit - -
loop-lit/jm2006_true-unreach-call.c.i true 310   140   5200 wit - -
loop-lit/jm2006_variant_true-unreach-call.c.i timeout 900   710   5700 wit - -
loop-lit/mcmillan2006_true-unreach-call.c.i timeout 900   880   2300 wit - -
loop-new/count_by_1_true-unreach-call.i true 150   140   3500 wit - -
loop-new/count_by_1_variant_true-unreach-call.i true 160   140   3600 wit - -
loop-new/count_by_2_true-unreach-call.i timeout 900   710   6000 wit - -
loop-new/count_by_k_true-unreach-call.i timeout 900   730   4600 wit - -
loop-new/count_by_nondet_true-unreach-call.i timeout 900   710   3700 wit - -
loop-new/gauss_sum_true-unreach-call.i true 77   30   2000 wit - -
loop-new/half_true-unreach-call.i timeout 900   720   5000 wit - -
loop-new/nested_true-unreach-call.i timeout 900   720   4100 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 45000 35000 330000 141 350   250   11000   141 800   520   27000  
    correct results 90 3600 2300 90000 34 260   160   11000   30 740   480   20000  
        correct true 56 3100 2000 73000 1 0   0   0   0 0   0   0  
        correct false 34 510 290 17000 33 260   160   11000   30 740   480   20000  
    incorrect results 1 310 140 4700 0 0   0   0   0 0   0   0  
        incorrect true 0
        incorrect false 1 310 140 4700 0 0   0   0   0 0   0   0  
score (141 tasks, max score: 234) 130
Run set sv-comp16.Loops