Tool ULTIMATE Taipan 0.1.23-3204b741 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-12-02 17:23:13 CET 2017-12-03 07:22:17 CET 2017-12-03 07:45:29 CET 2017-12-03 07:47:53 CET 2017-12-03 07:50:34 CET 2017-12-03 06:47:45 CET 2017-12-03 07:25:40 CET
Run set utaipan.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.ReachSafety-BitVectors
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.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/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.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/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/utaipan.2017-12-02_1723.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 110   1500 940 false(unreach-call) 1 wit inspect 3.6  280 false(unreach-call) 1 wit inspect 25     510   unknown 0 wit inspect 3.8  220 true -32 wit inspect .61   19    - wit inspect - wit inspect
bitvector/sum02_false-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   700 11000 error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .050 5.0 error (invalid witness file) 0 wit inspect .80 47 error (invalid witness file) 0 wit inspect .0037 .34 - wit inspect - wit inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i timeout 0 wit inspect 900   2600 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .017 5.0
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i timeout 0 wit inspect 900   3100 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.9
bitvector/gcd_1_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   1000 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .018 4.9
bitvector/gcd_2_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   1100 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .043 4.9
bitvector/gcd_3_true-unreach-call_true-no-overflow.i error (7) 0 wit inspect 510   1200 4100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .048 4.9
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 240   900 2800 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8  300 true 2 wit inspect 46     590  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect 230   1800 3100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1  310 true 2 wit inspect 120     650  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 4.6 290 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  270 true 2 wit inspect 5.5   260  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 4.7 290 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  280 true 2 wit inspect 11     280  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 4.8 290 44 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  280 true 2 wit inspect 5.2   260  
bitvector/jain_5_true-unreach-call_true-no-overflow.i true 1 wit inspect 6.3 310 53 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 630    7000 timeout 0 wit inspect 960     710  
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 8.0 300 86 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  290 true 2 wit inspect 6.6   280  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 5.1 290 44 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    510 true 2 wit inspect 40     300  
bitvector/modulus_true-unreach-call_true-no-overflow.i true 2 wit inspect 13   500 110 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 11    320 true 2 wit inspect 12     300  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 59   670 670 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  270 true 2 wit inspect 51     590  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   1300 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .050 5.0
bitvector/parity_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   1000 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .021 4.8
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   650 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .026 4.9
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 26   580 210 true -32 wit inspect 6.0  270 false(unreach-call) 1 wit inspect 15     450   unknown 0 wit inspect 4.1  220 true -32 wit inspect .64   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 27   690 210 true -32 wit inspect 6.0  270 false(unreach-call) 1 wit inspect 20     520   unknown 0 wit inspect 4.3  220 true -32 wit inspect .64   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 24   610 190 true -32 wit inspect 6.0  270 false(unreach-call) 1 wit inspect 17     410   unknown 0 wit inspect 3.7  220 true -32 wit inspect .63   20    - wit inspect - wit inspect
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 39   1100 330 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 72    810 true 2 wit inspect 41     760  
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 45   1400 360 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 21    560 true 2 wit inspect 42     920  
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 270   4800 3700 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 14    410 out of memory 0 wit inspect 120     7000  
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   5100 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.9
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 230   4700 2500 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4400 true 2 wit inspect 47     1000  
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c timeout 0 wit inspect 900   5400 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .020 4.9
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c timeout 0 wit inspect 900   5000 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .047 4.8
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 250   4800 2900 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5300 true 2 wit inspect 33     970  
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 230   4800 2800 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5400 true 2 wit inspect 35     870  
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c error (7) 0 wit inspect 110   870 1400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 42 error (2) 0 wit inspect .021 4.9
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 84   1300 830 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 true 2 wit inspect 51     690  
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c timeout 0 wit inspect 900   1100 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .018 4.9
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 860   940 11000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 250    630 true 2 wit inspect 310     840  
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 63   1200 620 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 true 2 wit inspect 22     590  
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.3 240 67 false(unreach-call) 1 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 8.3   230   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.0 240 37 false(unreach-call) 1 wit inspect 3.1  250 false(unreach-call) 1 wit inspect 4.3   220   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 9.6 320 76 false(unreach-call) 1 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 8.3   220   unknown 0 wit inspect 2.5  180 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 290   1200 4000 false(unreach-call) 1 wit inspect 5.3  280 true -32 wit inspect 4.9   270   unknown 0 wit inspect 3.6  210 true -32 wit inspect .60   19    - wit inspect - wit inspect
bitvector-regression/signextension2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.4 250 34 false(unreach-call) 1 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 4.4   220   unknown 0 wit inspect 2.8  190 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 4.1 250 34 false(unreach-call) 1 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 5.0   230   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c true 2 wit inspect 4.3 270 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  260 true 2 wit inspect 4.6   250  
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c true 2 wit inspect 8.9 290 70 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  240 true 2 wit inspect 8.6   250  
bitvector-regression/signextension2_true-unreach-call_true-termination.c true 2 wit inspect 4.7 290 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  260 true 2 wit inspect 5.3   250  
bitvector-regression/signextension_true-unreach-call_true-termination.c true 2 wit inspect 4.7 290 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  240 true 2 wit inspect 5.3   260  
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) 1 wit inspect 13   550 110 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 5.7   280   unknown 0 wit inspect 3.0  210 true -32 wit inspect .60   19    - wit inspect - wit inspect
bitvector-loops/overflow_false-unreach-call1.i timeout 0 wit inspect 900   1500 9700 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .043 4.9 error (invalid witness file) 0 wit inspect .81 49 error (invalid witness file) 0 wit inspect .0037 .34 - wit inspect - wit inspect
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 550   2000 8400 true -32 wit inspect 3.4  260 out of memory 0 wit inspect 57     7000   unknown 0 wit inspect 3.0  190 true -32 wit inspect .58   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 16000   72000 200000 14 -120 49 3300 14 -22 180   11000 14 0 40 2500 14 -219 7.2 230 36 32 6500 41000 36 42 2000 19000
    correct results 33 55 3200   38000 38000 8 8 27 2100 10 10 110   3300 0 5 5 2.9 92 16 32 410 5700 21 42 900 11000
        correct true 22 44 2700   31000 32000 0 0 0 0 16 32 410 5700 21 42 900 11000
        correct false 11 11 520   6400 6000 8 8 27 2100 10 10 110   3300 0 5 5 2.9 92 0 0
    correct-unconfimed results 2 1 560   2300 8500 0 0 0 0 0 0
        correct-unconfirmed true 1 1 6.3 310 53 0 0 0 0 0 0
        correct-unconfirmed false 1 0 550   2000 8400 0 0 0 0 0 0
    incorrect results 0 4 -128 21 1100 1 -32 4.9 270 0 7 -224 4.3 140 0 0
        incorrect true 0 4 -128 21 1100 1 -32 4.9 270 0 7 -224 4.3 140 0 0
        incorrect false 0 0 0 0 0 0 0
score (50 tasks, max score: 86) 56 -120 -22 0 -219 32 42
Run set utaipan.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.ReachSafety-BitVectors