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] 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-02 06:23:16 CET 2017-12-02 08:10:39 CET 2017-12-02 08:34:53 CET 2017-12-02 08:39:22 CET 2017-12-02 08:15:43 CET
Run set esbmc-incr.sv-comp18.NoOverflows-Other cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.NoOverflows-Other
Options -s incr -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-02_0623.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-incr.2017-12-02_0623.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/esbmc-incr.2017-12-02_0623.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-incr.2017-12-02_0623.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 .22  28 1.8  false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 7.3   260   false(no-overflow) 1 wit inspect .78   18    - wit inspect
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect .17  28 1.7  false(no-overflow) 1 wit inspect 4.9  270 false(no-overflow) 1 wit inspect 4.9   230   false(no-overflow) 1 wit inspect .64   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 4.4  260 false(no-overflow) 1 wit inspect 5.5   260   false(no-overflow) 1 wit inspect .63   18    - wit inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 440     15000 5400    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 450     15000 5100    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive/Ackermann03_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 460     15000 5000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
recursive/Ackermann04_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 450     15000 4700    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .026 4.8
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 810     15000 9200    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 840     15000 8100    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 830     15000 9000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .081 26 .85 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   210  
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 5.0
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     1100 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 5.0
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900     8800 7500    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .15  26 1.4  - wit inspect - wit inspect - wit inspect true 2 wit inspect 49     4000  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     8800 7000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     8800 6700    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     8800 7100    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.9
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     6400 7800    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     6300 7100    - 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 700     15000 6700    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory 0 wit inspect 220     15000 2400    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     890 8600    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     1200 9200    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900     13000 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 1.9   28 25    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2800  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 1.9   27 24    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2700  
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) 1 wit inspect .16  28 .91 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 6.7   260   false(no-overflow) 1 wit inspect .62   18    - wit inspect
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) 1 wit inspect .13  28 1.3  false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.3   260   false(no-overflow) 1 wit inspect .73   18    - wit inspect
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) 1 wit inspect .15  28 1.1  false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 7.2   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 3.5  260 false(no-overflow) 1 wit inspect 5.4   260   false(no-overflow) 1 wit inspect .65   19    - wit inspect
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) 1 wit inspect .18  28 1.9  timeout 0 wit inspect 91    670 false(no-overflow) 1 wit inspect 5.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 9500    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1200 9200    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1200 9500    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 5.0
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1200 9500    - 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 .024 4.8
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     460 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     460 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     470 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1100 9900    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1100 8700    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1100 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 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 .024 5.0
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 .020 4.9
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1100 10000    - 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 9300    - 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 9100    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 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 12    420 true -32 wit inspect 13     510   true -32 wit inspect .61   18    - wit inspect
bitvector/byte_add_2_false-no-overflow.i false(no-overflow) 1 wit inspect .98  29 7.9  false(no-overflow) 1 wit inspect 8.2  370 error 0 wit inspect 24     600   true -32 wit inspect .66   18    - wit inspect
bitvector/byte_add_false-no-overflow.i false(no-overflow) 1 wit inspect 1.3   29 12    false(no-overflow) 1 wit inspect 11    420 error 0 wit inspect 25     540   true -32 wit inspect .62   19    - wit inspect
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect .080 28 1.0  false(no-overflow) 1 wit inspect 3.8  280 false(no-overflow) 1 wit inspect 4.7   230   false(no-overflow) 1 wit inspect .61   18    - wit inspect
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect .11  28 .88 false(no-overflow) 1 wit inspect 4.0  280 false(no-overflow) 1 wit inspect 6.1   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect .088 28 .91 false(no-overflow) 1 wit inspect 4.0  270 false(no-overflow) 1 wit inspect 5.2   230   false(no-overflow) 1 wit inspect .82   18    - wit inspect
bitvector/jain_5_false-no-overflow.i timeout 0 wit inspect 900     12000 8900    error (invalid witness file) 0 wit inspect .66 42 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .0014 .28 - wit inspect
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect .12  28 .81 false(no-overflow) 1 wit inspect 4.7  270 false(no-overflow) 1 wit inspect 5.3   240   false(no-overflow) 1 wit inspect .67   18    - wit inspect
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect .091 28 1.1  false(no-overflow) 1 wit inspect 4.2  280 false(no-overflow) 1 wit inspect 4.7   240   false(no-overflow) 1 wit inspect .81   18    - wit inspect
bitvector/modulus_false-no-overflow.i false(no-overflow) 1 wit inspect .16  28 2.0  false(no-overflow) 1 wit inspect 3.5  260 error 0 wit inspect 6.3   250   false(no-overflow) 1 wit inspect .74   18    - wit inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .13  27 1.7  - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5   280  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .14  27 1.6  - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4   270  
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .21  27 2.3  - 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 .56  29 7.4  - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.0   270  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 9.9   43 110    - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.3   270  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 9.9   43 120    - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7   260  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .12  26 .72 - wit inspect - wit inspect - wit inspect true 2 wit inspect 13     480  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect .11  26 .96 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1   210  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900     1200 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900     790 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .029 4.8
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900     730 9800    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 5.0
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     11000 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900     730 8900    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900     1000 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 5.0
bitvector/modulus_true-unreach-call_true-no-overflow.i true 1 wit inspect 74     290 910    - wit inspect - wit inspect - wit inspect error 0 wit inspect 5.6   230  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 1 wit inspect .092 26 .98 - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.8   230  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 1 wit inspect .11  26 1.0  - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.5   230  
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect .82  26 9.4  - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   230  
bitvector/sum02_false-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     1400 9700    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     1400 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
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 44 38000   250000 400000 18 16 170 5400 18 -19 140 5100 18 -82 11   310 60 22 2100 13000
    correct results 28 39 28   800 300 16 16 82 4700 13 13 74 3200 14 14 9.6 260 11 22 120 6700
        correct true 11 22 22   330 250 0 0 0 11 22 120 6700
        correct false 17 17 5.4 480 49 16 16 82 4700 13 13 74 3200 14 14 9.6 260 0
    correct-unconfimed results 5 5 78   390 960 0 0 0 0
        correct-unconfirmed true 5 5 78   390 960 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0
    incorrect results 0 0 1 -32 13 510 3 -96 1.9 55 0
        incorrect true 0 0 1 -32 13 510 3 -96 1.9 55 0
        incorrect false 0 0 0 0 0
score (78 tasks, max score: 138) 44 16 -19 -82 22
Run set esbmc-incr.sv-comp18.NoOverflows-Other cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.NoOverflows-Other