Tool SMACK+Corral 1.5.2
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-07 09:05:16 CET [[ 2016-01-15 09:34:34 CET ]] [[ 2016-01-15 22:36:10 CET ]]
Run set sv-comp16.Loops
Options -w error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/smack.2016-01-07_0905.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/smack.2016-01-07_0905.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) 3.1 3.1 73 wit true 4.3 2.5 220 false(reach) 12 8.2 330
loops/bubble_sort_false-unreach-call.i witness unconfirmed 4.6 4.5 91 wit true 16   8.8 500 error 10 6.9 310
loops/count_up_down_false-unreach-call_true-termination.i false(reach) 3.3 3.3 75 wit false(reach) 4.7 2.9 230 false(reach) 12 6.9 340
loops/eureka_01_false-unreach-call.i false(reach) 3.8 3.7 91 wit timeout 90   75   960 false(reach) 60 44   1100
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(reach) 3.2 3.1 78 wit false(reach) 5.0 3.0 230 false(reach) 12 8.4 330
loops/insertion_sort_false-unreach-call.i false(reach) 3.9 3.8 81 wit timeout 90   73   1300 false(reach) 18 10   370
loops/invert_string_false-unreach-call.i false(reach) 3.5 3.4 80 wit timeout 90   74   1100 false(reach) 15 9.0 350
loops/linear_search_false-unreach-call.i false(reach) 24   24   100 wit true 7.4 4.1 290 false(reach) 73 64   430
loops/ludcmp_false-unreach-call.i witness timeout 98   98   580 wit timeout 91   87   790 timeout 47 35   7000
loops/matrix_false-unreach-call_true-termination.i false(reach) 3.4 3.4 76 wit timeout 91   81   810 false(reach) 14 7.5 340
loops/n.c24_false-unreach-call.i true 880   880   4000 wit - -
loops/nec11_false-unreach-call.i false(reach) 3.2 3.2 77 wit false(reach) 4.8 2.9 230 false(reach) 12 8.6 330
loops/nec20_false-unreach-call.i false(reach) 3.4 3.4 78 wit timeout 90   73   1600 false(reach) 12 6.6 340
loops/s3_false-unreach-call.i witness unconfirmed 16   16   200 wit true 14   7.4 460 true 17 12   340
loops/string_false-unreach-call.i false(reach) 3.6 3.6 83 wit true 5.0 3.1 220 false(reach) 33 20   420
loops/sum01_bug02_false-unreach-call_true-termination.i false(reach) 3.4 3.4 75 wit false(reach) 6.2 3.5 250 false(reach) 16 8.9 350
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(reach) 3.3 3.2 75 wit false(reach) 5.6 3.3 240 false(reach) 14 8.1 340
loops/sum01_false-unreach-call_true-termination.i false(reach) 3.3 3.3 83 wit false(reach) 6.7 3.8 280 false(reach) 16 9.3 340
loops/sum03_false-unreach-call_true-termination.i false(reach) 3.6 3.5 78 wit true 6.7 3.9 240 false(reach) 23 13   500
loops/sum04_false-unreach-call_true-termination.i witness unconfirmed 2.8 2.9 74 wit true 4.5 2.6 210 true 13 7.4 330
loops/sum_array_false-unreach-call.i false(reach) 3.5 3.5 76 wit timeout 90   76   910 false(reach) 14 7.7 350
loops/terminator_01_false-unreach-call_false-termination.i false(reach) 2.8 2.8 74 wit true 5.2 3.2 220 false(reach) 12 8.9 340
loops/terminator_02_false-unreach-call_true-termination.i false(reach) 3.0 3.0 73 wit false(reach) 4.8 2.8 220 false(reach) 11 8.1 340
loops/terminator_03_false-unreach-call_true-termination.i false(reach) 2.5 2.5 72 wit true 5.1 3.3 220 false(reach) 12 7.1 330
loops/trex01_false-unreach-call_true-termination.i false(reach) 3.3 3.2 79 wit false(reach) 6.9 3.9 340 false(reach) 13 8.3 350
loops/trex02_false-unreach-call_true-termination.i false(reach) 3.1 3.1 77 wit false(reach) 4.9 2.8 220 false(reach) 12 6.6 330
loops/trex03_false-unreach-call_true-termination.i false(reach) 3.2 3.2 79 wit false(reach) 4.9 2.8 230 false(reach) 11 7.0 320
loops/verisec_NetBSD-libc__loop_false-unreach-call.i false(reach) 3.3 3.2 76 wit true 4.9 2.9 230 false(reach) 13 8.5 340
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.i false(reach) 3.6 3.6 80 wit timeout 91   73   1400 false(reach) 31 17   490
loops/vogal_false-unreach-call.i witness unconfirmed 4.4 4.4 130 wit true 5.4 3.2 230 timeout 90 72   1000
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(reach) 3.2 3.2 75 wit false(reach) 4.9 2.9 230 false(reach) 13 7.2 340
loops/array_true-unreach-call.i true 2.6 2.6 64 wit - -
loops/bubble_sort_true-unreach-call.i true 3.0 3.0 78 wit - -
loops/count_up_down_true-unreach-call_true-termination.i true 880   880   1200 wit - -
loops/eureka_01_true-unreach-call.i timeout 880   930   660 wit - -
loops/eureka_05_true-unreach-call.i true 3.1 3.1 81 wit - -
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true 2.8 2.8 76 wit - -
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true 2.8 2.8 74 wit - -
loops/insertion_sort_true-unreach-call.i timeout 880   930   240 wit - -
loops/invert_string_true-unreach-call.i true 3.1 3.1 73 wit - -
loops/linear_sea.ch_true-unreach-call.i true 880   880   180 wit - -
loops/lu.cmp_true-unreach-call.i true 310   310   1100 wit - -
loops/matrix_true-unreach-call_true-termination.i true 2.8 2.8 67 wit - -
loops/n.c11_true-unreach-call.i true 890   880   620 wit - -
loops/n.c40_true-unreach-call.i true 3.1 3.1 75 wit - -
loops/nec40_true-unreach-call.i true 3.1 3.2 86 wit - -
loops/string_true-unreach-call.i true 3.1 3.1 79 wit - -
loops/sum01_true-unreach-call_true-termination.i true 880   880   790 wit - -
loops/sum03_true-unreach-call_false-termination.i true 250   240   390 wit - -
loops/sum04_true-unreach-call_true-termination.i true 2.5 2.6 64 wit - -
loops/sum_array_true-unreach-call.i true 880   880   480 wit - -
loops/terminator_02_true-unreach-call_true-termination.i true 2.9 2.9 71 wit - -
loops/terminator_03_true-unreach-call_true-termination.i true 2.9 2.9 76 wit - -
loops/trex01_true-unreach-call.i true 3.0 3.0 78 wit - -
loops/trex02_true-unreach-call_true-termination.i true 2.8 2.8 71 wit - -
loops/trex03_true-unreach-call.i true 880   880   470 wit - -
loops/trex04_true-unreach-call_false-termination.i true 2.9 2.9 74 wit - -
loops/veris.c_NetBSD-libc__loop_true-unreach-call.i true 3.0 3.0 74 wit - -
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.i true 3.0 3.0 73 wit - -
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i true 2.8 2.8 73 wit - -
loops/vogal_true-unreach-call.i true 6.2 6.3 89 wit - -
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true 2.8 2.8 69 wit - -
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 2.8 2.8 73 wit - -
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true 2.9 2.9 73 wit - -
loop-acceleration/array_false-unreach-call1.i witness unconfirmed 19   18   280 wit true 5.0 2.9 220 true 16 11   380
loop-acceleration/array_false-unreach-call2.i witness unconfirmed 190   180   2100 wit true 17   9.1 1100 timeout 91 56   5100
loop-acceleration/array_false-unreach-call3.i true 880   880   690 wit - -
loop-acceleration/const_false-unreach-call1.i witness unconfirmed 5.0 4.8 140 wit true 5.0 2.9 220 true 12 8.4 330
loop-acceleration/diamond_false-unreach-call1.i false(reach) 360   350   140 wit false(reach) 9.9 5.5 380 timeout 90 61   4000
loop-acceleration/functions_false-unreach-call1.i error (1) 880   880   1000 wit - -
loop-acceleration/multivar_false-unreach-call1.i false(reach) 3.2 3.2 78 wit false(reach) 4.8 2.8 230 false(reach) 11 6.5 340
loop-acceleration/nested_false-unreach-call1.i out of memory 530   530   15000 wit - -
loop-acceleration/phases_false-unreach-call1.i error (1) 880   880   330 wit - -
loop-acceleration/phases_false-unreach-call2.i true 880   880   93 wit - -
loop-acceleration/simple_false-unreach-call1.i out of memory 670   670   15000 wit - -
loop-acceleration/simple_false-unreach-call2.i false(reach) 3.2 3.2 76 wit true 4.7 2.8 220 false(reach) 12 7.1 340
loop-acceleration/simple_false-unreach-call3.i false(reach) 3.1 3.1 76 wit false(reach) 4.5 2.7 220 false(reach) 13 7.0 350
loop-acceleration/simple_false-unreach-call4.i out of memory 660   660   15000 wit - -
loop-acceleration/underapprox_false-unreach-call1.i witness unconfirmed 3.1 3.1 73 wit true 4.3 2.5 220 true 12 11   340
loop-acceleration/underapprox_false-unreach-call2.i witness unconfirmed 3.0 3.0 75 wit true 4.4 2.7 220 true 13 7.6 340
loop-acceleration/array_true-unreach-call1.i true 5.1 5.1 180 wit - -
loop-acceleration/array_true-unreach-call2.i true 37   37   1900 wit - -
loop-acceleration/array_true-unreach-call3.i true 880   880   710 wit - -
loop-acceleration/array_true-unreach-call4.i true 880   880   1000 wit - -
loop-acceleration/const_true-unreach-call1.i true 3.4 3.4 85 wit - -
loop-acceleration/diamond_true-unreach-call1.i true 880   880   200 wit - -
loop-acceleration/diamond_true-unreach-call2.i true 3.7 3.7 100 wit - -
loop-acceleration/functions_true-unreach-call1.i true 880   880   1100 wit - -
loop-acceleration/multivar_true-unreach-call1.i true 880   880   1000 wit - -
loop-acceleration/nested_true-unreach-call1.i out of memory 520   520   15000 wit - -
loop-acceleration/overflow_true-unreach-call1.i true 890   890   900 wit - -
loop-acceleration/phases_true-unreach-call1.i true 880   880   330 wit - -
loop-acceleration/phases_true-unreach-call2.i true 880   880   140 wit - -
loop-acceleration/simple_true-unreach-call1.i out of memory 670   670   15000 wit - -
loop-acceleration/simple_true-unreach-call2.i true 2.4 2.4 69 wit - -
loop-acceleration/simple_true-unreach-call3.i true 880   880   450 wit - -
loop-acceleration/simple_true-unreach-call4.i out of memory 650   650   15000 wit - -
loop-acceleration/underapprox_true-unreach-call1.i true 2.7 2.7 64 wit - -
loop-acceleration/underapprox_true-unreach-call2.i true 2.6 2.7 66 wit - -
loop-invgen/id_trans_false-unreach-call.i false(reach) 3.1 3.0 79 wit true 4.8 2.8 210 false(reach) 13 8.1 340
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call.i true 39   39   160 wit - -
loop-invgen/NetBSD_loop_true-unreach-call.i true 880   880   670 wit - -
loop-invgen/SpamAssassin-loop_true-unreach-call.i true 880   880   450 wit - -
loop-invgen/apache-escape-absolute_true-unreach-call.i true 880   880   330 wit - -
loop-invgen/apache-get-tag_true-unreach-call.i true 880   880   360 wit - -
loop-invgen/down_true-unreach-call.i true 880   880   390 wit - -
loop-invgen/fragtest_simple_true-unreach-call.i true 880   880   470 wit - -
loop-invgen/half_2_true-unreach-call.i true 690   690   280 wit - -
loop-invgen/heapsort_true-unreach-call.i true 880   880   400 wit - -
loop-invgen/id_build_true-unreach-call.i true 890   880   570 wit - -
loop-invgen/large_const_true-unreach-call.i true 2.6 2.6 75 wit - -
loop-invgen/nest-if3_true-unreach-call.i true 880   880   340 wit - -
loop-invgen/nested6_true-unreach-call.i true 880   880   320 wit - -
loop-invgen/nested9_true-unreach-call.i true 880   880   480 wit - -
loop-invgen/sendmail-close-angle_true-unreach-call.i true 880   880   390 wit - -
loop-invgen/seq_true-unreach-call.i true 880   880   320 wit - -
loop-invgen/string_concat-noarr_true-unreach-call.i true 880   880   680 wit - -
loop-invgen/up_true-unreach-call.i true 880   880   530 wit - -
loop-lit/afnp2014_true-unreach-call.c.i true 880   880   810 wit - -
loop-lit/bhmr2007_true-unreach-call.c.i true 880   880   120 wit - -
loop-lit/cggmp2005_true-unreach-call.c.i true 2.9 2.9 73 wit - -
loop-lit/cggmp2005_variant_true-unreach-call.c.i true 430   430   630 wit - -
loop-lit/cggmp2005b_true-unreach-call.c.i true 92   89   1800 wit - -
loop-lit/css2003_true-unreach-call.c.i true 710   700   510 wit - -
loop-lit/ddlm2013_true-unreach-call.c.i true 880   880   300 wit - -
loop-lit/gj2007_true-unreach-call.c.i true 310   310   260 wit - -
loop-lit/gj2007b_true-unreach-call.c.i true 880   880   330 wit - -
loop-lit/gr2006_true-unreach-call.c.i true 630   630   430 wit - -
loop-lit/gsv2008_true-unreach-call.c.i true 880   880   380 wit - -
loop-lit/hhk2008_true-unreach-call.c.i true 150   150   340 wit - -
loop-lit/jm2006_true-unreach-call.c.i true 880   880   1000 wit - -
loop-lit/jm2006_variant_true-unreach-call.c.i true 370   360   580 wit - -
loop-lit/mcmillan2006_true-unreach-call.c.i true 880   880   340 wit - -
loop-new/count_by_1_true-unreach-call.i true 2.6 2.6 64 wit - -
loop-new/count_by_1_variant_true-unreach-call.i true 58   57   180 wit - -
loop-new/count_by_2_true-unreach-call.i true 2.7 2.7 65 wit - -
loop-new/count_by_k_true-unreach-call.i true 480   470   280 wit - -
loop-new/count_by_nondet_true-unreach-call.i true 76   76   170 wit - -
loop-new/gauss_sum_true-unreach-call.i true 880   880   320 wit - -
loop-new/half_true-unreach-call.i true 880   880   250 wit - -
loop-new/nested_true-unreach-call.i true 880   880   570 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 51000 51000 140000 141 930   730   18000   141 940   630   31000  
    correct results 118 41000 40000 35000 23 760   600   14000   29 620   410   15000  
        correct true 88 40000 40000 32000 9 0   0   0   0 0   0   0  
        correct false 30 470 470 2400 14 760   600   14000   29 620   410   15000  
    incorrect results 3 2600 2600 4800 0 0   0   0   0 0   0   0  
        incorrect true 3 2600 2600 4800 0 0   0   0   0 0   0   0  
        incorrect false 0
score (141 tasks, max score: 234) 110
Run set sv-comp16.Loops