Tool CPAchecker 1.4-svcomp16c
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-04 13:17:38 CET [[ 2016-01-15 08:48:20 CET ]] [[ 2016-01-15 22:10:37 CET ]]
Run set sv-comp16.BitVectorsOverflows
Options -sv-comp16 -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-seq.2016-01-04_1317.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-seq.2016-01-04_1317.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 4.5 1.8 200 5.6 3.2 220 11 6.7 330
Multiplication_false-no-overflow.c.i 4.4 1.8 200 6.2 3.6 220 12 10   350
NoConversion_false-no-overflow.c.i 4.6 1.9 200 6.2 3.5 220 11 6.0 320
PostfixDecrement_false-no-overflow.c.i 3.7 1.5 200 6.1 3.4 220 11 6.1 340
PostfixIncrement_false-no-overflow.c.i 3.7 1.5 200 6.1 3.4 220 11 7.9 320
PrefixDecrement_false-no-overflow.c.i 4.5 1.8 210 6.3 3.6 230 12 6.5 340
PrefixIncrement_false-no-overflow.c.i 3.6 1.5 200 6.2 3.4 220 14 7.8 350
UnaryMinus_false-no-overflow.c.i 4.4 1.9 210 5.9 3.3 220 12 6.7 340
ConversionToSignedInt_true-no-overflow.c.i 3.3 1.4 190
IntegerPromotion_true-no-overflow.c.i 3.2 1.4 190
Multiplication_true-no-overflow.c.i 3.8 1.6 190
UsualArithmeticConversions_true-no-overflow.c.i 3.6 1.6 190
../../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 47 20   2400 12 49   27   1800   12 93   58   2700  
    correct results 12 47 20   2400 8 49   27   1800   8 93   58   2700  
        correct true 4 14 6.1 760 0 0   0   0   0 0   0   0  
        correct false 8 33 14   1600 8 49   27   1800   8 93   58   2700  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (12 tasks, max score: 16) 16
Run set sv-comp16.BitVectorsOverflows