Tool VeriAbs 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* [apollon020; apollon077; apollon078; apollon084; apollon149; apollon164] apollon* [apollon037; apollon065; apollon077; apollon078; apollon155; apollon159] 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 18:04:04 CET 2017-12-03 04:46:33 CET 2017-12-03 06:08:30 CET 2017-12-03 06:21:09 CET 2017-12-03 06:27:12 CET 2017-12-03 03:55:53 CET 2017-12-03 04:55:47 CET
Run set veriabs.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-BitVectors
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.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/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.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/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/veriabs.2017-12-02_1804.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 29   430 260 false(unreach-call) 1 wit inspect 3.8  270 false(unreach-call) 1 wit inspect 36     600   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .71   19    - wit inspect - wit inspect
bitvector/sum02_false-unreach-call_true-no-overflow.i unknown 0 wit inspect 470   3100 3700 error (invalid witness file) 0 wit inspect .40 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .68 51 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 29   570 210 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 14    320 timeout 0 wit inspect 960     2700  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 27   480 180 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    320 timeout 0 wit inspect 960     2700  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 21   300 190 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    320 false(unreach-call) -16 wit inspect 6.1   270  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 53   400 590 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 140    480 timeout 0 wit inspect 960     790  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 52   410 630 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 140    460 error (7) 0 wit inspect 550     900  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 17   320 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.2  320 false(unreach-call) -16 wit inspect 5.7   260  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect 18   330 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.2  370 true 2 wit inspect 380     1000  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i unknown 0 wit inspect 370   4800 4000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 46 error (2) 0 wit inspect .019 4.8
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i unknown 0 wit inspect 510   4300 6100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .018 4.8
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i unknown 0 wit inspect 620   5700 6900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .018 5.0
bitvector/jain_5_true-unreach-call_true-no-overflow.i true 1 wit inspect 8.0 220 63 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1700 timeout 0 wit inspect 960     640  
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i unknown 0 wit inspect 620   5400 6600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .020 4.9
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i unknown 0 wit inspect 510   5100 6800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .020 4.9
bitvector/modulus_true-unreach-call_true-no-overflow.i true 2 wit inspect 30   610 290 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 16    340 true 2 wit inspect 13     310  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 16   290 110 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  270 true 2 wit inspect 59     640  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 16   310 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  280 timeout 0 wit inspect 960     1100  
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect 32   340 330 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 25    410 timeout 0 wit inspect 960     1000  
bitvector/sum02_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 390   3200 3100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 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 59   420 590 false(unreach-call) 1 wit inspect 5.5  280 false(unreach-call) 1 wit inspect 20     490   unknown 0 wit inspect 3.1  220 false(unreach-call) 1 wit inspect .74   21    - wit inspect - wit inspect
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 150   880 1700 false(unreach-call) 1 wit inspect 6.0  290 false(unreach-call) 1 wit inspect 20     520   unknown 0 wit inspect 4.4  220 false(unreach-call) 1 wit inspect .74   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 130   790 1400 false(unreach-call) 1 wit inspect 3.7  300 false(unreach-call) 1 wit inspect 17     430   unknown 0 wit inspect 3.1  220 true -32 wit inspect .73   20    - wit inspect - wit inspect
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 93   750 900 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 30    560 true 2 wit inspect 200     2300  
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 1 wit inspect 170   900 1800 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 7.8  350 false(unreach-call) -16 wit inspect 8.6   330  
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 1 wit inspect 160   790 1700 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 7.1  290 false(unreach-call) -16 wit inspect 11     360  
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 550   1000 6400 - 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/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   1300 5000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 41 error (2) 0 wit inspect .020 4.9
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c timeout 0 wit inspect 900   1400 7400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .018 4.9
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c timeout 0 wit inspect 900   1400 7500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .018 4.9
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   1300 5600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 42 error (2) 0 wit inspect .018 5.0
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900   1200 5800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .019 4.9
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 98   820 960 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 true 2 wit inspect 120     770  
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 1 wit inspect 40   780 420 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4600 timeout 0 wit inspect 960     670  
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 1 wit inspect 85   740 850 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6300 timeout 0 wit inspect 960     750  
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 100   810 1100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 210    630 true 2 wit inspect 300     810  
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 1 wit inspect 40   740 390 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4600 timeout 0 wit inspect 960     680  
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.5 300 63 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 9.2   220   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.6 300 61 false(unreach-call) 1 wit inspect 2.1  260 false(unreach-call) 1 wit inspect 4.9   210   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.3 270 62 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 6.2   220   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c error 0 wit inspect 7.1 160 57 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .63 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
bitvector-regression/signextension2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.7 300 61 false(unreach-call) 1 wit inspect 2.0  260 true -32 wit inspect 4.6   210   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
bitvector-regression/signextension_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.2 280 61 false(unreach-call) 1 wit inspect 2.1  260 true -32 wit inspect 4.6   210   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c true 2 wit inspect 7.7 270 71 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 4.6   250  
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c true 2 wit inspect 7.8 260 67 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 8.8   230  
bitvector-regression/signextension2_true-unreach-call_true-termination.c true 2 wit inspect 8.1 270 69 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  240 true 2 wit inspect 3.5   260  
bitvector-regression/signextension_true-unreach-call_true-termination.c true 2 wit inspect 8.0 260 71 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 3.6   260  
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) 1 wit inspect 23   430 190 true -32 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 6.0   260   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
bitvector-loops/overflow_false-unreach-call1.i false(unreach-call) 1 wit inspect 11   280 84 timeout 0 wit inspect 91    1600 true -32 wit inspect 4.6   220   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect 4.3    18    - wit inspect - wit inspect
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 19   280 160 true -32 wit inspect 2.8  270 out of memory 0 wit inspect 59     7000   unknown 0 wit inspect 3.4  220 error (2) 0 wit inspect .62   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 53 10000 56000 91000 14 -55 130   4600 14 -88 190 11000 14 0 37 2600 14 -22 11    230 36 34 5200 30000 36 -44 10000 20000
    correct results 29 47 1100 13000 11000 9 9 32   2400 8 8 120 3000 0 10 10 10    190 17 34 640 6100 10 20 1100 6900
        correct true 18 36 640 7800 6200 0 0 0 0 17 34 640 6100 10 20 1100 6900
        correct false 11 11 440 4700 4500 9 9 32   2400 8 8 120 3000 0 10 10 10    190 0 0
    correct-unconfimed results 7 6 530 4400 5300 0 0 0 0 0 0
        correct-unconfirmed true 6 6 510 4200 5200 0 0 0 0 0 0
        correct-unconfirmed false 1 0 19 280 160 0 0 0 0 0 0
    incorrect results 0 2 -64 6.6 520 3 -96 14 640 0 1 -32 .73 20 0 4 -64 32 1200
        incorrect true 0 2 -64 6.6 520 3 -96 14 640 0 1 -32 .73 20 0 0
        incorrect false 0 0 0 0 0 0 4 -64 32 1200
score (50 tasks, max score: 86) 53 -55 -88 0 -22 34 -44
Run set veriabs.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-BitVectors