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 01:42:53 CET [[ 2016-01-15 08:36:34 CET ]] [[ 2016-01-15 22:02:40 CET ]]
Run set sv-comp16.Loops
Options -sv-comp16--k-induction -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-kind.2016-01-04_0142.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-kind.2016-01-04_0142.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) 5.7 2.0 360 wit false(reach) 5.3 3.1 240 false(reach) 12 7.1 330
loops/bubble_sort_false-unreach-call.i false(reach) 17   6.7 500 wit false(reach) 13   7.0 470 error 11 7.1 330
loops/count_up_down_false-unreach-call_true-termination.i false(reach) 4.9 1.9 320 wit false(reach) 3.7 2.2 230 false(reach) 12 7.1 330
loops/eureka_01_false-unreach-call.i timeout 900   420   5900 wit - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(reach) 6.8 2.6 350 wit false(reach) 5.3 3.1 230 false(reach) 12 8.2 340
loops/insertion_sort_false-unreach-call.i exception 58   19   1900 wit - -
loops/invert_string_false-unreach-call.i false(reach) 25   6.7 890 wit false(reach) 7.6 4.4 360 false(reach) 16 9.0 360
loops/linear_search_false-unreach-call.i unknown 6.2 2.1 380 wit - -
loops/ludcmp_false-unreach-call.i timeout 900   410   4100 wit - -
loops/matrix_false-unreach-call_true-termination.i false(reach) 57   20   3700 wit false(reach) 20   16   780 false(reach) 14 7.9 350
loops/n.c24_false-unreach-call.i timeout 900   420   4700 wit - -
loops/nec11_false-unreach-call.i false(reach) 5.9 2.2 330 wit false(reach) 4.9 2.9 230 false(reach) 12 7.3 330
loops/nec20_false-unreach-call.i false(reach) 6.6 2.6 360 wit false(reach) 6.1 3.5 330 false(reach) 11 7.1 340
loops/s3_false-unreach-call.i out of memory 110   60   15000 wit - -
loops/string_false-unreach-call.i witness unconfirmed 140   55   4100 wit true 6.3 3.6 250 timeout 91 57   870
loops/sum01_bug02_false-unreach-call_true-termination.i false(reach) 8.9 2.8 400 wit false(reach) 6.0 3.5 250 false(reach) 16 8.8 340
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(reach) 6.2 2.2 350 wit false(reach) 5.0 2.9 250 false(reach) 15 9.8 360
loops/sum01_false-unreach-call_true-termination.i false(reach) 9.6 2.8 430 wit false(reach) 5.2 3.0 260 false(reach) 18 11   360
loops/sum03_false-unreach-call_true-termination.i false(reach) 12   3.3 490 wit false(reach) 6.4 3.6 350 false(reach) 33 19   550
loops/sum04_false-unreach-call_true-termination.i false(reach) 8.1 2.7 390 wit false(reach) 5.3 3.1 240 false(reach) 15 8.4 340
loops/sum_array_false-unreach-call.i false(reach) 22   6.6 1000 wit false(reach) 7.5 4.5 380 false(reach) 14 8.8 340
loops/terminator_01_false-unreach-call_false-termination.i false(reach) 5.6 2.2 330 wit false(reach) 4.6 2.9 220 false(reach) 12 6.7 340
loops/terminator_02_false-unreach-call_true-termination.i false(reach) 5.7 2.2 340 wit false(reach) 4.3 2.5 230 false(reach) 12 6.6 330
loops/terminator_03_false-unreach-call_true-termination.i false(reach) 6.1 2.4 340 wit false(reach) 4.8 2.9 230 false(reach) 12 7.2 340
loops/trex01_false-unreach-call_true-termination.i false(reach) 6.3 2.5 340 wit false(reach) 4.4 2.5 240 false(reach) 14 7.9 350
loops/trex02_false-unreach-call_true-termination.i false(reach) 5.8 2.2 340 wit false(reach) 3.8 2.3 230 false(reach) 12 6.8 340
loops/trex03_false-unreach-call_true-termination.i false(reach) 5.0 2.0 340 wit false(reach) 5.3 3.1 240 false(reach) 12 7.4 350
loops/verisec_NetBSD-libc__loop_false-unreach-call.i unknown 4.7 1.9 330 wit - -
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.i false(reach) 38   8.7 930 wit false(reach) 7.2 4.0 340 false(reach) 26 15   500
loops/vogal_false-unreach-call.i false(reach) 63   13   1500 wit false(reach) 10   5.8 440 timeout 90 67   1500
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(reach) 4.7 1.9 330 wit false(reach) 4.6 2.7 230 false(reach) 12 6.9 330
loops/array_true-unreach-call.i true 4.6 1.8 260 wit - -
loops/bubble_sort_true-unreach-call.i true 4.3 1.8 230 wit - -
loops/count_up_down_true-unreach-call_true-termination.i timeout 900   430   7900 wit - -
loops/eureka_01_true-unreach-call.i timeout 900   410   5300 wit - -
loops/eureka_05_true-unreach-call.i timeout 900   410   4800 wit - -
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true 3.7 1.5 250 wit - -
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true 4.5 1.8 250 wit - -
loops/insertion_sort_true-unreach-call.i timeout 900   430   4000 wit - -
loops/invert_string_true-unreach-call.i true 64   12   1200 wit - -
loops/linear_sea.ch_true-unreach-call.i unknown 6.7 2.4 380 wit - -
loops/lu.cmp_true-unreach-call.i true 17   4.0 620 wit - -
loops/matrix_true-unreach-call_true-termination.i true 22   4.9 810 wit - -
loops/n.c11_true-unreach-call.i true 4.4 1.7 250 wit - -
loops/n.c40_true-unreach-call.i true 4.2 1.6 240 wit - -
loops/nec40_true-unreach-call.i true 4.3 1.6 250 wit - -
loops/string_true-unreach-call.i true 8.4 2.6 370 wit - -
loops/sum01_true-unreach-call_true-termination.i timeout 900   430   6100 wit - -
loops/sum03_true-unreach-call_false-termination.i true 4.5 1.7 250 wit - -
loops/sum04_true-unreach-call_true-termination.i true 6.0 2.2 280 wit - -
loops/sum_array_true-unreach-call.i timeout 900   420   5200 wit - -
loops/terminator_02_true-unreach-call_true-termination.i true 4.0 1.6 250 wit - -
loops/terminator_03_true-unreach-call_true-termination.i true 5.1 2.0 250 wit - -
loops/trex01_true-unreach-call.i true 6.5 2.1 360 wit - -
loops/trex02_true-unreach-call_true-termination.i true 4.5 1.9 250 wit - -
loops/trex03_true-unreach-call.i true 5.5 2.0 260 wit - -
loops/trex04_true-unreach-call_false-termination.i true 5.3 2.0 260 wit - -
loops/veris.c_NetBSD-libc__loop_true-unreach-call.i true 4.1 1.7 240 wit - -
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.i true 4.0 1.6 240 wit - -
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i true 5.0 1.9 250 wit - -
loops/vogal_true-unreach-call.i true 91   27   2000 wit - -
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true 4.4 1.8 240 wit - -
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 4.5 1.8 240 wit - -
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true 3.8 1.5 250 wit - -
loop-acceleration/array_false-unreach-call1.i timeout 900   430   11000 wit - -
loop-acceleration/array_false-unreach-call2.i timeout 900   430   9900 wit - -
loop-acceleration/array_false-unreach-call3.i timeout 900   430   7000 wit - -
loop-acceleration/const_false-unreach-call1.i timeout 900   430   12000 wit - -
loop-acceleration/diamond_false-unreach-call1.i false(reach) 31   9.7 1900 wit false(reach) 8.1 4.5 410 timeout 91 63   3400
loop-acceleration/functions_false-unreach-call1.i timeout 900   440   12000 wit - -
loop-acceleration/multivar_false-unreach-call1.i false(reach) 4.8 1.8 330 wit false(reach) 4.8 2.8 230 false(reach) 11 6.5 320
loop-acceleration/nested_false-unreach-call1.i timeout 900   430   4000 wit - -
loop-acceleration/phases_false-unreach-call1.i timeout 900   440   6100 wit - -
loop-acceleration/phases_false-unreach-call2.i false(reach) 5.1 1.9 330 wit false(reach) 4.5 2.6 230 false(reach) 12 7.5 330
loop-acceleration/simple_false-unreach-call1.i timeout 900   440   8600 wit - -
loop-acceleration/simple_false-unreach-call2.i false(reach) 4.7 1.8 320 wit false(reach) 4.5 2.7 220 false(reach) 11 6.8 320
loop-acceleration/simple_false-unreach-call3.i false(reach) 4.8 1.8 330 wit false(reach) 4.3 2.5 230 false(reach) 11 6.3 320
loop-acceleration/simple_false-unreach-call4.i timeout 900   440   8300 wit - -
loop-acceleration/underapprox_false-unreach-call1.i false(reach) 7.1 2.5 350 wit false(reach) 5.5 3.2 240 false(reach) 21 11   400
loop-acceleration/underapprox_false-unreach-call2.i false(reach) 5.8 2.1 350 wit false(reach) 5.2 3.1 240 false(reach) 17 9.5 360
loop-acceleration/array_true-unreach-call1.i true 3.8 1.5 250 wit - -
loop-acceleration/array_true-unreach-call2.i timeout 900   440   10000 wit - -
loop-acceleration/array_true-unreach-call3.i true 4.7 1.9 250 wit - -
loop-acceleration/array_true-unreach-call4.i timeout 900   430   6600 wit - -
loop-acceleration/const_true-unreach-call1.i true 3.8 1.5 250 wit - -
loop-acceleration/diamond_true-unreach-call1.i true 29   9.3 2400 wit - -
loop-acceleration/diamond_true-unreach-call2.i true 14   3.5 560 wit - -
loop-acceleration/functions_true-unreach-call1.i timeout 900   440   8900 wit - -
loop-acceleration/multivar_true-unreach-call1.i true 4.7 1.7 260 wit - -
loop-acceleration/nested_true-unreach-call1.i true 5.0 1.9 240 wit - -
loop-acceleration/overflow_true-unreach-call1.i timeout 900   440   8600 wit - -
loop-acceleration/phases_true-unreach-call1.i timeout 900   440   6000 wit - -
loop-acceleration/phases_true-unreach-call2.i true 4.6 1.8 240 wit - -
loop-acceleration/simple_true-unreach-call1.i timeout 900   440   8700 wit - -
loop-acceleration/simple_true-unreach-call2.i true 4.5 1.8 240 wit - -
loop-acceleration/simple_true-unreach-call3.i timeout 900   440   5700 wit - -
loop-acceleration/simple_true-unreach-call4.i true 4.6 1.8 250 wit - -
loop-acceleration/underapprox_true-unreach-call1.i true 5.8 2.1 280 wit - -
loop-acceleration/underapprox_true-unreach-call2.i true 3.8 1.6 250 wit - -
loop-invgen/id_trans_false-unreach-call.i false(reach) 5.3 2.1 340 wit false(reach) 5.0 2.9 240 false(reach) 12 6.9 330
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call.i timeout 900   430   4600 wit - -
loop-invgen/NetBSD_loop_true-unreach-call.i timeout 900   430   6600 wit - -
loop-invgen/SpamAssassin-loop_true-unreach-call.i timeout 900   420   4200 wit - -
loop-invgen/apache-escape-absolute_true-unreach-call.i timeout 900   420   4500 wit - -
loop-invgen/apache-get-tag_true-unreach-call.i true 21   4.4 610 wit - -
loop-invgen/down_true-unreach-call.i timeout 900   420   7500 wit - -
loop-invgen/fragtest_simple_true-unreach-call.i timeout 900   410   6800 wit - -
loop-invgen/half_2_true-unreach-call.i timeout 900   430   5800 wit - -
loop-invgen/heapsort_true-unreach-call.i timeout 900   420   4300 wit - -
loop-invgen/id_build_true-unreach-call.i true 5.7 1.9 280 wit - -
loop-invgen/large_const_true-unreach-call.i true 6.3 2.2 270 wit - -
loop-invgen/nest-if3_true-unreach-call.i timeout 900   430   4300 wit - -
loop-invgen/nested6_true-unreach-call.i timeout 900   420   4500 wit - -
loop-invgen/nested9_true-unreach-call.i timeout 900   430   4400 wit - -
loop-invgen/sendmail-close-angle_true-unreach-call.i timeout 900   430   7500 wit - -
loop-invgen/seq_true-unreach-call.i timeout 900   390   5900 wit - -
loop-invgen/string_concat-noarr_true-unreach-call.i timeout 900   420   9400 wit - -
loop-invgen/up_true-unreach-call.i timeout 900   420   7600 wit - -
loop-lit/afnp2014_true-unreach-call.c.i true 63   24   3900 wit - -
loop-lit/bhmr2007_true-unreach-call.c.i timeout 900   440   4000 wit - -
loop-lit/cggmp2005_true-unreach-call.c.i true 5.3 2.0 260 wit - -
loop-lit/cggmp2005_variant_true-unreach-call.c.i timeout 900   430   10000 wit - -
loop-lit/cggmp2005b_true-unreach-call.c.i true 4.7 1.7 260 wit - -
loop-lit/css2003_true-unreach-call.c.i true 5.1 2.0 260 wit - -
loop-lit/ddlm2013_true-unreach-call.c.i timeout 900   430   9800 wit - -
loop-lit/gj2007_true-unreach-call.c.i true 11   3.0 480 wit - -
loop-lit/gj2007b_true-unreach-call.c.i timeout 900   430   5200 wit - -
loop-lit/gr2006_true-unreach-call.c.i true 33   7.9 1100 wit - -
loop-lit/gsv2008_true-unreach-call.c.i timeout 900   440   3700 wit - -
loop-lit/hhk2008_true-unreach-call.c.i timeout 900   430   4700 wit - -
loop-lit/jm2006_true-unreach-call.c.i timeout 900   430   8800 wit - -
loop-lit/jm2006_variant_true-unreach-call.c.i timeout 900   430   12000 wit - -
loop-lit/mcmillan2006_true-unreach-call.c.i unknown 13   5.0 540 wit - -
loop-new/count_by_1_true-unreach-call.i true 3.8 1.5 240 wit - -
loop-new/count_by_1_variant_true-unreach-call.i true 3.8 1.6 240 wit - -
loop-new/count_by_2_true-unreach-call.i timeout 900   440   8900 wit - -
loop-new/count_by_k_true-unreach-call.i timeout 900   440   7600 wit - -
loop-new/count_by_nondet_true-unreach-call.i timeout 900   430   4200 wit - -
loop-new/gauss_sum_true-unreach-call.i true 77   30   2800 wit - -
loop-new/half_true-unreach-call.i timeout 900   430   7700 wit - -
loop-new/nested_true-unreach-call.i timeout 900   430   4200 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 49000 23000 430000 141 200   120   9200   141 690   430   16000  
    correct results 81 1000 330 45000 31 190   120   9000   28 600   370   15000  
        correct true 50 630 200 27000 0 0   0   0   0 0   0   0  
        correct false 31 410 130 19000 31 190   120   9000   28 600   370   15000  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (141 tasks, max score: 234) 131
Run set sv-comp16.Loops