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 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 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] 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-01 19:46:39 CET 2017-12-01 22:34:51 CET 2017-12-01 23:03:48 CET 2017-12-01 23:06:19 CET 2017-12-01 23:09:14 CET 2017-12-01 22:04:37 CET 2017-12-01 22:38:34 CET
Run set map2check.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.ReachSafety-BitVectors
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/map2check.2017-12-01_1946.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-01_1946.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/map2check.2017-12-01_1946.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/map2check.2017-12-01_1946.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/map2check.2017-12-01_1946.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/map2check.2017-12-01_1946.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 status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i 1 1.3  13 15   -32 10    400 -32 5.4   230   0 4.0  220 1 .72   18    - -
bitvector/sum02_false-unreach-call_true-no-overflow.i 0 900    700 13000   0 .59 44 0 .018 4.9 0 .88 49 0 .0016 .28 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i 2 4.1  13 56   - - - - 2 8.9  300 0 960     1100  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i 2 4.1  13 54   - - - - 2 8.5  340 0 960     1100  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i 2 .64 12 7.9 - - - - 2 11    300 0 960     670  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i 2 28    20 340   - - - - 2 150    460 0 960     1100  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i 2 30    18 380   - - - - 2 150    470 0 960     1300  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i 2 .36 11 3.6 - - - - 2 6.5  300 2 33     560  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i 2 .34 11 4.0 - - - - 2 5.6  320 2 150     610  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i 0 900    89 6500   - - - - 0 .67 43 0 .019 4.9
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i 0 900    190 9700   - - - - 0 .62 44 0 .024 4.8
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i 0 900    120 12000   - - - - 0 .39 43 0 .018 4.9
bitvector/jain_5_true-unreach-call_true-no-overflow.i 0 890    11 11000   - - - - 0 .70 44 0 .024 4.9
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i 0 890    110 11000   - - - - 0 .55 43 0 .019 4.9
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i 0 890    120 11000   - - - - 0 .42 44 0 .018 4.9
bitvector/modulus_true-unreach-call_true-no-overflow.i 2 790    63 9900   - - - - 2 13    320 2 15     330  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i 2 .32 11 3.6 - - - - 2 5.7  290 2 76     640  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i 0 .27 11 4.2 - - - - 0 .59 43 0 .019 4.9
bitvector/parity_true-unreach-call_true-no-overflow.i 2 9.4  13 130   - - - - 2 23    340 0 960     990  
bitvector/sum02_true-unreach-call_true-no-overflow.i 0 900    700 12000   - - - - 0 .60 43 0 .024 4.8
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c -32 67    19 870   0 15    570 1 28     540   0 1.3  53 0 .071  9.1  - -
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c 0 150    42 2200   0 .59 43 0 .020 4.9 0 1.1  49 0 .0015 .27 - -
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c -32 4.1  15 53   0 17    350 1 28     510   0 1.1  51 0 .078  9.1  - -
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c 0 890    42 11000   - - - - 0 .55 43 0 .029 4.8
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c 0 890    43 11000   - - - - 0 .68 41 0 .025 5.0
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c 0 890    43 11000   - - - - 0 .56 43 0 .023 4.9
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 0 .38 12 5.3 - - - - 0 .62 43 0 .018 4.9
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c 0 .41 12 4.8 - - - - 0 .55 44 0 .025 4.8
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c 0 890    110 13000   - - - - 0 .59 43 0 .024 4.8
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c 0 900    130 12000   - - - - 0 .68 42 0 .020 4.8
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900    170 9500   - - - - 0 .54 43 0 .019 4.8
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c 0 890    160 11000   - - - - 0 .57 43 0 .021 4.9
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c 0 900    220 12000   - - - - 0 .59 44 0 .020 5.0
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c 0 900    150 11000   - - - - 0 .55 43 0 .025 4.9
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c 0 900    200 11000   - - - - 0 .54 41 0 .018 4.9
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c 0 900    230 11000   - - - - 0 .70 43 0 .028 4.8
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c 0 890    150 10000   - - - - 0 .55 43 0 .024 4.8
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c 1 .31 11 3.8 -32 2.2  260 1 9.3   220   0 3.2  180 1 .64   18    - -
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c 1 .29 11 3.1 -32 3.6  250 1 3.0   220   0 3.2  190 1 .60   18    - -
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c 1 .31 11 4.0 -32 3.7  260 1 10     220   0 2.7  180 1 .58   19    - -
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c 1 1.9  12 26   0 92    1400 -32 6.8   270   0 2.8  210 1 .69   18    - -
bitvector-regression/signextension2_false-unreach-call_true-termination.c 1 .32 11 4.0 -32 3.5  260 1 5.3   230   0 3.3  180 1 .71   18    - -
bitvector-regression/signextension_false-unreach-call_true-termination.c 1 .32 11 4.0 -32 3.9  250 1 4.9   220   0 2.9  190 1 .77   18    - -
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c 0 .26 11 3.0 - - - - 0 .57 44 0 .018 4.8
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c 0 .30 11 3.4 - - - - 0 .71 43 0 .021 4.8
bitvector-regression/signextension2_true-unreach-call_true-termination.c 0 .26 11 3.2 - - - - 0 .55 44 0 .020 4.9
bitvector-regression/signextension_true-unreach-call_true-termination.c 0 .29 11 3.1 - - - - 0 .58 41 0 .025 4.8
bitvector-loops/diamond_false-unreach-call2.i 1 .42 11 4.6 -32 4.6  270 -32 5.3   260   0 3.6  210 1 .67   18    - -
bitvector-loops/overflow_false-unreach-call1.i 0 890    11 13000   0 .45 43 0 .023 4.8 0 .96 49 0 .0017 .26 - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i -32 2.7  14 35   0 16    470 0 97     570   0 .95 50 0 .067  9.0  - -
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 status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 50 -68 20000   4200 250000 14 -224 170 4800 14 -89 200 3500 14 0 32 1900 14 8 5.6 180 36 20 400 4600 36 8 6000 8500
    correct results 18 28 880   280 11000 0 7 7 88 2200 0 8 8 5.4 150 10 20 390 3400 4 8 270 2100
        correct true 10 20 870   190 11000 0 0 0 0 10 20 390 3400 4 8 270 2100
        correct false 8 8 5.2 92 65 0 7 7 88 2200 0 8 8 5.4 150 0 0
    incorrect results 3 -96 74   47 960 7 -224 32 1900 3 -96 18 760 0 0 0 0
        incorrect true 3 -96 74   47 960 7 -224 32 1900 3 -96 18 760 0 0 0 0
        incorrect false 0 0 0 0 0 0 0
score (50 tasks, max score: 86) -68 -224 -89 0 8 20 8
Run set map2check.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.ReachSafety-BitVectors