Tool ULTIMATE Kojak 0.1.23-3204b741 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-03 11:17:40 CET 2017-12-03 11:52:51 CET 2017-12-03 12:03:01 CET 2017-12-03 12:03:17 CET 2017-12-03 11:54:19 CET
Run set ukojak.sv-comp18.NoOverflows-Other cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.NoOverflows-Other
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-03_1117.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/ukojak.2017-12-03_1117.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/ukojak.2017-12-03_1117.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/ukojak.2017-12-03_1117.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 4.4 250 40 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.8   250   error (2) 0 wit inspect .64   18    - wit inspect
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect 4.5 260 39 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.8   250   error (2) 0 wit inspect .60   18    - wit inspect
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect 4.6 270 42 false(no-overflow) 1 wit inspect 3.0  250 false(no-overflow) 1 wit inspect 5.4   260   true -32 wit inspect .65   18    - wit inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   1700 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   1800 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   1700 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   1700 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   6000 15000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .048 4.8
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   6000 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .040 4.8
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   5800 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 5.0
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 4.2 250 31 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6   230  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   4800 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   5200 9700 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   1300 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   1400 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   1300 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .048 4.9
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   1500 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .032 4.9
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   1600 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 7.0 440 56 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.1   270  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 7.1 430 60 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.3   280  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   2000 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c timeout 0 wit inspect 900   1500 12000 - 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 true 2 wit inspect 8.3 480 70 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3   270  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 14   640 130 - wit inspect - wit inspect - wit inspect true 2 wit inspect 13     510  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   2900 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   4700 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   4600 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) 1 wit inspect 4.5 270 45 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.3   260   true -32 wit inspect .60   18    - wit inspect
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 260 34 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.6   270   true -32 wit inspect .63   18    - wit inspect
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) 1 wit inspect 4.7 260 36 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.8   260   true -32 wit inspect .60   18    - wit inspect
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) 1 wit inspect 4.7 260 37 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.4   260   true -32 wit inspect .62   18    - wit inspect
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) 1 wit inspect 5.8 330 49 false(no-overflow) 1 wit inspect 3.0  260 false(no-overflow) 1 wit inspect 5.6   260   true -32 wit inspect .62   18    - wit inspect
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 4.1 250 32 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   220  
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 4.4 250 39 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1   230  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 4.1 250 32 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5   220  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 4.1 240 36 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   230  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 4.2 240 33 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   220  
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 6.3 350 47 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.7   270  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 6.5 350 52 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.9   260  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 6.7 360 51 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1   270  
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 4.2 240 37 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1   210  
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 4.2 240 35 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5   220  
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 4.0 240 38 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   220  
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.9 240 34 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   210  
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 4.2 240 36 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3   220  
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.9 230 32 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0   220  
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 4.0 240 34 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   210  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 4.0 250 35 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5   220  
bitvector/byte_add_1_false-no-overflow.i timeout 0 wit inspect 900   1200 11000 error (invalid witness file) 0 wit inspect .53 45 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect .0028 .34 - wit inspect
bitvector/byte_add_2_false-no-overflow.i timeout 0 wit inspect 900   1300 12000 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .044 4.9 error (invalid witness file) 0 wit inspect .0040 .29 - wit inspect
bitvector/byte_add_false-no-overflow.i timeout 0 wit inspect 900   1200 12000 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0012 .31 - wit inspect
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect 4.4 250 35 true -32 wit inspect 3.0  250 false(no-overflow) 1 wit inspect 5.0   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect 4.1 250 32 true -32 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.3   230   false(no-overflow) 1 wit inspect .61   19    - wit inspect
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect 4.3 250 37 true -32 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.7   240   false(no-overflow) 1 wit inspect .64   18    - wit inspect
bitvector/jain_5_false-no-overflow.i timeout 0 wit inspect 900   6000 13000 error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .028 5.0 error (invalid witness file) 0 wit inspect .0037 .30 - wit inspect
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect 6.6 350 51 true -32 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.2   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect 4.3 250 34 true -32 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 3.4   240   false(no-overflow) 1 wit inspect .63   18    - wit inspect
bitvector/modulus_false-no-overflow.i error 0 wit inspect 4.3 250 36 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .050 4.8 error (invalid witness file) 0 wit inspect .0046 .26 - wit inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 7.4 370 61 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1   280  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 7.3 370 60 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9   270  
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 7.4 370 59 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1   270  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.2 300 43 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8   270  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.7 330 45 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3   260  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.9 330 49 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6   260  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 33   1100 360 - wit inspect - wit inspect - wit inspect true 2 wit inspect 14     500  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect 4.2 250 39 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3   210  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 3.9 230 32 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0   210  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 4.2 240 38 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5   210  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 3.9 240 31 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   220  
bitvector/jain_5_true-unreach-call_true-no-overflow.i true 2 wit inspect 4.4 250 33 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1   210  
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 4.1 240 33 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1   210  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 4.1 250 36 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0   210  
bitvector/modulus_true-unreach-call_true-no-overflow.i error 0 wit inspect 4.3 250 35 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i error 0 wit inspect 4.3 250 38 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i error 0 wit inspect 4.1 250 35 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .027 4.8
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect 4.1 240 35 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   230  
bitvector/sum02_false-unreach-call_true-no-overflow.i true 2 wit inspect 4.3 240 36 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   220  
bitvector/sum02_true-unreach-call_true-no-overflow.i true 2 wit inspect 4.3 240 34 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1   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 89 21000 84000 280000 18 -152 44 3600 18 13 65 3300 18 -187 8.1 240 60 76 210 9600
    correct results 51 89 290 16000 2500 8 8 26 2100 13 13 65 3300 5 5 3.1 92 38 76 210 9500
        correct true 38 76 230 12000 2000 0 0 0 38 76 210 9500
        correct false 13 13 61 3500 510 8 8 26 2100 13 13 65 3300 5 5 3.1 92 0
    incorrect results 0 5 -160 16 1300 0 6 -192 3.7 110 0
        incorrect true 0 5 -160 16 1300 0 6 -192 3.7 110 0
        incorrect false 0 0 0 0 0
score (78 tasks, max score: 138) 89 -152 13 -187 76
Run set ukojak.sv-comp18.NoOverflows-Other cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.NoOverflows-Other