Tool CPAchecker 1.6.1-svn 26725 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:36:53 CET 2017-12-01 08:24:12 CET 2017-12-01 08:27:09 CET 2017-12-01 08:31:26 CET 2017-12-01 04:24:37 CET 2017-12-01 07:42:15 CET
Run set cpa-bam-bnb.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-BitVectors
Options -svcomp18-bam-bnb -disable-java-assertions -heap 10000m -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-bnb.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/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-bnb.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/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-bam-bnb.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 error 0 wit inspect 11   470 87 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .81 49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
bitvector/sum02_false-unreach-call_true-no-overflow.i error 0 wit inspect 3.6 290 32 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i error 0 wit inspect 9.5 480 75 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 42 error (2) 0 wit inspect .018 4.9
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i error 0 wit inspect 13   520 100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .025 4.8
bitvector/gcd_1_true-unreach-call_true-no-overflow.i error 0 wit inspect 7.4 310 90 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .024 5.0
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 3.9 280 31 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 140    470 error (7) 0 wit inspect 820     950  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i error 0 wit inspect 5.3 300 49 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .019 4.9
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 3.3 270 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.1  320 false(unreach-call) -16 wit inspect 5.6   260  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i error 0 wit inspect 5.9 380 49 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .025 4.8
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 3.0 270 26 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5900 true 2 wit inspect 6.0   260  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 3.2 280 28 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 770    7000 true 2 wit inspect 5.3   270  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 3.2 270 25 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 710    7000 true 2 wit inspect 5.3   260  
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   3900 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 45 error (2) 0 wit inspect .020 4.9
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 3.2 280 32 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 580    7000 true 2 wit inspect 23     340  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 3.2 280 30 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 810    7000 true 2 wit inspect 5.1   260  
bitvector/modulus_true-unreach-call_true-no-overflow.i error 0 wit inspect 18   310 240 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 44 error (2) 0 wit inspect .018 4.8
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 3.3 280 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  270 true 2 wit inspect 49     630  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   330 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .023 4.9
bitvector/parity_true-unreach-call_true-no-overflow.i error 0 wit inspect 3.5 290 29 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .019 4.9
bitvector/sum02_true-unreach-call_true-no-overflow.i error 0 wit inspect 3.4 290 31 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .023 4.9
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   4400 12000 error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .023 5.0 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 27   1100 210 false(unreach-call) 1 wit inspect 5.7  280 false(unreach-call) 1 wit inspect 23     490   unknown 0 wit inspect 4.5  220 true -32 wit inspect .68   20    - wit inspect - wit inspect
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c error 0 wit inspect 6.9 400 66 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .93 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   4400 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .021 4.8
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 38   2000 260 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 17    450 true 2 wit inspect 46     970  
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 27   1100 210 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 15    410 true 2 wit inspect 37     840  
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   6700 9000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .022 4.8
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 11   510 86 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4600 true 2 wit inspect 50     1100  
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c true 2 wit inspect 11   500 87 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4000 true 2 wit inspect 36     1100  
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c true 2 wit inspect 12   520 95 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 true 2 wit inspect 33     1100  
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   4100 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 4.8
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   4100 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c error 0 wit inspect 5.0 320 47 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .019 5.0
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c error 0 wit inspect 5.5 300 43 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 44 error (2) 0 wit inspect .023 4.9
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c error 0 wit inspect 5.2 300 41 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .021 5.0
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c error 0 wit inspect 4.6 320 41 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 5.0
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c error 0 wit inspect 5.6 320 48 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 42 error (2) 0 wit inspect .022 4.9
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.1 280 27 false(unreach-call) 1 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 11     220   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c true -32 wit inspect 2.8 270 24 false(unreach-call) 1 wit inspect 4.4  250 false(unreach-call) 1 wit inspect 4.5   220   unknown 0 wit inspect .89 52 error (1) 0 wit inspect .074  9.0  - wit inspect - wit inspect
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.1 280 26 false(unreach-call) 1 wit inspect 3.9  260 false(unreach-call) 1 wit inspect 12     220   unknown 0 wit inspect 3.0  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect 3.3 290 30 timeout 0 wit inspect 91    1800 true -32 wit inspect 21     410   unknown 0 wit inspect 2.9  210 true -32 wit inspect .57   18    - wit inspect - wit inspect
bitvector-regression/signextension2_false-unreach-call_true-termination.c true -32 wit inspect 2.8 270 25 false(unreach-call) 1 wit inspect 3.7  250 false(unreach-call) 1 wit inspect 4.7   220   unknown 0 wit inspect 1.2  51 error (1) 0 wit inspect .066  9.0  - wit inspect - wit inspect
bitvector-regression/signextension_false-unreach-call_true-termination.c true -32 wit inspect 2.8 270 27 false(unreach-call) 1 wit inspect 4.6  250 false(unreach-call) 1 wit inspect 4.3   220   unknown 0 wit inspect .91 51 error (1) 0 wit inspect .070  9.0  - wit inspect - wit inspect
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c true 2 wit inspect 2.8 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  250 true 2 wit inspect 6.4   250  
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c true 2 wit inspect 3.0 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 9.3   250  
bitvector-regression/signextension2_true-unreach-call_true-termination.c true 2 wit inspect 2.8 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 6.3   260  
bitvector-regression/signextension_true-unreach-call_true-termination.c true 2 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.7   260  
bitvector-loops/diamond_false-unreach-call2.i true -32 wit inspect 9.8 480 78 unknown 0 wit inspect 6.5  280 false(unreach-call) 1 wit inspect 10     330   unknown 0 wit inspect 1.1  54 error (1) 0 wit inspect .069  9.1  - wit inspect - wit inspect
bitvector-loops/overflow_false-unreach-call1.i true -32 wit inspect 3.1 280 27 timeout 0 wit inspect 92    1700 false(unreach-call) 1 wit inspect 5.7   260   unknown 0 wit inspect .99 51 error (1) 0 wit inspect .068  9.1  - wit inspect - wit inspect
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i true -32 wit inspect 3.4 280 31 true -32 wit inspect 4.8  270 timeout 0 wit inspect 97     560   unknown 0 wit inspect 1.0  51 error (1) 0 wit inspect .072  9.0  - 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 -155 6600   45000 78000 14 -26 220   5700 14 -24 190 3200 14 0 23 1300 14 -62 2.9 130 36 18 6700 50000 36 14 1200   9400
    correct results 20 37 170   9500 1300 6 6 26   1600 8 8 75 2200 0 2 2 1.2 37 9 18 190 2900 15 30 320   8100
        correct true 17 34 140   7900 1100 0 0 0 0 9 18 190 2900 15 30 320   8100
        correct false 3 3 33   1700 260 6 6 26   1600 8 8 75 2200 0 2 2 1.2 37 0 0
    correct-unconfimed results 1 0 3.3 290 30 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 1 0 3.3 290 30 0 0 0 0 0 0
    incorrect results 6 -192 25   1900 210 1 -32 4.8 270 1 -32 21 410 0 2 -64 1.2 39 0 1 -16 5.6 260
        incorrect true 6 -192 25   1900 210 1 -32 4.8 270 1 -32 21 410 0 2 -64 1.2 39 0 0
        incorrect false 0 0 0 0 0 0 1 -16 5.6 260
score (50 tasks, max score: 86) -155 -26 -24 0 -62 18 14
Run set cpa-bam-bnb.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-BitVectors