Tool ESBMC ESBMC version 4.6.0 64-bit x86_64 linux 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* [apollon010; apollon035; apollon045; apollon077; apollon078; apollon138] [apollon007; apollon077; apollon078; apollon143] 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-01 08:49:27 CET 2017-12-01 22:53:44 CET 2017-12-01 23:38:04 CET 2017-12-01 23:47:42 CET 2017-12-01 23:55:24 CET 2017-12-01 22:20:30 CET 2017-12-01 23:01:53 CET
Run set esbmc-incr.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-BitVectors
Options -s incr -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.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/esbmc-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.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/esbmc-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/esbmc-incr.2017-12-01_0849.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 1.1   29 10    false(unreach-call) 1 wit inspect 4.7  270 true -32 wit inspect 4.5   280   unknown 0 wit inspect 3.2  220 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
bitvector/sum02_false-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     780 11000    error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .021 5.0 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect - wit inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .18  27 1.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.0  340 timeout 0 wit inspect 960     1100  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .17  27 2.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.8  330 timeout 0 wit inspect 960     1100  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .97  29 12    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    300 timeout 0 wit inspect 960     1700  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 27     45 330    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 120    460 timeout 0 wit inspect 960     610  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 30     43 370    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 160    460 error (7) 0 wit inspect 310     950  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .082 27 .78 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7  310 true 2 wit inspect 52     560  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect .099 26 1.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7  300 true 2 wit inspect 190     630  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900     1200 9800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .018 4.8
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900     830 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .018 4.9
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900     750 9700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .022 4.9
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     11000 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .018 4.8
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900     750 9100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 45 error (2) 0 wit inspect .022 4.9
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i timeout 0 wit inspect 900     1000 9700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.9
bitvector/modulus_true-unreach-call_true-no-overflow.i true 2 wit inspect 180     280 2100    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 15    310 true 2 wit inspect 12     330  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .090 26 .92 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 73     650  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .12  26 .88 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2  270 timeout 0 wit inspect 960     1100  
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect 7.0   28 93    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 25    320 timeout 0 wit inspect 960     1000  
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     760 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .023 4.9
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 5.9   87 60    false(unreach-call) 1 wit inspect 4.9  280 true -32 wit inspect 4.4   260   unknown 0 wit inspect 3.1  220 true -32 wit inspect .64   19    - wit inspect - wit inspect
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 6.1   96 63    false(unreach-call) 1 wit inspect 6.5  280 true -32 wit inspect 4.2   260   unknown 0 wit inspect 3.0  220 true -32 wit inspect .63   19    - wit inspect - wit inspect
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 2.6   58 26    false(unreach-call) 1 wit inspect 4.6  270 true -32 wit inspect 4.2   260   unknown 0 wit inspect 4.2  220 true -32 wit inspect .63   19    - wit inspect - wit inspect
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 22     190 260    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 73    760 true 2 wit inspect 41     770  
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 11     160 130    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 19    450 true 2 wit inspect 44     1100  
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 10     150 110    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 13    510 true 2 wit inspect 34     790  
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900     360 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .019 4.8
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900     2300 8400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .018 4.9
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c timeout 0 wit inspect 900     2100 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .018 4.8
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c timeout 0 wit inspect 900     2100 8300    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .018 5.0
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900     1800 9500    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .018 4.8
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c timeout 0 wit inspect 900     1800 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .020 5.0
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 4.3   34 52    - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6400 true 2 wit inspect 120     770  
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect .65  32 7.4  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6300 true 2 wit inspect 62     700  
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 1 wit inspect .47  30 5.5  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 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 23     35 310    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 250    580 true 2 wit inspect 320     850  
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect .67  32 8.5  - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6300 true 2 wit inspect 22     610  
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .11  28 .83 false(unreach-call) 1 wit inspect 3.3  270 false(unreach-call) 1 wit inspect 8.9   240   unknown 0 wit inspect 1.9  180 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 .11  28 .85 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 4.4   220   unknown 0 wit inspect 2.0  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .13  28 1.1  false(unreach-call) 1 wit inspect 3.1  250 false(unreach-call) 1 wit inspect 8.9   220   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .75  28 8.6  timeout 0 wit inspect 91    1600 true -32 wit inspect 11     260   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
bitvector-regression/signextension2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .091 28 .91 false(unreach-call) 1 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 4.6   220   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
bitvector-regression/signextension_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .080 28 .96 false(unreach-call) 1 wit inspect 4.3  260 false(unreach-call) 1 wit inspect 4.5   220   unknown 0 wit inspect 2.7  180 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 .070 26 .89 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 4.9   250  
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c true 2 wit inspect .089 26 .69 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  240 true 2 wit inspect 9.2   220  
bitvector-regression/signextension2_true-unreach-call_true-termination.c true 2 wit inspect .072 26 .81 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  240 true 2 wit inspect 4.9   260  
bitvector-regression/signextension_true-unreach-call_true-termination.c true 2 wit inspect .097 26 .74 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 6.0   260  
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) 1 wit inspect .55  28 4.8  false(unreach-call) 1 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 6.1   260   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
bitvector-loops/overflow_false-unreach-call1.i timeout 0 wit inspect 900     11000 11000    error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0012 .27 - wit inspect - wit inspect
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 2.1   30 18    true -32 wit inspect 3.7  260 timeout 0 wit inspect 98     5900   unknown 0 wit inspect 2.3  210 true -32 wit inspect .58   18    - 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    40000 160000   14 -22 140   4600 14 -154 160 8600 14 0 36 2600 14 -120 7.1 220 36 38 4400 33000 36 30 8000 17000
    correct results 33 55 330    1800 4000   10 10 42   2700 6 6 37 1400 0 8 8 4.6 150 19 38 740 7000 15 30 1000 8800
        correct true 22 44 320    1300 3800   0 0 0 0 19 38 740 7000 15 30 1000 8800
        correct false 11 11 18    460 180   10 10 42   2700 6 6 37 1400 0 8 8 4.6 150 0 0
    correct-unconfimed results 2 1 2.6  60 24   0 0 0 0 0 0
        correct-unconfirmed true 1 1 .47 30 5.5 0 0 0 0 0 0
        correct-unconfirmed false 1 0 2.1  30 18   0 0 0 0 0 0
    incorrect results 0 1 -32 3.7 260 5 -160 28 1300 0 4 -128 2.5 75 0 0
        incorrect true 0 1 -32 3.7 260 5 -160 28 1300 0 4 -128 2.5 75 0 0
        incorrect false 0 0 0 0 0 0 0
score (50 tasks, max score: 86) 56 -22 -154 0 -120 38 30
Run set esbmc-incr.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-BitVectors