Tool ULTIMATE Automizer cfb9fd9e
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-14 23:51:13 CET [[ 2016-01-15 09:43:48 CET ]] [[ 2016-01-15 22:41:15 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/uautomizer.2016-01-14_2351.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/uautomizer.2016-01-14_2351.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 3.4 330 4.6 2.6 240 12 7.0 330
loops/bubble_sort_false-unreach-call.i 9.6 3.3 340
loops/count_up_down_false-unreach-call_true-termination.i 7.8 2.6 310 4.4 2.6 220 11 6.0 330
loops/eureka_01_false-unreach-call.i 120   95   1000 8.5 5.0 390 17 11   360
loops/for_bounded_loop1_false-unreach-call_true-termination.i 9.8 3.5 320 5.5 3.2 240 12 6.7 330
loops/insertion_sort_false-unreach-call.i 86   51   940 90   74   1500 17 9.5 360
loops/invert_string_false-unreach-call.i 19   6.8 370 90   75   1500 14 8.1 350
loops/linear_search_false-unreach-call.i 190   180   430
loops/ludcmp_false-unreach-call.i 43   31   7100
loops/matrix_false-unreach-call_true-termination.i 9.5 2.9 330 91   82   1300 13 8.3 330
loops/n.c24_false-unreach-call.i 900   770   1200
loops/nec11_false-unreach-call.i 9.0 3.3 340 5.0 3.0 240 11 6.9 330
loops/nec20_false-unreach-call.i 8.1 3.0 320 6.3 3.8 330 11 6.3 330
loops/s3_false-unreach-call.i 270   220   930
loops/string_false-unreach-call.i 22   7.1 400 7.2 4.1 360 25 14   390
loops/sum01_bug02_false-unreach-call_true-termination.i 16   5.0 480 4.7 2.7 220 13 8.1 330
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i 11   3.9 360 4.2 2.5 220 13 7.7 340
loops/sum01_false-unreach-call_true-termination.i 18   6.8 470 5.0 2.9 230 15 9.6 340
loops/sum03_false-unreach-call_true-termination.i 19   6.6 470 7.2 4.0 370 27 15   530
loops/sum04_false-unreach-call_true-termination.i 10   3.6 330 5.5 3.2 250 14 8.5 350
loops/sum_array_false-unreach-call.i 9.7 3.1 330 90   76   1500 13 7.6 340
loops/terminator_01_false-unreach-call_false-termination.i 8.7 2.8 320 4.5 2.8 230 11 7.0 330
loops/terminator_02_false-unreach-call_true-termination.i 8.2 3.0 330 5.0 2.9 230 11 7.0 330
loops/terminator_03_false-unreach-call_true-termination.i 9.0 2.8 330 4.7 2.8 230 11 6.5 330
loops/trex01_false-unreach-call_true-termination.i 9.7 2.8 350 7.1 4.0 340 11 6.1 350
loops/trex02_false-unreach-call_true-termination.i 9.1 2.8 330 4.0 2.3 230 12 7.4 340
loops/trex03_false-unreach-call_true-termination.i 9.4 2.8 330 4.8 2.9 240 12 7.4 330
loops/verisec_NetBSD-libc__loop_false-unreach-call.i 11   3.3 340 5.8 3.3 320 12 6.9 330
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.i 16   5.0 480 90   74   3800 28 15   490
loops/vogal_false-unreach-call.i 170   150   1700
loops/while_infinite_loop_4_false-unreach-call_true-termination.i 8.4 2.7 320 5.0 2.8 230 12 7.5 330
loops/array_true-unreach-call.i 9.4 2.9 330
loops/bubble_sort_true-unreach-call.i 9.0 3.2 330
loops/count_up_down_true-unreach-call_true-termination.i 900   890   500
loops/eureka_01_true-unreach-call.i 900   780   1800
loops/eureka_05_true-unreach-call.i 35   17   590
loops/for_infinite_loop_1_true-unreach-call_false-termination.i 8.4 2.6 320
loops/for_infinite_loop_2_true-unreach-call_false-termination.i 8.6 3.0 320
loops/insertion_sort_true-unreach-call.i 160   100   940
loops/invert_string_true-unreach-call.i 130   100   1300
loops/linear_sea.ch_true-unreach-call.i 42   31   460
loops/lu.cmp_true-unreach-call.i 65   33   6900
loops/matrix_true-unreach-call_true-termination.i 12   3.5 370
loops/n.c11_true-unreach-call.i 10   3.3 330
loops/n.c40_true-unreach-call.i 390   380   890
loops/nec40_true-unreach-call.i 400   380   530
loops/string_true-unreach-call.i 20   6.1 430
loops/sum01_true-unreach-call_true-termination.i 900   760   1200
loops/sum03_true-unreach-call_false-termination.i 900   750   1200
loops/sum04_true-unreach-call_true-termination.i 12   3.8 340
loops/sum_array_true-unreach-call.i 900   800   1600
loops/terminator_02_true-unreach-call_true-termination.i 9.5 2.9 340
loops/terminator_03_true-unreach-call_true-termination.i 9.9 2.9 360
loops/trex01_true-unreach-call.i 9.6 2.9 330
loops/trex02_true-unreach-call_true-termination.i 9.2 2.8 330
loops/trex03_true-unreach-call.i 8.8 2.9 320
loops/trex04_true-unreach-call_false-termination.i 9.2 2.7 330
loops/veris.c_NetBSD-libc__loop_true-unreach-call.i 12   4.5 330
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.i 8.4 2.6 330
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i 9.8 3.2 320
loops/vogal_true-unreach-call.i 110   68   2400
loops/while_infinite_loop_1_true-unreach-call_false-termination.i 8.3 2.6 320
loops/while_infinite_loop_2_true-unreach-call_false-termination.i 9.2 2.7 340
loops/while_infinite_loop_3_true-unreach-call_false-termination.i 8.8 2.9 330
loop-acceleration/array_false-unreach-call1.i 900   740   1100
loop-acceleration/array_false-unreach-call2.i 900   750   1600
loop-acceleration/array_false-unreach-call3.i 900   740   1100
loop-acceleration/const_false-unreach-call1.i 900   750   990
loop-acceleration/diamond_false-unreach-call1.i 210   160   730 9.7 5.4 400 90 61   3500
loop-acceleration/functions_false-unreach-call1.i 900   740   1400
loop-acceleration/multivar_false-unreach-call1.i 9.3 4.2 330 4.7 2.7 230 12 7.2 350
loop-acceleration/nested_false-unreach-call1.i 900   750   2100
loop-acceleration/phases_false-unreach-call1.i 900   770   1400
loop-acceleration/phases_false-unreach-call2.i 9.7 3.9 320 4.6 2.7 240 12 7.5 330
loop-acceleration/simple_false-unreach-call1.i 900   760   1000
loop-acceleration/simple_false-unreach-call2.i 8.8 2.8 320 4.7 2.7 220 11 6.4 330
loop-acceleration/simple_false-unreach-call3.i 8.8 2.7 320 4.5 2.7 230 12 7.1 330
loop-acceleration/simple_false-unreach-call4.i 900   770   1200
loop-acceleration/underapprox_false-unreach-call1.i 11   3.3 340 5.1 2.9 240 16 9.1 360
loop-acceleration/underapprox_false-unreach-call2.i 10   3.3 330 5.1 3.0 240 17 9.6 370
loop-acceleration/array_true-unreach-call1.i 900   750   1600
loop-acceleration/array_true-unreach-call2.i 900   740   930
loop-acceleration/array_true-unreach-call3.i 9.3 2.9 320
loop-acceleration/array_true-unreach-call4.i 900   740   1100
loop-acceleration/const_true-unreach-call1.i 900   760   1100
loop-acceleration/diamond_true-unreach-call1.i 710   620   1400
loop-acceleration/diamond_true-unreach-call2.i 26   13   460
loop-acceleration/functions_true-unreach-call1.i 900   740   880
loop-acceleration/multivar_true-unreach-call1.i 9.4 3.2 340
loop-acceleration/nested_true-unreach-call1.i 900   750   2400
loop-acceleration/overflow_true-unreach-call1.i 900   760   990
loop-acceleration/phases_true-unreach-call1.i 900   780   1900
loop-acceleration/phases_true-unreach-call2.i 11   3.0 350
loop-acceleration/simple_true-unreach-call1.i 900   770   2000
loop-acceleration/simple_true-unreach-call2.i 9.8 4.0 330
loop-acceleration/simple_true-unreach-call3.i 900   790   1900
loop-acceleration/simple_true-unreach-call4.i 900   760   820
loop-acceleration/underapprox_true-unreach-call1.i 13   5.1 380
loop-acceleration/underapprox_true-unreach-call2.i 11   3.3 340
loop-invgen/id_trans_false-unreach-call.i 10   3.8 350 5.4 3.1 240 12 7.0 340
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call.i 900   740   1600
loop-invgen/NetBSD_loop_true-unreach-call.i 12   3.6 360
loop-invgen/SpamAssassin-loop_true-unreach-call.i 12   4.1 330
loop-invgen/apache-escape-absolute_true-unreach-call.i 13   4.0 330
loop-invgen/apache-get-tag_true-unreach-call.i 12   3.5 360
loop-invgen/down_true-unreach-call.i 900   720   1800
loop-invgen/fragtest_simple_true-unreach-call.i 900   730   1700
loop-invgen/half_2_true-unreach-call.i 900   740   1700
loop-invgen/heapsort_true-unreach-call.i 16   6.0 390
loop-invgen/id_build_true-unreach-call.i 9.1 2.7 340
loop-invgen/large_const_true-unreach-call.i 11   3.2 340
loop-invgen/nest-if3_true-unreach-call.i 8.8 3.1 350
loop-invgen/nested6_true-unreach-call.i 13   3.8 370
loop-invgen/nested9_true-unreach-call.i 900   750   2100
loop-invgen/sendmail-close-angle_true-unreach-call.i 900   740   1000
loop-invgen/seq_true-unreach-call.i 900   720   1500
loop-invgen/string_concat-noarr_true-unreach-call.i 520   440   1300
loop-invgen/up_true-unreach-call.i 900   720   1900
loop-lit/afnp2014_true-unreach-call.c.i 10   3.0 330
loop-lit/bhmr2007_true-unreach-call.c.i 900   640   2000
loop-lit/cggmp2005_true-unreach-call.c.i 10   3.0 330
loop-lit/cggmp2005_variant_true-unreach-call.c.i 900   770   1500
loop-lit/cggmp2005b_true-unreach-call.c.i 900   800   940
loop-lit/css2003_true-unreach-call.c.i 900   740   1400
loop-lit/ddlm2013_true-unreach-call.c.i 900   790   1000
loop-lit/gj2007_true-unreach-call.c.i 310   240   1600
loop-lit/gj2007b_true-unreach-call.c.i 12   4.1 360
loop-lit/gr2006_true-unreach-call.c.i 83   47   1100
loop-lit/gsv2008_true-unreach-call.c.i 8.9 2.7 340
loop-lit/hhk2008_true-unreach-call.c.i 900   770   1100
loop-lit/jm2006_true-unreach-call.c.i 900   760   810
loop-lit/jm2006_variant_true-unreach-call.c.i 900   760   800
loop-lit/mcmillan2006_true-unreach-call.c.i 900   740   1800
loop-new/count_by_1_true-unreach-call.i 900   740   970
loop-new/count_by_1_variant_true-unreach-call.i 900   730   2000
loop-new/count_by_2_true-unreach-call.i 900   750   1300
loop-new/count_by_k_true-unreach-call.i 900   830   2500
loop-new/count_by_nondet_true-unreach-call.i 900   750   1700
loop-new/gauss_sum_true-unreach-call.i 900   770   1100
loop-new/half_true-unreach-call.i 900   760   900
loop-new/nested_true-unreach-call.i 31   13   660
../../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 50000 41000 130000 141 600   470   17000   141 540   330   15000  
    correct results 82 3900 2900 39000 28 600   470   17000   32 540   330   15000  
        correct true 49 3100 2400 25000 3 0   0   0   0 0   0   0  
        correct false 33 750 420 13000 25 600   470   17000   32 540   330   15000  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (141 tasks, max score: 234) 131
Run set sv-comp16.Loops