Tool 2LS 0.6.0 CBMC 5.8 CPAchecker 1.6.1-svn 26725 CPAchecker 1.6.1-svn 26758M CPAchecker 1.6.1-svn 26773 DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 ESBMC ESBMC version 4.6.0 64-bit x86_64 linux Map2Check Map2Check 7.1 : Wed Nov 22 22:30:11 -04 2017 symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 ULTIMATE Automizer 0.1.23-3204b741 ULTIMATE Kojak 0.1.23-3204b741 ULTIMATE Taipan 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-12-01 10:20:37 CET 2017-12-01 11:16:27 CET 2017-12-01 08:43:54 CET 2017-12-01 08:51:01 CET 2017-12-01 10:49:29 CET 2017-12-01 13:07:37 CET 2017-12-02 06:23:16 CET 2017-12-02 18:23:42 CET 2017-12-02 00:52:46 CET 2017-12-03 04:09:48 CET 2017-12-03 11:17:40 CET 2017-12-03 08:43:49 CET
Run set 2ls.sv-comp18.NoOverflows-Other cbmc.sv-comp18.NoOverflows-Other cpa-bam-bnb.sv-comp18.NoOverflows-Other cpa-bam-slicing.sv-comp18.NoOverflows-Other cpa-seq.sv-comp18.NoOverflows-Other depthk.sv-comp18.NoOverflows-Other esbmc-incr.sv-comp18.NoOverflows-Other esbmc-kind.sv-comp18.NoOverflows-Other map2check.sv-comp18.NoOverflows-Other symbiotic.sv-comp18.NoOverflows-Other uautomizer.sv-comp18.NoOverflows-Other ukojak.sv-comp18.NoOverflows-Other utaipan.sv-comp18.NoOverflows-Other
Options --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp18-bam-bnb -disable-java-assertions -heap 10000m -ldv-bam-svcomp -disable-java-assertions -heap 10000m -svcomp18 -heap 10000M -benchmark -timelimit 900s -s incr -s kinduction --witness witness.graphml --full-output --full-output --full-output
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
recursive/Addition02WithOverflowBug_false-no-overflow.c error (5) .079 22 .75 0 false(no-overflow) .28 35 2.1 1 error (1) .49 41 4.4 0 error (1) .44 41 4.2 0 false(no-overflow) 2.8 280 25 1 false(no-overflow) .56 49 7.6 1 false(no-overflow) .22  28 1.8  1 false(no-overflow) .16  28 3.3  1 false(no-overflow) .43  12 5.7  1 false(no-overflow) .19 12 2.1 1 false(no-overflow) 6.0 330 42 1 false(no-overflow) 4.4 250 40 1 false(no-overflow) 4.1 230 36 1
recursive/Addition03_false-no-overflow.c error (5) .090 22 .98 0 false(no-overflow) .27 33 2.2 1 error (1) .46 40 4.6 0 error (1) .43 40 3.9 0 false(no-overflow) 3.1 300 29 1 false(no-overflow) .56 49 7.1 1 false(no-overflow) .17  28 1.7  1 false(no-overflow) .18  28 1.8  1 false(no-overflow) .42  12 5.4  1 false(no-overflow) .17 12 1.9 1 false(no-overflow) 4.4 240 35 1 false(no-overflow) 4.5 260 39 1 false(no-overflow) 4.1 240 39 1
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c error (5) .11  23 .60 0 false(no-overflow) .25 33 2.5 1 error (1) .46 40 4.2 0 error (1) .46 40 4.7 0 false(no-overflow) 2.6 270 22 1 unknown 64    73 750   0 false(no-overflow) .12  28 1.4  1 false(no-overflow) .12  28 1.4  1 false(no-overflow) .37  12 4.7  1 false(no-overflow) .20 12 1.8 1 false(no-overflow) 4.8 290 44 1 false(no-overflow) 4.6 270 42 1 false(no-overflow) 4.8 290 39 1
recursive/Ackermann01_true-unreach-call_true-no-overflow.c error (5) .11  22 .66 0 error (42) 870    330 2900   0 error (1) .46 41 4.6 0 error (1) .41 40 3.5 0 timeout 900   3600 12000 0 out of memory (false(no-overflow)) 450    15000 5400   0 out of memory 440     15000 5400    0 out of memory 620     15000 7700    0 unknown 890     17 12000    0 timeout (timeout) 900    2100 12000   0 timeout 900   12000 10000 0 timeout 900   1700 11000 0 timeout 910   13000 5800 0
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c error (5) .11  22 .64 0 error (42) 870    360 3500   0 error (1) .48 42 4.6 0 error (1) .46 40 4.3 0 timeout 900   4300 9600 0 unknown 460    15000 5300   0 out of memory 450     15000 5100    0 out of memory 630     15000 7700    0 unknown 890     19 14000    0 timeout (timeout) 900    2500 11000   0 timeout 900   13000 10000 0 timeout 900   1800 13000 0 timeout 910   13000 6500 0
recursive/Ackermann03_true-unreach-call_true-no-overflow.c error (5) .11  22 .60 0 error (42) 870    350 3400   0 error (1) .47 40 4.5 0 error (1) .43 40 3.6 0 timeout 900   4500 12000 0 unknown 460    15000 5500   0 out of memory 460     15000 5000    0 out of memory 640     15000 7100    0 unknown 890     18 12000    0 timeout (timeout) 900    2100 11000   0 timeout 910   13000 9400 0 timeout 900   1700 10000 0 timeout 910   13000 6600 0
recursive/Ackermann04_true-unreach-call_true-no-overflow.c error (5) .12  22 .62 0 error (42) 870    340 3000   0 error (1) .49 40 4.9 0 error (1) .48 41 4.2 0 timeout 900   5700 10000 0 unknown 460    15000 5900   0 out of memory 450     15000 4700    0 out of memory 610     15000 8800    0 unknown 890     18 12000    0 timeout (timeout) 900    2100 13000   0 timeout 910   13000 8200 0 timeout 900   1700 11000 0 timeout 910   13000 5400 0
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c error (5) .090 22 .81 0 out of memory 860    15000 8000   0 error (1) .45 40 4.7 0 error (1) .45 40 4.0 0 timeout 900   5700 10000 0 unknown 400    15000 5400   0 out of memory 810     15000 9200    0 out of memory 580     15000 5800    0 unknown 890     650 9400    0 timeout (timeout) 900    29 11000   0 timeout 900   5200 13000 0 timeout 900   6000 15000 0 timeout 900   4400 12000 0
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c error (5) .097 22 .81 0 error (42) 880    15000 9100   0 error (1) .49 41 4.5 0 error (1) .46 40 4.1 0 timeout 900   5700 9100 0 unknown 400    15000 5100   0 out of memory 840     15000 8100    0 out of memory 580     15000 7200    0 unknown 900     640 10000    0 timeout (timeout) 900    72 14000   0 timeout 900   5200 12000 0 timeout 900   6000 12000 0 timeout 900   5100 12000 0
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c error (5) .11  22 .71 0 error (42) 880    6800 4600   0 error (1) .49 41 4.5 0 error (1) .47 41 4.1 0 true 2.8 270 24 1 unknown 400    15000 5000   0 out of memory 830     15000 9000    0 out of memory 570     15000 6000    0 unknown .076 11 .38 0 timeout (timeout) 900    63 12000   0 timeout 900   5200 11000 0 timeout 900   5800 14000 0 timeout 900   2600 12000 0
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c error (5) .11  22 .65 0 true .43 33 3.9 2 error (1) .48 41 3.9 0 error (1) .46 40 4.1 0 true 2.8 270 26 2 unknown 1.2  49 14   0 true .081 26 .85 2 true .073 26 .77 2 true .38  11 5.5  2 true .15 11 1.4 2 true 4.2 240 34 2 true 4.2 250 31 2 true 4.4 250 35 2
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c error (5) .099 22 .73 0 error (42) 870    2800 6500   0 error (1) .52 43 4.3 0 error (1) .45 40 4.0 0 timeout 900   4100 10000 0 unknown 64    74 900   0 timeout 900     1100 10000    0 timeout 900     1100 10000    0 unknown 890     850 12000    0 timeout (timeout) 900    320 12000   0 true 10   520 90 2 timeout 900   4800 13000 0 true 7.3 380 60 2
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c error (5) .12  22 .61 0 error (42) 870    2800 7400   0 error (1) .48 41 4.4 0 error (1) .47 40 4.5 0 timeout 900   4400 9800 0 unknown 64    75 710   0 timeout 900     1100 13000    0 timeout 900     1100 10000    0 unknown 890     830 11000    0 timeout (timeout) 900    300 11000   0 true 11   510 98 2 timeout 900   5200 9700 0 true 7.7 380 55 2
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c error (5) .082 22 .71 0 error (42) 870    260 3700   0 error (1) .44 40 3.8 0 error (1) .43 40 4.2 0 true 4.4 290 39 1 unknown 860    15000 11000   0 timeout 900     8800 7500    0 timeout 900     4400 8600    0 unknown 890     13 13000    0 timeout (timeout) 900    220 9700   0 timeout 900   5000 11000 0 timeout 900   1300 11000 0 timeout 900   5000 12000 0
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c error (5) .096 22 .87 0 true 1.3  33 13   2 error (1) .46 40 4.6 0 error (1) .42 40 3.5 0 true 670   810 6100 2 unknown 1.4  49 16   0 true .15  26 1.4  2 true .16  26 1.4  2 unknown .29  11 3.2  0 true .18 11 1.7 2 true 36   3800 410 2 timeout 900   1400 11000 0 timeout 900   13000 7200 0
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c error (5) .085 22 .81 0 error (42) 870    260 3000   0 error (1) .47 40 4.1 0 error (1) .44 38 3.4 0 true 5.9 310 63 1 unknown 380    15000 5100   0 timeout 900     8800 7000    0 timeout 900     11000 11000    0 unknown 890     13 13000    0 timeout (timeout) 900    220 11000   0 timeout 900   5400 11000 0 timeout 900   1300 12000 0 true 63   1500 490 1
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c error (5) .12  22 .67 0 error (42) 870    250 2500   0 error (1) .47 41 4.5 0 error (1) .48 41 3.9 0 true 4.2 300 40 1 unknown 380    15000 4700   0 timeout 900     8800 6700    0 timeout 900     11000 9300    0 unknown 900     1400 11000    0 timeout (timeout) 900    280 12000   0 timeout 900   5000 13000 0 timeout 900   1500 11000 0 true 59   1500 450 1
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c error (5) .093 22 .73 0 error (42) 870    260 2900   0 error (1) .45 41 3.6 0 error (1) .44 40 4.2 0 true 4.2 290 42 1 unknown 380    15000 5100   0 timeout 900     8800 7100    0 timeout 900     11000 8600    0 unknown 900     1300 12000    0 timeout (timeout) 900    270 11000   0 timeout 900   4800 11000 0 timeout 900   1600 11000 0 true 58   1600 440 1
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c error (5) .083 22 .86 0 error (42) 870    2000 3500   0 error (1) .48 45 4.7 0 error (1) .44 40 3.8 0 true 3.4 280 26 2 out of memory (false(no-overflow)) 510    15000 6900   0 timeout 900     6400 7800    0 timeout 900     9100 10000    0 unknown 900     140 11000    0 timeout (timeout) 900    74 11000   0 true 6.8 310 53 2 true 7.0 440 56 2 true 6.6 310 53 2
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c error (5) .094 22 .73 0 error (42) 870    2000 3700   0 error (1) .46 41 3.9 0 error (1) .45 40 4.5 0 true 3.3 280 29 2 out of memory (false(no-overflow)) 510    15000 6100   0 timeout 900     6300 7100    0 timeout 900     9000 8700    0 unknown 900     160 10000    0 timeout (timeout) 900    74 12000   0 true 6.5 310 54 2 true 7.1 430 60 2 true 6.8 320 61 2
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c error (5) .082 22 .93 0 error (42) 870    450 2100   0 error (1) .49 44 4.5 0 error (1) .44 40 4.2 0 timeout 900   1500 10000 0 unknown 480    15000 6400   0 out of memory 700     15000 6700    0 out of memory 380     15000 3900    0 unknown 890     80 12000    0 timeout (timeout) 900    330 14000   0 timeout 900   3100 12000 0 timeout 900   2000 13000 0 true 240   4800 2700 1
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c error (5) .12  23 .71 0 error (42) 870    310 4100   0 error (1) .49 40 3.8 0 error (1) .45 41 3.8 0 timeout 900   1500 12000 0 unknown 530    15000 6700   0 out of memory 220     15000 2400    0 out of memory 450     15000 6100    0 unknown 900     53 13000    0 timeout (timeout) 900    44 11000   0 timeout 900   5000 14000 0 timeout 900   1500 12000 0 timeout 900   6800 12000 0
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c error (5) .098 22 .76 0 error (42) 870    5000 4200   0 error (1) .49 40 4.4 0 error (1) .42 41 4.0 0 true 3.4 310 29 2 unknown 420    15000 4600   0 timeout 900     890 8600    0 timeout 900     1600 9200    0 unknown 900     88 13000    0 timeout (timeout) 900    49 14000   0 true 5.7 300 47 2 true 8.3 480 70 2 true 5.7 300 49 2
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c error (5) .10  22 .76 0 error (42) 880    7200 5900   0 error (1) .49 43 5.1 0 error (1) .45 40 4.3 0 true 3.5 290 33 2 unknown 420    15000 5400   0 timeout 900     1200 9200    0 timeout 900     2300 8300    0 unknown 890     36 12000    0 timeout (timeout) 900    29 12000   0 true 11   530 100 2 true 14   640 130 2 true 32   820 270 2
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c error (5) .082 22 .81 0 error (42) 870    1400 2900   0 error (1) .46 40 4.9 0 error (1) .44 40 4.7 0 timeout 900   6800 9900 0 out of memory (false(no-overflow)) 410    15000 4700   0 timeout 900     13000 10000    0 timeout 900     5300 6400    0 unknown 890     13 12000    0 timeout (timeout) 900    1200 12000   0 timeout 900   4700 14000 0 timeout 900   2900 11000 0 timeout 910   13000 8900 0
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c error (5) .094 22 .79 0 true 2.6  36 27   1 error (1) .42 40 4.4 0 error (1) .45 40 4.0 0 timeout 900   5000 12000 0 unknown 1.9  49 21   0 true 1.9   28 25    1 true 2.0   27 29    1 true 2.1   12 27    1 true .64 14 8.4 1 true 60   1500 600 1 timeout 900   4700 13000 0 timeout 900   2700 11000 0
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c error (5) .10  22 .65 0 true 2.6  36 28   1 error (1) .45 43 4.9 0 error (1) .46 40 4.1 0 timeout 900   4400 9800 0 unknown 1.8  49 20   0 true 1.9   27 24    1 true 2.0   28 27    1 true 2.1   13 27    1 true .71 14 10   1 true 57   1700 520 1 timeout 900   4600 14000 0 timeout 900   2500 11000 0
recursive-simple/id_b3_o2_false-no-overflow.c error (5) .12  22 .55 0 false(no-overflow) .24 33 2.0 1 error (1) .45 40 4.7 0 error (1) .46 40 4.3 0 false(no-overflow) 2.8 270 24 1 false(no-overflow) .54 49 8.3 1 false(no-overflow) .16  28 .91 1 false(no-overflow) .13  28 1.6  1 false(no-overflow) .37  12 4.8  1 false(no-overflow) .16 12 2.4 1 false(no-overflow) 4.6 290 37 1 false(no-overflow) 4.5 270 45 1 false(no-overflow) 4.5 280 40 1
recursive-simple/id_b3_o5_false-no-overflow.c error (5) .12  22 .71 0 false(no-overflow) .27 33 2.1 1 error (1) .47 41 4.4 0 error (1) .43 38 3.6 0 false(no-overflow) 2.8 280 23 1 false(no-overflow) .56 49 7.3 1 false(no-overflow) .13  28 1.3  1 false(no-overflow) .17  28 1.2  1 false(no-overflow) .37  12 4.0  1 false(no-overflow) .18 12 1.9 1 false(no-overflow) 4.8 280 35 1 false(no-overflow) 4.4 260 34 1 false(no-overflow) 4.7 280 37 1
recursive-simple/id_b5_o10_false-no-overflow.c error (5) .096 22 .74 0 false(no-overflow) .26 33 2.2 1 error (1) .45 41 4.6 0 error (1) .43 41 4.0 0 false(no-overflow) 3.0 300 25 1 false(no-overflow) .57 49 6.4 1 false(no-overflow) .15  28 1.1  1 false(no-overflow) .13  28 1.4  1 false(no-overflow) .38  12 4.0  1 false(no-overflow) .17 12 2.2 1 false(no-overflow) 4.7 280 39 1 false(no-overflow) 4.7 260 36 1 false(no-overflow) 4.7 280 39 1
recursive-simple/sum_non_eq_false-no-overflow.c error (5) .12  22 .69 0 false(no-overflow) .26 33 2.1 1 error (1) .51 42 4.5 0 error (1) .47 41 4.1 0 false(no-overflow) 2.9 270 20 1 false(no-overflow) .56 49 6.4 1 false(no-overflow) .21  28 1.7  1 false(no-overflow) .21  28 1.7  1 false(no-overflow) .41  12 4.4  1 false(no-overflow) .19 12 2.0 1 false(no-overflow) 4.8 280 40 1 false(no-overflow) 4.7 260 37 1 false(no-overflow) 4.7 290 38 1
recursive-simple/sum_non_false-no-overflow.c error (5) .10  22 .66 0 false(no-overflow) .24 33 2.2 1 error (1) .47 41 4.4 0 error (1) .44 41 4.3 0 false(no-overflow) 2.7 270 26 1 false(no-overflow) .57 49 8.8 1 false(no-overflow) .18  28 1.9  1 false(no-overflow) .22  28 1.8  1 false(no-overflow) .47  12 6.2  1 false(no-overflow) .17 12 1.9 1 false(no-overflow) 5.2 300 46 1 false(no-overflow) 5.8 330 49 1 false(no-overflow) 5.4 310 40 1
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error (5) .12  22 .67 0 error (42) 870    5200 5200   0 error (1) .47 41 4.2 0 error (1) .42 40 3.6 0 true 3.0 270 28 2 unknown 1.5  49 16   0 timeout 900     1200 9500    0 timeout 900     1200 11000    0 unknown 900     690 10000    0 true .14 11 1.4 2 true 4.2 250 38 2 true 4.1 250 32 2 true 4.2 250 32 2
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c error (5) .089 22 .73 0 error (42) 870    5200 5900   0 error (1) .49 45 4.4 0 error (1) .45 40 4.2 0 true 3.0 290 30 2 unknown 1.5  49 17   0 timeout 900     1200 9200    0 timeout 900     1200 12000    0 unknown 900     660 12000    0 true .15 11 1.4 2 true 4.2 250 34 2 true 4.4 250 39 2 true 4.1 240 35 2
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error (5) .10  22 .73 0 error (42) 870    5200 5700   0 error (1) .48 40 4.0 0 error (1) .43 40 3.8 0 true 2.9 270 27 2 unknown 1.5  49 17   0 timeout 900     1200 9500    0 timeout 900     1200 10000    0 unknown 900     700 11000    0 true .15 11 1.4 2 true 4.0 240 33 2 true 4.1 250 32 2 true 4.1 250 40 2
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error (5) .10  22 .75 0 error (42) 870    5200 4800   0 error (1) .49 41 4.4 0 error (1) .48 40 4.1 0 true 2.8 270 23 2 unknown 1.5  49 20   0 timeout 900     1200 9500    0 timeout 900     1200 10000    0 unknown 890     660 8300    0 true .15 11 1.4 2 true 4.1 250 39 2 true 4.1 240 36 2 true 4.2 250 34 2
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error (5) .098 22 .65 0 error (42) 870    9200 4300   0 error (1) .46 43 4.5 0 error (1) .45 40 4.1 0 true 2.8 270 27 2 unknown 1.4  49 17   0 timeout 900     1200 9900    0 timeout 900     1200 9900    0 unknown 890     1200 8500    0 true .13 11 1.3 2 true 4.0 230 35 2 true 4.2 240 33 2 true 4.1 250 36 2
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c error (5) .11  22 .64 0 error (42) 880    5200 7500   0 error (1) .50 42 4.2 0 error (1) .45 42 4.0 0 true 3.7 290 32 2 false(no-overflow) .53 49 5.9 -16 timeout 900     460 11000    0 timeout 900     470 11000    0 false(no-overflow) .38  12 4.2  -16 timeout (timeout) 900    2300 12000   0 true 6.2 310 53 2 true 6.3 350 47 2 true 7.8 370 62 2
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error (5) .11  22 .73 0 error (42) 870    5200 7600   0 error (1) .50 41 4.3 0 error (1) .44 38 3.9 0 true 3.7 290 31 2 false(no-overflow) .56 49 7.0 -16 timeout 900     460 11000    0 timeout 900     470 11000    0 false(no-overflow) .36  12 5.1  -16 timeout (timeout) 900    2300 9300   0 true 6.0 310 52 2 true 6.5 350 52 2 true 8.1 370 63 2
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error (5) .12  22 .66 0 error (42) 880    6100 5000   0 error (1) .47 41 4.6 0 error (1) .45 40 4.2 0 true 4.5 300 40 2 false(no-overflow) .56 49 6.3 -16 timeout 900     470 12000    0 timeout 900     470 11000    0 false(no-overflow) .37  12 5.6  -16 timeout (timeout) 900    2500 9100   0 true 5.9 300 55 2 true 6.7 360 51 2 true 8.1 380 68 2
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c error (5) .089 22 .64 0 out of memory 640    15000 3900   0 error (1) .49 40 4.2 0 error (1) .42 38 3.7 0 true 2.8 260 24 2 unknown 1.2  49 16   0 timeout 900     1100 9900    0 timeout 900     1100 11000    0 unknown 890     1000 8900    0 true .15 11 1.3 2 true 4.1 250 35 2 true 4.2 240 37 2 true 4.0 250 36 2
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c error (5) .11  22 .75 0 out of memory 660    15000 3800   0 error (1) .45 41 4.0 0 error (1) .41 40 3.8 0 true 2.9 290 25 2 unknown 1.2  49 15   0 timeout 900     1100 8700    0 timeout 900     1100 9600    0 unknown 890     1100 9100    0 true .15 11 1.5 2 true 4.3 240 35 2 true 4.2 240 35 2 true 4.2 240 32 2
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c error (5) .082 22 .76 0 out of memory 560    15000 5600   0 error (1) .50 41 4.4 0 error (1) .47 40 4.0 0 true 2.7 260 25 2 unknown 1.2  49 13   0 timeout 900     1100 10000    0 timeout 900     1100 11000    0 unknown 890     1100 9600    0 true .13 11 1.2 2 true 4.1 240 38 2 true 4.0 240 38 2 true 3.9 250 33 2
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c error (5) .098 22 .64 0 out of memory 670    15000 3700   0 error (1) .45 40 4.4 0 error (1) .46 40 4.1 0 true 3.0 300 25 2 unknown 1.2  49 13   0 timeout 900     1100 12000    0 timeout 900     1100 12000    0 unknown 890     1000 8100    0 true .15 11 1.4 2 true 4.1 240 37 2 true 3.9 240 34 2 true 4.1 240 37 2
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c error (5) .097 22 .63 0 out of memory 650    15000 3600   0 error (1) .48 42 4.7 0 error (1) .43 38 3.6 0 true 3.0 290 24 2 unknown 1.2  49 14   0 timeout 900     1100 11000    0 timeout 900     1100 11000    0 unknown 900     1100 8800    0 true .13 11 1.5 2 true 4.1 240 34 2 true 4.2 240 36 2 true 4.1 250 34 2
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c error (5) .095 22 .86 0 out of memory 660    15000 3400   0 error (1) .49 40 4.6 0 error (1) .42 40 4.7 0 true 2.8 270 25 2 unknown 1.2  49 13   0 timeout 900     1100 10000    0 timeout 900     1100 9700    0 unknown 900     1000 9600    0 true .15 11 1.5 2 true 4.2 250 35 2 true 3.9 230 32 2 true 4.2 250 37 2
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c error (5) .095 22 .70 0 out of memory 780    15000 6300   0 error (1) .48 41 4.5 0 error (1) .44 40 3.5 0 true 2.8 270 27 2 unknown 1.2  49 14   0 timeout 900     1000 9300    0 timeout 900     1000 10000    0 unknown 900     740 9200    0 true .16 11 1.3 2 true 3.8 240 34 2 true 4.0 240 34 2 true 4.3 250 31 2
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c error (5) .10  22 .78 0 out of memory 870    15000 4000   0 error (1) .47 43 4.6 0 error (1) .45 40 4.2 0 true 2.8 270 23 2 unknown 1.2  49 14   0 timeout 900     1000 9100    0 timeout 900     1000 12000    0 unknown 890     730 8800    0 true .13 11 1.4 2 true 3.9 240 32 2 true 4.0 250 35 2 true 4.2 250 38 2
bitvector/byte_add_1_false-no-overflow.i false(no-overflow) .34  31 4.2  1 false(no-overflow) .66 33 6.1 0 error (1) .46 42 4.5 0 error (1) .44 40 3.7 0 false(no-overflow) 5.9 320 55 1 unknown 1.8  100 23   0 false(no-overflow) 1.1   29 11    1 false(no-overflow) 1.1   29 11    1 true 4.1   13 49    -32 false(no-overflow) .25 12 2.7 1 error 25   650 250 0 timeout 900   1200 11000 0 error 110   4000 1100 0
bitvector/byte_add_2_false-no-overflow.i false(no-overflow) .36  31 3.5  1 false(no-overflow) .66 34 6.6 0 error (1) .48 40 4.4 0 error (1) .43 40 4.0 0 false(no-overflow) 6.4 330 55 1 unknown 1.8  100 21   0 false(no-overflow) .98  29 7.9  1 false(no-overflow) 1.1   29 9.6  1 true 4.1   13 49    -32 false(no-overflow) .25 12 2.2 1 error 38   800 370 0 timeout 900   1300 12000 0 error 230   4600 2600 0
bitvector/byte_add_false-no-overflow.i false(no-overflow) .36  31 4.0  1 false(no-overflow) .68 33 5.9 0 error (1) .47 41 4.2 0 error (1) .46 41 4.2 0 false(no-overflow) 6.8 350 57 1 unknown 2.1  110 23   0 false(no-overflow) 1.3   29 12    1 false(no-overflow) 1.4   29 9.9  1 true 39     17 440    -32 false(no-overflow) .28 13 3.4 1 error 69   810 790 0 timeout 900   1200 12000 0 error 160   2700 1800 0
bitvector/jain_1_false-no-overflow.i false(no-overflow) .093 22 .79 1 false(no-overflow) .24 33 1.8 1 error (1) .47 43 4.3 0 error (1) .46 40 4.3 0 false(no-overflow) 2.8 280 29 1 false(no-overflow) .56 75 6.5 1 false(no-overflow) .080 28 1.0  1 false(no-overflow) .10  28 .83 1 false(no-overflow) .44  12 5.1  1 false(no-overflow) .19 12 1.7 1 false(no-overflow) 4.2 250 37 1 false(no-overflow) 4.4 250 35 1 false(no-overflow) 4.2 240 38 1
bitvector/jain_2_false-no-overflow.i false(no-overflow) .14  23 .86 1 false(no-overflow) .23 33 2.5 1 error (1) .50 42 4.2 0 error (1) .41 40 4.2 0 false(no-overflow) 2.9 290 24 1 false(no-overflow) .63 75 8.3 1 false(no-overflow) .11  28 .88 1 false(no-overflow) .13  28 .87 1 false(no-overflow) .70  12 9.5  1 false(no-overflow) .20 12 2.0 1 false(no-overflow) 4.1 240 34 1 false(no-overflow) 4.1 250 32 1 false(no-overflow) 4.2 240 39 1
bitvector/jain_4_false-no-overflow.i false(no-overflow) .13  24 .94 1 false(no-overflow) .24 34 2.5 1 error (1) .49 41 4.0 0 error (1) .42 40 4.0 0 false(no-overflow) 2.9 280 29 1 false(no-overflow) 29    80 330   1 false(no-overflow) .088 28 .91 1 false(no-overflow) .11  28 1.2  1 false(no-overflow) .59  12 8.2  1 false(no-overflow) .18 12 2.2 1 false(no-overflow) 4.2 240 33 1 false(no-overflow) 4.3 250 37 1 false(no-overflow) 4.4 250 40 1
bitvector/jain_5_false-no-overflow.i timeout 900     1100 8900    0 out of memory 370    15000 5400   0 error (1) .48 40 4.2 0 error (1) .41 40 3.5 0 timeout 900   3900 8100 0 unknown 900    2300 11000   0 timeout 900     12000 8900    0 timeout 900     12000 9600    0 false(no-overflow) 2.3   11 29    1 false(no-overflow) .50 40 8.0 1 timeout 900   5200 12000 0 timeout 900   6000 13000 0 timeout 900   1500 13000 0
bitvector/jain_6_false-no-overflow.i false(no-overflow) .13  26 .98 1 false(no-overflow) .26 34 2.4 1 error (1) .48 40 4.5 0 error (1) .44 40 3.8 0 false(no-overflow) 2.9 290 26 1 false(no-overflow) 24    80 320   1 false(no-overflow) .12  28 .81 1 false(no-overflow) .14  28 1.2  1 false(no-overflow) .72  12 8.0  1 false(no-overflow) .19 12 1.8 1 false(no-overflow) 4.3 250 37 1 false(no-overflow) 6.6 350 51 1 false(no-overflow) 4.4 250 38 1
bitvector/jain_7_false-no-overflow.i false(no-overflow) .13  24 .93 1 false(no-overflow) .27 33 2.2 1 error (1) .46 40 4.1 0 error (1) .46 40 4.8 0 false(no-overflow) 2.8 280 24 1 false(no-overflow) 93    97 1300   1 false(no-overflow) .091 28 1.1  1 false(no-overflow) .13  28 1.1  1 false(no-overflow) .70  12 8.5  1 false(no-overflow) .19 12 1.9 1 false(no-overflow) 4.2 250 35 1 false(no-overflow) 4.3 250 34 1 false(no-overflow) 4.4 250 37 1
bitvector/modulus_false-no-overflow.i false(no-overflow) .15  26 1.1  1 false(no-overflow) .24 33 2.0 1 error (1) .49 42 4.9 0 error (1) .42 40 4.9 0 false(no-overflow) 2.6 270 21 1 false(no-overflow) .50 100 5.3 1 false(no-overflow) .16  28 2.0  1 false(no-overflow) .18  28 1.6  1 false(no-overflow) .35  12 4.5  1 false(no-overflow) .18 11 2.4 1 error 4.2 240 36 0 error 4.3 250 36 0 error 4.4 250 30 0
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true .12  24 .92 2 true .86 34 8.4 2 error (1) .48 41 4.7 0 error (1) .46 40 4.3 0 true 3.8 310 36 2 unknown 1.9  100 21   0 true .13  27 1.7  2 true .098 27 1.0  2 true 4.1   13 48    2 true .33 12 4.3 2 true 5.0 280 41 2 true 7.4 370 61 2 true 5.1 280 43 2
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true .12  24 1.0  2 true .86 33 7.8 2 error (1) .49 41 4.9 0 error (1) .46 40 4.5 0 true 3.4 280 31 2 unknown 1.8  100 23   0 true .14  27 1.6  2 true .12  27 1.0  2 true 4.1   13 55    2 true .36 12 4.1 2 true 5.5 290 45 2 true 7.3 370 60 2 true 5.5 280 40 2
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true .10  24 1.0  2 true .88 33 8.8 2 error (1) .47 41 4.2 0 error (1) .47 41 4.6 0 true 3.5 280 32 2 unknown 2.0  110 25   0 true .21  27 2.3  2 true .10  27 1.1  2 true 38     18 460    2 true .84 13 10   2 true 5.1 290 41 2 true 7.4 370 59 2 true 5.0 280 37 2
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true .12  25 1.1  2 true .53 35 5.4 2 error (1) .48 41 4.2 0 error (1) .44 40 3.5 0 true 2.8 280 25 2 unknown 500    99 6600   0 true .56  29 7.4  2 true .35  27 4.7  2 true .66  12 8.4  2 true .31 12 4.3 2 true 5.5 310 44 2 true 5.2 300 43 2 true 5.5 330 45 2
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true .11  24 .89 2 true 1.6  42 19   2 error (1) .52 40 4.1 0 error (1) .41 40 3.9 0 true 2.8 270 24 2 unknown 20    75 270   0 true 9.9   43 110    2 true .29  26 3.0  2 true 28     18 380    2 true 21    16 260   2 true 5.5 290 46 2 true 5.7 330 45 2 true 5.4 280 39 2
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true .096 23 1.2  2 true 1.6  42 17   2 error (1) .46 40 4.4 0 error (1) .45 40 4.3 0 true 2.7 270 25 2 unknown 21    75 250   0 true 9.9   43 120    2 true .26  27 3.2  2 true 30     17 380    2 true 25    16 340   2 true 5.3 290 44 2 true 5.9 330 49 2 true 5.2 280 38 2
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true .56  33 6.1  2 true .81 33 7.0 2 error (1) .47 41 4.6 0 error (1) .47 41 3.9 0 true 2.7 270 24 2 unknown 500    110 7100   0 true .12  26 .72 2 true .15  26 1.7  2 unknown .078 11 .36 0 true .17 11 1.7 2 true 11   540 92 2 true 33   1100 360 2 true 19   640 170 2
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true .12  24 .95 2 true 1.6  33 16   2 error (1) .46 40 4.7 0 error (1) .43 40 4.8 0 true 2.5 270 23 2 unknown 1.4  76 16   0 true .11  26 .96 2 true .078 26 .74 2 true .37  11 3.7  2 true .15 11 1.6 2 true 4.3 250 34 2 true 4.2 250 39 2 true 4.2 250 35 2
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i true .086 22 .77 2 error (42) 870    910 4200   0 error (1) .47 40 4.5 0 error (1) .45 40 4.1 0 true 2.6 280 23 2 unknown 1.2  75 16   0 timeout 900     1200 11000    0 true .079 26 .77 2 unknown 900     92 9600    0 true .15 11 1.5 2 true 4.2 250 35 2 true 3.9 230 32 2 true 4.2 250 35 2
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i true .096 22 .64 2 error (42) 870    1300 4700   0 error (1) .48 43 5.1 0 error (1) .46 40 4.3 0 true 2.6 270 26 2 unknown 1.2  75 13   0 timeout 900     790 10000    0 true .12  26 .76 2 unknown 900     120 7600    0 true .14 11 1.5 2 true 6.6 340 48 2 true 4.2 240 38 2 true 4.1 250 31 2
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i true .096 22 .73 2 error (42) 870    1600 5300   0 error (1) .49 40 4.3 0 error (1) .47 40 4.1 0 true 2.6 270 24 2 unknown 1.2  75 15   0 timeout 900     730 9800    0 true .094 26 .96 2 unknown 890     120 12000    0 true .14 11 1.5 2 true 4.0 240 33 2 true 3.9 240 31 2 true 3.9 230 32 2
bitvector/jain_5_true-unreach-call_true-no-overflow.i true .099 22 .74 2 out of memory 380    15000 4500   0 error (1) .46 41 4.3 0 error (1) .44 40 3.6 0 true 2.5 270 23 2 unknown 1.2  75 13   0 timeout 900     11000 10000    0 true .089 26 .74 2 unknown 890     11 11000    0 true .13 11 1.3 2 true 4.2 250 40 2 true 4.4 250 33 2 true 4.2 250 34 2
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i true .12  23 .72 2 error (42) 870    1600 4300   0 error (1) .49 41 4.6 0 error (1) .43 40 3.4 0 true 2.6 270 26 2 unknown 1.2  75 13   0 timeout 900     730 8900    0 true .11  26 .88 2 false(no-overflow) .48  12 5.7  -16 true .15 11 1.5 2 true 4.1 240 34 2 true 4.1 240 33 2 true 4.1 240 36 2
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i true .10  23 .80 2 error (42) 870    1600 3700   0 error (1) .45 40 3.6 0 error (1) .44 40 3.6 0 true 2.7 270 24 2 unknown 1.2  75 13   0 timeout 900     1000 12000    0 true .080 26 .80 2 false(no-overflow) .49  12 6.5  -16 true .15 11 1.6 2 true 4.0 240 32 2 true 4.1 250 36 2 true 4.0 240 33 2
bitvector/modulus_true-unreach-call_true-no-overflow.i true .13  28 .97 1 true 120    1000 660   1 error (1) .50 41 4.8 0 error (1) .44 40 4.2 0 true 2.7 270 25 1 unknown 900    630 6900   0 true 74     290 910    1 true .14  26 1.2  1 true 790     64 12000    1 true 660    62 8800   1 error 4.3 240 36 0 error 4.3 250 35 0 error 4.3 250 34 0
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true .10  22 .80 1 true 1.2  33 12   1 error (1) .49 41 3.9 0 error (1) .47 41 4.0 0 true 2.8 270 25 1 unknown 1.4  75 15   0 true .092 26 .98 1 true .11  26 .90 1 true .33  11 3.9  1 true .17 11 1.8 1 error 4.2 250 35 0 error 4.3 250 38 0 error 4.3 250 36 0
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true .11  22 .80 1 true 1.2  33 12   1 error (1) .49 40 4.9 0 error (1) .44 40 4.0 0 true 3.0 270 24 1 unknown 1.4  75 16   0 true .11  26 1.0  1 true .087 26 .75 1 unknown .30  11 3.5  0 true .99 13 9.3 1 error 4.5 250 32 0 error 4.1 250 35 0 error 4.0 240 33 0
bitvector/parity_true-unreach-call_true-no-overflow.i true .10  22 .89 2 true 2.5  34 25   2 error (1) .50 41 4.1 0 error (1) .40 38 3.4 0 true 2.8 260 24 2 unknown 1.4  76 19   0 true .82  26 9.4  2 true .10  26 .84 2 true 9.4   13 120    2 true .13 11 1.5 2 true 4.3 250 35 2 true 4.1 240 35 2 true 4.2 250 34 2
bitvector/sum02_false-unreach-call_true-no-overflow.i true .12  25 .71 2 error (42) 870    6800 5100   0 error (1) .48 40 3.6 0 error (1) .44 40 3.6 0 true 2.8 270 24 2 unknown 1.2  75 13   0 timeout 900     1400 9700    0 true .093 26 .77 2 unknown 900     670 11000    0 true .13 11 1.4 2 true 4.1 240 33 2 true 4.3 240 36 2 true 4.3 240 35 2
bitvector/sum02_true-unreach-call_true-no-overflow.i true .11  24 1.0  2 error (42) 870    6400 3800   0 error (1) .48 40 4.0 0 error (1) .45 40 3.4 0 true 2.7 270 24 2 unknown 1.2  75 17   0 timeout 900     1400 11000    0 true .074 26 .89 2 unknown .065 11 .53 0 true .15 11 1.5 2 true 4.1 240 34 2 true 4.3 240 34 2 true 4.2 250 34 2
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
total 78 910    2900 8900   46 78 37000   280000 210000 41 78 37 3200 340 0 78 35 3100 310 0 78 13000 80000 150000 103 78 12000   280000 140000 -35 78 38000   250000 400000 44 78 30000   230000 340000 60 78 34000   20000 410000 -139 78 21000   20000 280000 87 78 14000 130000 180000 97 78 21000 84000 280000 89 78 14000 150000 150000 97
    correct results 26 4.1  640 38   43 25 16   850 160 36 0 0 56 840 16000 7600 95 13 150   850 2000 13 28 28   800 300 39 36 8.2 980 78 55 24 120   300 1600 33 50 56   600 710 82 54 310 19000 2700 95 51 290 16000 2500 89 53 300 15000 2500 93
        correct true 17 2.3  410 20   34 11 13   390 130 22 0 0 39 790 11000 7100 78 0 11 22   330 250 22 19 2.5 500 26 38 9 120   130 1500 18 32 52   360 670 64 41 250 15000 2200 82 38 230 12000 2000 76 40 240 12000 2000 80
        correct false 9 1.8  240 17   9 14 3.6 470 31 14 0 0 17 59 4900 510 17 13 150   850 2000 13 17 5.4 480 49 17 17 5.7 480 52 17 15 9.0 180 110 15 18 3.8 240 44 18 13 60 3500 490 13 13 61 3500 510 13 13 59 3400 500 13
    correct-unconfimed results 3 .34 73 2.6 3 8 130   1300 760 5 0 0 8 30 2300 280 8 0 5 78   390 960 5 5 4.3 130 58 5 4 800   100 12000 4 5 660   110 8800 5 2 120 3200 1100 2 0 4 420 9400 4100 4
        correct-unconfirmed true 3 .34 73 2.6 3 5 130   1200 740 5 0 0 8 30 2300 280 8 0 5 78   390 960 5 5 4.3 130 58 5 4 800   100 12000 4 5 660   110 8800 5 2 120 3200 1100 2 0 4 420 9400 4100 4
        correct-unconfirmed false 0 3 2.0 100 19 0 0 0 0 0 0 0 0 0 0 0 0
    incorrect results 0 0 0 0 0 3 1.6 150 19 -48 0 0 8 49   100 560 -176 0 0 0 0
        incorrect true 0 0 0 0 0 0 0 0 3 47   43 540 -96 0 0 0 0
        incorrect false 0 0 0 0 0 3 1.6 150 19 -48 0 0 5 2.1 59 27 -80 0 0 0 0
score (78 tasks, max score: 138) 46 41 0 0 103 -35 44 60 -139 87 97 89 97
Run set 2ls.sv-comp18.NoOverflows-Other cbmc.sv-comp18.NoOverflows-Other cpa-bam-bnb.sv-comp18.NoOverflows-Other cpa-bam-slicing.sv-comp18.NoOverflows-Other cpa-seq.sv-comp18.NoOverflows-Other depthk.sv-comp18.NoOverflows-Other esbmc-incr.sv-comp18.NoOverflows-Other esbmc-kind.sv-comp18.NoOverflows-Other map2check.sv-comp18.NoOverflows-Other symbiotic.sv-comp18.NoOverflows-Other uautomizer.sv-comp18.NoOverflows-Other ukojak.sv-comp18.NoOverflows-Other utaipan.sv-comp18.NoOverflows-Other