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