Tool SeaHorn-F16 0.1.0
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-11 21:35:00 [[ 2016-01-15 18:20:27 CET ]] [[ 2016-01-15 22:30:28 CET ]]
Run set sv-comp16.Loops
Options --cex=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/seahorn.2016-01-11_2135.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/seahorn.2016-01-11_2135.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) .21 .13 37 wit false(reach) 5.0 2.9 240 true 12   6.9 340
loops/bubble_sort_false-unreach-call.i error (245) .53 .33 56 wit - -
loops/count_up_down_false-unreach-call_true-termination.i false(reach) .27 .16 37 wit false(reach) 5.2 3.0 240 true 11   6.5 310
loops/eureka_01_false-unreach-call.i witness timeout .67 .36 63 wit timeout 90   72   1300 true 12   7.6 340
loops/for_bounded_loop1_false-unreach-call_true-termination.i false(reach) .29 .17 40 wit false(reach) 7.1 4.0 340 true 12   6.6 330
loops/insertion_sort_false-unreach-call.i witness timeout .52 .28 49 wit timeout 90   75   3500 true 12   7.9 330
loops/invert_string_false-unreach-call.i witness timeout .32 .19 43 wit timeout 90   72   2400 true 11   7.4 340
loops/linear_search_false-unreach-call.i false(reach) .30 .18 40 wit false(reach) 16   8.8 490 true 11   6.7 320
loops/ludcmp_false-unreach-call.i witness unconfirmed .30 .18 33 wit true 30   18   1300 error 50   39   6900
loops/matrix_false-unreach-call_true-termination.i witness timeout .47 .26 48 wit timeout 90   77   1300 true 12   7.9 320
loops/n.c24_false-unreach-call.i timeout 900    450    680 wit - -
loops/nec11_false-unreach-call.i witness unconfirmed .27 .18 34 wit true 6.4 3.7 260 true 10   5.8 320
loops/nec20_false-unreach-call.i false(reach) .28 .18 37 wit false(reach) 5.6 3.2 260 true 11   6.9 330
loops/s3_false-unreach-call.i false(reach) 3.1  1.6  75 wit false(reach) 27   15   650 true 15   9.0 320
loops/string_false-unreach-call.i false(reach) .33 .18 47 wit false(reach) 76   57   3500 true 10   6.2 340
loops/sum01_bug02_false-unreach-call_true-termination.i false(reach) .49 .29 42 wit false(reach) 19   10   710 true 10   6.1 330
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i false(reach) .37 .21 41 wit false(reach) 21   11   680 true 11   6.9 330
loops/sum01_false-unreach-call_true-termination.i false(reach) .51 .29 42 wit false(reach) 27   15   800 true 12   7.1 350
loops/sum03_false-unreach-call_true-termination.i false(reach) .49 .28 42 wit false(reach) 7.9 4.4 330 true 12   9.3 340
loops/sum04_false-unreach-call_true-termination.i witness unconfirmed .26 .17 34 wit true 8.4 4.8 280 true 11   6.2 320
loops/sum_array_false-unreach-call.i witness timeout .45 .25 51 wit timeout 90   71   2400 true 13   7.3 360
loops/terminator_01_false-unreach-call_false-termination.i witness unconfirmed .16 .10 34 wit true 5.6 3.3 230 true 10   6.1 330
loops/terminator_02_false-unreach-call_true-termination.i false(reach) .22 .13 39 wit false(reach) 5.4 3.1 240 true 9.7 5.4 330
loops/terminator_03_false-unreach-call_true-termination.i false(reach) .30 .19 39 wit false(reach) 5.3 3.2 230 true 12   7.7 340
loops/trex01_false-unreach-call_true-termination.i witness timeout .22 .13 28 wit timeout 90   76   1800 true 11   7.5 310
loops/trex02_false-unreach-call_true-termination.i false(reach) .29 .18 39 wit false(reach) 5.0 3.0 230 true 11   6.3 330
loops/trex03_false-unreach-call_true-termination.i false(reach) .32 .20 39 wit false(reach) 7.8 4.4 270 true 12   8.3 340
loops/verisec_NetBSD-libc__loop_false-unreach-call.i false(reach) .28 .17 39 wit false(reach) 5.8 3.3 320 true 11   7.5 320
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.i false(reach) .54 .30 52 wit false(reach) 7.3 4.2 340 true 12   6.7 330
loops/vogal_false-unreach-call.i witness timeout 1.1  .57 53 wit timeout 90   76   1200 true 12   7.3 330
loops/while_infinite_loop_4_false-unreach-call_true-termination.i witness unconfirmed .28 .18 35 wit true 5.4 3.1 230 true 10   7.7 330
loops/array_true-unreach-call.i true .20 .13 30 wit - -
loops/bubble_sort_true-unreach-call.i true .24 .14 25 wit - -
loops/count_up_down_true-unreach-call_true-termination.i true .17 .10 30 wit - -
loops/eureka_01_true-unreach-call.i timeout 900    450    220 wit - -
loops/eureka_05_true-unreach-call.i killed by signal 9 240    120    15000 wit - -
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true .24 .16 27 wit - -
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true .19 .13 28 wit - -
loops/insertion_sort_true-unreach-call.i false(reach) .51 .26 49 wit - -
loops/invert_string_true-unreach-call.i true 5.5  2.8  43 wit - -
loops/linear_sea.ch_true-unreach-call.i false(reach) .29 .18 40 wit - -
loops/lu.cmp_true-unreach-call.i true .30 .18 39 wit - -
loops/matrix_true-unreach-call_true-termination.i true .26 .17 30 wit - -
loops/n.c11_true-unreach-call.i true .37 .23 37 wit - -
loops/n.c40_true-unreach-call.i true .27 .17 34 wit - -
loops/nec40_true-unreach-call.i true .23 .14 34 wit - -
loops/string_true-unreach-call.i true .33 .18 38 wit - -
loops/sum01_true-unreach-call_true-termination.i true .36 .22 34 wit - -
loops/sum03_true-unreach-call_false-termination.i true .25 .15 33 wit - -
loops/sum04_true-unreach-call_true-termination.i true .22 .14 30 wit - -
loops/sum_array_true-unreach-call.i false(reach) .38 .21 51 wit - -
loops/terminator_02_true-unreach-call_true-termination.i true .32 .19 36 wit - -
loops/terminator_03_true-unreach-call_true-termination.i true .26 .16 36 wit - -
loops/trex01_true-unreach-call.i true .28 .17 38 wit - -
loops/trex02_true-unreach-call_true-termination.i true .30 .18 36 wit - -
loops/trex03_true-unreach-call.i true .40 .24 37 wit - -
loops/trex04_true-unreach-call_false-termination.i true .35 .21 36 wit - -
loops/veris.c_NetBSD-libc__loop_true-unreach-call.i false(reach) .29 .18 39 wit - -
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.i true .26 .16 25 wit - -
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i true .19 .12 30 wit - -
loops/vogal_true-unreach-call.i timeout 900    450    250 wit - -
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true .18 .12 24 wit - -
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true .16 .10 28 wit - -
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true .18 .12 29 wit - -
loop-acceleration/array_false-unreach-call1.i timeout 900    450    11000 wit - -
loop-acceleration/array_false-unreach-call2.i witness timeout .26 .17 35 wit timeout 91   70   1400 true 11   6.4 310
loop-acceleration/array_false-unreach-call3.i witness timeout 220    110    630 wit timeout 91   67   810 error 14   7.7 340
loop-acceleration/const_false-unreach-call1.i false(reach) 660    330    200 wit false(reach) 82   52   1300 error 13   7.0 330
loop-acceleration/diamond_false-unreach-call1.i false(reach) 620    310    290 wit false(reach) 39   25   840 true 13   7.0 340
loop-acceleration/functions_false-unreach-call1.i timeout 900    450    250 wit - -
loop-acceleration/multivar_false-unreach-call1.i witness unconfirmed .25 .17 34 wit true 6.0 3.4 240 true 11   7.2 310
loop-acceleration/nested_false-unreach-call1.i witness timeout .20 .13 34 wit timeout 90   75   3700 true 11   7.7 320
loop-acceleration/phases_false-unreach-call1.i timeout 900    450    260 wit - -
loop-acceleration/phases_false-unreach-call2.i witness unconfirmed .30 .18 36 wit true 8.9 4.8 290 true 12   6.6 350
loop-acceleration/simple_false-unreach-call1.i witness timeout .20 .13 35 wit timeout 91   83   760 true 11   6.1 330
loop-acceleration/simple_false-unreach-call2.i witness unconfirmed .27 .17 27 wit true 5.3 3.2 230 true 9.7 5.5 310
loop-acceleration/simple_false-unreach-call3.i witness timeout .27 .18 35 wit timeout 90   77   850 true 11   5.9 310
loop-acceleration/simple_false-unreach-call4.i witness timeout .19 .12 35 wit timeout 91   82   750 true 11   6.4 330
loop-acceleration/underapprox_false-unreach-call1.i witness unconfirmed .21 .14 34 wit true 7.1 4.0 270 true 11   7.5 330
loop-acceleration/underapprox_false-unreach-call2.i witness unconfirmed .19 .13 34 wit true 7.8 4.4 270 true 10   6.4 320
loop-acceleration/array_true-unreach-call1.i true .30 .17 37 wit - -
loop-acceleration/array_true-unreach-call2.i true .20 .13 30 wit - -
loop-acceleration/array_true-unreach-call3.i true .54 .30 38 wit - -
loop-acceleration/array_true-unreach-call4.i timeout 900    450    280 wit - -
loop-acceleration/const_true-unreach-call1.i true .26 .16 37 wit - -
loop-acceleration/diamond_true-unreach-call1.i timeout 900    450    220 wit - -
loop-acceleration/diamond_true-unreach-call2.i true 5.8  2.9  58 wit - -
loop-acceleration/functions_true-unreach-call1.i true .27 .16 36 wit - -
loop-acceleration/multivar_true-unreach-call1.i true .21 .13 25 wit - -
loop-acceleration/nested_true-unreach-call1.i true .23 .15 31 wit - -
loop-acceleration/overflow_true-unreach-call1.i true .19 .12 30 wit - -
loop-acceleration/phases_true-unreach-call1.i timeout 900    450    260 wit - -
loop-acceleration/phases_true-unreach-call2.i false(reach) .28 .17 40 wit - -
loop-acceleration/simple_true-unreach-call1.i true .19 .12 30 wit - -
loop-acceleration/simple_true-unreach-call2.i true .18 .12 30 wit - -
loop-acceleration/simple_true-unreach-call3.i true .23 .14 25 wit - -
loop-acceleration/simple_true-unreach-call4.i true .22 .15 30 wit - -
loop-acceleration/underapprox_true-unreach-call1.i true .24 .16 30 wit - -
loop-acceleration/underapprox_true-unreach-call2.i true .24 .15 30 wit - -
loop-invgen/id_trans_false-unreach-call.i false(reach) .35 .21 40 wit false(reach) 5.7 3.3 240 true 12   8.1 330
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call.i true .46 .27 40 wit - -
loop-invgen/NetBSD_loop_true-unreach-call.i true .27 .16 37 wit - -
loop-invgen/SpamAssassin-loop_true-unreach-call.i true .48 .27 51 wit - -
loop-invgen/apache-escape-absolute_true-unreach-call.i true .80 .44 58 wit - -
loop-invgen/apache-get-tag_true-unreach-call.i true .42 .23 47 wit - -
loop-invgen/down_true-unreach-call.i true .32 .20 37 wit - -
loop-invgen/fragtest_simple_true-unreach-call.i true .34 .19 43 wit - -
loop-invgen/half_2_true-unreach-call.i false(reach) .32 .20 40 wit - -
loop-invgen/heapsort_true-unreach-call.i true 1.3  .67 72 wit - -
loop-invgen/id_build_true-unreach-call.i true .28 .17 38 wit - -
loop-invgen/large_const_true-unreach-call.i true 160    82    140 wit - -
loop-invgen/nest-if3_true-unreach-call.i true .39 .23 41 wit - -
loop-invgen/nested6_true-unreach-call.i true .53 .28 49 wit - -
loop-invgen/nested9_true-unreach-call.i true 900    450    910 wit - -
loop-invgen/sendmail-close-angle_true-unreach-call.i true .32 .17 39 wit - -
loop-invgen/seq_true-unreach-call.i true .31 .18 37 wit - -
loop-invgen/string_concat-noarr_true-unreach-call.i true .36 .21 40 wit - -
loop-invgen/up_true-unreach-call.i true .31 .19 38 wit - -
loop-lit/afnp2014_true-unreach-call.c.i true .29 .17 37 wit - -
loop-lit/bhmr2007_true-unreach-call.c.i true .35 .20 39 wit - -
loop-lit/cggmp2005_true-unreach-call.c.i true .42 .24 38 wit - -
loop-lit/cggmp2005_variant_true-unreach-call.c.i true .32 .19 34 wit - -
loop-lit/cggmp2005b_true-unreach-call.c.i true .33 .20 35 wit - -
loop-lit/css2003_true-unreach-call.c.i true .33 .20 37 wit - -
loop-lit/ddlm2013_true-unreach-call.c.i true .39 .21 39 wit - -
loop-lit/gj2007_true-unreach-call.c.i true .20 .13 30 wit - -
loop-lit/gj2007b_true-unreach-call.c.i true .32 .18 38 wit - -
loop-lit/gr2006_true-unreach-call.c.i true 670    340    430 wit - -
loop-lit/gsv2008_true-unreach-call.c.i true .28 .16 37 wit - -
loop-lit/hhk2008_true-unreach-call.c.i true .31 .19 35 wit - -
loop-lit/jm2006_true-unreach-call.c.i true .27 .18 35 wit - -
loop-lit/jm2006_variant_true-unreach-call.c.i true .32 .20 35 wit - -
loop-lit/mcmillan2006_true-unreach-call.c.i false(reach) .29 .18 40 wit - -
loop-new/count_by_1_true-unreach-call.i true .20 .13 30 wit - -
loop-new/count_by_1_variant_true-unreach-call.i true .39 .23 37 wit - -
loop-new/count_by_2_true-unreach-call.i true .18 .12 30 wit - -
loop-new/count_by_k_true-unreach-call.i timeout 900    450    440 wit - -
loop-new/count_by_nondet_true-unreach-call.i true .31 .18 37 wit - -
loop-new/gauss_sum_true-unreach-call.i false(reach) .28 .18 37 wit - -
loop-new/half_true-unreach-call.i true .73 .39 40 wit - -
loop-new/nested_true-unreach-call.i true .56 .31 40 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 13000   6300   36000 141 1600   1300   38000   141 520   330   21000  
    correct results 98 3100   1500   5400 20 380   240   12000   19 230   140   6600  
        correct true 78 1800   890   4200 0 0   0   0   19 0   0   0  
        correct false 20 1300   640   1300 20 380   240   12000   0 230   140   6600  
    incorrect results 8 2.6 1.5 340 0 0   0   0   0 0   0   0  
        incorrect true 0
        incorrect false 8 2.6 1.5 340 0 0   0   0   0 0   0   0  
score (141 tasks, max score: 234) 48
Run set sv-comp16.Loops