Tool Map2Check Map2Check 7.1 : Wed Nov 22 22:30:11 -04 2017 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* [apollon072; apollon077; apollon078; apollon135] [apollon041; apollon077; apollon078] [apollon042; apollon077; apollon078] [apollon072; 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]
Date of execution 2017-12-02 00:52:46 CET 2017-12-02 02:12:50 CET 2017-12-02 02:29:49 CET 2017-12-02 02:31:32 CET 2017-12-02 02:13:30 CET
Run set map2check.sv-comp18.NoOverflows-Other cpa-seq-validate-violation-witnesses-map2check.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-violation-witnesses-map2check.sv-comp18-violation-witness.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.NoOverflows-Other
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/map2check.2017-12-02_0052.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/map2check.2017-12-02_0052.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/map2check.2017-12-02_0052.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/map2check.2017-12-02_0052.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 .43  12 5.7  false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.5 240 false(no-overflow) 1 wit inspect .59  18   - wit inspect
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect .42  12 5.4  false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 3.3 230 false(no-overflow) 1 wit inspect .58  19   - wit inspect
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect .37  12 4.7  false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 3.6 260 false(no-overflow) 1 wit inspect .59  18   - wit inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 890     17 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 890     19 14000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive/Ackermann03_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 890     18 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
recursive/Ackermann04_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 890     18 12000    - 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 unknown 0 wit inspect 890     650 9400    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .044 4.9
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 900     640 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect .076 11 .38 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .38  11 5.5  - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1   230  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 890     850 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .042 5.0
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 890     830 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 890     13 13000    - 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 unknown 0 wit inspect .29  11 3.2  - 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 unknown 0 wit inspect 890     13 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 900     1400 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 900     1300 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 900     140 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .045 4.9
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 900     160 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 890     80 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c unknown 0 wit inspect 900     53 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .046 4.9
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 900     88 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 890     36 12000    - 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 unknown 0 wit inspect 890     13 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 2.1   12 27    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     3000  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 2.1   13 27    - 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 .37  12 4.8  false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.3 260 true -32 wit inspect .63  18   - wit inspect
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) 1 wit inspect .37  12 4.0  false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 3.6 270 true -32 wit inspect .59  18   - wit inspect
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) 1 wit inspect .38  12 4.0  true -32 wit inspect 2.5  260 false(no-overflow) 1 wit inspect 3.9 260 true -32 wit inspect .59  18   - wit inspect
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) 1 wit inspect .41  12 4.4  false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.4 260 false(no-overflow) 1 wit inspect .61  18   - wit inspect
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) 1 wit inspect .47  12 6.2  false(no-overflow) 1 wit inspect 2.4  260 false(no-overflow) 1 wit inspect 4.5 270 false(no-overflow) 1 wit inspect .62  18   - wit inspect
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 900     690 10000    - 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 unknown 0 wit inspect 900     660 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 900     700 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 890     660 8300    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 890     1200 8500    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(no-overflow) -16 wit inspect .38  12 4.2  - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7   250  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c false(no-overflow) -16 wit inspect .36  12 5.1  - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0   250  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c false(no-overflow) -16 wit inspect .37  12 5.6  - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5   250  
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 890     1000 8900    - 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 unknown 0 wit inspect 890     1100 9100    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 890     1100 9600    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .027 4.8
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 890     1000 8100    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .045 4.8
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 900     1100 8800    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 900     1000 9600    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 900     740 9200    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 890     730 8800    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
bitvector/byte_add_1_false-no-overflow.i true -32 wit inspect 4.1   13 49    error (1) 0 wit inspect .64 45 error 0 wit inspect 17   570 error (1) 0 wit inspect .068 9.0 - wit inspect
bitvector/byte_add_2_false-no-overflow.i true -32 wit inspect 4.1   13 49    error (1) 0 wit inspect .62 48 error 0 wit inspect 36   660 error (1) 0 wit inspect .082 9.0 - wit inspect
bitvector/byte_add_false-no-overflow.i true -32 wit inspect 39     17 440    error (1) 0 wit inspect .47 45 error 0 wit inspect 52   690 error (1) 0 wit inspect .082 9.0 - wit inspect
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect .44  12 5.1  false(no-overflow) 1 wit inspect 2.5  270 false(no-overflow) 1 wit inspect 3.4 240 false(no-overflow) 1 wit inspect .59  18   - wit inspect
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect .70  12 9.5  false(no-overflow) 1 wit inspect 3.8  290 false(no-overflow) 1 wit inspect 5.4 230 false(no-overflow) 1 wit inspect .59  18   - wit inspect
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect .59  12 8.2  false(no-overflow) 1 wit inspect 2.6  270 false(no-overflow) 1 wit inspect 3.4 240 false(no-overflow) 1 wit inspect .62  18   - wit inspect
bitvector/jain_5_false-no-overflow.i false(no-overflow) 1 wit inspect 2.3   11 29    true -32 wit inspect 3.1  250 true -32 wit inspect 3.0 220 false(no-overflow) 1 wit inspect .62  18   - wit inspect
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect .72  12 8.0  false(no-overflow) 1 wit inspect 2.9  290 false(no-overflow) 1 wit inspect 5.0 230 false(no-overflow) 1 wit inspect .59  18   - wit inspect
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect .70  12 8.5  false(no-overflow) 1 wit inspect 2.5  270 false(no-overflow) 1 wit inspect 4.8 230 false(no-overflow) 1 wit inspect .62  18   - wit inspect
bitvector/modulus_false-no-overflow.i false(no-overflow) 1 wit inspect .35  12 4.5  true -32 wit inspect 3.1  260 error 0 wit inspect 3.7 260 false(no-overflow) 1 wit inspect .59  18   - wit inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 4.1   13 48    - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   270  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 4.1   13 55    - 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 38     18 460    - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7   270  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .66  12 8.4  - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6   270  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 28     18 380    - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   260  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 30     17 380    - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9   260  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i unknown 0 wit inspect .078 11 .36 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect .37  11 3.7  - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   210  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i unknown 0 wit inspect 900     92 9600    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i unknown 0 wit inspect 900     120 7600    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i unknown 0 wit inspect 890     120 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
bitvector/jain_5_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 890     11 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i false(no-overflow) -16 wit inspect .48  12 5.7  - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5   220  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i false(no-overflow) -16 wit inspect .49  12 6.5  - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9   220  
bitvector/modulus_true-unreach-call_true-no-overflow.i true 1 wit inspect 790     64 12000    - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.6   230  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 1 wit inspect .33  11 3.9  - wit inspect - wit inspect - wit inspect error 0 wit inspect 3.2   230  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i unknown 0 wit inspect .30  11 3.5  - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect 9.4   13 120    - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1   220  
bitvector/sum02_false-unreach-call_true-no-overflow.i unknown 0 wit inspect 900     670 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
bitvector/sum02_true-unreach-call_true-no-overflow.i unknown 0 wit inspect .065 11 .53 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
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 -139 34000   20000 410000 18 -84 45   4100 18 -19 170   5600 18 -84 9.2 300 60 28 2000 10000
    correct results 24 33 120   300 1600 12 12 35   3200 13 13 56   3200 12 12 7.2 220 14 28 66 3500
        correct true 9 18 120   130 1500 0 0 0 14 28 66 3500
        correct false 15 15 9.0 180 110 12 12 35   3200 13 13 56   3200 12 12 7.2 220 0
    correct-unconfimed results 4 4 800   100 12000 0 0 0 0
        correct-unconfirmed true 4 4 800   100 12000 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0
    incorrect results 8 -176 49   100 560 3 -96 8.7 770 1 -32 3.0 220 3 -96 1.8 55 0
        incorrect true 3 -96 47   43 540 3 -96 8.7 770 1 -32 3.0 220 3 -96 1.8 55 0
        incorrect false 5 -80 2.1 59 27 0 0 0 0
score (78 tasks, max score: 138) -139 -84 -19 -84 28
Run set map2check.sv-comp18.NoOverflows-Other cpa-seq-validate-violation-witnesses-map2check.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-violation-witnesses-map2check.sv-comp18-violation-witness.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.NoOverflows-Other