Tool ULTIMATE Kojak fd30d3d8
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-08 15:10:30 CET [[ 2016-01-15 09:49:48 CET ]] [[ 2016-01-15 22:43:29 CET ]]
Run set sv-comp16.Loops
Options [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/ukojak.2016-01-08_1510.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/ukojak.2016-01-08_1510.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 9.1 2.9 320 5.1 3.1 230 12 6.7 340
loops/bubble_sort_false-unreach-call.i 8.7 2.6 320
loops/count_up_down_false-unreach-call_true-termination.i 9.2 2.8 330 4.6 2.9 230 10 6.6 330
loops/eureka_01_false-unreach-call.i 130   930   1800
loops/for_bounded_loop1_false-unreach-call_true-termination.i 11   3.3 340 5.2 3.0 230 11 6.3 330
loops/insertion_sort_false-unreach-call.i 33   14   570 90   73   1500 16 9.5 360
loops/invert_string_false-unreach-call.i 15   4.4 470 90   76   1500 13 7.0 330
loops/linear_search_false-unreach-call.i 770   750   650
loops/ludcmp_false-unreach-call.i 55   30   7100
loops/matrix_false-unreach-call_true-termination.i 12   4.1 330 91   79   1300 13 7.4 340
loops/n.c24_false-unreach-call.i 59   930   1400
loops/nec11_false-unreach-call.i 8.8 2.7 320 4.9 3.0 230 10 6.5 330
loops/nec20_false-unreach-call.i 9.1 2.8 330 5.2 3.0 250 12 6.8 330
loops/s3_false-unreach-call.i 39   930   710
loops/string_false-unreach-call.i 23   7.8 380 8.2 4.6 340 27 15   380
loops/sum01_bug02_false-unreach-call_true-termination.i 16   4.4 430 5.9 3.3 260 14 8.1 340
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i 9.9 2.9 330 5.2 3.0 240 12 7.3 340
loops/sum01_false-unreach-call_true-termination.i 15   4.4 340 6.5 3.8 330 15 8.8 360
loops/sum03_false-unreach-call_true-termination.i 25   6.9 510 7.8 4.5 330 25 14   500
loops/sum04_false-unreach-call_true-termination.i 11   3.4 320 5.1 3.0 230 12 6.7 330
loops/sum_array_false-unreach-call.i 23   14   330 90   76   1500 13 7.6 350
loops/terminator_01_false-unreach-call_false-termination.i 9.4 2.8 340 4.6 2.8 230 11 6.5 320
loops/terminator_02_false-unreach-call_true-termination.i 8.7 2.8 320 4.9 2.8 230 10 6.1 330
loops/terminator_03_false-unreach-call_true-termination.i 9.1 2.8 320 5.0 3.0 230 11 6.4 340
loops/trex01_false-unreach-call_true-termination.i 8.3 2.7 330 5.1 3.1 230 12 6.7 330
loops/trex02_false-unreach-call_true-termination.i 8.7 2.9 320 4.0 2.4 220 11 6.1 330
loops/trex03_false-unreach-call_true-termination.i 9.2 2.8 330 5.1 2.9 230 11 6.7 330
loops/verisec_NetBSD-libc__loop_false-unreach-call.i 9.9 3.1 320 5.1 3.2 230 12 6.6 340
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.i 13   3.6 340 90   72   3500 27 15   510
loops/vogal_false-unreach-call.i 54   15   940 91   72   1500 91 69   1400
loops/while_infinite_loop_4_false-unreach-call_true-termination.i 8.6 2.6 320 4.6 2.7 220 11 6.6 320
loops/array_true-unreach-call.i 9.3 2.9 330
loops/bubble_sort_true-unreach-call.i 11   3.1 340
loops/count_up_down_true-unreach-call_true-termination.i 140   930   570
loops/eureka_01_true-unreach-call.i 98   930   1800
loops/eureka_05_true-unreach-call.i 97   67   1300
loops/for_infinite_loop_1_true-unreach-call_false-termination.i 8.1 2.6 330
loops/for_infinite_loop_2_true-unreach-call_false-termination.i 8.5 2.7 320
loops/insertion_sort_true-unreach-call.i 79   930   1200
loops/invert_string_true-unreach-call.i 68   930   660
loops/linear_sea.ch_true-unreach-call.i 720   930   770
loops/lu.cmp_true-unreach-call.i 47   30   7100
loops/matrix_true-unreach-call_true-termination.i 14   3.7 350
loops/n.c11_true-unreach-call.i 11   3.2 340
loops/n.c40_true-unreach-call.i 410   390   1800
loops/nec40_true-unreach-call.i 410   390   1700
loops/string_true-unreach-call.i 8.6 2.7 320
loops/sum01_true-unreach-call_true-termination.i 11   3.3 330
loops/sum03_true-unreach-call_false-termination.i 9.0 2.8 320
loops/sum04_true-unreach-call_true-termination.i 13   3.9 350
loops/sum_array_true-unreach-call.i 770   930   1100
loops/terminator_02_true-unreach-call_true-termination.i 8.3 2.6 330
loops/terminator_03_true-unreach-call_true-termination.i 9.0 2.8 330
loops/trex01_true-unreach-call.i 9.3 2.9 330
loops/trex02_true-unreach-call_true-termination.i 8.6 2.6 330
loops/trex03_true-unreach-call.i 9.2 2.8 320
loops/trex04_true-unreach-call_false-termination.i 9.5 2.9 330
loops/veris.c_NetBSD-libc__loop_true-unreach-call.i 10   3.2 320
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.i 9.5 2.9 320
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i 10   2.9 340
loops/vogal_true-unreach-call.i 79   930   1000
loops/while_infinite_loop_1_true-unreach-call_false-termination.i 9.5 2.8 330
loops/while_infinite_loop_2_true-unreach-call_false-termination.i 8.9 2.8 320
loops/while_infinite_loop_3_true-unreach-call_false-termination.i 8.9 2.8 340
loop-acceleration/array_false-unreach-call1.i 53   930   1500
loop-acceleration/array_false-unreach-call2.i 55   930   860
loop-acceleration/array_false-unreach-call3.i 54   930   1000
loop-acceleration/const_false-unreach-call1.i 44   930   730
loop-acceleration/diamond_false-unreach-call1.i 20   930   480
loop-acceleration/functions_false-unreach-call1.i 44   930   940
loop-acceleration/multivar_false-unreach-call1.i 8.8 2.7 330 4.8 2.9 230 10 5.9 330
loop-acceleration/nested_false-unreach-call1.i 44   930   640
loop-acceleration/phases_false-unreach-call1.i 900   840   4200
loop-acceleration/phases_false-unreach-call2.i 10   3.0 350 4.9 2.8 220 11 6.2 330
loop-acceleration/simple_false-unreach-call1.i 43   930   1100
loop-acceleration/simple_false-unreach-call2.i 8.9 2.9 320 4.4 2.7 220 10 6.0 330
loop-acceleration/simple_false-unreach-call3.i 9.5 2.9 330 4.7 2.8 220 11 5.9 340
loop-acceleration/simple_false-unreach-call4.i 37   930   1100
loop-acceleration/underapprox_false-unreach-call1.i 11   3.5 340 5.5 3.2 240 16 9.1 390
loop-acceleration/underapprox_false-unreach-call2.i 11   3.3 340 5.3 3.1 240 16 8.6 380
loop-acceleration/array_true-unreach-call1.i 55   930   740
loop-acceleration/array_true-unreach-call2.i 54   930   1200
loop-acceleration/array_true-unreach-call3.i 8.8 2.7 320
loop-acceleration/array_true-unreach-call4.i 51   930   940
loop-acceleration/const_true-unreach-call1.i 43   930   900
loop-acceleration/diamond_true-unreach-call1.i 21   930   450
loop-acceleration/diamond_true-unreach-call2.i 25   930   470
loop-acceleration/functions_true-unreach-call1.i 43   930   760
loop-acceleration/multivar_true-unreach-call1.i 8.4 2.7 320
loop-acceleration/nested_true-unreach-call1.i 42   930   880
loop-acceleration/overflow_true-unreach-call1.i 43   930   740
loop-acceleration/phases_true-unreach-call1.i 900   840   4200
loop-acceleration/phases_true-unreach-call2.i 16   10   330
loop-acceleration/simple_true-unreach-call1.i 39   930   620
loop-acceleration/simple_true-unreach-call2.i 9.0 2.8 330
loop-acceleration/simple_true-unreach-call3.i 9.9 3.3 330
loop-acceleration/simple_true-unreach-call4.i 8.8 2.7 330
loop-acceleration/underapprox_true-unreach-call1.i 900   880   400
loop-acceleration/underapprox_true-unreach-call2.i 12   3.5 330
loop-invgen/id_trans_false-unreach-call.i 10   3.1 320 5.2 3.0 240 11 6.5 330
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call.i 13   3.9 350
loop-invgen/NetBSD_loop_true-unreach-call.i 11   3.5 350
loop-invgen/SpamAssassin-loop_true-unreach-call.i 28   11   730
loop-invgen/apache-escape-absolute_true-unreach-call.i 26   8.2 460
loop-invgen/apache-get-tag_true-unreach-call.i 14   4.3 450
loop-invgen/down_true-unreach-call.i 59   930   1300
loop-invgen/fragtest_simple_true-unreach-call.i 53   930   790
loop-invgen/half_2_true-unreach-call.i 50   930   690
loop-invgen/heapsort_true-unreach-call.i 77   930   1200
loop-invgen/id_build_true-unreach-call.i 11   3.2 360
loop-invgen/large_const_true-unreach-call.i 12   3.4 360
loop-invgen/nest-if3_true-unreach-call.i 11   3.4 320
loop-invgen/nested6_true-unreach-call.i 24   9.2 470
loop-invgen/nested9_true-unreach-call.i 99   930   1600
loop-invgen/sendmail-close-angle_true-unreach-call.i 25   8.3 590
loop-invgen/seq_true-unreach-call.i 58   930   670
loop-invgen/string_concat-noarr_true-unreach-call.i 58   930   1000
loop-invgen/up_true-unreach-call.i 53   930   780
loop-lit/afnp2014_true-unreach-call.c.i 57   930   940
loop-lit/bhmr2007_true-unreach-call.c.i 9.5 2.9 320
loop-lit/cggmp2005_true-unreach-call.c.i 9.9 3.2 320
loop-lit/cggmp2005_variant_true-unreach-call.c.i 9.7 3.0 320
loop-lit/cggmp2005b_true-unreach-call.c.i 10   3.2 340
loop-lit/css2003_true-unreach-call.c.i 8.3 2.6 330
loop-lit/ddlm2013_true-unreach-call.c.i 41   930   660
loop-lit/gj2007_true-unreach-call.c.i 55   930   1100
loop-lit/gj2007b_true-unreach-call.c.i 11   3.1 330
loop-lit/gr2006_true-unreach-call.c.i 59   930   1400
loop-lit/gsv2008_true-unreach-call.c.i 9.9 3.1 320
loop-lit/hhk2008_true-unreach-call.c.i 8.8 2.7 320
loop-lit/jm2006_true-unreach-call.c.i 11   3.3 360
loop-lit/jm2006_variant_true-unreach-call.c.i 13   4.1 330
loop-lit/mcmillan2006_true-unreach-call.c.i 88   930   1000
loop-new/count_by_1_true-unreach-call.i 51   930   800
loop-new/count_by_1_variant_true-unreach-call.i 56   930   1000
loop-new/count_by_2_true-unreach-call.i 45   930   860
loop-new/count_by_k_true-unreach-call.i 38   930   850
loop-new/count_by_nondet_true-unreach-call.i 59   930   1500
loop-new/gauss_sum_true-unreach-call.i 8.9 2.8 330
loop-new/half_true-unreach-call.i 51   930   930
loop-new/nested_true-unreach-call.i 81   930   750
../../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 9700 50000 110000 141 680   530   17000   141 500   310   12000  
    correct results 83 1900 1200 33000 26 590   460   16000   31 410   240   11000  
        correct true 52 1500 1000 22000 0 0   0   0   0 0   0   0  
        correct false 31 380 130 11000 26 590   460   16000   31 410   240   11000  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (141 tasks, max score: 234) 135
Run set sv-comp16.Loops