Tool symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 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 04:09:48 CET 2017-12-03 05:12:06 CET 2017-12-03 05:44:30 CET 2017-12-03 05:48:14 CET 2017-12-03 05:20:50 CET
Run set symbiotic.sv-comp18.NoOverflows-Other cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.NoOverflows-Other
Options --witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-03_0409.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/symbiotic.2017-12-03_0409.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/symbiotic.2017-12-03_0409.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2017-12-03_0409.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 .19 12 2.1 false(no-overflow) 1 wit inspect 3.5 260 true -32 wit inspect 4.5 220 false(no-overflow) 1 wit inspect .63 18 - wit inspect
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect .17 12 1.9 false(no-overflow) 1 wit inspect 3.5 260 true -32 wit inspect 5.0 230 false(no-overflow) 1 wit inspect .62 18 - wit inspect
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect .20 12 1.8 false(no-overflow) 1 wit inspect 3.2 260 true -32 wit inspect 4.6 220 false(no-overflow) 1 wit inspect .62 18 - wit inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout (timeout) 0 wit inspect 900    2100 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 5.0
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 0 wit inspect 900    2500 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout (timeout) 0 wit inspect 900    2100 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout (timeout) 0 wit inspect 900    2100 13000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 0 wit inspect 900    29 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 0 wit inspect 900    72 14000   - 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 timeout (timeout) 0 wit inspect 900    63 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .15 11 1.4 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0   220  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 0 wit inspect 900    320 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 0 wit inspect 900    300 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout (timeout) 0 wit inspect 900    220 9700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .18 11 1.7 - wit inspect - wit inspect - wit inspect true 2 wit inspect 39     3800  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 0 wit inspect 900    220 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 5.0
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 0 wit inspect 900    280 12000   - 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 timeout (timeout) 0 wit inspect 900    270 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 0 wit inspect 900    74 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 0 wit inspect 900    74 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 0 wit inspect 900    330 14000   - 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 (timeout) 0 wit inspect 900    44 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 0 wit inspect 900    49 14000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 0 wit inspect 900    29 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 0 wit inspect 900    1200 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect .64 14 8.4 - 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 .71 14 10   - 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 12 2.4 false(no-overflow) 1 wit inspect 3.6 260 true -32 wit inspect 5.6 300 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 .18 12 1.9 false(no-overflow) 1 wit inspect 3.3 260 true -32 wit inspect 4.5 220 false(no-overflow) 1 wit inspect .59 18 - wit inspect
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) 1 wit inspect .17 12 2.2 false(no-overflow) 1 wit inspect 3.4 260 true -32 wit inspect 4.3 220 false(no-overflow) 1 wit inspect .68 18 - wit inspect
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) 1 wit inspect .19 12 2.0 false(no-overflow) 1 wit inspect 3.3 260 true -32 wit inspect 5.1 240 false(no-overflow) 1 wit inspect .62 18 - wit inspect
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) 1 wit inspect .17 12 1.9 false(no-overflow) 1 wit inspect 3.4 270 true -32 wit inspect 4.7 220 false(no-overflow) 1 wit inspect .62 18 - wit inspect
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect .14 11 1.4 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8   230  
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect .15 11 1.4 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6   220  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect .15 11 1.4 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6   230  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect .15 11 1.4 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3   220  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect .13 11 1.3 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5   220  
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900    2300 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900    2300 9300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.9
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900    2500 9100   - 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 true 2 wit inspect .15 11 1.3 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   210  
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect .15 11 1.5 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   220  
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect .13 11 1.2 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0   210  
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect .15 11 1.4 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6   210  
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect .13 11 1.5 - 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 .15 11 1.5 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   210  
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect .16 11 1.3 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   220  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect .13 11 1.4 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1   220  
bitvector/byte_add_1_false-no-overflow.i false(no-overflow) 1 wit inspect .25 12 2.7 false(no-overflow) 1 wit inspect 8.4 400 true -32 wit inspect 7.6 240 true -32 wit inspect .60 18 - wit inspect
bitvector/byte_add_2_false-no-overflow.i false(no-overflow) 1 wit inspect .25 12 2.2 false(no-overflow) 1 wit inspect 8.5 410 true -32 wit inspect 5.8 240 true -32 wit inspect .61 18 - wit inspect
bitvector/byte_add_false-no-overflow.i false(no-overflow) 1 wit inspect .28 13 3.4 false(no-overflow) 1 wit inspect 9.6 400 true -32 wit inspect 5.9 240 true -32 wit inspect .59 18 - wit inspect
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect .19 12 1.7 false(no-overflow) 1 wit inspect 3.7 270 false(no-overflow) 1 wit inspect 5.4 220 false(no-overflow) 1 wit inspect .62 18 - wit inspect
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect .20 12 2.0 false(no-overflow) 1 wit inspect 2.5 270 false(no-overflow) 1 wit inspect 5.1 220 false(no-overflow) 1 wit inspect .59 18 - wit inspect
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect .18 12 2.2 false(no-overflow) 1 wit inspect 3.9 270 false(no-overflow) 1 wit inspect 5.0 230 false(no-overflow) 1 wit inspect .63 18 - wit inspect
bitvector/jain_5_false-no-overflow.i false(no-overflow) 1 wit inspect .50 40 8.0 timeout 0 wit inspect 91   1300 true -32 wit inspect 5.4 260 false(no-overflow) 1 wit inspect .62 18 - wit inspect
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect .19 12 1.8 false(no-overflow) 1 wit inspect 3.9 270 false(no-overflow) 1 wit inspect 4.9 230 false(no-overflow) 1 wit inspect .64 18 - wit inspect
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect .19 12 1.9 false(no-overflow) 1 wit inspect 3.1 270 false(no-overflow) 1 wit inspect 6.1 230 false(no-overflow) 1 wit inspect .93 18 - wit inspect
bitvector/modulus_false-no-overflow.i false(no-overflow) 1 wit inspect .18 11 2.4 false(no-overflow) 1 wit inspect 3.3 260 true -32 wit inspect 5.4 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 .33 12 4.3 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3   280  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .36 12 4.1 - 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 .84 13 10   - 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 .31 12 4.3 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7   270  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 21    16 260   - 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 25    16 340   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1   260  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .17 11 1.7 - wit inspect - wit inspect - wit inspect true 2 wit inspect 10     500  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect .15 11 1.6 - 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 true 2 wit inspect .15 11 1.5 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   210  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect .14 11 1.5 - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9   210  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect .14 11 1.5 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   210  
bitvector/jain_5_true-unreach-call_true-no-overflow.i true 2 wit inspect .13 11 1.3 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   210  
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect .15 11 1.5 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9   210  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect .15 11 1.6 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6   220  
bitvector/modulus_true-unreach-call_true-no-overflow.i true 1 wit inspect 660    62 8800   - wit inspect - wit inspect - wit inspect error 0 wit inspect 5.4   230  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 1 wit inspect .17 11 1.8 - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.7   230  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 1 wit inspect .99 13 9.3 - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.7   230  
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect .13 11 1.5 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6   230  
bitvector/sum02_false-unreach-call_true-no-overflow.i true 2 wit inspect .13 11 1.4 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   210  
bitvector/sum02_true-unreach-call_true-no-overflow.i true 2 wit inspect .15 11 1.5 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7   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 87 21000   20000 280000 18 17 170 6300 18 -411 95 4200 18 -81 11   330 60 64 2100 17000
    correct results 50 82 56   600 710 17 17 74 4900 5 5 27 1100 15 15 9.6 280 32 64 180 11000
        correct true 32 64 52   360 670 0 0 0 32 64 180 11000
        correct false 18 18 3.8 240 44 17 17 74 4900 5 5 27 1100 15 15 9.6 280 0
    correct-unconfimed results 5 5 660   110 8800 0 0 0 0
        correct-unconfirmed true 5 5 660   110 8800 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0
    incorrect results 0 0 13 -416 69 3100 3 -96 1.8 55 0
        incorrect true 0 0 13 -416 69 3100 3 -96 1.8 55 0
        incorrect false 0 0 0 0 0
score (78 tasks, max score: 138) 87 17 -411 -81 64
Run set symbiotic.sv-comp18.NoOverflows-Other cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.NoOverflows-Other