Tool CBMC 5.8 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* [apollon058; apollon077; apollon078; apollon114] [apollon077; apollon078; apollon135; apollon137; apollon144] apollon* [apollon039; apollon060; apollon077; apollon078]
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: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 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-01 11:16:27 CET 2017-12-01 12:31:21 CET 2017-12-01 12:51:49 CET 2017-12-01 12:54:09 CET 2017-12-01 12:35:01 CET
Run set cbmc.sv-comp18.NoOverflows-Other cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.NoOverflows-Other
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-12-01_1116.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/cbmc.2017-12-01_1116.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc.2017-12-01_1116.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2017-12-01_1116.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 .28 35 2.1 false(no-overflow) 1 wit inspect 20    460 false(no-overflow) 1 wit inspect 8.8   290   false(no-overflow) 1 wit inspect .66   18    - wit inspect
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 2.2 false(no-overflow) 1 wit inspect 3.9  270 false(no-overflow) 1 wit inspect 8.7   280   false(no-overflow) 1 wit inspect .62   19    - wit inspect
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.5 false(no-overflow) 1 wit inspect 4.3  270 false(no-overflow) 1 wit inspect 5.5   270   false(no-overflow) 1 wit inspect .82   18    - wit inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c error (42) 0 wit inspect 870    330 2900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 870    360 3500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive/Ackermann03_true-unreach-call_true-no-overflow.c error (42) 0 wit inspect 870    350 3400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive/Ackermann04_true-unreach-call_true-no-overflow.c error (42) 0 wit inspect 870    340 3000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.9
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 860    15000 8000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 880    15000 9100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 880    6800 4600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .037 4.9
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .43 33 3.9 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6   230  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 870    2800 6500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 870    2800 7400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c error (42) 0 wit inspect 870    260 3700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 1.3  33 13   - wit inspect - wit inspect - wit inspect true 2 wit inspect 42     3900  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 870    260 3000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 870    250 2500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 870    260 2900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 5.0
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 870    2000 3500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 870    2000 3700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 870    450 2100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c error (42) 0 wit inspect 870    310 4100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 870    5000 4200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 wit inspect 880    7200 5900   - 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 error (42) 0 wit inspect 870    1400 2900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 2.6  36 27   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2900  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 2.6  36 28   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2800  
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) 1 wit inspect .24 33 2.0 false(no-overflow) 1 wit inspect 2.9  260 false(no-overflow) 1 wit inspect 4.0   270   false(no-overflow) 1 wit inspect .60   18    - wit inspect
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 2.1 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 3.9   270   false(no-overflow) 1 wit inspect .79   18    - wit inspect
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) 1 wit inspect .26 33 2.2 false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 3.8   260   false(no-overflow) 1 wit inspect .78   18    - wit inspect
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) 1 wit inspect .26 33 2.1 false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 4.1   270   false(no-overflow) 1 wit inspect .75   18    - wit inspect
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) 1 wit inspect .24 33 2.2 false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 4.6   270   false(no-overflow) 1 wit inspect .77   18    - wit inspect
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    5200 5200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    5200 5900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    5200 5700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    5200 4800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    9200 4300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 5.0
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c error (42) 0 wit inspect 880    5200 7500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    5200 7600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 wit inspect 880    6100 5000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c out of memory 0 wit inspect 640    15000 3900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c out of memory 0 wit inspect 660    15000 3800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c out of memory 0 wit inspect 560    15000 5600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c out of memory 0 wit inspect 670    15000 3700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c out of memory 0 wit inspect 650    15000 3600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c out of memory 0 wit inspect 660    15000 3400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c out of memory 0 wit inspect 780    15000 6300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c out of memory 0 wit inspect 870    15000 4000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
bitvector/byte_add_1_false-no-overflow.i false(no-overflow) 0 wit inspect .66 33 6.1 true -32 wit inspect 27    740 error 0 wit inspect 16     540   true -32 wit inspect .78   19    - wit inspect
bitvector/byte_add_2_false-no-overflow.i false(no-overflow) 0 wit inspect .66 34 6.6 true -32 wit inspect 26    790 error 0 wit inspect 16     650   true -32 wit inspect .86   19    - wit inspect
bitvector/byte_add_false-no-overflow.i false(no-overflow) 0 wit inspect .68 33 5.9 true -32 wit inspect 43    2000 error 0 wit inspect 22     650   true -32 wit inspect .86   19    - wit inspect
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect .24 33 1.8 false(no-overflow) 1 wit inspect 4.0  280 false(no-overflow) 1 wit inspect 3.4   230   false(no-overflow) 1 wit inspect .82   18    - wit inspect
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect .23 33 2.5 false(no-overflow) 1 wit inspect 3.6  340 false(no-overflow) 1 wit inspect 3.6   250   false(no-overflow) 1 wit inspect .80   18    - wit inspect
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect .24 34 2.5 false(no-overflow) 1 wit inspect 3.2  280 false(no-overflow) 1 wit inspect 3.5   230   false(no-overflow) 1 wit inspect .80   18    - wit inspect
bitvector/jain_5_false-no-overflow.i out of memory 0 wit inspect 370    15000 5400   error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0018 .26 - wit inspect
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect .26 34 2.4 false(no-overflow) 1 wit inspect 3.4  280 false(no-overflow) 1 wit inspect 3.9   250   false(no-overflow) 1 wit inspect .68   18    - wit inspect
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect .27 33 2.2 false(no-overflow) 1 wit inspect 3.7  280 false(no-overflow) 1 wit inspect 3.6   240   false(no-overflow) 1 wit inspect .67   18    - wit inspect
bitvector/modulus_false-no-overflow.i false(no-overflow) 1 wit inspect .24 33 2.0 false(no-overflow) 1 wit inspect 2.8  260 error 0 wit inspect 5.9   230   false(no-overflow) 1 wit inspect .64   18    - wit inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .86 34 8.4 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3   270  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .86 33 7.8 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   270  
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .88 33 8.8 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4   270  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .53 35 5.4 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0   260  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.6  42 19   - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5   280  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.6  42 17   - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2   260  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .81 33 7.0 - wit inspect - wit inspect - wit inspect true 2 wit inspect 13     490  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.6  33 16   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   220  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i error (42) 0 wit inspect 870    910 4200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i error (42) 0 wit inspect 870    1300 4700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 5.0
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i error (42) 0 wit inspect 870    1600 5300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
bitvector/jain_5_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 380    15000 4500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i error (42) 0 wit inspect 870    1600 4300   - 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 error (42) 0 wit inspect 870    1600 3700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
bitvector/modulus_true-unreach-call_true-no-overflow.i true 1 wit inspect 120    1000 660   - wit inspect - wit inspect - wit inspect error 0 wit inspect 12     300  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 1 wit inspect 1.2  33 12   - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.9   230  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 1 wit inspect 1.2  33 12   - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.9   230  
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.5  34 25   - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7   220  
bitvector/sum02_false-unreach-call_true-no-overflow.i error (42) 0 wit inspect 870    6800 5100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .035 4.8
bitvector/sum02_true-unreach-call_true-no-overflow.i error (42) 0 wit inspect 870    6400 3800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 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 41 37000   280000 210000 18 -82 160 7500 18 13 120 5500 18 -82 13   310 60 22 2000 13000
    correct results 25 36 16   850 160 14 14 67 4000 13 13 61 3400 14 14 10   260 11 22 100 6700
        correct true 11 22 13   390 130 0 0 0 11 22 100 6700
        correct false 14 14 3.6 470 31 14 14 67 4000 13 13 61 3400 14 14 10   260 0
    correct-unconfimed results 8 5 130   1300 760 0 0 0 0
        correct-unconfirmed true 5 5 130   1200 740 0 0 0 0
        correct-unconfirmed false 3 0 2.0 100 19 0 0 0 0
    incorrect results 0 3 -96 95 3500 0 3 -96 2.5 57 0
        incorrect true 0 3 -96 95 3500 0 3 -96 2.5 57 0
        incorrect false 0 0 0 0 0
score (78 tasks, max score: 138) 41 -82 13 -82 22
Run set cbmc.sv-comp18.NoOverflows-Other cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.NoOverflows-Other