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.Recursive
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)
recursive/Ackermann02_false-unreach-call_false-termination.c witness unconfirmed 2.7 2.7 75 wit true 15   7.9 570 true 84 44   1200
recursive/Addition02_false-unreach-call_false-termination.c false(reach) 3.2 3.2 75 wit true 6.1 3.5 260 false(reach) 14 7.8 350
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call.c false(reach) 2.9 2.9 76 wit true 4.6 2.8 220 false(reach) 12 7.7 330
recursive/EvenOdd03_false-unreach-call_false-termination.c false(reach) 2.7 2.7 69 wit true 5.8 3.3 250 false(reach) 12 7.2 330
recursive/Fibonacci04_false-unreach-call_true-termination.c false(reach) 3.2 3.1 77 wit true 9.4 5.2 420 false(reach) 64 44   2000
recursive/Fibonacci05_false-unreach-call_true-termination.c witness unconfirmed 4.2 4.0 82 wit true 17   9.2 600 timeout 90 62   3300
recursive/McCarthy91_false-unreach-call_false-termination.c false(reach) 3.1 3.1 73 wit true 5.3 3.1 250 false(reach) 13 8.3 340
recursive/Ackermann01_true-unreach-call.c true 880   880   330 wit - -
recursive/Ackermann03_true-unreach-call.c true 3.0 3.0 71 wit - -
recursive/Ackermann04_true-unreach-call.c true 880   880   410 wit - -
recursive/Addition01_true-unreach-call_true-termination.c true 880   880   360 wit - -
recursive/Addition03_true-unreach-call.c true 890   880   360 wit - -
recursive/EvenOdd01_true-unreach-call_true-termination.c true 880   880   140 wit - -
recursive/Fibonacci01_true-unreach-call.c true 890   880   5800 wit - -
recursive/Fibonacci02_true-unreach-call_true-termination.c true 3.5 3.5 82 wit - -
recursive/Fibonacci03_true-unreach-call_true-termination.c timeout (true) 900   880   5800 wit - -
recursive/McCarthy91_true-unreach-call.c true 880   880   310 wit - -
recursive/MultCommutative_true-unreach-call_true-termination.c true 880   880   120 wit - -
recursive/Primes_true-unreach-call.c true 880   880   520 wit - -
recursive/gcd01_true-unreach-call_true-termination.c true 880   880   160 wit - -
recursive/gcd02_true-unreach-call.c true 880   880   89 wit - -
recursive/recHanoi01_true-unreach-call_true-termination.c true 890   880   5800 wit - -
recursive/recHanoi02_true-unreach-call_true-termination.c true 3.5 3.5 70 wit - -
recursive/recHanoi03_true-unreach-call_true-termination.c true 3.8 3.8 70 wit - -
recursive-simple/afterrec_2calls_false-unreach-call.c false(reach) 3.2 3.2 71 wit true 5.4 3.1 240 false(reach) 11 6.5 320
recursive-simple/afterrec_false-unreach-call.c false(reach) 3.1 3.1 75 wit true 5.2 3.0 240 false(reach) 13 9.5 330
recursive-simple/fibo_10_false-unreach-call.c witness unconfirmed 5.4 5.2 110 wit true 26   14   750 timeout 91 63   3600
recursive-simple/fibo_15_false-unreach-call.c witness unconfirmed 140   140   820 wit true 42   22   1400 timeout 92 53   3000
recursive-simple/fibo_20_false-unreach-call.c error (1) 900   880   2800 wit - -
recursive-simple/fibo_25_false-unreach-call.c error (1) 900   880   3000 wit - -
recursive-simple/fibo_2calls_10_false-unreach-call.c witness unconfirmed 5.7 5.4 110 wit true 29   15   790 timeout 92 50   2500
recursive-simple/fibo_2calls_15_false-unreach-call.c witness unconfirmed 170   160   730 wit true 44   24   1500 timeout 92 49   2800
recursive-simple/fibo_2calls_20_false-unreach-call.c timeout 900   930   2800 wit - -
recursive-simple/fibo_2calls_25_false-unreach-call.c timeout 900   930   3000 wit - -
recursive-simple/fibo_2calls_2_false-unreach-call.c false(reach) 3.1 3.1 76 wit true 4.5 2.6 220 false(reach) 12 6.7 340
recursive-simple/fibo_2calls_4_false-unreach-call.c false(reach) 3.2 3.1 75 wit true 7.7 4.4 310 false(reach) 25 15   570
recursive-simple/fibo_2calls_5_false-unreach-call.c false(reach) 2.5 2.5 74 wit true 9.8 5.6 430 false(reach) 35 20   790
recursive-simple/fibo_2calls_6_false-unreach-call.c witness unconfirmed 3.3 3.3 76 wit true 12   6.3 520 timeout 90 57   3100
recursive-simple/fibo_2calls_8_false-unreach-call.c witness unconfirmed 4.0 3.8 79 wit true 20   10   580 timeout 92 56   4100
recursive-simple/fibo_5_false-unreach-call.c false(reach) 3.3 3.3 75 wit true 8.2 4.6 320 false(reach) 66 43   1800
recursive-simple/fibo_7_false-unreach-call.c witness unconfirmed 3.6 3.6 74 wit true 13   7.0 540 timeout 92 61   3900
recursive-simple/id2_b3_o2_false-unreach-call.c false(reach) 3.1 3.1 72 wit true 6.0 3.4 260 false(reach) 12 8.4 330
recursive-simple/id2_i5_o5_false-unreach-call.c false(reach) 3.2 3.3 74 wit true 6.1 3.5 260 false(reach) 15 9.4 360
recursive-simple/id_b3_o2_false-unreach-call.c false(reach) 3.0 3.0 73 wit true 5.3 3.1 250 false(reach) 13 8.4 340
recursive-simple/id_i10_o10_false-unreach-call.c false(reach) 3.3 3.2 74 wit true 7.9 4.5 300 false(reach) 24 14   530
recursive-simple/id_i15_o15_false-unreach-call.c false(reach) 3.3 3.3 76 wit true 9.4 5.3 370 false(reach) 29 15   610
recursive-simple/id_i20_o20_false-unreach-call.c false(reach) 3.5 3.4 76 wit true 13   7.2 550 false(reach) 31 18   840
recursive-simple/id_i25_o25_false-unreach-call.c false(reach) 3.8 3.7 78 wit true 17   9.1 670 false(reach) 38 23   1200
recursive-simple/id_i5_o5_false-unreach-call.c false(reach) 3.0 3.0 75 wit true 6.0 3.4 270 false(reach) 17 9.3 390
recursive-simple/id_o1000_false-unreach-call.c true 880   880   200 wit - -
recursive-simple/id_o100_false-unreach-call.c witness timeout 22   22   120 wit timeout 92   74   1100 timeout 92 56   4500
recursive-simple/id_o10_false-unreach-call.c false(reach) 3.2 3.2 72 wit true 8.0 4.5 310 false(reach) 24 13   560
recursive-simple/id_o200_false-unreach-call.c witness timeout 210   210   260 wit timeout 90   73   1400 timeout 91 60   3800
recursive-simple/id_o20_false-unreach-call.c false(reach) 3.1 3.1 76 wit true 15   8.0 590 false(reach) 31 17   850
recursive-simple/id_o3_false-unreach-call.c false(reach) 3.1 3.1 73 wit true 5.8 3.4 260 false(reach) 13 8.6 350
recursive-simple/sum_10x0_false-unreach-call.c false(reach) 3.2 3.2 74 wit true 8.0 4.5 300 false(reach) 21 12   500
recursive-simple/sum_15x0_false-unreach-call.c false(reach) 3.4 3.3 75 wit true 8.9 4.9 360 false(reach) 26 14   590
recursive-simple/sum_20x0_false-unreach-call.c false(reach) 2.6 2.6 73 wit true 13   7.2 450 false(reach) 30 16   780
recursive-simple/sum_25x0_false-unreach-call.c false(reach) 3.7 3.6 70 wit true 15   8.0 620 false(reach) 32 18   880
recursive-simple/sum_2x3_false-unreach-call.c false(reach) 2.8 2.8 73 wit true 5.3 3.1 260 false(reach) 12 8.7 340
recursive-simple/sum_non_eq_false-unreach-call.c false(reach) 3.2 3.2 73 wit true 5.3 3.1 240 false(reach) 12 6.6 340
recursive-simple/sum_non_false-unreach-call.c false(reach) 3.1 3.1 73 wit true 5.3 3.1 240 false(reach) 11 5.8 340
recursive-simple/afterrec_2calls_true-unreach-call.c true 2.7 2.7 64 wit - -
recursive-simple/afterrec_true-unreach-call.c true 2.7 2.7 64 wit - -
recursive-simple/fibo_10_true-unreach-call.c true 4.2 4.1 91 wit - -
recursive-simple/fibo_15_true-unreach-call.c true 140   130   620 wit - -
recursive-simple/fibo_20_true-unreach-call.c true 900   880   2800 wit - -
recursive-simple/fibo_25_true-unreach-call.c true 900   880   3100 wit - -
recursive-simple/fibo_2calls_10_true-unreach-call.c true 4.9 4.7 92 wit - -
recursive-simple/fibo_2calls_15_true-unreach-call.c true 100   100   630 wit - -
recursive-simple/fibo_2calls_20_true-unreach-call.c timeout 900   930   2800 wit - -
recursive-simple/fibo_2calls_25_true-unreach-call.c timeout 900   930   3000 wit - -
recursive-simple/fibo_2calls_2_true-unreach-call.c true 2.7 2.8 63 wit - -
recursive-simple/fibo_2calls_4_true-unreach-call.c true 2.7 2.7 66 wit - -
recursive-simple/fibo_2calls_5_true-unreach-call.c true 2.8 2.8 69 wit - -
recursive-simple/fibo_2calls_6_true-unreach-call.c true 2.8 2.8 68 wit - -
recursive-simple/fibo_2calls_8_true-unreach-call.c true 2.9 2.9 75 wit - -
recursive-simple/fibo_5_true-unreach-call.c true 2.7 2.8 68 wit - -
recursive-simple/fibo_7_true-unreach-call.c true 2.9 2.9 73 wit - -
recursive-simple/id2_b2_o3_true-unreach-call.c true 2.8 2.8 67 wit - -
recursive-simple/id2_b3_o5_true-unreach-call.c true 2.6 2.7 76 wit - -
recursive-simple/id2_b5_o10_true-unreach-call.c true 2.8 2.8 67 wit - -
recursive-simple/id2_i5_o5_true-unreach-call.c true 2.7 2.8 62 wit - -
recursive-simple/id_b2_o3_true-unreach-call.c true 2.7 2.7 64 wit - -
recursive-simple/id_b3_o5_true-unreach-call.c true 2.8 2.8 63 wit - -
recursive-simple/id_b5_o10_true-unreach-call.c true 2.3 2.3 64 wit - -
recursive-simple/id_i10_o10_true-unreach-call.c true 2.8 2.8 69 wit - -
recursive-simple/id_i15_o15_true-unreach-call.c true 2.8 2.8 67 wit - -
recursive-simple/id_i20_o20_true-unreach-call.c true 2.9 3.0 68 wit - -
recursive-simple/id_i25_o25_true-unreach-call.c true 3.2 3.2 68 wit - -
recursive-simple/id_i5_o5_true-unreach-call.c true 2.8 2.8 64 wit - -
recursive-simple/sum_10x0_true-unreach-call.c true 2.7 2.8 65 wit - -
recursive-simple/sum_15x0_true-unreach-call.c true 2.8 2.8 65 wit - -
recursive-simple/sum_20x0_true-unreach-call.c true 2.2 2.2 68 wit - -
recursive-simple/sum_25x0_true-unreach-call.c true 2.9 2.9 78 wit - -
recursive-simple/sum_2x3_true-unreach-call.c true 2.6 2.6 66 wit - -
recursive-simple/sum_non_eq_true-unreach-call.c true 880   880   470 wit - -
recursive-simple/sum_non_true-unreach-call.c true 880   880   240 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 22000 22000 53000 98 630   390   19000   98 1700   1000   53000  
    correct results 79 15000 15000 27000 29 230   130   9700   29 670   400   18000  
        correct true 50 15000 14000 25000 29 0   0   0   0 0   0   0  
        correct false 29 91 91 2100 0 230   130   9700   29 670   400   18000  
    incorrect results 1 880 880 200 0 0   0   0   0 0   0   0  
        incorrect true 1 880 880 200 0 0   0   0   0 0   0   0  
        incorrect false 0
score (98 tasks, max score: 151) 97
Run set sv-comp16.Recursive