Tool BLAST 2.7.3
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-03 17:36:26 CET [[ 2016-01-15 08:15:11 CET ]] [[ 2016-01-15 21:49:51 CET ]]
Run set sv-comp16.Loops
Options -alias empty -enable-recursion -noprofile -cref -sv-comp -lattice -include-lattice symb -nosserr -svcomp-witness error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/blast.2016-01-03_1736.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/blast.2016-01-03_1736.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) .54  .73  24   wit true 4.4 2.5 230 false(reach) 13   7.5 340
loops/bubble_sort_false-unreach-call.i exception (gremlins) .034 .038 24   wit - -
loops/count_up_down_false-unreach-call_true-termination.i false(reach) .072 .075 18   wit false(reach) 5.2 3.0 240 false(reach) 11   6.2 360
loops/eureka_01_false-unreach-call.i witness timeout 5.3   6.4   39   wit timeout 91   78   1500 timeout 91   66   1300
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(reach) .96  1.2   28   wit timeout 90   74   3900 false(reach) 13   7.9 340
loops/insertion_sort_false-unreach-call.i witness timeout 4.0   5.6   26   wit timeout 90   74   1400 timeout 91   58   1500
loops/invert_string_false-unreach-call.i false(reach) 1.3   1.6   28   wit timeout 90   76   1500 false(reach) 30   17   520
loops/linear_search_false-unreach-call.i witness unconfirmed .13  .14  20   wit true 8.7 4.8 310 error 30   22   480
loops/ludcmp_false-unreach-call.i witness unconfirmed 1.9   2.5   33   wit true 9.4 5.4 360 timeout 46   35   7000
loops/matrix_false-unreach-call_true-termination.i exception (gremlins) .031 .035 9.3 wit - -
loops/n.c24_false-unreach-call.i timeout 670     930     230   wit - -
loops/nec11_false-unreach-call.i false(reach) .071 .076 18   wit true 5.4 3.0 240 false(reach) 13   7.1 360
loops/nec20_false-unreach-call.i false(reach) .29  .34  24   wit timeout 91   68   1500 false(reach) 11   7.0 340
loops/s3_false-unreach-call.i witness unconfirmed 19     25     48   wit true 11   6.3 430 timeout 91   82   490
loops/string_false-unreach-call.i false(reach) 1.4   1.8   28   wit true 15   8.5 520 false(reach) 37   21   390
loops/sum01_bug02_false-unreach-call_true-termination.i false(reach) 26     32     46   wit false(reach) 6.5 3.7 330 false(reach) 16   9.5 340
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(reach) 12     15     34   wit false(reach) 5.0 2.9 250 false(reach) 13   7.5 340
loops/sum01_false-unreach-call_true-termination.i false(reach) 44     52     46   wit false(reach) 6.8 3.9 340 false(reach) 15   8.0 340
loops/sum03_false-unreach-call_true-termination.i false(reach) 4.6   6.4   37   wit false(reach) 7.2 4.0 330 false(reach) 29   15   540
loops/sum04_false-unreach-call_true-termination.i false(reach) 1.1   1.5   27   wit false(reach) 5.0 3.0 230 false(reach) 14   7.6 370
loops/sum_array_false-unreach-call.i false(reach) .72  .90  29   wit timeout 90   76   1400 false(reach) 14   8.6 340
loops/terminator_01_false-unreach-call_false-termination.i false(reach) .12  .13  15   wit false(reach) 4.6 2.7 230 false(reach) 12   7.2 350
loops/terminator_02_false-unreach-call_true-termination.i false(reach) .093 .098 15   wit false(reach) 4.8 3.0 230 false(reach) 12   6.3 330
loops/terminator_03_false-unreach-call_true-termination.i false(reach) .22  .26  21   wit false(reach) 4.6 2.7 230 false(reach) 12   7.0 330
loops/trex01_false-unreach-call_true-termination.i false(reach) .12  .12  20   wit true 23   13   650 false(reach) 13   7.4 360
loops/trex02_false-unreach-call_true-termination.i false(reach) .088 .093 19   wit true 5.4 3.1 240 false(reach) 11   7.3 330
loops/trex03_false-unreach-call_true-termination.i false(reach) .075 .078 18   wit false(reach) 4.9 2.9 240 false(reach) 13   8.4 350
loops/verisec_NetBSD-libc__loop_false-unreach-call.i false(reach) .33  .46  28   wit false(reach) 6.1 3.6 330 false(reach) 12   7.0 330
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.i false(reach) 33     47     42   wit false(reach) 18   9.9 560 false(reach) 28   16   500
loops/vogal_false-unreach-call.i timeout 680     930     200   wit - -
loops/while_infinite_loop_4_false-unreach-call_true-termination.i false(reach) .11  .12  17   wit true 4.4 2.6 210 false(reach) 11   6.7 330
loops/array_true-unreach-call.i true .61  .91  26   wit - -
loops/bubble_sort_true-unreach-call.i true .020 .025 14   wit - -
loops/count_up_down_true-unreach-call_true-termination.i false(reach) .084 .089 18   wit - -
loops/eureka_01_true-unreach-call.i timeout 880     930     540   wit - -
loops/eureka_05_true-unreach-call.i false(reach) 7.8   10     38   wit - -
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true .023 .025 13   wit - -
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true .041 .047 16   wit - -
loops/insertion_sort_true-unreach-call.i false(reach) 3.7   5.1   27   wit - -
loops/invert_string_true-unreach-call.i false(reach) 2.4   2.9   37   wit - -
loops/linear_sea.ch_true-unreach-call.i false(reach) .058 .063 19   wit - -
loops/lu.cmp_true-unreach-call.i true 67     76     70   wit - -
loops/matrix_true-unreach-call_true-termination.i exception (gremlins) .015 .020 7.6 wit - -
loops/n.c11_true-unreach-call.i true .70  .91  28   wit - -
loops/n.c40_true-unreach-call.i false(reach) .25  .31  25   wit - -
loops/nec40_true-unreach-call.i false(reach) .28  .35  24   wit - -
loops/string_true-unreach-call.i true .70  .89  25   wit - -
loops/sum01_true-unreach-call_true-termination.i timeout 630     930     200   wit - -
loops/sum03_true-unreach-call_false-termination.i true .21  .27  24   wit - -
loops/sum04_true-unreach-call_true-termination.i true 1.0   1.3   28   wit - -
loops/sum_array_true-unreach-call.i false(reach) .73  .91  29   wit - -
loops/terminator_02_true-unreach-call_true-termination.i true 1.2   1.5   31   wit - -
loops/terminator_03_true-unreach-call_true-termination.i true .45  .56  29   wit - -
loops/trex01_true-unreach-call.i true 1.5   2.0   26   wit - -
loops/trex02_true-unreach-call_true-termination.i true .10  .12  21   wit - -
loops/trex03_true-unreach-call.i false(reach) .13  .13  21   wit - -
loops/trex04_true-unreach-call_false-termination.i true .56  .67  29   wit - -
loops/veris.c_NetBSD-libc__loop_true-unreach-call.i true .26  .32  20   wit - -
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.i true .033 .038 19   wit - -
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i true .26  .32  24   wit - -
loops/vogal_true-unreach-call.i timeout 690     930     360   wit - -
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true .027 .029 14   wit - -
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true .038 .041 15   wit - -
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true .039 .045 14   wit - -
loop-acceleration/array_false-unreach-call1.i timeout 710     930     230   wit - -
loop-acceleration/array_false-unreach-call2.i timeout 860     930     370   wit - -
loop-acceleration/array_false-unreach-call3.i timeout 780     930     330   wit - -
loop-acceleration/const_false-unreach-call1.i timeout 700     930     200   wit - -
loop-acceleration/diamond_false-unreach-call1.i witness timeout 60     82     47   wit timeout 91   81   1300 timeout 91   63   3600
loop-acceleration/functions_false-unreach-call1.i timeout 740     930     170   wit - -
loop-acceleration/multivar_false-unreach-call1.i false(reach) .099 .10  20   wit false(reach) 4.7 2.9 230 false(reach) 9.4 5.4 320
loop-acceleration/nested_false-unreach-call1.i timeout 640     930     240   wit - -
loop-acceleration/phases_false-unreach-call1.i exception (gremlins) .087 .10  19   wit - -
loop-acceleration/phases_false-unreach-call2.i false(reach) .087 .091 18   wit true 3.9 2.3 220 false(reach) 10   5.7 340
loop-acceleration/simple_false-unreach-call1.i timeout 870     930     160   wit - -
loop-acceleration/simple_false-unreach-call2.i false(reach) .089 .097 18   wit false(reach) 4.7 2.8 220 false(reach) 11   6.3 340
loop-acceleration/simple_false-unreach-call3.i false(reach) .068 .072 16   wit false(reach) 4.6 2.7 220 false(reach) 12   7.6 330
loop-acceleration/simple_false-unreach-call4.i exception (gremlins) 1.0   1.3   42   wit - -
loop-acceleration/underapprox_false-unreach-call1.i false(reach) 1.4   1.8   27   wit true 4.7 2.9 220 false(reach) 14   7.8 340
loop-acceleration/underapprox_false-unreach-call2.i false(reach) .75  .97  27   wit true 4.6 2.7 220 false(reach) 15   8.1 370
loop-acceleration/array_true-unreach-call1.i timeout 700     930     230   wit - -
loop-acceleration/array_true-unreach-call2.i timeout 860     930     370   wit - -
loop-acceleration/array_true-unreach-call3.i true .27  .32  24   wit - -
loop-acceleration/array_true-unreach-call4.i timeout 780     930     330   wit - -
loop-acceleration/const_true-unreach-call1.i true .18  .21  23   wit - -
loop-acceleration/diamond_true-unreach-call1.i false(reach) 56     77     48   wit - -
loop-acceleration/diamond_true-unreach-call2.i false(reach) 97     130     45   wit - -
loop-acceleration/functions_true-unreach-call1.i timeout 770     930     160   wit - -
loop-acceleration/multivar_true-unreach-call1.i true .15  .16  20   wit - -
loop-acceleration/nested_true-unreach-call1.i timeout 650     930     240   wit - -
loop-acceleration/overflow_true-unreach-call1.i true .16  .20  20   wit - -
loop-acceleration/phases_true-unreach-call1.i exception (gremlins) .15  .17  20   wit - -
loop-acceleration/phases_true-unreach-call2.i false(reach) .55  .70  23   wit - -
loop-acceleration/simple_true-unreach-call1.i timeout 870     930     160   wit - -
loop-acceleration/simple_true-unreach-call2.i exception (gremlins) .11  .12  20   wit - -
loop-acceleration/simple_true-unreach-call3.i false(reach) .10  .11  20   wit - -
loop-acceleration/simple_true-unreach-call4.i exception (gremlins) 1.7   2.2   48   wit - -
loop-acceleration/underapprox_true-unreach-call1.i true .58  .73  27   wit - -
loop-acceleration/underapprox_true-unreach-call2.i true .25  .33  20   wit - -
loop-invgen/id_trans_false-unreach-call.i exception (gremlins) .41  .51  28   wit - -
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call.i true 13     18     42   wit - -
loop-invgen/NetBSD_loop_true-unreach-call.i true .66  .86  26   wit - -
loop-invgen/SpamAssassin-loop_true-unreach-call.i true 260     360     130   wit - -
loop-invgen/apache-escape-absolute_true-unreach-call.i true 37     48     51   wit - -
loop-invgen/apache-get-tag_true-unreach-call.i true 7.0   9.2   38   wit - -
loop-invgen/down_true-unreach-call.i timeout 710     930     180   wit - -
loop-invgen/fragtest_simple_true-unreach-call.i timeout 740     930     170   wit - -
loop-invgen/half_2_true-unreach-call.i exception (gremlins) .11  .13  22   wit - -
loop-invgen/heapsort_true-unreach-call.i exception (gremlins) .18  .24  29   wit - -
loop-invgen/id_build_true-unreach-call.i true .56  .67  29   wit - -
loop-invgen/large_const_true-unreach-call.i exception (gremlins) 120     160     55   wit - -
loop-invgen/nest-if3_true-unreach-call.i false(reach) .53  .65  25   wit - -
loop-invgen/nested6_true-unreach-call.i true 200     240     53   wit - -
loop-invgen/nested9_true-unreach-call.i true .68  .91  26   wit - -
loop-invgen/sendmail-close-angle_true-unreach-call.i exception (gremlins) 11     15     44   wit - -
loop-invgen/seq_true-unreach-call.i timeout 740     930     160   wit - -
loop-invgen/string_concat-noarr_true-unreach-call.i timeout 810     930     190   wit - -
loop-invgen/up_true-unreach-call.i timeout 720     930     180   wit - -
loop-lit/afnp2014_true-unreach-call.c.i true 1.4   1.9   27   wit - -
loop-lit/bhmr2007_true-unreach-call.c.i false(reach) .074 .077 20   wit - -
loop-lit/cggmp2005_true-unreach-call.c.i true .45  .58  26   wit - -
loop-lit/cggmp2005_variant_true-unreach-call.c.i false(reach) .13  .14  19   wit - -
loop-lit/cggmp2005b_true-unreach-call.c.i true .84  1.1   25   wit - -
loop-lit/css2003_true-unreach-call.c.i false(reach) .13  .13  19   wit - -
loop-lit/ddlm2013_true-unreach-call.c.i false(reach) 34     38     35   wit - -
loop-lit/gj2007_true-unreach-call.c.i timeout 860     930     300   wit - -
loop-lit/gj2007b_true-unreach-call.c.i true 2.5   3.6   33   wit - -
loop-lit/gr2006_true-unreach-call.c.i timeout 770     930     170   wit - -
loop-lit/gsv2008_true-unreach-call.c.i true .40  .49  24   wit - -
loop-lit/hhk2008_true-unreach-call.c.i false(reach) .11  .11  21   wit - -
loop-lit/jm2006_true-unreach-call.c.i exception (gremlins) 2.6   3.4   46   wit - -
loop-lit/jm2006_variant_true-unreach-call.c.i true 34     39     44   wit - -
loop-lit/mcmillan2006_true-unreach-call.c.i false(reach) .70  .92  29   wit - -
loop-new/count_by_1_true-unreach-call.i true .26  .31  21   wit - -
loop-new/count_by_1_variant_true-unreach-call.i true .22  .27  25   wit - -
loop-new/count_by_2_true-unreach-call.i exception (gremlins) 400     450     160   wit - -
loop-new/count_by_k_true-unreach-call.i false(reach) .072 .079 17   wit - -
loop-new/count_by_nondet_true-unreach-call.i timeout 700     930     180   wit - -
loop-new/gauss_sum_true-unreach-call.i false(reach) .12  .13  19   wit - -
loop-new/half_true-unreach-call.i exception (gremlins) 2.9   4.0   28   wit - -
loop-new/nested_true-unreach-call.i false(reach) .12  .12  22   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 21000 26000 9600 141 830   640   21000   141 860   570   25000  
    correct results 70 770 980 1900 24 530   390   15000   28 420   240   10000  
        correct true 42 640 820 1200 9 0   0   0   0 0   0   0  
        correct false 28 130 170 710 15 530   390   15000   28 420   240   10000  
    incorrect results 23 200 270 600 0 0   0   0   0 0   0   0  
        incorrect true 0
        incorrect false 23 200 270 600 0 0   0   0   0 0   0   0  
score (141 tasks, max score: 234) -256
Run set sv-comp16.Loops