Tool 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:29:20 CET 2017-12-01 08:07:14 CET 2017-12-01 08:15:38 CET 2017-12-01 08:19:10 CET 2017-12-01 04:11:27 CET 2017-12-01 07:35:08 CET
Run set cpa-seq.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-BitVectors
Options -svcomp18 -heap 10000M -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.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-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.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-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-seq.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 17   440 180 false(unreach-call) 1 wit inspect 4.6  270 false(unreach-call) 1 wit inspect 40     570   unknown 0 wit inspect 3.5  220 true -32 wit inspect .68   19    - wit inspect - wit inspect
bitvector/sum02_false-unreach-call_true-no-overflow.i timeout 0 wit inspect 910   7700 10000 error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 12   440 100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9  340 timeout 0 wit inspect 960     1100  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 13   470 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.8  300 timeout 0 wit inspect 960     1100  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 6.8 280 76 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 10    300 timeout 0 wit inspect 960     1700  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 7.6 280 83 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 130    460 timeout 0 wit inspect 960     610  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 150   310 2000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 170    480 timeout 0 wit inspect 960     1000  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 2.5 260 20 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.5  320 false(unreach-call) -16 wit inspect 5.9   260  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect 7.4 450 75 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.8  320 true 2 wit inspect 160     610  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 3.1 270 28 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5700 true 2 wit inspect 6.4   250  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 3.2 280 26 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 890    7000 true 2 wit inspect 5.2   260  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 3.3 280 29 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 710    7000 true 2 wit inspect 5.4   260  
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   3500 9800 - 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/jain_6_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 3.4 280 29 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 710    7000 true 2 wit inspect 21     270  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 4.6 280 52 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 800    7000 true 2 wit inspect 5.6   260  
bitvector/modulus_true-unreach-call_true-no-overflow.i true 2 wit inspect 220   2100 2400 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 14    320 false(unreach-call) -16 wit inspect 11     280  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.4 250 20 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4  270 true 2 wit inspect 51     640  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 16   470 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0  270 timeout 0 wit inspect 960     1100  
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect 120   980 1400 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 23    340 timeout 0 wit inspect 960     990  
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 910   7000 8100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.9
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 8.6 320 68 false(unreach-call) 1 wit inspect 5.1  290 false(unreach-call) 1 wit inspect 18     470   unknown 0 wit inspect 4.4  230 true -32 wit inspect .71   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 26   810 260 false(unreach-call) 1 wit inspect 5.4  280 false(unreach-call) 1 wit inspect 20     460   unknown 0 wit inspect 4.5  220 true -32 wit inspect .70   21    - wit inspect - wit inspect
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 6.1 300 52 false(unreach-call) 1 wit inspect 4.2  270 false(unreach-call) 1 wit inspect 17     400   unknown 0 wit inspect 3.9  220 true -32 wit inspect .85   20    - wit inspect - wit inspect
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 15   750 160 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 59    950 true 2 wit inspect 46     810  
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 14   730 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 18    480 true 2 wit inspect 48     970  
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 15   750 160 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 15    560 true 2 wit inspect 20     920  
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   4200 8900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .023 4.9
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 17   760 150 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5300 true 2 wit inspect 50     1200  
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c true 2 wit inspect 51   1300 560 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4200 true 2 wit inspect 33     1100  
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c true 2 wit inspect 56   2400 630 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4200 true 2 wit inspect 39     1100  
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 17   760 160 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6100 true 2 wit inspect 50     1200  
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 16   770 170 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 true 2 wit inspect 36     1300  
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 12   380 130 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6400 true 2 wit inspect 130     760  
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 110   1300 1300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6300 true 2 wit inspect 60     700  
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 1 wit inspect 100   1300 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6300 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 170   400 2400 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 180    620 true 2 wit inspect 370     790  
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 110   1200 1400 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6300 true 2 wit inspect 24     610  
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.5 250 22 false(unreach-call) 1 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 9.0   220   unknown 0 wit inspect 2.9  190 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.8 270 27 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.5   220   unknown 0 wit inspect 2.7  190 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.5 250 21 false(unreach-call) 1 wit inspect 3.1  250 false(unreach-call) 1 wit inspect 8.9   220   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .75   18    - wit inspect - wit inspect
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 64   1600 700 false(unreach-call) 1 wit inspect 7.4  280 false(unreach-call) 1 wit inspect 40     1000   unknown 0 wit inspect 4.7  220 false(unreach-call) 1 wit inspect .61   19    - wit inspect - wit inspect
bitvector-regression/signextension2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 250 25 false(unreach-call) 1 wit inspect 3.0  250 true -32 wit inspect 4.3   220   unknown 0 wit inspect 3.4  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
bitvector-regression/signextension_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.5 260 26 false(unreach-call) 1 wit inspect 3.1  260 true -32 wit inspect 5.7   290   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .69   18    - wit inspect - wit inspect
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c true 2 wit inspect 2.6 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 4.5   240  
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c true 2 wit inspect 2.4 250 22 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  240 true 2 wit inspect 9.2   230  
bitvector-regression/signextension2_true-unreach-call_true-termination.c true 2 wit inspect 2.3 240 18 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  240 true 2 wit inspect 5.4   260  
bitvector-regression/signextension_true-unreach-call_true-termination.c true 2 wit inspect 2.3 250 20 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.6   260  
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) 1 wit inspect 5.3 280 46 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 6.5   260   unknown 0 wit inspect 3.3  190 true -32 wit inspect .72   19    - wit inspect - wit inspect
bitvector-loops/overflow_false-unreach-call1.i timeout 0 wit inspect 900   6800 9300 error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0011 .34 - wit inspect - wit inspect
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 210   1400 2700 false(unreach-call) 1 wit inspect 4.4  290 out of memory 0 wit inspect 53     7000   unknown 0 wit inspect 3.5  220 false(unreach-call) 1 wit inspect .76   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 77 6200 57000 66000 14 12 52 3300 14 -55 230 11000 14 0 44 2600 14 -153 8.3 230 36 38 13000 91000 36 14 8900 24000
    correct results 44 76 1600 27000 18000 12 12 51 3200 9 9 160 3800 0 7 7 4.6 130 19 38 670 7300 23 46 1200 15000
        correct true 32 64 1200 20000 14000 0 0 0 0 19 38 670 7300 23 46 1200 15000
        correct false 12 12 350 6400 4100 12 12 51 3200 9 9 160 3800 0 7 7 4.6 130 0 0
    correct-unconfimed results 1 1 100 1300 1100 0 0 0 0 0 0
        correct-unconfirmed true 1 1 100 1300 1100 0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0
    incorrect results 0 0 2 -64 10 510 0 5 -160 3.7 99 0 2 -32 17 540
        incorrect true 0 0 2 -64 10 510 0 5 -160 3.7 99 0 0
        incorrect false 0 0 0 0 0 0 2 -32 17 540
score (50 tasks, max score: 86) 77 12 -55 0 -153 38 14
Run set cpa-seq.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-BitVectors