Tool PAC-MAN
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-13 07:33:23 CET [[ 2016-01-15 09:22:08 CET ]] [[ 2016-01-15 22:28:32 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/pacman.2016-01-13_0733.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/pacman.2016-01-13_0733.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 witness unconfirmed 1.6 1.7 110 wit true 23   12   800 unknown 11   6.2 320
bitvector/byte_add_1_true-unreach-call.i true 640   900   160 wit - -
bitvector/byte_add_2_true-unreach-call.i true 660   900   160 wit - -
bitvector/gcd_1_true-unreach-call.i true 680   900   200 wit - -
bitvector/gcd_2_true-unreach-call.i true 710   900   210 wit - -
bitvector/gcd_3_true-unreach-call.i true 680   900   210 wit - -
bitvector/gcd_4_true-unreach-call.i true 670   900   200 wit - -
bitvector/interleave_bits_true-unreach-call.i true 690   900   210 wit - -
bitvector/jain_1_true-unreach-call.i out of memory 14   14   15000 wit - -
bitvector/jain_2_true-unreach-call.i out of memory 19   19   15000 wit - -
bitvector/jain_4_true-unreach-call.i out of memory 20   20   15000 wit - -
bitvector/jain_5_true-unreach-call.i out of memory 42   42   15000 wit - -
bitvector/jain_6_true-unreach-call.i out of memory 21   21   15000 wit - -
bitvector/jain_7_true-unreach-call.i out of memory 21   21   15000 wit - -
bitvector/modulus_true-unreach-call.i true 670   900   180 wit - -
bitvector/num_conversion_1_true-unreach-call.i true 680   900   210 wit - -
bitvector/num_conversion_2_true-unreach-call.i true 660   900   170 wit - -
bitvector/parity_true-unreach-call.i true 660   900   170 wit - -
bitvector/sum02_true-unreach-call.i out of memory 17   17   15000 wit - -
bitvector/s3_clnt_1_false-unreach-call.BV.c.cil.c out of memory 29   34   15000 wit - -
bitvector/s3_clnt_2_false-unreach-call.BV.c.cil.c true 670   900   170 wit - -
bitvector/s3_clnt_3_false-unreach-call.BV.c.cil.c witness unconfirmed 1.9 2.0 110 wit true 9.1 5.0 320 unknown 9.4 6.7 300
bitvector/s3_clnt_1_true-unreach-call.BV.c.cil.c true 670   900   170 wit - -
bitvector/s3_clnt_2_true-unreach-call.BV.c.cil.c true 660   900   160 wit - -
bitvector/s3_clnt_3_true-unreach-call.BV.c.cil.c true 680   900   170 wit - -
bitvector/s3_srvr_1_alt_true-unreach-call.BV.c.cil.c out of memory 69   93   15000 wit - -
bitvector/s3_srvr_1_true-unreach-call.BV.c.cil.c true 670   900   170 wit - -
bitvector/s3_srvr_2_alt_true-unreach-call.BV.c.cil.c out of memory 19   23   15000 wit - -
bitvector/s3_srvr_2_true-unreach-call.BV.c.cil.c true 660   900   160 wit - -
bitvector/s3_srvr_3_alt_true-unreach-call.BV.c.cil.c true 670   900   170 wit - -
bitvector/s3_srvr_3_true-unreach-call.BV.c.cil.c true 670   900   160 wit - -
bitvector/soft_float_1_true-unreach-call.c.cil.c true 660   900   150 wit - -
bitvector/soft_float_2_true-unreach-call.c.cil.c true 660   900   150 wit - -
bitvector/soft_float_3_true-unreach-call.c.cil.c true 650   900   150 wit - -
bitvector/soft_float_4_true-unreach-call.c.cil.c true 650   900   150 wit - -
bitvector/soft_float_5_true-unreach-call.c.cil.c true 660   900   160 wit - -
bitvector-regression/implicitfloatconversion_false-unreach-call.i witness unconfirmed 1.5 1.6 110 wit true 4.0 2.4 210 unknown 10   5.8 320
bitvector-regression/implicitunsignedconversion_false-unreach-call.i witness unconfirmed 1.5 1.6 110 wit true 4.0 2.6 210 unknown 9.1 6.1 310
bitvector-regression/integerpromotion_false-unreach-call.i witness unconfirmed 1.5 1.6 110 wit true 5.3 3.1 230 unknown 10   5.7 330
bitvector-regression/signextension2_false-unreach-call.i witness unconfirmed 1.6 1.6 110 wit true 5.5 3.2 240 unknown 10   6.2 320
bitvector-regression/signextension_false-unreach-call.i witness unconfirmed 1.5 1.5 110 wit true 5.4 3.1 240 unknown 9.7 7.0 310
bitvector-regression/implicitunsignedconversion_true-unreach-call.i true 690   900   210 wit - -
bitvector-regression/integerpromotion_true-unreach-call.i true 710   900   210 wit - -
bitvector-regression/signextension2_true-unreach-call.i true 690   900   200 wit - -
bitvector-regression/signextension_true-unreach-call.i true 680   900   200 wit - -
bitvector-loops/diamond_false-unreach-call2.i witness unconfirmed 1.6 1.7 110 wit true 4.7 2.8 230 unknown 9.3 6.0 300
bitvector-loops/overflow_false-unreach-call1.i out of memory 65   65   15000 wit - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i true 670   900   160 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 20000 27000 170000 48 62   35   2500   48 79   50   2500  
    correct results 27 18000 24000 4800 0 0   0   0   0 0   0   0  
        correct true 27 18000 24000 4800 0 0   0   0   0 0   0   0  
        correct false 0
    incorrect results 2 1300 1800 330 0 0   0   0   0 0   0   0  
        incorrect true 2 1300 1800 330 0 0   0   0   0 0   0   0  
        incorrect false 0
score (48 tasks, max score: 84) -10
Run set sv-comp16.BitVectorsReach