Tool 2LS 0.3.4
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24]
OS Linux 4.2.0-22-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135149 MB
Date of execution 2016-01-02 22:42:27 CET [[ 2016-01-15 08:01:51 CET ]] [[ 2016-01-15 21:37:22 CET ]]
Run set sv-comp16.BitVectorsReach
Options --k-induction --competition-mode --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/2ls.2016-01-02_2242.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/2ls.2016-01-02_2242.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
bitvector/byte_add_false-unreach-call.i .44  .44 28 38   20   1000 36   25   510
bitvector/byte_add_1_true-unreach-call.i .60  .60 31
bitvector/byte_add_2_true-unreach-call.i .61  .61 30
bitvector/gcd_1_true-unreach-call.i .35  .35 27
bitvector/gcd_2_true-unreach-call.i 1.1   1.1  39
bitvector/gcd_3_true-unreach-call.i 1.2   1.3  40
bitvector/gcd_4_true-unreach-call.i 1.5   1.5  41
bitvector/interleave_bits_true-unreach-call.i 1.1   1.1  57
bitvector/jain_1_true-unreach-call.i 900     900    1300
bitvector/jain_2_true-unreach-call.i 900     900    1600
bitvector/jain_4_true-unreach-call.i 900     900    1800
bitvector/jain_5_true-unreach-call.i 900     900    1500
bitvector/jain_6_true-unreach-call.i 900     900    1900
bitvector/jain_7_true-unreach-call.i 900     900    1800
bitvector/modulus_true-unreach-call.i 1.2   1.2  41
bitvector/num_conversion_1_true-unreach-call.i .24  .24 25
bitvector/num_conversion_2_true-unreach-call.i .26  .27 25
bitvector/parity_true-unreach-call.i 3.7   3.7  40
bitvector/sum02_true-unreach-call.i 900     900    1300
bitvector/s3_clnt_1_false-unreach-call.BV.c.cil.c 86     86    340 90   75   3600 37   23   520
bitvector/s3_clnt_2_false-unreach-call.BV.c.cil.c 54     54    330 90   76   3600 39   22   510
bitvector/s3_clnt_3_false-unreach-call.BV.c.cil.c 32     32    220 90   76   3600 35   19   480
bitvector/s3_clnt_1_true-unreach-call.BV.c.cil.c 900     900    310
bitvector/s3_clnt_2_true-unreach-call.BV.c.cil.c 59     59    360
bitvector/s3_clnt_3_true-unreach-call.BV.c.cil.c 61     61    340
bitvector/s3_srvr_1_alt_true-unreach-call.BV.c.cil.c 900     900    880
bitvector/s3_srvr_1_true-unreach-call.BV.c.cil.c 900     900    7400
bitvector/s3_srvr_2_alt_true-unreach-call.BV.c.cil.c 900     900    6700
bitvector/s3_srvr_2_true-unreach-call.BV.c.cil.c 900     900    6700
bitvector/s3_srvr_3_alt_true-unreach-call.BV.c.cil.c 900     900    7200
bitvector/s3_srvr_3_true-unreach-call.BV.c.cil.c 900     900    7200
bitvector/soft_float_1_true-unreach-call.c.cil.c .25  .25 30
bitvector/soft_float_2_true-unreach-call.c.cil.c .21  .21 29
bitvector/soft_float_3_true-unreach-call.c.cil.c 18     18    210
bitvector/soft_float_4_true-unreach-call.c.cil.c 1.3   1.3  32
bitvector/soft_float_5_true-unreach-call.c.cil.c .17  .17 28
bitvector-regression/implicitfloatconversion_false-unreach-call.i .10  .10 22 4.5 2.7 220 10   5.6 320
bitvector-regression/implicitunsignedconversion_false-unreach-call.i .12  .12 22 3.9 2.4 220 9.8 5.6 320
bitvector-regression/integerpromotion_false-unreach-call.i .15  .15 27 7.3 4.2 340 19   12   360
bitvector-regression/signextension2_false-unreach-call.i .11  .12 25 7.0 3.9 340 12   6.6 340
bitvector-regression/signextension_false-unreach-call.i .11  .11 25 7.1 4.0 330 12   6.8 330
bitvector-regression/implicitunsignedconversion_true-unreach-call.i .099 .10 23
bitvector-regression/integerpromotion_true-unreach-call.i .11  .11 25
bitvector-regression/signextension2_true-unreach-call.i .12  .12 25
bitvector-regression/signextension_true-unreach-call.i .16  .16 25
bitvector-loops/diamond_false-unreach-call2.i .15  .15 25 5.7 3.2 250 12   8.6 330
bitvector-loops/overflow_false-unreach-call1.i 900     900    1200
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i 2.5   2.6  49 7.8 4.4 360 91   81   480
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
total tasks 48 14000 14000 51000 48 350   270   14000   48 310   210   4500  
    correct results 31 300 300 2400 7 220   170   9300   7 240   170   3500  
        correct true 22 150 150 1500 0 0   0   0   0 0   0   0  
        correct false 9 140 140 870 7 220   170   9300   7 240   170   3500  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 84) 53
Run set sv-comp16.BitVectorsReach