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.Recursive
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)
recursive/Ackermann02_false-unreach-call_false-termination.c false(reach) .37 .21 46 wit false(reach) 12   6.3 450 true 11   6.7 350
recursive/Addition02_false-unreach-call_false-termination.c false(reach) .48 .28 44 wit false(reach) 8.1 4.5 380 true 11   6.7 340
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call.c false(reach) .36 .22 45 wit false(reach) 7.7 4.4 370 true 10   6.5 320
recursive/EvenOdd03_false-unreach-call_false-termination.c false(reach) .33 .19 44 wit false(reach) 7.0 3.9 360 true 12   7.0 350
recursive/Fibonacci04_false-unreach-call_true-termination.c false(reach) .51 .29 45 wit false(reach) 64   42   1500 true 11   6.2 350
recursive/Fibonacci05_false-unreach-call_true-termination.c witness timeout .61 .33 46 wit timeout 91   68   2700 true 11   6.1 320
recursive/McCarthy91_false-unreach-call_false-termination.c false(reach) .29 .17 45 wit false(reach) 8.2 4.5 380 true 11   6.7 330
recursive/Ackermann01_true-unreach-call.c true .37 .22 43 wit - -
recursive/Ackermann03_true-unreach-call.c true 4.8  2.4  63 wit - -
recursive/Ackermann04_true-unreach-call.c true 1.1  .58 50 wit - -
recursive/Addition01_true-unreach-call_true-termination.c true .49 .27 43 wit - -
recursive/Addition03_true-unreach-call.c true 41    21    220 wit - -
recursive/EvenOdd01_true-unreach-call_true-termination.c timeout 900    450    270 wit - -
recursive/Fibonacci01_true-unreach-call.c true .36 .21 41 wit - -
recursive/Fibonacci02_true-unreach-call_true-termination.c true 3.3  1.7  53 wit - -
recursive/Fibonacci03_true-unreach-call_true-termination.c true 1.1  .57 45 wit - -
recursive/McCarthy91_true-unreach-call.c true .34 .20 43 wit - -
recursive/MultCommutative_true-unreach-call_true-termination.c timeout 900    450    340 wit - -
recursive/Primes_true-unreach-call.c true 2.1  1.1  76 wit - -
recursive/gcd01_true-unreach-call_true-termination.c true .48 .27 45 wit - -
recursive/gcd02_true-unreach-call.c timeout 900    450    390 wit - -
recursive/recHanoi01_true-unreach-call_true-termination.c timeout 900    450    710 wit - -
recursive/recHanoi02_true-unreach-call_true-termination.c true .30 .19 39 wit - -
recursive/recHanoi03_true-unreach-call_true-termination.c true .26 .16 40 wit - -
recursive-simple/afterrec_2calls_false-unreach-call.c false(reach) .28 .17 40 wit false(reach) 6.7 3.8 350 true 11   6.2 330
recursive-simple/afterrec_false-unreach-call.c false(reach) .29 .17 39 wit false(reach) 7.4 4.2 350 true 11   6.6 340
recursive-simple/fibo_10_false-unreach-call.c false(reach) 1.3  .70 52 wit false(reach) 13   7.2 520 true 11   5.9 340
recursive-simple/fibo_15_false-unreach-call.c witness timeout 1.1  .58 48 wit timeout (false(reach)) 92   60   2000 true 9.9 7.8 320
recursive-simple/fibo_20_false-unreach-call.c witness timeout 12    6.2  96 wit timeout 91   67   1900 true 11   6.2 330
recursive-simple/fibo_25_false-unreach-call.c witness timeout 46    23    180 wit timeout 92   52   4600 true 11   7.1 340
recursive-simple/fibo_2calls_10_false-unreach-call.c false(reach) .55 .31 46 wit false(reach) 18   9.3 570 true 11   7.9 330
recursive-simple/fibo_2calls_15_false-unreach-call.c false(reach) 1.2  .61 49 wit false(reach) 81   56   1900 true 10   7.1 320
recursive-simple/fibo_2calls_20_false-unreach-call.c witness timeout 5.6  2.8  60 wit timeout 91   66   1900 true 12   6.7 340
recursive-simple/fibo_2calls_25_false-unreach-call.c witness timeout 51    25    190 wit timeout 92   52   4900 true 11   6.3 350
recursive-simple/fibo_2calls_2_false-unreach-call.c witness unconfirmed .28 .17 27 wit true 9.3 5.1 320 true 9.4 6.4 320
recursive-simple/fibo_2calls_4_false-unreach-call.c false(reach) .34 .20 42 wit false(reach) 14   7.8 520 true 11   6.7 320
recursive-simple/fibo_2calls_5_false-unreach-call.c false(reach) .49 .28 45 wit false(reach) 9.2 5.3 420 true 11   7.7 320
recursive-simple/fibo_2calls_6_false-unreach-call.c false(reach) .41 .23 45 wit false(reach) 9.7 5.4 440 true 10   6.3 330
recursive-simple/fibo_2calls_8_false-unreach-call.c false(reach) .47 .26 46 wit false(reach) 13   7.0 490 true 11   7.8 320
recursive-simple/fibo_5_false-unreach-call.c false(reach) .49 .29 43 wit false(reach) 7.5 4.3 360 true 9.9 5.4 340
recursive-simple/fibo_7_false-unreach-call.c false(reach) .63 .34 45 wit false(reach) 9.1 5.1 390 true 10   7.5 330
recursive-simple/id2_b3_o2_false-unreach-call.c false(reach) .40 .24 42 wit false(reach) 8.0 4.4 380 true 12   8.4 340
recursive-simple/id2_i5_o5_false-unreach-call.c false(reach) .39 .23 42 wit false(reach) 6.5 3.7 350 true 10   6.1 330
recursive-simple/id_b3_o2_false-unreach-call.c false(reach) .33 .19 42 wit false(reach) 7.6 4.2 380 true 11   8.2 320
recursive-simple/id_i10_o10_false-unreach-call.c false(reach) .65 .43 55 wit false(reach) 6.9 3.9 360 true 9.3 5.1 330
recursive-simple/id_i15_o15_false-unreach-call.c false(reach) .61 .33 45 wit false(reach) 7.5 4.1 380 true 9.5 5.8 320
recursive-simple/id_i20_o20_false-unreach-call.c false(reach) .78 .42 46 wit false(reach) 7.7 4.4 390 true 12   9.0 320
recursive-simple/id_i25_o25_false-unreach-call.c false(reach) .89 .47 48 wit false(reach) 7.8 4.3 390 true 9.6 8.1 300
recursive-simple/id_i5_o5_false-unreach-call.c false(reach) .31 .18 45 wit false(reach) 7.3 4.2 360 true 9.5 5.3 330
recursive-simple/id_o1000_false-unreach-call.c witness invalid (error) 650    330    1100 wit error 53   35   1300 true 9.8 5.5 320
recursive-simple/id_o100_false-unreach-call.c witness invalid (error) 3.5  1.8  68 wit error 49   31   1300 true 11   5.8 310
recursive-simple/id_o10_false-unreach-call.c witness invalid (error) .47 .27 46 wit error 52   33   1200 true 11   7.6 310
recursive-simple/id_o200_false-unreach-call.c witness invalid (error) 12    5.8  110 wit error 51   31   1300 true 11   8.0 310
recursive-simple/id_o20_false-unreach-call.c witness invalid (error) .73 .39 48 wit error 50   32   1300 true 9.5 5.3 320
recursive-simple/id_o3_false-unreach-call.c false(reach) .36 .22 45 wit false(reach) 9.7 5.3 410 true 11   6.2 320
recursive-simple/sum_10x0_false-unreach-call.c false(reach) .64 .35 46 wit false(reach) 6.7 3.8 360 true 12   7.7 330
recursive-simple/sum_15x0_false-unreach-call.c false(reach) .68 .36 46 wit false(reach) 7.7 4.5 370 true 11   6.2 330
recursive-simple/sum_20x0_false-unreach-call.c false(reach) .81 .42 48 wit false(reach) 7.5 4.2 380 true 9.2 5.2 320
recursive-simple/sum_25x0_false-unreach-call.c false(reach) .96 .49 49 wit false(reach) 8.3 4.6 390 true 10   6.0 330
recursive-simple/sum_2x3_false-unreach-call.c false(reach) .46 .27 44 wit false(reach) 6.5 3.6 350 true 11   6.1 330
recursive-simple/sum_non_eq_false-unreach-call.c false(reach) .32 .20 43 wit false(reach) 6.5 3.7 350 true 9.9 7.2 330
recursive-simple/sum_non_false-unreach-call.c false(reach) .35 .22 43 wit false(reach) 6.6 3.7 350 true 11   7.2 340
recursive-simple/afterrec_2calls_true-unreach-call.c true .26 .17 24 wit - -
recursive-simple/afterrec_true-unreach-call.c true .32 .20 37 wit - -
recursive-simple/fibo_10_true-unreach-call.c true 5.1  2.6  61 wit - -
recursive-simple/fibo_15_true-unreach-call.c true 13    6.5  76 wit - -
recursive-simple/fibo_20_true-unreach-call.c true 59    30    120 wit - -
recursive-simple/fibo_25_true-unreach-call.c true 100    50    120 wit - -
recursive-simple/fibo_2calls_10_true-unreach-call.c true 1.9  .98 52 wit - -
recursive-simple/fibo_2calls_15_true-unreach-call.c true 6.6  3.3  71 wit - -
recursive-simple/fibo_2calls_20_true-unreach-call.c true 12    6.2  77 wit - -
recursive-simple/fibo_2calls_25_true-unreach-call.c true 67    33    130 wit - -
recursive-simple/fibo_2calls_2_true-unreach-call.c true .21 .12 25 wit - -
recursive-simple/fibo_2calls_4_true-unreach-call.c true .52 .29 43 wit - -
recursive-simple/fibo_2calls_5_true-unreach-call.c true .68 .37 45 wit - -
recursive-simple/fibo_2calls_6_true-unreach-call.c true .78 .41 45 wit - -
recursive-simple/fibo_2calls_8_true-unreach-call.c true 1.6  .80 50 wit - -
recursive-simple/fibo_5_true-unreach-call.c true 1.1  .59 46 wit - -
recursive-simple/fibo_7_true-unreach-call.c true 2.2  1.1  50 wit - -
recursive-simple/id2_b2_o3_true-unreach-call.c true .30 .18 40 wit - -
recursive-simple/id2_b3_o5_true-unreach-call.c true .39 .24 39 wit - -
recursive-simple/id2_b5_o10_true-unreach-call.c true .29 .17 40 wit - -
recursive-simple/id2_i5_o5_true-unreach-call.c true .54 .31 40 wit - -
recursive-simple/id_b2_o3_true-unreach-call.c true .29 .17 39 wit - -
recursive-simple/id_b3_o5_true-unreach-call.c true .30 .18 40 wit - -
recursive-simple/id_b5_o10_true-unreach-call.c true .30 .17 40 wit - -
recursive-simple/id_i10_o10_true-unreach-call.c true .37 .22 41 wit - -
recursive-simple/id_i15_o15_true-unreach-call.c true .30 .19 42 wit - -
recursive-simple/id_i20_o20_true-unreach-call.c true .41 .24 41 wit - -
recursive-simple/id_i25_o25_true-unreach-call.c true .31 .18 41 wit - -
recursive-simple/id_i5_o5_true-unreach-call.c true .31 .19 41 wit - -
recursive-simple/sum_10x0_true-unreach-call.c true .29 .16 43 wit - -
recursive-simple/sum_15x0_true-unreach-call.c true .31 .18 43 wit - -
recursive-simple/sum_20x0_true-unreach-call.c true .35 .19 43 wit - -
recursive-simple/sum_25x0_true-unreach-call.c true .41 .23 43 wit - -
recursive-simple/sum_2x3_true-unreach-call.c true .44 .25 43 wit - -
recursive-simple/sum_non_eq_true-unreach-call.c true .30 .17 42 wit - -
recursive-simple/sum_non_true-unreach-call.c true .35 .20 43 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 4700 2400   7800 98 1200   780   40000   98 480   300   15000  
    correct results 82 350 180   4200 33 410   250   16000   33 350   220   11000  
        correct true 49 330 170   2700 0 0   0   0   33 0   0   0  
        correct false 33 18 10   1500 33 410   250   16000   0 350   220   11000  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (98 tasks, max score: 151) 131
Run set sv-comp16.Recursive