Tool CBMC
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 00:42:25 CET [[ 2016-01-15 08:22:02 CET ]] [[ 2016-01-15 21:54:19 CET ]]
Run set sv-comp16.Recursive
Options --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cbmc.2016-01-03_0042.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)
recursive/Ackermann02_false-unreach-call_false-termination.c false(reach) 2.1  2.1  78 wit false(reach) 11   6.0 440 false(reach) 13 7.3 340
recursive/Addition02_false-unreach-call_false-termination.c false(reach) .11 .12 25 wit false(reach) 7.3 4.1 370 false(reach) 13 8.0 330
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call.c false(reach) .16 .18 24 wit false(reach) 6.5 3.6 360 false(reach) 14 8.1 360
recursive/EvenOdd03_false-unreach-call_false-termination.c false(reach) .18 .19 25 wit false(reach) 8.0 4.4 380 true 14 7.6 340
recursive/Fibonacci04_false-unreach-call_true-termination.c false(reach) .74 .76 34 wit timeout 90   60   1400 false(reach) 40 22   860
recursive/Fibonacci05_false-unreach-call_true-termination.c true 850    850    270 wit - -
recursive/McCarthy91_false-unreach-call_false-termination.c false(reach) .14 .15 24 wit false(reach) 4.9 3.1 220 false(reach) 11 6.2 330
recursive/Ackermann01_true-unreach-call.c true 850    850    520 wit - -
recursive/Ackermann03_true-unreach-call.c true 850    850    510 wit - -
recursive/Ackermann04_true-unreach-call.c true 850    850    520 wit - -
recursive/Addition01_true-unreach-call_true-termination.c true 850    850    12000 wit - -
recursive/Addition03_true-unreach-call.c true 850    850    13000 wit - -
recursive/EvenOdd01_true-unreach-call_true-termination.c true 66    66    420 wit - -
recursive/Fibonacci01_true-unreach-call.c true 850    850    270 wit - -
recursive/Fibonacci02_true-unreach-call_true-termination.c true 1.2  1.2  24 wit - -
recursive/Fibonacci03_true-unreach-call_true-termination.c true 850    850    270 wit - -
recursive/McCarthy91_true-unreach-call.c true 850    850    1200 wit - -
recursive/MultCommutative_true-unreach-call_true-termination.c true 850    850    400 wit - -
recursive/Primes_true-unreach-call.c true 850    850    290 wit - -
recursive/gcd01_true-unreach-call_true-termination.c true 850    850    2900 wit - -
recursive/gcd02_true-unreach-call.c true 850    850    190 wit - -
recursive/recHanoi01_true-unreach-call_true-termination.c true 850    850    660 wit - -
recursive/recHanoi02_true-unreach-call_true-termination.c true 12    12    78 wit - -
recursive/recHanoi03_true-unreach-call_true-termination.c true 5.0  5.0  88 wit - -
recursive-simple/afterrec_2calls_false-unreach-call.c false(reach) .13 .14 24 wit false(reach) 6.6 3.9 350 false(reach) 12 7.5 330
recursive-simple/afterrec_false-unreach-call.c false(reach) .15 .16 24 wit false(reach) 5.8 3.3 340 false(reach) 13 6.9 360
recursive-simple/fibo_10_false-unreach-call.c false(reach) .31 .33 27 wit timeout 91   70   2000 false(reach) 77 47   860
recursive-simple/fibo_15_false-unreach-call.c witness invalid (exception) 3.3  3.4  90 wit exception 27   14   1100 timeout 91 58   2100
recursive-simple/fibo_20_false-unreach-call.c witness timeout 310    310    970 wit timeout 92   47   4400 timeout 91 58   2100
recursive-simple/fibo_25_false-unreach-call.c true 850    850    480 wit - -
recursive-simple/fibo_2calls_10_false-unreach-call.c witness unconfirmed .31 .33 27 wit true 7.0 3.9 290 timeout 91 55   1400
recursive-simple/fibo_2calls_15_false-unreach-call.c witness unconfirmed 3.3  3.3  94 wit true 14   7.6 810 timeout 91 59   2000
recursive-simple/fibo_2calls_20_false-unreach-call.c witness unconfirmed 250    250    1000 wit true 65   33   2900 timeout 91 58   1700
recursive-simple/fibo_2calls_25_false-unreach-call.c true 850    850    490 wit - -
recursive-simple/fibo_2calls_2_false-unreach-call.c false(reach) .13 .14 24 wit true 4.7 2.7 210 false(reach) 14 7.8 330
recursive-simple/fibo_2calls_4_false-unreach-call.c false(reach) .12 .13 24 wit true 4.4 2.5 220 false(reach) 38 22   530
recursive-simple/fibo_2calls_5_false-unreach-call.c false(reach) .14 .15 24 wit true 5.1 3.0 230 false(reach) 28 18   490
recursive-simple/fibo_2calls_6_false-unreach-call.c false(reach) .12 .13 24 wit true 5.2 2.9 220 false(reach) 38 22   680
recursive-simple/fibo_2calls_8_false-unreach-call.c witness unconfirmed .26 .28 25 wit true 5.6 3.2 240 timeout 92 55   1300
recursive-simple/fibo_5_false-unreach-call.c false(reach) .28 .30 24 wit true 19   9.7 530 false(reach) 20 12   500
recursive-simple/fibo_7_false-unreach-call.c false(reach) .24 .25 24 wit true 70   46   2000 false(reach) 34 20   590
recursive-simple/id2_b3_o2_false-unreach-call.c false(reach) .13 .14 24 wit false(reach) 7.9 4.4 360 false(reach) 13 7.7 330
recursive-simple/id2_i5_o5_false-unreach-call.c false(reach) .12 .13 24 wit true 4.0 2.3 220 false(reach) 15 8.4 350
recursive-simple/id_b3_o2_false-unreach-call.c false(reach) .12 .13 24 wit false(reach) 7.2 4.0 360 false(reach) 14 8.3 340
recursive-simple/id_i10_o10_false-unreach-call.c false(reach) .38 .40 24 wit false(reach) 8.8 4.9 410 true 12 7.6 330
recursive-simple/id_i15_o15_false-unreach-call.c false(reach) .38 .40 24 wit false(reach) 10   5.7 440 true 15 9.0 360
recursive-simple/id_i20_o20_false-unreach-call.c false(reach) .53 .56 24 wit false(reach) 13   6.8 510 true 13 7.7 370
recursive-simple/id_i25_o25_false-unreach-call.c false(reach) .69 .72 24 wit false(reach) 18   9.4 540 true 14 8.4 370
recursive-simple/id_i5_o5_false-unreach-call.c false(reach) .24 .26 24 wit false(reach) 7.0 3.9 360 false(reach) 16 9.0 340
recursive-simple/id_o1000_false-unreach-call.c true 3.6  3.7  70 wit - -
recursive-simple/id_o100_false-unreach-call.c false(reach) 1.9  2.0  39 wit false(reach) 90   62   2000 true 20 11   580
recursive-simple/id_o10_false-unreach-call.c false(reach) .40 .43 24 wit false(reach) 10   5.5 440 true 12 6.3 330
recursive-simple/id_o200_false-unreach-call.c witness timeout 1.8  1.8  37 wit timeout 90   73   1400 true 26 14   690
recursive-simple/id_o20_false-unreach-call.c false(reach) .67 .70 25 wit false(reach) 19   10   550 true 14 7.6 360
recursive-simple/id_o3_false-unreach-call.c false(reach) .24 .25 24 wit false(reach) 7.5 4.2 350 false(reach) 11 5.9 350
recursive-simple/sum_10x0_false-unreach-call.c false(reach) .36 .38 24 wit false(reach) 9.0 4.9 400 false(reach) 25 17   490
recursive-simple/sum_15x0_false-unreach-call.c false(reach) .52 .55 24 wit false(reach) 11   5.9 440 false(reach) 24 16   500
recursive-simple/sum_20x0_false-unreach-call.c false(reach) .62 .65 24 wit false(reach) 12   6.3 510 false(reach) 34 22   680
recursive-simple/sum_25x0_false-unreach-call.c false(reach) .75 .79 24 wit false(reach) 14   7.5 590 false(reach) 44 30   750
recursive-simple/sum_2x3_false-unreach-call.c false(reach) .12 .13 24 wit false(reach) 6.5 3.7 360 false(reach) 14 7.9 340
recursive-simple/sum_non_eq_false-unreach-call.c false(reach) .12 .13 24 wit false(reach) 6.4 3.6 360 false(reach) 11 6.0 330
recursive-simple/sum_non_false-unreach-call.c false(reach) .12 .13 24 wit false(reach) 6.4 3.6 350 false(reach) 13 6.8 350
recursive-simple/afterrec_2calls_true-unreach-call.c true .97 1.0  24 wit - -
recursive-simple/afterrec_true-unreach-call.c true .84 .88 24 wit - -
recursive-simple/fibo_10_true-unreach-call.c true 1.2  1.3  24 wit - -
recursive-simple/fibo_15_true-unreach-call.c true 13    13    32 wit - -
recursive-simple/fibo_20_true-unreach-call.c true 850    850    320 wit - -
recursive-simple/fibo_25_true-unreach-call.c true 850    850    460 wit - -
recursive-simple/fibo_2calls_10_true-unreach-call.c true 1.4  1.4  24 wit - -
recursive-simple/fibo_2calls_15_true-unreach-call.c true 15    15    32 wit - -
recursive-simple/fibo_2calls_20_true-unreach-call.c true 850    850    330 wit - -
recursive-simple/fibo_2calls_25_true-unreach-call.c true 850    850    470 wit - -
recursive-simple/fibo_2calls_2_true-unreach-call.c true .90 .95 24 wit - -
recursive-simple/fibo_2calls_4_true-unreach-call.c true .85 .90 24 wit - -
recursive-simple/fibo_2calls_5_true-unreach-call.c true .93 .97 24 wit - -
recursive-simple/fibo_2calls_6_true-unreach-call.c true .69 .71 24 wit - -
recursive-simple/fibo_2calls_8_true-unreach-call.c true 1.1  1.1  24 wit - -
recursive-simple/fibo_5_true-unreach-call.c true .69 .73 24 wit - -
recursive-simple/fibo_7_true-unreach-call.c true 1.0  1.0  24 wit - -
recursive-simple/id2_b2_o3_true-unreach-call.c true 19    19    320 wit - -
recursive-simple/id2_b3_o5_true-unreach-call.c true 19    19    320 wit - -
recursive-simple/id2_b5_o10_true-unreach-call.c true 19    19    320 wit - -
recursive-simple/id2_i5_o5_true-unreach-call.c true .87 .93 24 wit - -
recursive-simple/id_b2_o3_true-unreach-call.c true 5.5  5.6  130 wit - -
recursive-simple/id_b3_o5_true-unreach-call.c true 5.6  5.6  120 wit - -
recursive-simple/id_b5_o10_true-unreach-call.c true 5.5  5.6  120 wit - -
recursive-simple/id_i10_o10_true-unreach-call.c true 1.0  1.1  24 wit - -
recursive-simple/id_i15_o15_true-unreach-call.c true .89 .94 24 wit - -
recursive-simple/id_i20_o20_true-unreach-call.c true .88 .93 24 wit - -
recursive-simple/id_i25_o25_true-unreach-call.c true .89 .93 24 wit - -
recursive-simple/id_i5_o5_true-unreach-call.c true .96 1.0  24 wit - -
recursive-simple/sum_10x0_true-unreach-call.c true .85 .90 24 wit - -
recursive-simple/sum_15x0_true-unreach-call.c true .93 .97 24 wit - -
recursive-simple/sum_20x0_true-unreach-call.c true .88 .92 24 wit - -
recursive-simple/sum_25x0_true-unreach-call.c true .96 1.0  24 wit - -
recursive-simple/sum_2x3_true-unreach-call.c true .98 1.0  24 wit - -
recursive-simple/sum_non_eq_true-unreach-call.c true 850    850    320 wit - -
recursive-simple/sum_non_true-unreach-call.c true 850    850    320 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 98 19000 20000 42000 98 910   570   30000   98 1300   780   26000  
    correct results 87 16000 16000 38000 32 610   380   19000   34 710   420   15000  
        correct true 53 16000 16000 37000 7 0   0   0   8 0   0   0  
        correct false 34 13 14 900 25 610   380   19000   26 710   420   15000  
    incorrect results 4 2600 2600 1300 0 0   0   0   0 0   0   0  
        incorrect true 4 2600 2600 1300 0 0   0   0   0 0   0   0  
        incorrect false 0
score (98 tasks, max score: 151) 12
Run set sv-comp16.Recursive