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 false(no-overflow) 1 wit inspect .16  28 3.3  false(no-overflow) 1 wit inspect 4.7  270 false(no-overflow) 1 wit inspect 5.4   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect .18  28 1.8  false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 5.9   260   false(no-overflow) 1 wit inspect .63   18    - wit inspect
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect .12  28 1.4  false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.6   260   false(no-overflow) 1 wit inspect .62   18    - wit inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 620     15000 7700    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 630     15000 7700    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
recursive/Ackermann03_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 640     15000 7100    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
recursive/Ackermann04_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 610     15000 8800    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 580     15000 5800    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 580     15000 7200    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 570     15000 6000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .027 4.8
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .073 26 .77 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   220  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     1100 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     1100 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900     4400 8600    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .16  26 1.4  - wit inspect - wit inspect - wit inspect true 2 wit inspect 53     4200  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     11000 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     11000 9300    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     11000 8600    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     9100 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     9000 8700    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 380     15000 3900    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory 0 wit inspect 450     15000 6100    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     1600 9200    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     2300 8300    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     5300 6400    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 2.0   27 29    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2700  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 2.0   28 27    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2600  
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) 1 wit inspect .13  28 1.6  false(no-overflow) 1 wit inspect 2.4  260 false(no-overflow) 1 wit inspect 5.1   260   false(no-overflow) 1 wit inspect .71   18    - wit inspect
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) 1 wit inspect .17  28 1.2  false(no-overflow) 1 wit inspect 4.3  290 false(no-overflow) 1 wit inspect 6.1   260   false(no-overflow) 1 wit inspect .70   18    - wit inspect
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) 1 wit inspect .13  28 1.4  false(no-overflow) 1 wit inspect 4.3  260 false(no-overflow) 1 wit inspect 5.5   260   false(no-overflow) 1 wit inspect .66   18    - wit inspect
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) 1 wit inspect .21  28 1.7  false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 5.8   250   false(no-overflow) 1 wit inspect .61   18    - wit inspect
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) 1 wit inspect .22  28 1.8  false(no-overflow) 1 wit inspect 4.6  260 false(no-overflow) 1 wit inspect 6.6   260   false(no-overflow) 1 wit inspect .65   18    - wit inspect
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1200 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1200 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1200 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1200 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1200 9900    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     470 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .026 4.8
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     470 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     470 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1100 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 5.0
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1100 9600    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1100 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 5.0
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1100 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1100 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 5.0
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1100 9700    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1000 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1000 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
bitvector/byte_add_1_false-no-overflow.i false(no-overflow) 1 wit inspect 1.1   29 11    false(no-overflow) 1 wit inspect 9.7  420 true -32 wit inspect 17     500   true -32 wit inspect .62   19    - wit inspect
bitvector/byte_add_2_false-no-overflow.i false(no-overflow) 1 wit inspect 1.1   29 9.6  false(no-overflow) 1 wit inspect 8.9  360 error 0 wit inspect 27     610   true -32 wit inspect .78   19    - wit inspect
bitvector/byte_add_false-no-overflow.i false(no-overflow) 1 wit inspect 1.4   29 9.9  false(no-overflow) 1 wit inspect 11    380 error 0 wit inspect 21     560   true -32 wit inspect .61   18    - wit inspect
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect .10  28 .83 false(no-overflow) 1 wit inspect 4.4  270 false(no-overflow) 1 wit inspect 4.9   230   false(no-overflow) 1 wit inspect .66   18    - wit inspect
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect .13  28 .87 false(no-overflow) 1 wit inspect 4.2  270 false(no-overflow) 1 wit inspect 4.9   230   false(no-overflow) 1 wit inspect .68   18    - wit inspect
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect .11  28 1.2  false(no-overflow) 1 wit inspect 3.9  270 false(no-overflow) 1 wit inspect 5.2   230   false(no-overflow) 1 wit inspect .64   18    - wit inspect
bitvector/jain_5_false-no-overflow.i timeout 0 wit inspect 900     12000 9600    error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .0015 .27 - wit inspect
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect .14  28 1.2  false(no-overflow) 1 wit inspect 4.6  270 false(no-overflow) 1 wit inspect 6.1   230   false(no-overflow) 1 wit inspect .74   18    - wit inspect
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect .13  28 1.1  false(no-overflow) 1 wit inspect 2.6  270 false(no-overflow) 1 wit inspect 5.6   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
bitvector/modulus_false-no-overflow.i false(no-overflow) 1 wit inspect .18  28 1.6  false(no-overflow) 1 wit inspect 2.2  260 error 0 wit inspect 6.0   240   false(no-overflow) 1 wit inspect .63   18    - wit inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .098 27 1.0  - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6   270  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .12  27 1.0  - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6   270  
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .10  27 1.1  - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9   270  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .35  27 4.7  - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5   270  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .29  26 3.0  - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6   260  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect .26  27 3.2  - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.9   270  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .15  26 1.7  - wit inspect - wit inspect - wit inspect true 2 wit inspect 12     500  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect .078 26 .74 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   210  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect .079 26 .77 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   220  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect .12  26 .76 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6   220  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect .094 26 .96 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6   210  
bitvector/jain_5_true-unreach-call_true-no-overflow.i true 2 wit inspect .089 26 .74 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5   210  
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect .11  26 .88 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8   210  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect .080 26 .80 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1   220  
bitvector/modulus_true-unreach-call_true-no-overflow.i true 1 wit inspect .14  26 1.2  - wit inspect - wit inspect - wit inspect error 0 wit inspect 5.0   240  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 1 wit inspect .11  26 .90 - wit inspect - wit inspect - wit inspect error 0 wit inspect 5.6   220  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 1 wit inspect .087 26 .75 - wit inspect - wit inspect - wit inspect error 0 wit inspect 5.0   230  
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect .10  26 .84 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5   230  
bitvector/sum02_false-unreach-call_true-no-overflow.i true 2 wit inspect .093 26 .77 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   210  
bitvector/sum02_true-unreach-call_true-no-overflow.i true 2 wit inspect .074 26 .89 - wit inspect - wit inspect - wit inspect true 2 wit inspect 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