Tool 2LS 0.3.4 CBMC CPAchecker 1.4-svcomp16c CPAchecker 1.4-svn 18373 CPAchecker 1.4-svcomp16c ESBMC ESBMC version 2.0.0 64-bit x86_64 linux DepthK ESBMC+DepthK version 2.1 impara 0.45 SeaHorn-F16 0.1.0 SMACK+Corral 1.5.2 symbiotic 3.0.1 ULTIMATE Automizer cfb9fd9e ULTIMATE Kojak fd30d3d8
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 Linux 4.2.0-23-generic Linux 4.2.0-22-generic 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-02 22:42:27 CET [[ 2016-01-15 08:01:51 CET ]] [[ 2016-01-15 21:37:22 CET ]] 2016-01-03 00:42:25 CET [[ 2016-01-15 08:22:02 CET ]] [[ 2016-01-15 21:54:19 CET ]] 2016-01-04 06:25:51 CET [[ 2016-01-15 08:31:02 CET ]] [[ 2016-01-15 21:59:57 CET ]] 2016-01-04 01:42:53 CET [[ 2016-01-15 08:36:34 CET ]] [[ 2016-01-15 22:02:40 CET ]] 2016-01-04 20:04:07 CET [[ 2016-01-15 08:41:31 CET ]] [[ 2016-01-15 22:05:37 CET ]] 2016-01-04 13:17:38 CET [[ 2016-01-15 08:48:20 CET ]] [[ 2016-01-15 22:10:37 CET ]] 2016-01-16 17:45:19 CET [[ 2016-01-17 00:36:28 CET ]] [[ 2016-01-17 00:39:38 CET ]] 2016-01-05 14:06:34 CET [[ 2016-01-15 09:00:06 CET ]] [[ 2016-01-15 22:17:52 CET ]] 2016-01-13 07:41:14 CET [[ 2016-01-15 09:11:00 CET ]] [[ 2016-01-15 22:23:23 CET ]] 2016-01-13 15:22:34 CET [[ 2016-01-15 18:20:27 CET ]] [[ 2016-01-15 22:30:28 CET ]] 2016-01-07 09:05:16 CET [[ 2016-01-15 09:34:34 CET ]] [[ 2016-01-15 22:36:10 CET ]] 2016-01-07 09:04:54 CET [[ 2016-01-15 09:39:10 CET ]] [[ 2016-01-15 22:39:28 CET ]] 2016-01-14 23:51:13 CET [[ 2016-01-15 09:43:48 CET ]] [[ 2016-01-15 22:41:15 CET ]] 2016-01-08 15:10:30 CET [[ 2016-01-15 09:49:48 CET ]] [[ 2016-01-15 22:43:29 CET ]]
Run set 2ls.sv-comp16.BitVectorsOverflows cbmc.sv-comp16.BitVectorsOverflows cpa-bam.sv-comp16.BitVectorsOverflows cpa-kind.sv-comp16.BitVectorsOverflows cpa-refsel.sv-comp16.BitVectorsOverflows cpa-seq.sv-comp16.BitVectorsOverflows esbmc.sv-comp16.BitVectorsOverflows esbmcdepthk.sv-comp16.BitVectorsOverflows impara.sv-comp16.BitVectorsOverflows seahorn.sv-comp16.BitVectorsOverflows smack.sv-comp16.BitVectorsOverflows symbiotic3.sv-comp16.BitVectorsOverflows uautomizer.sv-comp16.BitVectorsOverflows ukojak.sv-comp16.BitVectorsOverflows
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 ]] --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16-bam -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-bam.2016-01-04_0625.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-bam.2016-01-04_0625.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16--k-induction -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-kind.2016-01-04_0142.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-kind.2016-01-04_0142.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -sv-comp16--refsel -disable-java-assertions -heap 12500m -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-refsel.2016-01-04_2004.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-refsel.2016-01-04_2004.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -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 ]] [[ -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 ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/esbmcdepthk.2016-01-05_1406.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/esbmcdepthk.2016-01-05_1406.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] --eager --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/impara.2016-01-13_0741.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/impara.2016-01-13_0741.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] --cex=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/seahorn.2016-01-11_2135.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/seahorn.2016-01-11_2135.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] -w error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/smack.2016-01-07_0905.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/smack.2016-01-07_0905.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/symbiotic3.2016-01-07_0904.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/symbiotic3.2016-01-07_0904.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]] [[ -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 ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/ukojak.2016-01-08_1510.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/ukojak.2016-01-08_1510.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/signedintegeroverflow-regression/ status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB)
AdditionIntMax_false-no-overflow.c.i true .089 25 false(reach) .16 26 error .53 49 false(no-overflow) 4.6 220 error .66 49 false(no-overflow) 4.5 200 false(no-overflow) .10  17 unknown .26 13 true .084 24 error (3) .033 5.6 error (1) 1.1 18 error (1) .022 4.0 false(no-overflow) 9.0 320 timeout 130   1200
Multiplication_false-no-overflow.c.i true .086 24 false(reach) .12 26 error .60 52 false(no-overflow) 4.6 210 error .61 48 false(no-overflow) 4.4 200 false(no-overflow) .095 17 unknown .18 13 true .13  25 error (3) .030 5.6 error (1) 1.4 18 error (1) .021 4.0 false(no-overflow) 8.7 330 false(no-overflow) 8.4 320
NoConversion_false-no-overflow.c.i true .11  24 false(reach) .10 26 error .57 48 false(no-overflow) 4.7 220 error .64 49 false(no-overflow) 4.6 200 false(no-overflow) .10  17 unknown .16 12 true .13  24 error (3) .043 5.6 error (1) 1.4 18 error (1) .035 3.8 false(no-overflow) 8.5 330 timeout 130   1100
PostfixDecrement_false-no-overflow.c.i true .14  24 false(reach) .12 25 error .56 46 false(no-overflow) 4.6 210 error .63 49 false(no-overflow) 3.7 200 false(no-overflow) .15  17 unknown .16 13 true .12  25 error (3) .034 5.6 error (1) 1.4 18 error (1) .019 3.9 false(no-overflow) 11   340 timeout 130   1100
PostfixIncrement_false-no-overflow.c.i true .085 25 false(reach) .16 26 error .50 48 false(no-overflow) 4.6 210 error .54 49 false(no-overflow) 3.7 200 false(no-overflow) .46  17 unknown .16 13 true .11  24 error (3) .023 5.4 error (1) 1.5 18 error (1) .020 3.9 false(no-overflow) 8.9 330 timeout 130   1300
PrefixDecrement_false-no-overflow.c.i true .15  25 false(reach) .13 26 error .58 49 false(no-overflow) 3.9 210 error .68 49 false(no-overflow) 4.5 210 false(no-overflow) .093 17 unknown .22 12 true .15  24 error (3) .020 5.6 error (1) 1.4 18 error (1) .027 4.0 false(no-overflow) 9.2 330 timeout 130   960
PrefixIncrement_false-no-overflow.c.i true .11  24 false(reach) .12 26 error .59 47 false(no-overflow) 4.5 210 error .53 49 false(no-overflow) 3.6 200 false(no-overflow) .66  17 unknown .16 12 true .10  25 error (3) .029 5.5 error (1) 1.4 18 error (1) .014 3.9 false(no-overflow) 8.6 320 timeout 130   1300
UnaryMinus_false-no-overflow.c.i true .11  24 false(reach) .10 26 error .55 50 false(no-overflow) 3.8 210 error .61 49 false(no-overflow) 4.4 210 false(no-overflow) .44  17 unknown .15 13 true .089 25 error (3) .042 5.6 error (1) 1.4 18 error (1) .033 3.9 false(no-overflow) 10   340 timeout 140   1200
ConversionToSignedInt_true-no-overflow.c.i true .11  24 false(reach) .13 26 error .57 49 true 4.0 200 error .62 48 true 3.3 190 true .12  17 unknown .15 12 true .13  24 error (3) .045 5.5 error (1) 1.5 18 error (1) .035 3.9 true 8.7 320 true 8.2 310
IntegerPromotion_true-no-overflow.c.i true .090 24 true 1.2  26 error .54 49 true 4.2 200 error .52 49 true 3.2 190 true .080 17 unknown .25 13 true .10  24 error (3) .026 5.5 error (1) 1.4 18 error (1) .011 3.9 true 9.0 330 timeout 140   1500
Multiplication_true-no-overflow.c.i true .11  25 true 1.2  26 error .59 48 true 4.1 190 error .61 48 true 3.8 190 true .088 17 unknown .20 12 true .12  25 error (3) .025 5.5 error (1) 1.4 18 error (1) .013 3.8 true 8.9 320 timeout 130   1200
UsualArithmeticConversions_true-no-overflow.c.i true .11  24 true 1.1  26 error .57 48 true 3.5 190 error .66 49 true 3.6 190 true .13  17 unknown .22 13 true .12  24 error (3) .037 5.6 error (1) 1.3 18 error (1) .035 3.9 true 8.4 320 timeout 130   1300
../../sv-benchmarks/c/signedintegeroverflow-regression/ status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB) status cputime (s) memUsage (MB)
total tasks 12 1.3  290 12 4.6 310 12 6.7 580 12 51 2500 12 7.3 580 12 47 2400 12 2.5  210 12 2.3 150 12 1.4  290 12 .39 66 12 17 220 12 .29 47 12 110 3900 12 1300   13000
    correct results 4 .42 98 3 3.4 77 0 12 51 2500 0 12 47 2400 12 2.5  210 0 4 .48 98 0 0 0 12 110 3900 2 17   640
        correct true 4 .42 98 3 3.4 77 0 4 16 780 0 4 14 760 4 .41 68 0 4 .48 98 0 0 0 4 35 1300 1 8.2 310
        correct false 0 0 0 8 35 1700 0 8 33 1600 8 2.1  140 0 0 0 0 0 8 74 2600 1 8.4 320
    incorrect results 8 .89 200 0 0 0 0 0 0 0 8 .91 200 0 0 0 0 0
        incorrect true 8 .89 200 0 0 0 0 0 0 0 8 .91 200 0 0 0 0 0
        incorrect false 0 0 0 0 0 0 0 0 0 0 0 0 0 0
score (12 tasks, max score: 16) -248 6 0 16 0 16 16 0 -248 0 0 0 16 3
Run set 2ls.sv-comp16.BitVectorsOverflows cbmc.sv-comp16.BitVectorsOverflows cpa-bam.sv-comp16.BitVectorsOverflows cpa-kind.sv-comp16.BitVectorsOverflows cpa-refsel.sv-comp16.BitVectorsOverflows cpa-seq.sv-comp16.BitVectorsOverflows esbmc.sv-comp16.BitVectorsOverflows esbmcdepthk.sv-comp16.BitVectorsOverflows impara.sv-comp16.BitVectorsOverflows seahorn.sv-comp16.BitVectorsOverflows smack.sv-comp16.BitVectorsOverflows symbiotic3.sv-comp16.BitVectorsOverflows uautomizer.sv-comp16.BitVectorsOverflows ukojak.sv-comp16.BitVectorsOverflows