Tool CPAchecker 1.4-svn 18356M
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-10 22:01:17 CET [[ 2016-01-15 09:16:15 CET ]] [[ 2016-01-15 22:26:01 CET ]]
Run set sv-comp16.Loops
Options -lpi-svcomp16 -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/lpi.2016-01-10_2201.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/lpi.2016-01-10_2201.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) 6.7 2.6 310 wit false(reach) 5.3 3.1 240 false(reach) 12 7.0 330
loops/bubble_sort_false-unreach-call.i false(reach) 14   6.5 430 wit false(reach) 13   7.5 460 error 10 5.9 310
loops/count_up_down_false-unreach-call_true-termination.i false(reach) 4.6 1.9 310 wit false(reach) 4.4 2.6 230 false(reach) 12 7.3 350
loops/eureka_01_false-unreach-call.i timeout 900   370   7200 wit - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(reach) 6.3 2.4 320 wit false(reach) 5.3 3.0 240 false(reach) 12 6.7 320
loops/insertion_sort_false-unreach-call.i exception 26   5.4 650 wit - -
loops/invert_string_false-unreach-call.i false(reach) 16   5.0 450 wit false(reach) 7.7 4.5 360 false(reach) 16 9.2 350
loops/linear_search_false-unreach-call.i unknown 6.2 2.4 320 wit - -
loops/ludcmp_false-unreach-call.i timeout 910   360   6200 wit - -
loops/matrix_false-unreach-call_true-termination.i false(reach) 15   4.5 670 wit false(reach) 20   16   770 false(reach) 16 8.9 360
loops/n.c24_false-unreach-call.i timeout 900   380   5800 wit - -
loops/nec11_false-unreach-call.i false(reach) 5.2 1.9 310 wit false(reach) 3.9 2.3 240 false(reach) 12 7.0 350
loops/nec20_false-unreach-call.i false(reach) 6.5 2.6 340 wit false(reach) 6.3 3.7 330 false(reach) 13 6.8 330
loops/s3_false-unreach-call.i out of memory 96   58   15000 wit - -
loops/string_false-unreach-call.i witness unconfirmed 48   12   1100 wit true 5.4 3.0 250 timeout 92 61   810
loops/sum01_bug02_false-unreach-call_true-termination.i false(reach) 7.1 2.4 330 wit false(reach) 6.2 3.5 250 false(reach) 16 9.4 330
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(reach) 6.3 2.3 320 wit false(reach) 4.6 2.7 240 false(reach) 15 8.4 340
loops/sum01_false-unreach-call_true-termination.i false(reach) 8.1 2.6 340 wit false(reach) 6.9 4.1 350 false(reach) 17 9.5 340
loops/sum03_false-unreach-call_true-termination.i false(reach) 10   2.8 360 wit false(reach) 7.9 4.4 340 false(reach) 33 18   550
loops/sum04_false-unreach-call_true-termination.i false(reach) 7.1 2.4 330 wit false(reach) 5.5 3.2 250 false(reach) 17 9.0 360
loops/sum_array_false-unreach-call.i false(reach) 13   4.6 390 wit false(reach) 7.4 4.2 380 false(reach) 14 8.0 330
loops/terminator_01_false-unreach-call_false-termination.i false(reach) 5.5 2.1 320 wit false(reach) 4.5 2.7 230 false(reach) 12 9.2 320
loops/terminator_02_false-unreach-call_true-termination.i false(reach) 4.7 1.9 320 wit false(reach) 4.7 2.9 230 false(reach) 11 6.5 330
loops/terminator_03_false-unreach-call_true-termination.i false(reach) 4.9 2.0 320 wit false(reach) 4.7 2.7 230 false(reach) 13 9.5 340
loops/trex01_false-unreach-call_true-termination.i false(reach) 5.3 2.1 320 wit false(reach) 5.1 2.9 240 false(reach) 12 8.0 320
loops/trex02_false-unreach-call_true-termination.i false(reach) 4.8 2.0 310 wit false(reach) 4.7 2.8 230 false(reach) 12 7.0 330
loops/trex03_false-unreach-call_true-termination.i false(reach) 5.3 2.1 320 wit false(reach) 5.6 3.2 230 false(reach) 13 7.4 340
loops/verisec_NetBSD-libc__loop_false-unreach-call.i unknown 5.0 1.9 330 wit - -
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.i false(reach) 27   7.6 750 wit false(reach) 7.0 3.9 340 false(reach) 26 15   510
loops/vogal_false-unreach-call.i false(reach) 45   8.3 950 wit false(reach) 8.9 5.0 420 timeout 91 67   1300
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(reach) 5.2 2.2 310 wit false(reach) 4.6 2.7 220 false(reach) 11 7.2 340
loops/array_true-unreach-call.i true 5.2 2.0 240 wit - -
loops/bubble_sort_true-unreach-call.i true 3.9 1.6 230 wit - -
loops/count_up_down_true-unreach-call_true-termination.i unknown 5.1 1.9 310 wit - -
loops/eureka_01_true-unreach-call.i timeout 900   390   5200 wit - -
loops/eureka_05_true-unreach-call.i true 210   76   4100 wit - -
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true 3.8 1.7 220 wit - -
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true 4.4 1.9 220 wit - -
loops/insertion_sort_true-unreach-call.i timeout 900   360   5500 wit - -
loops/invert_string_true-unreach-call.i true 17   3.8 490 wit - -
loops/linear_sea.ch_true-unreach-call.i unknown 5.4 2.0 330 wit - -
loops/lu.cmp_true-unreach-call.i true 31   6.1 800 wit - -
loops/matrix_true-unreach-call_true-termination.i true 7.5 2.3 340 wit - -
loops/n.c11_true-unreach-call.i true 5.2 2.1 240 wit - -
loops/n.c40_true-unreach-call.i true 3.8 1.6 230 wit - -
loops/nec40_true-unreach-call.i true 4.0 1.7 230 wit - -
loops/string_true-unreach-call.i true 7.7 2.5 320 wit - -
loops/sum01_true-unreach-call_true-termination.i true 7.9 2.4 330 wit - -
loops/sum03_true-unreach-call_false-termination.i true 4.3 1.7 230 wit - -
loops/sum04_true-unreach-call_true-termination.i true 5.5 1.9 300 wit - -
loops/sum_array_true-unreach-call.i timeout 900   370   6400 wit - -
loops/terminator_02_true-unreach-call_true-termination.i true 4.0 1.6 230 wit - -
loops/terminator_03_true-unreach-call_true-termination.i true 4.1 1.7 230 wit - -
loops/trex01_true-unreach-call.i true 5.3 1.9 300 wit - -
loops/trex02_true-unreach-call_true-termination.i true 4.8 2.0 230 wit - -
loops/trex03_true-unreach-call.i unknown 5.2 2.0 310 wit - -
loops/trex04_true-unreach-call_false-termination.i true 4.4 1.7 240 wit - -
loops/veris.c_NetBSD-libc__loop_true-unreach-call.i timeout 900   420   4100 wit - -
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.i true 4.1 1.7 230 wit - -
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i true 5.6 2.0 300 wit - -
loops/vogal_true-unreach-call.i true 46   9.1 1100 wit - -
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true 3.7 1.6 220 wit - -
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 3.8 1.6 230 wit - -
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true 3.7 1.6 230 wit - -
loop-acceleration/array_false-unreach-call1.i timeout 900   410   4600 wit - -
loop-acceleration/array_false-unreach-call2.i timeout 900   410   4500 wit - -
loop-acceleration/array_false-unreach-call3.i false(reach) 700   320   4000 wit false(reach) 84   64   1800 timeout 90 60   4000
loop-acceleration/const_false-unreach-call1.i timeout 900   420   4100 wit - -
loop-acceleration/diamond_false-unreach-call1.i false(reach) 49   9.7 1300 wit false(reach) 8.7 4.8 410 timeout 91 62   4000
loop-acceleration/functions_false-unreach-call1.i timeout 900   420   3900 wit - -
loop-acceleration/multivar_false-unreach-call1.i false(reach) 5.1 2.0 310 wit false(reach) 4.1 2.4 230 false(reach) 11 8.9 320
loop-acceleration/nested_false-unreach-call1.i timeout 900   420   4200 wit - -
loop-acceleration/phases_false-unreach-call1.i timeout 900   420   3900 wit - -
loop-acceleration/phases_false-unreach-call2.i false(reach) 4.9 1.9 310 wit false(reach) 4.2 2.5 230 false(reach) 11 6.6 330
loop-acceleration/simple_false-unreach-call1.i timeout 900   420   3900 wit - -
loop-acceleration/simple_false-unreach-call2.i false(reach) 5.1 2.0 310 wit false(reach) 4.6 2.7 230 false(reach) 12 6.9 330
loop-acceleration/simple_false-unreach-call3.i false(reach) 5.9 2.3 330 wit false(reach) 4.6 2.6 220 false(reach) 12 7.2 340
loop-acceleration/simple_false-unreach-call4.i timeout 900   420   4000 wit - -
loop-acceleration/underapprox_false-unreach-call1.i false(reach) 5.7 2.1 330 wit false(reach) 5.5 3.2 230 false(reach) 17 9.6 370
loop-acceleration/underapprox_false-unreach-call2.i false(reach) 5.8 2.2 320 wit false(reach) 5.3 3.0 240 false(reach) 17 12   360
loop-acceleration/array_true-unreach-call1.i true 4.0 1.7 230 wit - -
loop-acceleration/array_true-unreach-call2.i timeout 900   410   4600 wit - -
loop-acceleration/array_true-unreach-call3.i true 4.7 1.9 230 wit - -
loop-acceleration/array_true-unreach-call4.i timeout 900   420   4000 wit - -
loop-acceleration/const_true-unreach-call1.i true 3.8 1.6 220 wit - -
loop-acceleration/diamond_true-unreach-call1.i unknown 88   28   2400 wit - -
loop-acceleration/diamond_true-unreach-call2.i timeout 900   400   4400 wit - -
loop-acceleration/functions_true-unreach-call1.i true 4.2 1.7 230 wit - -
loop-acceleration/multivar_true-unreach-call1.i true 4.2 1.7 230 wit - -
loop-acceleration/nested_true-unreach-call1.i true 6.2 2.1 310 wit - -
loop-acceleration/overflow_true-unreach-call1.i true 3.8 1.6 230 wit - -
loop-acceleration/phases_true-unreach-call1.i timeout 900   420   3900 wit - -
loop-acceleration/phases_true-unreach-call2.i unknown 6.2 2.3 320 wit - -
loop-acceleration/simple_true-unreach-call1.i true 4.0 1.6 230 wit - -
loop-acceleration/simple_true-unreach-call2.i true 3.8 1.6 230 wit - -
loop-acceleration/simple_true-unreach-call3.i true 4.0 1.6 230 wit - -
loop-acceleration/simple_true-unreach-call4.i true 3.9 1.6 220 wit - -
loop-acceleration/underapprox_true-unreach-call1.i true 6.2 2.1 340 wit - -
loop-acceleration/underapprox_true-unreach-call2.i true 4.8 2.0 230 wit - -
loop-invgen/id_trans_false-unreach-call.i false(reach) 5.5 2.0 320 wit false(reach) 5.1 3.0 230 false(reach) 12 8.7 320
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call.i true 180   75   3800 wit - -
loop-invgen/NetBSD_loop_true-unreach-call.i true 12   3.0 430 wit - -
loop-invgen/SpamAssassin-loop_true-unreach-call.i timeout 900   410   4500 wit - -
loop-invgen/apache-escape-absolute_true-unreach-call.i true 15   3.5 420 wit - -
loop-invgen/apache-get-tag_true-unreach-call.i true 7.9 2.4 340 wit - -
loop-invgen/down_true-unreach-call.i true 20   4.4 500 wit - -
loop-invgen/fragtest_simple_true-unreach-call.i true 43   9.0 1100 wit - -
loop-invgen/half_2_true-unreach-call.i timeout 900   420   4300 wit - -
loop-invgen/heapsort_true-unreach-call.i timeout 900   400   4600 wit - -
loop-invgen/id_build_true-unreach-call.i true 5.3 2.0 230 wit - -
loop-invgen/large_const_true-unreach-call.i true 5.7 2.0 310 wit - -
loop-invgen/nest-if3_true-unreach-call.i true 16   3.9 440 wit - -
loop-invgen/nested6_true-unreach-call.i true 59   14   1400 wit - -
loop-invgen/nested9_true-unreach-call.i true 37   6.9 930 wit - -
loop-invgen/sendmail-close-angle_true-unreach-call.i true 24   4.7 650 wit - -
loop-invgen/seq_true-unreach-call.i true 110   34   4000 wit - -
loop-invgen/string_concat-noarr_true-unreach-call.i true 13   3.2 370 wit - -
loop-invgen/up_true-unreach-call.i true 41   7.4 920 wit - -
loop-lit/afnp2014_true-unreach-call.c.i true 6.5 2.2 320 wit - -
loop-lit/bhmr2007_true-unreach-call.c.i true 26   6.3 950 wit - -
loop-lit/cggmp2005_true-unreach-call.c.i true 4.4 1.7 230 wit - -
loop-lit/cggmp2005_variant_true-unreach-call.c.i true 9.4 2.5 380 wit - -
loop-lit/cggmp2005b_true-unreach-call.c.i true 4.5 1.7 230 wit - -
loop-lit/css2003_true-unreach-call.c.i true 4.4 1.7 230 wit - -
loop-lit/ddlm2013_true-unreach-call.c.i timeout 900   410   5400 wit - -
loop-lit/gj2007_true-unreach-call.c.i true 36   7.5 900 wit - -
loop-lit/gj2007b_true-unreach-call.c.i true 5.6 2.0 300 wit - -
loop-lit/gr2006_true-unreach-call.c.i true 32   6.4 960 wit - -
loop-lit/gsv2008_true-unreach-call.c.i true 4.0 1.6 230 wit - -
loop-lit/hhk2008_true-unreach-call.c.i true 24   4.7 830 wit - -
loop-lit/jm2006_true-unreach-call.c.i true 16   3.6 580 wit - -
loop-lit/jm2006_variant_true-unreach-call.c.i true 31   6.3 850 wit - -
loop-lit/mcmillan2006_true-unreach-call.c.i unknown 9.2 4.4 360 wit - -
loop-new/count_by_1_true-unreach-call.i true 3.6 1.5 230 wit - -
loop-new/count_by_1_variant_true-unreach-call.i true 4.7 2.0 220 wit - -
loop-new/count_by_2_true-unreach-call.i true 4.5 1.8 230 wit - -
loop-new/count_by_k_true-unreach-call.i timeout 900   420   3900 wit - -
loop-new/count_by_nondet_true-unreach-call.i timeout 900   410   4700 wit - -
loop-new/gauss_sum_true-unreach-call.i unknown 6.2 2.3 320 wit - -
loop-new/half_true-unreach-call.i timeout 900   420   4100 wit - -
loop-new/nested_true-unreach-call.i true 43   8.4 920 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 26000 11000 200000 141 290   180   11000   141 780   500   20000  
    correct results 103 2300 820 56000 32 280   180   11000   28 690   440   19000  
        correct true 71 1300 400 40000 0 0   0   0   0 0   0   0  
        correct false 32 1000 420 17000 32 280   180   11000   28 690   440   19000  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (141 tasks, max score: 234) 174
Run set sv-comp16.Loops