Tool 2LS 0.6.0 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:32:03 CET 2017-12-01 08:01:50 CET 2017-12-01 08:11:41 CET 2017-12-01 08:15:34 CET 2017-12-01 04:23:32 CET 2017-12-01 07:36:49 CET
Run set 2ls.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-BitVectors
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.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/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.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/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/2ls.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 .32  28 3.8  false(unreach-call) 1 wit inspect 3.7  270 true -32 wit inspect 20     530   unknown 0 wit inspect 3.9  220 false(unreach-call) 1 wit inspect .70   18    - wit inspect - wit inspect
bitvector/sum02_false-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     1400 10000    error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .90 49 error (invalid witness file) 0 wit inspect .0015 .27 - wit inspect - wit inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .33  29 4.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.2  370 timeout 0 wit inspect 960     1100  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .34  31 3.7  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.6  310 timeout 0 wit inspect 960     1100  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .25  27 2.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.7  310 false(unreach-call) -16 wit inspect 5.3   260  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .76  39 9.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 160    460 timeout 0 wit inspect 960     630  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect .64  40 7.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 160    480 timeout 0 wit inspect 960     4300  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .56  33 6.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.8  320 true 2 wit inspect 45     570  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect .48  55 5.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6  310 true 2 wit inspect 170     610  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900     1500 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .030 5.0
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900     1500 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .019 5.0
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900     1900 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 5.0
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     1400 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .020 4.9
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900     1800 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 42 error (2) 0 wit inspect .018 4.9
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900     1700 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 46 error (2) 0 wit inspect .018 4.8
bitvector/modulus_true-unreach-call_true-no-overflow.i true 2 wit inspect .63  39 8.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 13    330 true 2 wit inspect 16     330  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .12  24 1.2  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  270 true 2 wit inspect 54     640  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .17  24 1.2  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  280 timeout 0 wit inspect 960     1100  
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.7   44 30    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 26    380 timeout 0 wit inspect 960     1000  
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     1500 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .019 4.9
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 9.4   220 77    true -32 wit inspect 4.6  270 true -32 wit inspect 6.4   320   unknown 0 wit inspect 4.0  220 false(unreach-call) 1 wit inspect .81   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 7.3   240 83    true -32 wit inspect 4.9  270 true -32 wit inspect 9.4   350   unknown 0 wit inspect 4.7  230 false(unreach-call) 1 wit inspect .94   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 7.3   150 67    true -32 wit inspect 4.6  270 true -32 wit inspect 6.8   300   unknown 0 wit inspect 4.3  220 false(unreach-call) 1 wit inspect .72   19    - wit inspect - wit inspect
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 46     320 410    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 81    810 true 2 wit inspect 40     760  
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 8.0   280 95    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 19    480 true 2 wit inspect 48     880  
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 9.1   250 84    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 16    410 true 2 wit inspect 34     800  
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900     810 9700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .048 5.0
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900     7600 9900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .019 4.8
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c timeout 0 wit inspect 900     6700 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 42 error (2) 0 wit inspect .023 4.8
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c timeout 0 wit inspect 900     6800 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .019 4.9
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900     7100 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .020 4.8
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900     7000 9700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 45 error (2) 0 wit inspect .020 4.9
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect .22  28 2.0  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 true 2 wit inspect 110     780  
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect .17  29 1.4  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6200 true 2 wit inspect 50     700  
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 1 wit inspect 4.0   160 48    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6300 timeout 0 wit inspect 960     770  
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 1.1   36 12    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 220    640 true 2 wit inspect 310     820  
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect .17  28 1.3  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 true 2 wit inspect 24     620  
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .090 22 1.2  true -32 wit inspect 2.8  260 true -32 wit inspect 5.0   220   unknown 0 wit inspect 2.7  210 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 .099 22 .83 true -32 wit inspect 2.8  260 true -32 wit inspect 5.2   220   unknown 0 wit inspect 3.6  190 false(unreach-call) 1 wit inspect .76   18    - wit inspect - wit inspect
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12  22 .82 true -32 wit inspect 3.1  260 true -32 wit inspect 4.6   210   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c error (5) 0 wit inspect .11  22 .64 error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .92 48 error (invalid witness file) 0 wit inspect .0012 .33 - wit inspect - wit inspect
bitvector-regression/signextension2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .13  22 .83 true -32 wit inspect 3.0  260 true -32 wit inspect 4.8   210   unknown 0 wit inspect 3.3  180 false(unreach-call) 1 wit inspect .71   18    - wit inspect - wit inspect
bitvector-regression/signextension_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12  22 .77 true -32 wit inspect 2.7  260 true -32 wit inspect 4.8   210   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c true 2 wit inspect .10  22 .82 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 6.0   250  
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c true 2 wit inspect .12  22 .84 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 9.2   240  
bitvector-regression/signextension2_true-unreach-call_true-termination.c true 2 wit inspect .12  22 .74 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 4.9   260  
bitvector-regression/signextension_true-unreach-call_true-termination.c true 2 wit inspect .12  22 .76 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  250 true 2 wit inspect 5.4   250  
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) 1 wit inspect .12  24 1.1  false(unreach-call) 1 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 5.2   270   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
bitvector-loops/overflow_false-unreach-call1.i timeout 0 wit inspect 900     1300 11000    error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .91 49 error (invalid witness file) 0 wit inspect .0018 .26 - wit inspect - wit inspect
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .54  37 6.0  false(unreach-call) 1 wit inspect 4.5  290 out of memory 0 wit inspect 49     7000   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .65   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 56 14000   52000 160000 14 -253 42 3000 14 -287 120   9800 14 0 43 2500 14 11 7.7 210 36 38 4400 32000 36 14 7700   19000
    correct results 33 55 98   2200 930 3 3 12 810 1 1 5.2 270 0 11 11 7.7 210 19 38 760 7200 15 30 920   8500
        correct true 22 44 72   1400 690 0 0 0 0 19 38 760 7200 15 30 920   8500
        correct false 11 11 26   800 240 3 3 12 810 1 1 5.2 270 0 11 11 7.7 210 0 0
    correct-unconfimed results 1 1 4.0 160 48 0 0 0 0 0 0
        correct-unconfirmed true 1 1 4.0 160 48 0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0
    incorrect results 0 8 -256 28 2100 9 -288 67   2600 0 0 0 1 -16 5.3 260
        incorrect true 0 8 -256 28 2100 9 -288 67   2600 0 0 0 0
        incorrect false 0 0 0 0 0 0 1 -16 5.3 260
score (50 tasks, max score: 86) 56 -253 -287 0 11 38 14
Run set 2ls.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-BitVectors