Tool symbiotic 6.0.3-77d4af47 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* [apollon013; apollon098] 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-07 21:42:05 CET 2018-12-08 23:40:56 CET 2018-12-09 00:46:04 CET 2018-12-09 01:29:54 CET 2018-12-12 21:10:03 CET 2018-12-08 23:47:25 CET
Run set symbiotic.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-seq-validate-violation-witnesses-symbiotic.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-violation-witnesses-symbiotic.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-nooverflow.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-correctness-witnesses-symbiotic.sv-comp19_prop-nooverflow.NoOverflows-Other
Options --witness witness.graphml -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/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2018-12-07_2142.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/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2018-12-07_2142.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 .27 .27 19 3.0 0     0      1 3.9  2.2  260 0   0      -32 7.3   4.1   310   .62 0   1 3.9  2.3  250 0   .80   1 .59   .59   20    .049 0      -
recursive/Addition03_false-no-overflow.c 1 .26 .26 18 2.8 0     0      1 4.8  2.7  260 0   .020  -32 7.3   4.1   300   .62 0   1 3.7  2.1  250 0   0      1 .60   .60   20    .049 0      -
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c 1 .28 .27 19 3.1 0     0      1 3.8  2.1  250 0   0      -32 7.3   4.1   300   .62 0   1 3.8  2.2  250 0   .80   1 .59   .59   20    .049 0      -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 0 900    910    13000 12000   .041 0      - - - - 0 .025 .026 5.5 0    0     
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c 0 900    910    15000 11000   .041 0      - - - - 0 .021 .022 5.6 0    0     
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 0 900    910    13000 12000   .045 0      - - - - 0 .021 .022 5.6 0    0     
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 0 900    910    13000 14000   .041 0      - - - - 0 .021 .022 5.6 0    0     
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 0 900    900    250 12000   .025 0      - - - - 0 .022 .024 5.6 0    0     
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 0 900    900    250 13000   .025 0      - - - - 0 .022 .023 5.6 0    0     
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c 0 900    900    440 11000   .025 0      - - - - 0 .026 .027 5.6 0    0     
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 2 .20 .19 16 2.4 0     0      - - - - 2 6.6   4.1   300   .66 0     
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 0 900    900    1300 11000   .025 0      - - - - 0 .030 .032 5.6 0    0     
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 0 900    900    1300 11000   .025 0      - - - - 0 .021 .021 5.6 0    0     
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 0 770    780    15000 12000   .057 .0041 - - - - 0 .021 .022 5.6 0    0     
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 2 .21 .21 17 1.9 0     0      - - - - 2 35     21     1100   .62 0     
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 0 710    720    15000 9800   .037 .0041 - - - - 0 .025 .026 5.6 0    0     
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 0 900    900    2400 11000   .029 0      - - - - 0 .023 .024 5.6 0    0     
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 0 900    900    3000 10000   .037 0      - - - - 0 .022 .023 5.6 0    0     
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 0 900    900    260 12000   .025 0      - - - - 0 .023 .025 5.8 0    0     
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 0 900    900    260 11000   .025 0      - - - - 0 .026 .027 5.6 0    0     
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 0 900    900    220 11000   .025 0      - - - - 0 .022 .023 5.6 0    0     
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 0 900    900    120 12000   .020 0      - - - - 0 .025 .025 5.6 0    0     
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 0 900    900    63 12000   .012 0      - - - - 0 .021 .022 5.6 0    0     
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 0 900    900    62 13000   .012 0      - - - - 0 .027 .028 5.5 0    0     
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 0 830    840    15000 14000   .049 .0041 - - - - 0 .022 .022 5.6 0    0     
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 2 .68 .69 23 8.5 0     5.1    - - - - 2 82     53     870   .62 0     
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 2 .67 .66 18 8.1 0     0      - - - - 2 89     57     850   .62 0     
recursive-simple/id_b3_o2_false-no-overflow.c 1 .24 .24 18 2.8 0     0      1 3.8  2.2  260 0   .0041 -32 6.5   3.8   290   .62 0   1 3.9  2.3  250 0   1.2    1 .59   .59   20    .045 0      -
recursive-simple/id_b3_o5_false-no-overflow.c 1 .29 .28 18 3.2 0     .28   1 4.2  2.3  260 0   0      -32 6.5   3.7   300   .62 0   1 3.6  2.1  250 0   1.2    1 .60   .60   20    .045 0      -
recursive-simple/id_b5_o10_false-no-overflow.c 1 .25 .24 18 2.8 0     0      1 3.9  2.2  260 0   0      -32 6.7   3.8   300   .66 0   1 3.5  2.1  250 0   0      1 .59   .59   20    .045 0      -
recursive-simple/sum_non_eq_false-no-overflow.c 1 .26 .25 19 2.3 0     0      1 5.0  2.7  260 0   0      -32 6.8   3.9   300   .62 0   1 3.6  2.2  250 0   .80   1 .60   .60   20    .049 0      -
recursive-simple/sum_non_false-no-overflow.c 1 .26 .25 19 3.2 0     0      1 5.1  2.9  260 0   0      -32 7.1   4.0   300   .62 0   1 3.6  2.1  250 0   0      1 .60   .60   20    .049 0      -
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 2 .20 .20 17 2.9 0     0      - - - - 2 8.3   4.6   300   .66 0     
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 2 .20 .19 16 2.2 0     0      - - - - 2 8.5   4.6   300   .66 0     
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 2 .19 .19 15 2.6 0     0      - - - - 2 6.9   4.3   300   .62 0     
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 2 .20 .19 16 1.9 0     0      - - - - 2 7.6   4.2   300   .66 0     
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 2 .20 .19 17 2.4 0     0      - - - - 2 6.7   4.1   300   .66 .0082
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 0 900    900    1500 12000   .025 4.5    - - - - 0 .022 .022 5.6 0    0     
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 0 900    900    1500 8200   .025 0      - - - - 0 .024 .025 5.6 0    0     
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 0 900    900    1500 9300   .025 0      - - - - 0 .021 .023 5.7 0    0     
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c 2 .19 .18 17 2.4 0     0      - - - - 2 6.6   4.1   300   .66 .0082
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c 2 .20 .20 17 2.1 0     0      - - - - 2 7.1   4.2   300   .66 0     
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c 2 .19 .19 16 2.1 0     0      - - - - 2 7.4   4.1   300   .66 0     
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c 2 .19 .18 16 2.0 0     0      - - - - 2 7.8   4.7   290   .66 0     
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c 2 .19 .19 17 2.3 0     0      - - - - 2 8.4   4.5   300   .66 0     
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c 2 .20 .20 17 2.6 0     .41   - - - - 2 7.8   4.4   310   .66 0     
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c 2 .19 .18 16 2.4 0     0      - - - - 2 7.1   4.4   310   .62 0     
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c 2 .20 .20 16 2.1 0     0      - - - - 2 7.1   4.4   300   .62 0     
bitvector/byte_add_1_false-no-overflow.i 1 .55 .55 18 6.8 0     0      1 8.5  4.5  410 0   0      -32 7.9   4.4   310   .62 0   -32 4.7  2.7  250 0   .80   1 .63   .63   20    .057 0      -
bitvector/byte_add_2_false-no-overflow.i 1 .55 .54 18 6.9 0     0      1 10    5.6  400 0   0      -32 8.6   4.9   320   .62 0   -32 4.0  2.3  250 0   .80   1 .63   .63   20    .057 0      -
bitvector/byte_add_false-no-overflow.i 1 1.0  1.0  18 14   0     0      1 11    5.7  400 0   0      -32 7.7   4.8   310   .62 0   -32 3.8  2.2  250 0   0      1 .62   .62   20    .057 0      -
bitvector/jain_1_false-no-overflow.i 1 .25 .24 19 3.6 0     0      1 5.5  3.3  290 0   0      1 7.0   4.0   310   .62 0   0 4.7  2.7  250 0   0      1 .61   .61   20    .045 0      -
bitvector/jain_2_false-no-overflow.i 1 .27 .26 18 3.1 0     0      1 4.7  2.8  290 0   0      1 7.2   4.5   310   .62 0   0 3.6  2.1  250 0   .80   1 .60   .61   20    .049 1.4    -
bitvector/jain_4_false-no-overflow.i 1 .25 .24 18 2.7 0     0      1 5.4  3.2  280 0   .020  1 7.4   4.6   310   .62 0   0 3.7  2.2  250 0   .0041 1 .59   .59   20    .049 .0041 -
bitvector/jain_5_false-no-overflow.i 1 1.2  1.1  50 15   0     0      0 94    79    1200 0   .098  -32 7.8   4.4   310   .62 0   1 3.6  2.1  250 0   0      1 .62   .61   20    .045 0      -
bitvector/jain_6_false-no-overflow.i 1 .25 .24 17 2.5 0     0      1 4.2  2.5  280 0   0      1 7.4   4.3   310   .62 0   0 3.6  2.1  250 0   .80   1 .59   .59   20    .049 0      -
bitvector/jain_7_false-no-overflow.i 1 .28 .27 19 3.0 0     0      1 5.8  3.3  280 0   0      1 7.0   4.4   310   .62 0   0 4.0  2.3  250 0   0      1 .61   .60   20    .049 0      -
bitvector/modulus_false-no-overflow.i 1 .27 .26 19 3.3 0     0      1 3.7  2.1  250 0   .020  -32 7.2   4.0   310   .62 0   1 3.5  2.0  240 0   0      1 .60   .61   20    .049 1.4    -
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i 2 .67 .67 18 9.5 0     0      - - - - 2 7.6   4.4   300   .66 0     
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i 2 .70 .69 19 11   0     0      - - - - 2 8.6   5.3   310   .66 0     
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i 2 2.0  2.0  19 27   0     0      - - - - 2 10     5.9   310   .66 0     
bitvector/gcd_1_true-unreach-call_true-no-overflow.i 2 .40 .40 21 4.8 0     0      - - - - 2 8.3   4.8   310   .66 0     
bitvector/gcd_2_true-unreach-call_true-no-overflow.i 2 93    93    46 1200   0     0      - - - - 2 8.2   4.7   310   .66 0     
bitvector/gcd_3_true-unreach-call_true-no-overflow.i 2 100    100    44 1300   0     0      - - - - 2 8.9   5.1   310   .66 0     
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i 2 .19 .18 16 2.2 0     0      - - - - 2 18     11     470   .62 0     
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i 2 .19 .18 16 2.2 0     0      - - - - 2 7.6   4.2   310   .62 0     
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i 2 .20 .20 17 2.1 0     0      - - - - 2 8.0   4.4   300   .66 0     
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i 2 .22 .21 17 2.1 0     0      - - - - 2 7.2   4.0   300   .66 0     
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i 2 .19 .18 16 2.3 0     0      - - - - 2 6.5   3.7   300   .66 0     
bitvector/jain_5_true-unreach-call_true-no-overflow.i 2 .18 .18 16 3.1 0     0      - - - - 2 7.4   4.4   300   .66 0     
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i 2 .18 .18 15 2.2 0     0      - - - - 2 8.1   4.5   290   .62 0     
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i 2 .21 .20 16 2.1 0     0      - - - - 2 7.5   4.1   290   .66 .0041
bitvector/modulus_true-unreach-call_true-no-overflow.i 0 900    900    140 9900   .025 0      - - - - 0 .024 .025 5.6 0    0     
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i 1 .18 .17 17 2.2 0     0      - - - - 0 7.6   4.3   310   .66 0     
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i 1 3.6  3.6  19 45   0     0      - - - - 0 7.2   4.0   300   .66 0     
bitvector/parity_true-unreach-call_true-no-overflow.i 2 .19 .18 17 2.2 0     0      - - - - 2 9.1   5.1   310   .66 0     
bitvector/sum02_false-unreach-call_true-no-overflow.i 2 .21 .20 16 3.1 0     0      - - - - 2 6.5   4.1   290   .66 .0041
bitvector/sum02_true-unreach-call_true-no-overflow.i 2 .21 .20 16 2.0 0     0      - - - - 2 6.6   3.7   290   .62 .0082
psyco/psyco_abp_1_false-no-overflow.c 0 900    900    2700 7200   .025 0      0 .60 .37 41 0   0      0 .021 .021 5.6 0    0   0 .95 .61 47 0   0      0 .0050 .0064 .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 88 22000   22000   120000 280000 .74 10    19 17 190 130 6100 0   .16  19 -411 130 76 5500 11   0   19 -86 70 41   4500 0   8.1 19 18 11 11 360 .89 2.8 60 68 470 280 13000 23 .033
    correct results 52 86 210   210   990 2700 0    5.8  17 17 94 52 4900 0   .066 5 5 36 22 1500 3.1 0   10 10 37 22   2500 0   4.8 18 18 11 11 360 .89 2.8 34 68 450 280 12000 22 .033
        correct true 34 68 210   200   630 2600 0    5.5  0 0 0 0 34 68 450 280 12000 22 .033
        correct false 18 18 6.9 6.8 360 84 0    .28 17 17 94 52 4900 0   .066 5 5 36 22 1500 3.1 0   10 10 37 22   2500 0   4.8 18 18 11 11 360 .89 2.8 0
    correct-unconfimed results 2 2 3.8 3.8 35 47 0    0    0 0 0 0 0
        correct-unconfirmed true 2 2 3.8 3.8 35 47 0    0    0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0
    incorrect results 0 0 13 -416 95 54 4000 8.1 0   3 -96 12 7.3 750 0   1.6 0 0
        incorrect true 0 0 13 -416 95 54 4000 8.1 0   3 -96 12 7.3 750 0   1.6 0 0
        incorrect false 0 0 0 0 0 0
score (79 tasks, max score: 139) 88 17 -411 -86 18 68
Run set symbiotic.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-seq-validate-violation-witnesses-symbiotic.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-violation-witnesses-symbiotic.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-nooverflow.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-correctness-witnesses-symbiotic.sv-comp19_prop-nooverflow.NoOverflows-Other