Tool 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* [apollon004; apollon025; apollon077; apollon078; apollon080] [apollon077; apollon078; apollon157] [apollon038; apollon077; apollon078; apollon164] [apollon025; apollon052; 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 10:49:29 CET 2017-12-01 12:01:34 CET 2017-12-01 12:20:33 CET 2017-12-01 12:23:03 CET 2017-12-01 12:03:46 CET
Run set cpa-seq.sv-comp18.NoOverflows-Other cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.NoOverflows-Other
Options -svcomp18 -heap 10000M -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-12-01_1049.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/cpa-seq.2017-12-01_1049.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cpa-seq.2017-12-01_1049.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cpa-seq.2017-12-01_1049.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 2.8 280 25 false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 6.0   260   false(no-overflow) 1 wit inspect .78   18    - wit inspect
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect 3.1 300 29 false(no-overflow) 1 wit inspect 3.9  270 false(no-overflow) 1 wit inspect 3.9   270   false(no-overflow) 1 wit inspect .75   18    - wit inspect
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 22 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 3.7   270   false(no-overflow) 1 wit inspect .59   18    - wit inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   3600 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   4300 9600 - 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   4500 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   5700 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   5700 10000 - 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 timeout 0 wit inspect 900   5700 9100 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 5.0
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 2.8 270 24 - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     4700  
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 2.8 270 26 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   210  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   4100 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 5.0
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   4400 9800 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c true 1 wit inspect 4.4 290 39 - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     4900  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 670   810 6100 - wit inspect - wit inspect - wit inspect true 2 wit inspect 33     3800  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 5.9 310 63 - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     5000  
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 4.2 300 40 - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     5000  
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 4.2 290 42 - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     5300  
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 3.4 280 26 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.6   280  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 3.3 280 29 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7   280  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   1500 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
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 3.4 310 29 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5   270  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 3.5 290 33 - wit inspect - wit inspect - wit inspect true 2 wit inspect 16     510  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   6800 9900 - 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 timeout 0 wit inspect 900   5000 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   4400 9800 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 5.0
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 270 24 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 3.9   280   false(no-overflow) 1 wit inspect .81   18    - wit inspect
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 280 23 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.1   270   false(no-overflow) 1 wit inspect .62   18    - wit inspect
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) 1 wit inspect 3.0 300 25 false(no-overflow) 1 wit inspect 3.8  260 false(no-overflow) 1 wit inspect 5.0   260   false(no-overflow) 1 wit inspect .60   18    - wit inspect
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) 1 wit inspect 2.9 270 20 false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 4.8   270   false(no-overflow) 1 wit inspect .74   19    - wit inspect
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 26 false(no-overflow) 1 wit inspect 4.2  270 false(no-overflow) 1 wit inspect 4.2   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 true 2 wit inspect 3.0 270 28 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4   230  
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.0 290 30 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8   220  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 2.9 270 27 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4   220  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 2.8 270 23 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3   240  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 2.8 270 27 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0   230  
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.7 290 32 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.7   270  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.7 290 31 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8   260  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 4.5 300 40 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8   270  
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 2.8 260 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   210  
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 2.9 290 25 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1   210  
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 2.7 260 25 - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9   220  
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.0 300 25 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7   220  
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.0 290 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9   220  
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 2.8 270 25 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   210  
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 2.8 270 27 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1   220  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 2.8 270 23 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0   220  
bitvector/byte_add_1_false-no-overflow.i false(no-overflow) 1 wit inspect 5.9 320 55 false(no-overflow) 1 wit inspect 6.6  280 error 0 wit inspect 18     580   true -32 wit inspect .89   19    - wit inspect
bitvector/byte_add_2_false-no-overflow.i false(no-overflow) 1 wit inspect 6.4 330 55 false(no-overflow) 1 wit inspect 5.2  280 error 0 wit inspect 24     680   true -32 wit inspect .69   19    - wit inspect
bitvector/byte_add_false-no-overflow.i false(no-overflow) 1 wit inspect 6.8 350 57 false(no-overflow) 1 wit inspect 4.2  290 error 0 wit inspect 17     590   true -32 wit inspect .69   19    - wit inspect
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect 2.8 280 29 false(no-overflow) 1 wit inspect 4.3  270 false(no-overflow) 1 wit inspect 4.1   240   false(no-overflow) 1 wit inspect .78   18    - wit inspect
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect 2.9 290 24 false(no-overflow) 1 wit inspect 2.4  280 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 2.9 280 29 false(no-overflow) 1 wit inspect 2.5  270 false(no-overflow) 1 wit inspect 4.7   240   false(no-overflow) 1 wit inspect .60   18    - wit inspect
bitvector/jain_5_false-no-overflow.i timeout 0 wit inspect 900   3900 8100 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect 2.9 290 26 false(no-overflow) 1 wit inspect 4.2  270 false(no-overflow) 1 wit inspect 5.2   250   false(no-overflow) 1 wit inspect .64   18    - wit inspect
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect 2.8 280 24 false(no-overflow) 1 wit inspect 3.4  270 false(no-overflow) 1 wit inspect 5.4   250   false(no-overflow) 1 wit inspect .65   18    - wit inspect
bitvector/modulus_false-no-overflow.i false(no-overflow) 1 wit inspect 2.6 270 21 false(no-overflow) 1 wit inspect 4.2  260 error 0 wit inspect 4.3   260   false(no-overflow) 1 wit inspect .96   18    - wit inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 3.8 310 36 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   280  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 3.4 280 31 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1   270  
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 3.5 280 32 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.0   270  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.8 280 25 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1   270  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.8 270 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.2   260  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.7 270 25 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   260  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 2.7 270 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.4   500  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.5 270 23 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0   210  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 2.6 280 23 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9   210  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 2.6 270 26 - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9   220  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 2.6 270 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.7   220  
bitvector/jain_5_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.5 270 23 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   210  
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 2.6 270 26 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   220  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 2.7 270 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9   220  
bitvector/modulus_true-unreach-call_true-no-overflow.i true 1 wit inspect 2.7 270 25 - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.7   230  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 1 wit inspect 2.8 270 25 - wit inspect - wit inspect - wit inspect error 0 wit inspect 3.5   230  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 1 wit inspect 3.0 270 24 - wit inspect - wit inspect - wit inspect error 0 wit inspect 5.6   230  
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.8 260 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1   230  
bitvector/sum02_false-unreach-call_true-no-overflow.i true 2 wit inspect 2.8 270 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1   210  
bitvector/sum02_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.7 270 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1   220  
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 103 13000 80000 150000 18 17 67 4600 18 13 120 5500 18 -82 12   320 60 78 5000 39000
    correct results 56 95 840 16000 7600 17 17 66 4600 13 13 60 3400 14 14 10   260 39 78 230 13000
        correct true 39 78 790 11000 7100 0 0 0 39 78 230 13000
        correct false 17 17 59 4900 510 17 17 66 4600 13 13 60 3400 14 14 10   260 0
    correct-unconfimed results 8 8 30 2300 280 0 0 0 0
        correct-unconfirmed true 8 8 30 2300 280 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0
    incorrect results 0 0 0 3 -96 2.3 58 0
        incorrect true 0 0 0 3 -96 2.3 58 0
        incorrect false 0 0 0 0 0
score (78 tasks, max score: 138) 103 17 13 -82 78
Run set cpa-seq.sv-comp18.NoOverflows-Other cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.NoOverflows-Other