Tool ESBMC ESBMC version 4.6.0 64-bit x86_64 linux CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CProver witness2test 0.1 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
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 CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-02 18:23:42 CET 2017-12-02 20:05:51 CET 2017-12-02 20:31:31 CET 2017-12-02 20:34:26 CET 2017-12-02 20:11:47 CET
Run set esbmc-kind.sv-comp18.NoOverflows-Other cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.NoOverflows-Other
Options -s kinduction -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-02_1823.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/esbmc-kind.2017-12-02_1823.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/esbmc-kind.2017-12-02_1823.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2017-12-02_1823.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
recursive/Addition02WithOverflowBug_false-no-overflow.c 1 .16  28 3.3  1 4.7  270 1 5.4   230   1 .63   18    -
recursive/Addition03_false-no-overflow.c 1 .18  28 1.8  1 3.9  260 1 5.9   260   1 .63   18    -
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c 1 .12  28 1.4  1 3.4  260 1 5.6   260   1 .62   18    -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 0 620     15000 7700    - - - 0 .021 4.8
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c 0 630     15000 7700    - - - 0 .024 4.8
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 0 640     15000 7100    - - - 0 .021 4.8
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 0 610     15000 8800    - - - 0 .019 4.9
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 0 580     15000 5800    - - - 0 .018 4.9
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 0 580     15000 7200    - - - 0 .023 4.8
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c 0 570     15000 6000    - - - 0 .027 4.8
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 2 .073 26 .77 - - - 2 4.4   220  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 0 900     1100 10000    - - - 0 .023 4.9
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 0 900     1100 10000    - - - 0 .022 4.8
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 0 900     4400 8600    - - - 0 .024 4.9
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 2 .16  26 1.4  - - - 2 53     4200  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 0 900     11000 11000    - - - 0 .022 4.8
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 0 900     11000 9300    - - - 0 .025 4.8
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 0 900     11000 8600    - - - 0 .025 4.8
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 0 900     9100 10000    - - - 0 .018 4.9
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 0 900     9000 8700    - - - 0 .024 4.8
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 0 380     15000 3900    - - - 0 .019 4.9
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 0 450     15000 6100    - - - 0 .019 4.8
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 0 900     1600 9200    - - - 0 .019 5.0
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 0 900     2300 8300    - - - 0 .023 4.8
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 0 900     5300 6400    - - - 0 .019 4.9
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 1 2.0   27 29    - - - 0 960     2700  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 1 2.0   28 27    - - - 0 960     2600  
recursive-simple/id_b3_o2_false-no-overflow.c 1 .13  28 1.6  1 2.4  260 1 5.1   260   1 .71   18    -
recursive-simple/id_b3_o5_false-no-overflow.c 1 .17  28 1.2  1 4.3  290 1 6.1   260   1 .70   18    -
recursive-simple/id_b5_o10_false-no-overflow.c 1 .13  28 1.4  1 4.3  260 1 5.5   260   1 .66   18    -
recursive-simple/sum_non_eq_false-no-overflow.c 1 .21  28 1.7  1 2.3  260 1 5.8   250   1 .61   18    -
recursive-simple/sum_non_false-no-overflow.c 1 .22  28 1.8  1 4.6  260 1 6.6   260   1 .65   18    -
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 0 900     1200 11000    - - - 0 .020 4.8
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 0 900     1200 12000    - - - 0 .019 4.8
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 0 900     1200 10000    - - - 0 .018 4.8
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 0 900     1200 10000    - - - 0 .018 4.8
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 0 900     1200 9900    - - - 0 .020 4.8
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 0 900     470 11000    - - - 0 .026 4.8
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 0 900     470 11000    - - - 0 .018 4.8
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 0 900     470 11000    - - - 0 .018 5.0
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c 0 900     1100 11000    - - - 0 .024 5.0
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c 0 900     1100 9600    - - - 0 .021 4.9
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c 0 900     1100 11000    - - - 0 .021 5.0
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c 0 900     1100 12000    - - - 0 .018 4.8
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c 0 900     1100 11000    - - - 0 .024 5.0
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c 0 900     1100 9700    - - - 0 .024 4.8
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c 0 900     1000 10000    - - - 0 .024 4.8
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c 0 900     1000 12000    - - - 0 .019 4.8
bitvector/byte_add_1_false-no-overflow.i 1 1.1   29 11    1 9.7  420 -32 17     500   -32 .62   19    -
bitvector/byte_add_2_false-no-overflow.i 1 1.1   29 9.6  1 8.9  360 0 27     610   -32 .78   19    -
bitvector/byte_add_false-no-overflow.i 1 1.4   29 9.9  1 11    380 0 21     560   -32 .61   18    -
bitvector/jain_1_false-no-overflow.i 1 .10  28 .83 1 4.4  270 1 4.9   230   1 .66   18    -
bitvector/jain_2_false-no-overflow.i 1 .13  28 .87 1 4.2  270 1 4.9   230   1 .68   18    -
bitvector/jain_4_false-no-overflow.i 1 .11  28 1.2  1 3.9  270 1 5.2   230   1 .64   18    -
bitvector/jain_5_false-no-overflow.i 0 900     12000 9600    0 .61 44 0 .021 4.8 0 .0015 .27 -
bitvector/jain_6_false-no-overflow.i 1 .14  28 1.2  1 4.6  270 1 6.1   230   1 .74   18    -
bitvector/jain_7_false-no-overflow.i 1 .13  28 1.1  1 2.6  270 1 5.6   230   1 .62   18    -
bitvector/modulus_false-no-overflow.i 1 .18  28 1.6  1 2.2  260 0 6.0   240   1 .63   18    -
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i 2 .098 27 1.0  - - - 2 6.6   270  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i 2 .12  27 1.0  - - - 2 6.6   270  
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i 2 .10  27 1.1  - - - 2 5.9   270  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i 2 .35  27 4.7  - - - 2 6.5   270  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i 2 .29  26 3.0  - - - 2 5.6   260  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i 2 .26  27 3.2  - - - 2 6.9   270  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i 2 .15  26 1.7  - - - 2 12     500  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i 2 .078 26 .74 - - - 2 5.5   210  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i 2 .079 26 .77 - - - 2 5.2   220  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i 2 .12  26 .76 - - - 2 4.6   220  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i 2 .094 26 .96 - - - 2 4.6   210  
bitvector/jain_5_true-unreach-call_true-no-overflow.i 2 .089 26 .74 - - - 2 4.5   210  
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i 2 .11  26 .88 - - - 2 4.8   210  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i 2 .080 26 .80 - - - 2 4.1   220  
bitvector/modulus_true-unreach-call_true-no-overflow.i 1 .14  26 1.2  - - - 0 5.0   240  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i 1 .11  26 .90 - - - 0 5.6   220  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i 1 .087 26 .75 - - - 0 5.0   230  
bitvector/parity_true-unreach-call_true-no-overflow.i 2 .10  26 .84 - - - 2 4.5   230  
bitvector/sum02_false-unreach-call_true-no-overflow.i 2 .093 26 .77 - - - 2 4.2   210  
bitvector/sum02_true-unreach-call_true-no-overflow.i 2 .074 26 .89 - - - 2 5.7   230  
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 78 60 30000   230000 340000 18 17 82 5000 18 -19 140 5100 18 -82 11   310 60 38 2100 15000
    correct results 36 55 8.2 980 78 17 17 81 4900 13 13 73 3200 14 14 9.2 260 19 38 160 8700
        correct true 19 38 2.5 500 26 0 0 0 19 38 160 8700
        correct false 17 17 5.7 480 52 17 17 81 4900 13 13 73 3200 14 14 9.2 260 0
    correct-unconfimed results 5 5 4.3 130 58 0 0 0 0
        correct-unconfirmed true 5 5 4.3 130 58 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0
    incorrect results 0 0 1 -32 17 500 3 -96 2.0 55 0
        incorrect true 0 0 1 -32 17 500 3 -96 2.0 55 0
        incorrect false 0 0 0 0 0
score (78 tasks, max score: 138) 60 17 -19 -82 38
Run set esbmc-kind.sv-comp18.NoOverflows-Other cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.NoOverflows-Other