Tool 2LS 0.6.0 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* [apollon013; apollon077; apollon078; apollon114] [apollon077; apollon078; apollon089; apollon164] [apollon077; apollon078; apollon089; apollon134] [apollon022; 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:20:37 CET 2017-12-01 11:18:40 CET 2017-12-01 11:36:11 CET 2017-12-01 11:38:17 CET 2017-12-01 11:21:10 CET
Run set 2ls.sv-comp18.NoOverflows-Other cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.NoOverflows-Other
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-12-01_1020.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/2ls.2017-12-01_1020.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/2ls.2017-12-01_1020.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/2ls.2017-12-01_1020.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 error (5) 0 wit inspect .079 22 .75 error (invalid witness file) 0 wit inspect .42 44 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0014 .31 - wit inspect
recursive/Addition03_false-no-overflow.c error (5) 0 wit inspect .090 22 .98 error (invalid witness file) 0 wit inspect .40 45 error (2) 0 wit inspect .024 5.0 error (invalid witness file) 0 wit inspect .0011 .32 - wit inspect
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c error (5) 0 wit inspect .11  23 .60 error (invalid witness file) 0 wit inspect .43 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c error (5) 0 wit inspect .11  22 .66 - 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 error (5) 0 wit inspect .11  22 .64 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
recursive/Ackermann03_true-unreach-call_true-no-overflow.c error (5) 0 wit inspect .11  22 .60 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive/Ackermann04_true-unreach-call_true-no-overflow.c error (5) 0 wit inspect .12  22 .62 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .090 22 .81 - 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 (5) 0 wit inspect .097 22 .81 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .039 5.0
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .11  22 .71 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .11  22 .65 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .099 22 .73 - 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 (5) 0 wit inspect .12  22 .61 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c error (5) 0 wit inspect .082 22 .71 - 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 error (5) 0 wit inspect .096 22 .87 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .085 22 .81 - 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 error (5) 0 wit inspect .12  22 .67 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .093 22 .73 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .028 4.8
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .083 22 .86 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .094 22 .73 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.9
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .082 22 .93 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .048 4.9
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c error (5) 0 wit inspect .12  23 .71 - 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 (5) 0 wit inspect .098 22 .76 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .10  22 .76 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .082 22 .81 - 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 error (5) 0 wit inspect .094 22 .79 - 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 error (5) 0 wit inspect .10  22 .65 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive-simple/id_b3_o2_false-no-overflow.c error (5) 0 wit inspect .12  22 .55 error (invalid witness file) 0 wit inspect .40 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0015 .30 - wit inspect
recursive-simple/id_b3_o5_false-no-overflow.c error (5) 0 wit inspect .12  22 .71 error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
recursive-simple/id_b5_o10_false-no-overflow.c error (5) 0 wit inspect .096 22 .74 error (invalid witness file) 0 wit inspect .43 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0013 .32 - wit inspect
recursive-simple/sum_non_eq_false-no-overflow.c error (5) 0 wit inspect .12  22 .69 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .047 5.0 error (invalid witness file) 0 wit inspect .0014 .30 - wit inspect
recursive-simple/sum_non_false-no-overflow.c error (5) 0 wit inspect .10  22 .66 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .0015 .30 - wit inspect
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error (5) 0 wit inspect .12  22 .67 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c error (5) 0 wit inspect .089 22 .73 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error (5) 0 wit inspect .10  22 .73 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error (5) 0 wit inspect .10  22 .75 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error (5) 0 wit inspect .098 22 .65 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c error (5) 0 wit inspect .11  22 .64 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error (5) 0 wit inspect .11  22 .73 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error (5) 0 wit inspect .12  22 .66 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c error (5) 0 wit inspect .089 22 .64 - 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 error (5) 0 wit inspect .11  22 .75 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c error (5) 0 wit inspect .082 22 .76 - 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 error (5) 0 wit inspect .098 22 .64 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c error (5) 0 wit inspect .097 22 .63 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c error (5) 0 wit inspect .095 22 .86 - 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 error (5) 0 wit inspect .095 22 .70 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.9
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c error (5) 0 wit inspect .10  22 .78 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
bitvector/byte_add_1_false-no-overflow.i false(no-overflow) 1 wit inspect .34  31 4.2  false(no-overflow) 1 wit inspect 35    850 true -32 wit inspect 6.4   280   true -32 wit inspect .80   19    - wit inspect
bitvector/byte_add_2_false-no-overflow.i false(no-overflow) 1 wit inspect .36  31 3.5  false(no-overflow) 1 wit inspect 36    830 true -32 wit inspect 5.9   280   true -32 wit inspect .76   19    - wit inspect
bitvector/byte_add_false-no-overflow.i false(no-overflow) 1 wit inspect .36  31 4.0  false(no-overflow) 1 wit inspect 35    900 true -32 wit inspect 4.2   280   true -32 wit inspect .78   19    - wit inspect
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect .093 22 .79 false(no-overflow) 1 wit inspect 3.6  270 false(no-overflow) 1 wit inspect 6.2   230   false(no-overflow) 1 wit inspect .76   18    - wit inspect
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect .14  23 .86 false(no-overflow) 1 wit inspect 3.5  300 false(no-overflow) 1 wit inspect 5.0   240   false(no-overflow) 1 wit inspect .78   18    - wit inspect
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect .13  24 .94 false(no-overflow) 1 wit inspect 5.9  320 false(no-overflow) 1 wit inspect 5.6   250   false(no-overflow) 1 wit inspect .70   18    - wit inspect
bitvector/jain_5_false-no-overflow.i timeout 0 wit inspect 900     1100 8900    error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .0015 .32 - wit inspect
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect .13  26 .98 false(no-overflow) 1 wit inspect 4.7  330 false(no-overflow) 1 wit inspect 6.0   260   false(no-overflow) 1 wit inspect .74   18    - wit inspect
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect .13  24 .93 false(no-overflow) 1 wit inspect 6.1  330 false(no-overflow) 1 wit inspect 5.1   260   false(no-overflow) 1 wit inspect .60   18    - wit inspect
bitvector/modulus_false-no-overflow.i false(no-overflow) 1 wit inspect .15  26 1.1  false(no-overflow) 1 wit inspect 2.3  260 error 0 wit inspect 4.8   250   false(no-overflow) 1 wit inspect .76   18    - wit inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .12  24 .92 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1   270  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .12  24 1.0  - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1   270  
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .10  24 1.0  - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1   280  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .12  25 1.1  - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0   280  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .11  24 .89 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0   260  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect .096 23 1.2  - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9   260  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .56  33 6.1  - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.6   490  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect .12  24 .95 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0   210  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect .086 22 .77 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0   220  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect .096 22 .64 - 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 .096 22 .73 - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9   210  
bitvector/jain_5_true-unreach-call_true-no-overflow.i true 2 wit inspect .099 22 .74 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0   220  
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect .12  23 .72 - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9   210  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect .10  23 .80 - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9   210  
bitvector/modulus_true-unreach-call_true-no-overflow.i true 1 wit inspect .13  28 .97 - wit inspect - wit inspect - wit inspect error 0 wit inspect 3.6   250  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 1 wit inspect .10  22 .80 - wit inspect - wit inspect - wit inspect error 0 wit inspect 3.2   220  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 1 wit inspect .11  22 .80 - wit inspect - wit inspect - wit inspect error 0 wit inspect 3.2   230  
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect .10  22 .89 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7   220  
bitvector/sum02_false-unreach-call_true-no-overflow.i true 2 wit inspect .12  25 .71 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0   220  
bitvector/sum02_true-unreach-call_true-no-overflow.i true 2 wit inspect .11  24 1.0  - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   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 46 910    2900 8900   18 9 140 4800 18 -91 50 2400 18 -90 6.7 170 60 34 83 5200
    correct results 26 43 4.1  640 38   9 9 130 4400 5 5 28 1200 6 6 4.3 110 17 34 72 4300
        correct true 17 34 2.3  410 20   0 0 0 17 34 72 4300
        correct false 9 9 1.8  240 17   9 9 130 4400 5 5 28 1200 6 6 4.3 110 0
    correct-unconfimed results 3 3 .34 73 2.6 0 0 0 0
        correct-unconfirmed true 3 3 .34 73 2.6 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0
    incorrect results 0 0 3 -96 17 830 3 -96 2.3 57 0
        incorrect true 0 0 3 -96 17 830 3 -96 2.3 57 0
        incorrect false 0 0 0 0 0
score (78 tasks, max score: 138) 46 9 -91 -90 34
Run set 2ls.sv-comp18.NoOverflows-Other cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.NoOverflows-Other