Tool HIPrec
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host [zeus01; zeus02; zeus03; zeus04; zeus05; zeus09; zeus10; zeus11; zeus13; zeus14; zeus15; zeus16; zeus21; 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-06 11:47:08 CET [[ 2016-01-15 09:08:50 CET ]] [[ 2016-01-15 22:21:40 CET ]]
Run set sv-comp16
Options [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/hiprec.2016-01-06_1147.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/hiprec.2016-01-06_1147.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 .82 .79 74 12   6.8 430 36 22   600
recursive/Addition02_false-unreach-call_false-termination.c .33 .31 72 6.8 4.0 350 13 9.4 330
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call.c .30 .28 73 7.5 4.2 370 16 8.6 340
recursive/EvenOdd03_false-unreach-call_false-termination.c .79 .76 83 6.2 3.6 340 12 10   320
recursive/Fibonacci04_false-unreach-call_true-termination.c .46 .45 78 91   71   2200 90 61   3100
recursive/Fibonacci05_false-unreach-call_true-termination.c 5.5  5.4  78 90   76   1400 90 61   3000
recursive/McCarthy91_false-unreach-call_false-termination.c .31 .29 73 5.8 3.4 350 11 9.3 330
recursive/Ackermann01_true-unreach-call.c .51 .49 74
recursive/Ackermann03_true-unreach-call.c .90 .88 78
recursive/Ackermann04_true-unreach-call.c .62 .60 77
recursive/Addition01_true-unreach-call_true-termination.c .30 .28 73
recursive/Addition03_true-unreach-call.c .28 .26 72
recursive/EvenOdd01_true-unreach-call_true-termination.c 3.1  3.1  100
recursive/Fibonacci01_true-unreach-call.c .46 .45 77
recursive/Fibonacci02_true-unreach-call_true-termination.c 21    20    78
recursive/Fibonacci03_true-unreach-call_true-termination.c 1.7  1.6  79
recursive/McCarthy91_true-unreach-call.c 7.2  7.1  100
recursive/MultCommutative_true-unreach-call_true-termination.c 25    25    120
recursive/Primes_true-unreach-call.c 900    900    710
recursive/gcd01_true-unreach-call_true-termination.c .96 .94 77
recursive/gcd02_true-unreach-call.c 4.8  4.7  110
recursive/recHanoi01_true-unreach-call_true-termination.c 18    18    110
recursive/recHanoi02_true-unreach-call_true-termination.c .32 .30 72
recursive/recHanoi03_true-unreach-call_true-termination.c .33 .31 72
recursive-simple/afterrec_2calls_false-unreach-call.c .25 .24 72 6.3 3.6 340 13 8.5 350
recursive-simple/afterrec_false-unreach-call.c .30 .27 71 6.3 3.6 360 12 7.6 320
recursive-simple/fibo_10_false-unreach-call.c .56 .53 77 90   76   1200 90 57   3400
recursive-simple/fibo_15_false-unreach-call.c 10    10    81 90   74   1300 91 49   2500
recursive-simple/fibo_20_false-unreach-call.c 570    570    240 91   68   1800 92 53   4300
recursive-simple/fibo_25_false-unreach-call.c 900    900    280
recursive-simple/fibo_2calls_10_false-unreach-call.c .78 .76 84 90   75   1300 90 53   3100
recursive-simple/fibo_2calls_15_false-unreach-call.c 11    11    110 91   71   1400 15 10   340
recursive-simple/fibo_2calls_20_false-unreach-call.c 760    760    260 91   66   2400 90 50   3600
recursive-simple/fibo_2calls_25_false-unreach-call.c 900    900    280
recursive-simple/fibo_2calls_2_false-unreach-call.c .87 .84 83 5.3 3.0 240 14 8.8 340
recursive-simple/fibo_2calls_4_false-unreach-call.c .86 .83 83 18   9.6 550 11 7.5 310
recursive-simple/fibo_2calls_5_false-unreach-call.c .74 .72 83 23   12   610 91 53   1900
recursive-simple/fibo_2calls_6_false-unreach-call.c 1.1  1.0  83 46   25   990 91 54   2800
recursive-simple/fibo_2calls_8_false-unreach-call.c 3.8  3.7  83 91   70   1600 92 58   3400
recursive-simple/fibo_5_false-unreach-call.c .53 .51 78 21   11   630 91 50   1500
recursive-simple/fibo_7_false-unreach-call.c 1.7  1.6  77 91   73   1400 91 64   2800
recursive-simple/id2_b3_o2_false-unreach-call.c .43 .41 73 26   14   590 13 9.8 330
recursive-simple/id2_i5_o5_false-unreach-call.c .31 .29 72 6.5 3.7 350 21 12   420
recursive-simple/id_b3_o2_false-unreach-call.c .31 .30 72 8.6 4.8 390 14 10   350
recursive-simple/id_i10_o10_false-unreach-call.c 1.5  1.5  71 7.2 4.1 350 91 58   2200
recursive-simple/id_i15_o15_false-unreach-call.c 1.5  1.5  71 23   12   610 91 69   4100
recursive-simple/id_i20_o20_false-unreach-call.c 1.5  1.4  71 47   29   970 90 72   3700
recursive-simple/id_i25_o25_false-unreach-call.c 1.7  1.7  71 65   48   1400 90 70   4400
recursive-simple/id_i5_o5_false-unreach-call.c 1.5  1.4  71 6.8 4.0 350 32 19   520
recursive-simple/id_o1000_false-unreach-call.c 2.9  2.9  74 90   75   1000 92 55   4000
recursive-simple/id_o100_false-unreach-call.c 1.5  1.4  74 90   79   890 91 57   4300
recursive-simple/id_o10_false-unreach-call.c 1.5  1.4  74 16   8.4 500 91 54   2000
recursive-simple/id_o200_false-unreach-call.c 1.6  1.6  74 90   72   900 92 57   3000
recursive-simple/id_o20_false-unreach-call.c 1.7  1.6  74 50   31   1400 90 73   4400
recursive-simple/id_o3_false-unreach-call.c 1.4  1.4  74 6.6 3.8 340 21 14   390
recursive-simple/sum_10x0_false-unreach-call.c .24 .22 71 6.8 3.9 370 86 54   2300
recursive-simple/sum_15x0_false-unreach-call.c .35 .33 71 22   12   690 90 62   3900
recursive-simple/sum_20x0_false-unreach-call.c .34 .32 71 40   25   970 91 73   4000
recursive-simple/sum_25x0_false-unreach-call.c .46 .44 71 71   51   1400 91 69   4100
recursive-simple/sum_2x3_false-unreach-call.c .29 .28 71 6.6 3.7 360 17 11   350
recursive-simple/sum_non_eq_false-unreach-call.c .26 .24 71 6.2 3.5 360 12 9.0 340
recursive-simple/sum_non_false-unreach-call.c .21 .19 71 6.3 3.5 350 13 8.0 330
recursive-simple/afterrec_2calls_true-unreach-call.c .24 .23 71
recursive-simple/afterrec_true-unreach-call.c .20 .18 71
recursive-simple/fibo_10_true-unreach-call.c 86    85    81
recursive-simple/fibo_15_true-unreach-call.c 900    900    160
recursive-simple/fibo_20_true-unreach-call.c 900    890    190
recursive-simple/fibo_25_true-unreach-call.c 900    890    180
recursive-simple/fibo_2calls_10_true-unreach-call.c 54    53    89
recursive-simple/fibo_2calls_15_true-unreach-call.c 900    900    180
recursive-simple/fibo_2calls_20_true-unreach-call.c 900    900    190
recursive-simple/fibo_2calls_25_true-unreach-call.c 900    900    190
recursive-simple/fibo_2calls_2_true-unreach-call.c .83 .81 84
recursive-simple/fibo_2calls_4_true-unreach-call.c .90 .87 83
recursive-simple/fibo_2calls_5_true-unreach-call.c .89 .86 84
recursive-simple/fibo_2calls_6_true-unreach-call.c 1.1  1.1  83
recursive-simple/fibo_2calls_8_true-unreach-call.c 3.3  3.2  83
recursive-simple/fibo_5_true-unreach-call.c .68 .66 77
recursive-simple/fibo_7_true-unreach-call.c 1.6  1.6  78
recursive-simple/id2_b2_o3_true-unreach-call.c .36 .34 73
recursive-simple/id2_b3_o5_true-unreach-call.c .33 .32 73
recursive-simple/id2_b5_o10_true-unreach-call.c .51 .48 74
recursive-simple/id2_i5_o5_true-unreach-call.c .28 .26 72
recursive-simple/id_b2_o3_true-unreach-call.c .25 .23 72
recursive-simple/id_b3_o5_true-unreach-call.c .25 .24 72
recursive-simple/id_b5_o10_true-unreach-call.c .31 .30 73
recursive-simple/id_i10_o10_true-unreach-call.c 1.5  1.4  72
recursive-simple/id_i15_o15_true-unreach-call.c 1.4  1.3  71
recursive-simple/id_i20_o20_true-unreach-call.c 1.4  1.4  71
recursive-simple/id_i25_o25_true-unreach-call.c 1.5  1.4  71
recursive-simple/id_i5_o5_true-unreach-call.c 1.5  1.4  72
recursive-simple/sum_10x0_true-unreach-call.c .20 .19 71
recursive-simple/sum_15x0_true-unreach-call.c .23 .22 71
recursive-simple/sum_20x0_true-unreach-call.c .21 .20 71
recursive-simple/sum_25x0_true-unreach-call.c .26 .24 71
recursive-simple/sum_2x3_true-unreach-call.c .30 .28 71
recursive-simple/sum_non_eq_true-unreach-call.c .31 .29 71
recursive-simple/sum_non_true-unreach-call.c .21 .20 71
../../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 9700 9700 9600 98 1800   1300   36000   98 2600   1700   88000  
local summary 1300
    correct results 70 210 210 5200 29 560   340   17000   17 1400   990   47000  
        correct true 41 190 180 3100 0 0   0   0   1 0   0   0  
        correct false 29 22 21 2200 29 560   340   17000   16 1400   990   47000  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (98 tasks, max score: 151) 111
Run set sv-comp16