Tool Map2Check v7.2-Flock : Tue Nov 27 22:00:00 -04 2018 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 ULTIMATE Automizer 0.1.23-635dfa2a
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* [apollon053; apollon130] apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-06 12:20:21 CET 2018-12-07 01:02:57 CET 2018-12-07 02:56:49 CET 2018-12-07 03:56:35 CET 2018-12-12 20:36:04 CET 2018-12-07 01:25:40 CET
Run set map2check.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-seq-validate-violation-witnesses-map2check.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-violation-witnesses-map2check.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-witness2test-validate-violation-witnesses-map2check.sv-comp19_prop-nooverflow.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-map2check.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-correctness-witnesses-map2check.sv-comp19_prop-nooverflow.NoOverflows-Other
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -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 -witness ../../results-verified/map2check.2018-12-06_1220.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/map2check.2018-12-06_1220.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/map2check.2018-12-06_1220.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/map2check.2018-12-06_1220.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/map2check.2018-12-06_1220.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
recursive/Addition02WithOverflowBug_false-no-overflow.c 1 150    150    190 2400   .11  .13   1 4.1  2.2  260 0   0   1 7.1   4.1   310   .62 0   1 3.5  2.1  240 0   .80 1 .61   .61   20    .049 0      -
recursive/Addition03_false-no-overflow.c 1 44    44    140 530   .16  .39   1 4.4  2.4  260 0   0   1 6.9   3.9   310   .66 0   -32 3.6  2.2  250 0   .93 -32 .62   .61   20    .049 0      -
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c 1 15    15    85 240   .020 0      1 3.8  2.1  250 0   0   1 7.5   4.3   310   .66 0   1 4.8  2.8  250 0   .80 1 .63   .64   20    .049 .51   -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 0 900    450    130 11000   390     .0041 - - - - 0 .020 .020 5.7 0    0  
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c 0 900    450    140 10000   580     0      - - - - 0 .023 .023 5.6 0    0  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 0 900    450    230 10000   2500     .0082 - - - - 0 .021 .022 5.6 0    0  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 0 900    450    280 11000   2500     .0082 - - - - 0 .021 .022 5.6 0    0  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 0 900    900    1300 11000   3.3   0      - - - - 0 .020 .021 5.6 0    0  
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 0 900    900    2000 12000   .045 0      - - - - 0 .021 .021 5.6 0    0  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c -16 45    45    140 530   .14  0      - - - - 2 7.7   4.8   310   .62 0  
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 0 900    460    2200 11000   28000     .0041 - - - - 0 .021 .022 5.6 0    0  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 0 900    900    1900 11000   1.0   0      - - - - 0 .020 .021 5.6 0    0  
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 0 900    900    1900 11000   .033 0      - - - - 0 .033 .034 5.6 0    0  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 0 900    450    86 9600   33     0      - - - - 0 .021 .022 5.6 0    0  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 0 900    450    83 9100   24000     .0041 - - - - 0 .021 .022 5.6 0    0  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 0 900    450    86 9800   31     0      - - - - 0 .053 .054 5.6 0    0  
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 0 900    900    1300 13000   .21  0      - - - - 0 .021 .021 5.6 0    0  
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 0 900    900    1300 13000   .20  0      - - - - 0 .025 .028 5.6 0    0  
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 0 900    900    320 11000   .31  0      - - - - 0 .021 .022 5.8 0    0  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 0 900    900    330 11000   .45  0      - - - - 0 .020 .021 5.6 0    0  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 0 900    450    1600 11000   23000     .0082 - - - - 0 .021 .022 5.6 0    0  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 0 900    900    1300 12000   1.6   .066  - - - - 0 .020 .021 5.5 0    0  
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 0 900    900    99 14000   .54  0      - - - - 0 .021 .021 5.6 0    0  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 0 900    900    90 12000   .11  0      - - - - 0 .024 .025 5.7 0    0  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 0 900    450    92 9300   170     0      - - - - 0 .020 .022 5.8 0    0  
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 0 900    470    2200 10000   28000     0      - - - - 0 .021 .022 5.7 0    0  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 0 900    460    2200 9800   29000     .0082 - - - - 0 .026 .027 5.6 0    0  
recursive-simple/id_b3_o2_false-no-overflow.c 1 6.7  6.7  91 91   .066 0      1 3.7  2.1  260 0   0   1 7.3   4.6   310   .66 0   1 3.7  2.2  250 0   .96 1 .59   .59   20    .045 0      -
recursive-simple/id_b3_o5_false-no-overflow.c 1 6.7  6.7  91 92   .061 0      1 4.0  2.2  260 0   0   1 7.1   4.1   310   .66 0   1 3.6  2.1  250 0   0    1 .61   .63   20    .045 .0041 -
recursive-simple/id_b5_o10_false-no-overflow.c 1 6.7  6.7  91 86   .049 0      1 3.9  2.1  260 0   0   1 7.5   4.6   310   .66 0   1 3.6  2.1  250 0   .80 1 .59   .59   20    .045 0      -
recursive-simple/sum_non_eq_false-no-overflow.c 1 18    18    100 220   .094 0      1 4.0  2.2  260 0   0   1 8.7   5.2   310   .62 0   1 3.7  2.2  250 0   .80 1 .60   .60   20    .049 1.4    -
recursive-simple/sum_non_false-no-overflow.c 1 56    56    120 800   .20  0      1 4.1  2.2  260 0   0   1 8.2   5.1   310   .62 0   -32 3.7  2.2  250 0   1.1  -32 .62   .62   20    .049 0      -
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 0 900    900    290 8700   11     0      - - - - 0 .022 .024 5.6 0    0  
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 0 900    900    290 9200   11     0      - - - - 0 .021 .022 5.6 0    0  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 0 900    900    290 8900   11     0      - - - - 0 .021 .022 5.6 0    0  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 0 900    900    290 8700   11     0      - - - - 0 .020 .021 5.6 0    0  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 0 900    900    290 10000   11     .13   - - - - 0 .021 .022 5.6 0    0  
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 0 900    900    1300 8800   9.8   0      - - - - 0 .020 .021 5.6 0    0  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 0 900    900    1300 11000   9.9   0      - - - - 0 .026 .027 5.5 0    0  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 0 900    900    1300 11000   9.9   0      - - - - 0 .021 .021 5.6 0    0  
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c 0 900    900    300 8300   10     0      - - - - 0 .021 .021 5.6 0    0  
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c 0 900    900    300 8500   10     0      - - - - 0 .021 .023 5.6 0    0  
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c 0 900    900    300 8200   10     0      - - - - 0 .021 .021 5.6 0    0  
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c 0 900    900    300 7200   10     0      - - - - 0 .021 .021 5.6 0    0  
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c 0 900    900    300 8600   11     0      - - - - 0 .021 .022 5.6 0    0  
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c 0 900    900    310 9400   11     0      - - - - 0 .021 .022 5.6 0    0  
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c 0 300    300    340 3300   1.8   .0041 - - - - 0 .021 .021 5.6 0    0  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c 0 360    360    390 3700   2.2   0      - - - - 0 .024 .025 5.6 0    0  
bitvector/byte_add_1_false-no-overflow.i 0 900    440    2000 11000   25000     .0082 0 .58 .36 40 0   0   0 .020 .021 5.6 0    0   0 .92 .61 48 0   0    0 .0022 .0037 .53 0     0      -
bitvector/byte_add_2_false-no-overflow.i 0 900    440    2000 9800   25000     .0082 0 .59 .36 41 0   0   0 .021 .022 5.6 0    0   0 1.1  .74 47 0   0    0 .0025 .0031 .52 0     0      -
bitvector/byte_add_false-no-overflow.i 0 900    440    3900 9300   25000     0      0 .59 .37 41 0   0   0 .020 .021 5.6 0    0   0 1.0  .65 48 0   0    0 .0049 .0067 .52 0     0      -
bitvector/jain_1_false-no-overflow.i 1 130    81    4400 1300   .041 0      1 4.1  2.5  280 0   0   1 6.7   3.8   300   .66 0   1 3.7  2.2  250 0   1.2  1 .62   .64   20    .045 0      -
bitvector/jain_2_false-no-overflow.i 1 110    64    4100 1100   .041 0      1 4.4  2.6  280 0   0   1 7.2   4.5   310   .66 0   1 3.8  2.2  250 0   .96 1 .60   .61   20    .049 1.4    -
bitvector/jain_4_false-no-overflow.i 1 110    64    4200 1100   .029 0      1 4.2  2.4  290 0   0   1 7.2   4.6   310   .66 0   1 3.5  2.1  250 0   .80 1 .59   .59   20    .049 0      -
bitvector/jain_5_false-no-overflow.i 1 .40 .38 83 4.8 .016 0      0 93    80    1300 0   0   -32 9.3   5.3   320   .66 0   1 3.6  2.1  250 0   0    1 .60   .60   20    .045 0      -
bitvector/jain_6_false-no-overflow.i 1 110    67    4300 1200   .025 0      1 4.3  2.5  290 0   0   1 6.8   4.4   300   .62 0   1 4.2  2.5  250 0   .96 1 .64   .63   20    .049 0      -
bitvector/jain_7_false-no-overflow.i 1 120    69    4500 1100   .029 0      1 4.1  2.3  290 0   0   1 7.0   4.3   310   .66 0   1 3.8  2.2  250 0   0    1 .59   .60   20    .049 1.0    -
bitvector/modulus_false-no-overflow.i 0 900    900    920 11000   20     0      0 .60 .36 41 0   0   0 .021 .021 5.6 0    0   0 .92 .60 47 0   0    0 .0062 .0077 .52 0     0      -
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i 0 900    440    2000 10000   25000     .0082 - - - - 0 .021 .022 5.7 0    0  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i 0 900    440    2000 9300   25000     .0041 - - - - 0 .021 .021 5.6 0    0  
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i 0 900    440    3800 10000   25000     0      - - - - 0 .023 .023 5.6 0    0  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i 2 900    460    4300 11000   28000     .0082 - - - - 2 8.8   5.0   310   .66 0  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i 0 900    460    4300 10000   28000     .0082 - - - - 0 .021 .022 5.6 0    0  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i 0 900    470    4300 10000   28000     0      - - - - 0 .020 .021 5.7 0    0  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i 0 900    460    84 9700   27000     .0082 - - - - 0 .021 .021 5.6 0    0  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i 0 900    460    4300 9600   28000     .0082 - - - - 0 .021 .021 5.6 0    0  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i 0 900    850    4200 7800   .029 0      - - - - 0 .020 .021 5.6 0    0  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i 0 900    850    4000 8300   .020 0      - - - - 0 .021 .022 5.6 0    0  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i 0 900    850    4400 8400   .029 0      - - - - 0 .050 .051 5.6 0    0  
bitvector/jain_5_true-unreach-call_true-no-overflow.i 0 900    450    74 8600   .012 0      - - - - 0 .020 .021 5.6 0    0  
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i 0 900    850    4200 9800   .029 0      - - - - 0 .021 .021 5.6 0    0  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i 0 900    850    5400 11000   .029 0      - - - - 0 .020 .021 5.6 0    0  
bitvector/modulus_true-unreach-call_true-no-overflow.i 0 900    610    4300 11000   7900     0      - - - - 0 .020 .021 5.6 0    0  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i 0 900    460    84 9600   28000     .0082 - - - - 0 .020 .021 5.6 0    0  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i 0 900    450    2100 9400   27000     .0082 - - - - 0 .021 .022 5.6 0    0  
bitvector/parity_true-unreach-call_true-no-overflow.i 0 900    460    2100 10000   28000     .0082 - - - - 0 .020 .021 5.6 0    0  
bitvector/sum02_false-unreach-call_true-no-overflow.i 0 900    450    75 9000   .43  0      - - - - 0 .020 .021 5.6 0    0  
bitvector/sum02_true-unreach-call_true-no-overflow.i 0 900    450    75 10000   .27  0      - - - - 0 .020 .020 5.6 0    0  
psyco/psyco_abp_1_false-no-overflow.c 0 900    850    4300 6700   1.1   0      0 .62 .38 41 0   0   0 .020 .021 5.6 0    0   0 .94 .61 47 0   0    0 .0058 .0070 .52 0     0      -
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 79 0 57000 44000 120000 640000 520000    .85   19 13 150 110 5000 0   0   19 -19 100   63   4300 9.0  0   19 -52 58   34   3700 0   10   19 -52 8.5 8.6 290 .67  4.3 60 4 18 11   950 1.3 0  
    correct results 15 16 1800 1100 27000 21000 28000    .53   13 13 53 30 3500 0   0   13 13 95   58   4000 8.4  0   12 12 46   27   3000 0   8.1 12 12 7.3 7.3 240 .57  4.3 2 4 16 9.8 620 1.3 0  
        correct true 1 2 900 460 4300 11000 28000    .0082 0 0 0 0 2 4 16 9.8 620 1.3 0  
        correct false 14 14 890 650 23000 10000 .94 .52   13 13 53 30 3500 0   0   13 13 95   58   4000 8.4  0   12 12 46   27   3000 0   8.1 12 12 7.3 7.3 240 .57  4.3 0
    incorrect results 1 -16 45 45 140 530 .14 0      0 1 -32 9.3 5.3 320 .66 0   2 -64 7.4 4.3 500 0   2.0 2 -64 1.2 1.2 40 .098 0   0
        incorrect true 0 0 1 -32 9.3 5.3 320 .66 0   2 -64 7.4 4.3 500 0   2.0 2 -64 1.2 1.2 40 .098 0   0
        incorrect false 1 -16 45 45 140 530 .14 0      0 0 0 0 0
score (79 tasks, max score: 139) 0 13 -19 -52 -52 4
Run set map2check.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-seq-validate-violation-witnesses-map2check.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-violation-witnesses-map2check.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-witness2test-validate-violation-witnesses-map2check.sv-comp19_prop-nooverflow.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-map2check.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-correctness-witnesses-map2check.sv-comp19_prop-nooverflow.NoOverflows-Other