Tool ESBMC ESBMC version 2.0.0 64-bit x86_64 linux
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-16 17:45:19 CET [[ 2016-01-17 00:36:28 CET ]] [[ 2016-01-17 00:39:38 CET ]]
Run set sv-comp16.BitVectorsOverflows
Options [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/esbmc.2016-01-16_1745.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/esbmc.2016-01-16_1745.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/signedintegeroverflow-regression/ 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)
AdditionIntMax_false-no-overflow.c.i false(no-overflow) .10  .12  17 wit false(no-overflow) 6.1 3.6 220 true 10   5.9 320
Multiplication_false-no-overflow.c.i false(no-overflow) .095 .11  17 wit false(no-overflow) 6.3 3.7 220 true 9.4 5.3 330
NoConversion_false-no-overflow.c.i false(no-overflow) .10  .12  17 wit false(no-overflow) 6.4 3.6 220 true 11   7.9 310
PostfixDecrement_false-no-overflow.c.i false(no-overflow) .15  .16  17 wit false(no-overflow) 6.2 3.6 230 true 10   7.1 320
PostfixIncrement_false-no-overflow.c.i false(no-overflow) .46  .60  17 wit false(no-overflow) 6.3 3.5 220 true 11   7.9 350
PrefixDecrement_false-no-overflow.c.i false(no-overflow) .093 .10  17 wit false(no-overflow) 6.0 3.4 230 true 11   6.4 320
PrefixIncrement_false-no-overflow.c.i false(no-overflow) .66  .88  17 wit false(no-overflow) 6.1 3.7 220 true 10   6.2 320
UnaryMinus_false-no-overflow.c.i false(no-overflow) .44  .59  17 wit false(no-overflow) 6.3 3.6 230 true 10   5.5 330
ConversionToSignedInt_true-no-overflow.c.i true .12  .13  17 wit - -
IntegerPromotion_true-no-overflow.c.i true .080 .090 17 wit - -
Multiplication_true-no-overflow.c.i true .088 .098 17 wit - -
UsualArithmeticConversions_true-no-overflow.c.i true .13  .14  17 wit - -
../../sv-benchmarks/c/signedintegeroverflow-regression/ 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 12 2.5  3.1  210 12 50   29   1800   12 83   52   2600  
    correct results 12 2.5  3.1  210 8 50   29   1800   8 83   52   2600  
        correct true 4 .41 .46 68 0 0   0   0   8 0   0   0  
        correct false 8 2.1  2.7  140 8 50   29   1800   0 83   52   2600  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (12 tasks, max score: 16) 16
Run set sv-comp16.BitVectorsOverflows