Tool ULTIMATE Automizer cfb9fd9e
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-23-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-14 23:51:13 CET [[ 2016-01-15 09:43:48 CET ]] [[ 2016-01-15 22:41:15 CET ]]
Run set sv-comp16.BitVectorsReach
Options [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/uautomizer.2016-01-14_2351.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/uautomizer.2016-01-14_2351.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 false(reach) 51   20   530 wit true 27   15   940 false(reach) 52 29   550
bitvector/byte_add_1_true-unreach-call.i timeout 900   760   2300 wit - -
bitvector/byte_add_2_true-unreach-call.i timeout 900   760   5100 wit - -
bitvector/gcd_1_true-unreach-call.i error 28   17   400 wit - -
bitvector/gcd_2_true-unreach-call.i error 170   160   570 wit - -
bitvector/gcd_3_true-unreach-call.i timeout 900   880   1000 wit - -
bitvector/gcd_4_true-unreach-call.i error 52   40   430 wit - -
bitvector/interleave_bits_true-unreach-call.i error 100   81   430 wit - -
bitvector/jain_1_true-unreach-call.i true 9.0 2.7 320 wit - -
bitvector/jain_2_true-unreach-call.i true 12   4.5 350 wit - -
bitvector/jain_4_true-unreach-call.i true 23   14   370 wit - -
bitvector/jain_5_true-unreach-call.i true 9.7 3.1 330 wit - -
bitvector/jain_6_true-unreach-call.i error 36   29   390 wit - -
bitvector/jain_7_true-unreach-call.i error 29   22   360 wit - -
bitvector/modulus_true-unreach-call.i error 95   81   400 wit - -
bitvector/num_conversion_1_true-unreach-call.i timeout 900   890   530 wit - -
bitvector/num_conversion_2_true-unreach-call.i timeout 900   890   540 wit - -
bitvector/parity_true-unreach-call.i timeout 900   860   1300 wit - -
bitvector/sum02_true-unreach-call.i unknown 9.2 3.5 320 wit - -
bitvector/s3_clnt_1_false-unreach-call.BV.c.cil.c false(reach) 40   9.8 530 wit false(reach) 21   11   680 false(reach) 36 20   560
bitvector/s3_clnt_2_false-unreach-call.BV.c.cil.c false(reach) 150   32   560 wit false(reach) 28   15   810 false(reach) 44 24   570
bitvector/s3_clnt_3_false-unreach-call.BV.c.cil.c unknown 30   10   390 wit - -
bitvector/s3_clnt_1_true-unreach-call.BV.c.cil.c true 43   12   550 wit - -
bitvector/s3_clnt_2_true-unreach-call.BV.c.cil.c true 55   14   610 wit - -
bitvector/s3_clnt_3_true-unreach-call.BV.c.cil.c true 29   8.6 780 wit - -
bitvector/s3_srvr_1_alt_true-unreach-call.BV.c.cil.c timeout 900   870   1200 wit - -
bitvector/s3_srvr_1_true-unreach-call.BV.c.cil.c true 31   8.3 690 wit - -
bitvector/s3_srvr_2_alt_true-unreach-call.BV.c.cil.c true 72   34   3900 wit - -
bitvector/s3_srvr_2_true-unreach-call.BV.c.cil.c true 68   33   2900 wit - -
bitvector/s3_srvr_3_alt_true-unreach-call.BV.c.cil.c true 28   8.0 640 wit - -
bitvector/s3_srvr_3_true-unreach-call.BV.c.cil.c true 28   8.0 550 wit - -
bitvector/soft_float_1_true-unreach-call.c.cil.c error 140   110   630 wit - -
bitvector/soft_float_2_true-unreach-call.c.cil.c true 17   6.2 470 wit - -
bitvector/soft_float_3_true-unreach-call.c.cil.c timeout 900   860   1500 wit - -
bitvector/soft_float_4_true-unreach-call.c.cil.c true 700   660   850 wit - -
bitvector/soft_float_5_true-unreach-call.c.cil.c true 16   5.2 340 wit - -
bitvector-regression/implicitfloatconversion_false-unreach-call.i error 7.0 2.2 300 wit - -
bitvector-regression/implicitunsignedconversion_false-unreach-call.i false(reach) 8.4 3.0 330 wit false(reach) 4.2 2.5 230 false(reach) 11 6.3 320
bitvector-regression/integerpromotion_false-unreach-call.i false(reach) 14   4.9 350 wit false(reach) 7.3 4.1 340 false(reach) 18 10   360
bitvector-regression/signextension2_false-unreach-call.i false(reach) 9.3 3.2 330 wit false(reach) 6.6 3.7 330 false(reach) 11 6.4 340
bitvector-regression/signextension_false-unreach-call.i false(reach) 8.5 2.8 320 wit false(reach) 7.2 4.0 330 false(reach) 13 7.3 350
bitvector-regression/implicitunsignedconversion_true-unreach-call.i true 9.3 3.9 340 wit - -
bitvector-regression/integerpromotion_true-unreach-call.i true 15   6.2 350 wit - -
bitvector-regression/signextension2_true-unreach-call.i true 8.8 2.8 320 wit - -
bitvector-regression/signextension_true-unreach-call.i true 8.3 2.6 330 wit - -
bitvector-loops/diamond_false-unreach-call2.i false(reach) 12   3.5 360 wit false(reach) 6.1 3.7 250 false(reach) 13 7.7 330
bitvector-loops/overflow_false-unreach-call1.i timeout 900   760   1100 wit - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i timeout 900   890   570 wit - -
../../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 11000 9900 38000 48 110   59   3900   48 200   110   3400  
    correct results 27 1500 910 18000 8 110   59   3900   8 200   110   3400  
        correct true 19 1200 830 15000 1 0   0   0   0 0   0   0  
        correct false 8 290 79 3300 7 110   59   3900   8 200   110   3400  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 84) 46
Run set sv-comp16.BitVectorsReach