Tool CBMC 5.8 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]
Date of execution 2017-11-30 11:20:26 CET 2017-12-01 07:26:01 CET 2017-12-01 07:56:00 CET 2017-12-01 08:08:00 CET 2017-12-01 08:15:34 CET 2017-12-01 04:22:29 CET 2017-12-01 07:31:28 CET
Run set cbmc.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-BitVectors
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-11-30_1120.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/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-11-30_1120.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/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cbmc.2017-11-30_1120.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 false(unreach-call) 1 wit inspect .70 34 6.7 true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 34     530   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .68   19    - wit inspect - wit inspect
bitvector/sum02_false-unreach-call_true-no-overflow.i error (42) 0 wit inspect 870    6000 3300   error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .025 5.0 error (invalid witness file) 0 wit inspect .89 47 error (invalid witness file) 0 wit inspect .0013 .31 - wit inspect - wit inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 1 wit inspect .86 34 8.1 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 8.9  280 timeout 0 wit inspect 960     1100  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 1 wit inspect .85 34 8.5 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 7.2  280 timeout 0 wit inspect 960     1100  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 1 wit inspect .53 36 5.7 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 5.6  290 timeout 0 wit inspect 960     660  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 1 wit inspect 2.0  42 24   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.8  280 timeout 0 wit inspect 960     1800  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 1 wit inspect 2.0  42 26   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 5.5  280 timeout 0 wit inspect 960     5100  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .76 33 9.5 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 23    560 true 2 wit inspect 64     510  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.6  33 14   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 5.7  270 true 2 wit inspect 170     650  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i error (42) 0 wit inspect 870    970 7200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .018 4.9
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i error (42) 0 wit inspect 870    1300 5200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 41 error (2) 0 wit inspect .019 4.8
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i error (42) 0 wit inspect 870    1700 6900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .020 4.8
bitvector/jain_5_true-unreach-call_true-no-overflow.i out of memory 0 wit inspect 380    15000 4800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .024 4.9
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i error (42) 0 wit inspect 870    1600 4300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 4.8
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i error (42) 0 wit inspect 870    1700 5900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .022 5.0
bitvector/modulus_true-unreach-call_true-no-overflow.i true 2 wit inspect 460    1100 2100   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 25    1100 true 2 wit inspect 24     370  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.2  33 11   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.9  270 true 2 wit inspect 66     630  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 1 wit inspect 1.2  33 12   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 5.0  260 timeout 0 wit inspect 960     1100  
bitvector/parity_true-unreach-call_true-no-overflow.i true 1 wit inspect 4.1  35 44   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 5.1  290 timeout 0 wit inspect 960     1000  
bitvector/sum02_true-unreach-call_true-no-overflow.i error (42) 0 wit inspect 880    6300 4400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .018 4.9
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 5.9  220 76   true -32 wit inspect 4.7  280 false(unreach-call) 1 wit inspect 21     530   unknown 0 wit inspect 12    420 true -32 wit inspect .95   20    - wit inspect - wit inspect
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 5.2  180 70   true -32 wit inspect 4.6  260 false(unreach-call) 1 wit inspect 21     480   unknown 0 wit inspect 12    420 true -32 wit inspect .74   20    - wit inspect - wit inspect
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 1.5  64 18   true -32 wit inspect 5.0  260 false(unreach-call) 1 wit inspect 16     400   unknown 0 wit inspect 6.1  280 true -32 wit inspect .73   19    - wit inspect - wit inspect
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 21    360 240   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 530    5600 true 2 wit inspect 47     770  
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 18    290 240   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 230    3900 true 2 wit inspect 68     930  
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 18    280 220   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 240    4000 true 2 wit inspect 36     840  
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c error (42) 0 wit inspect 870    460 8600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .021 4.9
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c error (42) 0 wit inspect 870    940 3500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 4.9
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c error (42) 0 wit inspect 870    800 3200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .019 4.9
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c error (42) 0 wit inspect 870    840 5800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .018 5.0
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c error (42) 0 wit inspect 870    860 5600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .020 4.9
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c error (42) 0 wit inspect 870    840 5600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 5.0
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 6.1  54 72   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 27    670 true 2 wit inspect 120     780  
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 4.5  54 63   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 12    440 true 2 wit inspect 58     710  
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 1 wit inspect 4.6  53 63   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 14    450 timeout 0 wit inspect 960     790  
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 12    52 160   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 70    420 true 2 wit inspect 340     790  
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 4.6  53 53   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 13    460 true 2 wit inspect 29     640  
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .23 33 1.7 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 10     230   unknown 0 wit inspect 2.5  180 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .23 33 1.6 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 4.8   220   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .70   18    - wit inspect - wit inspect
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .23 33 2.0 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 12     310   unknown 0 wit inspect 2.6  210 false(unreach-call) 1 wit inspect .69   18    - wit inspect - wit inspect
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.4  34 22   false(unreach-call) 1 wit inspect 8.8  430 true -32 wit inspect 4.7   260   unknown 0 wit inspect 4.5  230 false(unreach-call) 1 wit inspect .64   19    - wit inspect - wit inspect
bitvector-regression/signextension2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .27 33 2.2 false(unreach-call) 1 wit inspect 3.2  260 true -32 wit inspect 4.2   210   unknown 0 wit inspect 3.1  220 false(unreach-call) 1 wit inspect .74   18    - wit inspect - wit inspect
bitvector-regression/signextension_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .24 33 2.5 false(unreach-call) 1 wit inspect 3.5  250 true -32 wit inspect 4.9   210   unknown 0 wit inspect 3.3  190 false(unreach-call) 1 wit inspect .76   18    - wit inspect - wit inspect
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c true 2 wit inspect .42 33 3.2 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  250 true 2 wit inspect 5.0   240  
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c true 2 wit inspect .40 33 4.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 8.4   220  
bitvector-regression/signextension2_true-unreach-call_true-termination.c true 2 wit inspect .40 33 4.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.2   260  
bitvector-regression/signextension_true-unreach-call_true-termination.c true 2 wit inspect .41 33 4.2 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 5.2   260  
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) 1 wit inspect .25 33 2.3 true -32 wit inspect 2.2  260 false(unreach-call) 1 wit inspect 6.8   260   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
bitvector-loops/overflow_false-unreach-call1.i out of memory 0 wit inspect 310    15000 4300   error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 1.0  34 8.9 true -32 wit inspect 4.5  260 out of memory 0 wit inspect 66     7000   unknown 0 wit inspect 3.4  210 error (2) 0 wit inspect .63   19    - wit inspect - wit inspect
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 49 13000   58000 82000   14 -186 51 3400 14 -88 210 11000 14 0 61 3100 14 -88 8.5 230 36 14 1200 22000 36 30 8700 21000
    correct results 26 41 560   3200 3400   6 6 25 1700 8 8 130 3000 0 8 8 5.5 150 7 14 1000 14000 15 30 1000 8600
        correct true 15 30 550   2400 3200   0 0 0 0 7 14 1000 14000 15 30 1000 8600
        correct false 11 11 17   740 210   6 6 25 1700 8 8 130 3000 0 8 8 5.5 150 0 0
    correct-unconfimed results 9 8 17   340 200   0 0 0 0 0 0
        correct-unconfirmed true 8 8 16   310 190   0 0 0 0 0 0
        correct-unconfirmed false 1 0 1.0 34 8.9 0 0 0 0 0 0
    incorrect results 0 6 -192 25 1600 3 -96 14 690 0 3 -96 2.4 60 0 0
        incorrect true 0 6 -192 25 1600 3 -96 14 690 0 3 -96 2.4 60 0 0
        incorrect false 0 0 0 0 0 0 0
score (50 tasks, max score: 86) 49 -186 -88 0 -88 14 30
Run set cbmc.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-BitVectors