Tool 2LS 0.3.4 BLAST 2.7.3 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 Forest svc_16_20151108 impara 0.45 CPAchecker 1.4-svn 18356M SeaHorn-F16 0.1.0 skink SMACK+Corral 1.5.2 symbiotic 3.0.1 ULTIMATE Automizer cfb9fd9e ULTIMATE Kojak fd30d3d8 VVT prerelease
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] [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23] [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 17:36:26 CET [[ 2016-01-15 08:15:11 CET ]] [[ 2016-01-15 21:49:51 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-09 23:49:59 CET [[ 2016-01-15 09:05:13 CET ]] [[ 2016-01-15 22:20:31 CET ]] 2016-01-13 07:41:14 CET [[ 2016-01-15 09:11:00 CET ]] [[ 2016-01-15 22:23:23 CET ]] 2016-01-10 22:01:17 CET [[ 2016-01-15 09:16:15 CET ]] [[ 2016-01-15 22:26:01 CET ]] 2016-01-11 21:35:00 [[ 2016-01-15 18:20:27 CET ]] [[ 2016-01-15 22:30:28 CET ]] 2016-01-15 22:52:00 CET [[ 2016-01-16 00:34:30 CET ]] [[ 2016-01-16 00:56:26 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 ]] 2016-01-17 23:14:00 CET [[ 2016-01-18 06:54:01 CET ]] [[ 2016-01-18 07:05:55 CET ]]
Run set 2ls.sv-comp16.ControlFlow blast.sv-comp16.ControlFlow cbmc.sv-comp16.ControlFlow cpa-bam.sv-comp16.ControlFlow cpa-kind.sv-comp16.ControlFlow cpa-refsel.sv-comp16.ControlFlow cpa-seq.sv-comp16.ControlFlow esbmc.sv-comp16.ControlFlow esbmcdepthk.sv-comp16.ControlFlow forest.sv-comp16.ControlFlow impara.sv-comp16.ControlFlow lpi.sv-comp16.ControlFlow seahorn.sv-comp16.ControlFlow skink.sv-comp16.ControlFlow smack.sv-comp16.ControlFlow symbiotic3.sv-comp16.ControlFlow uautomizer.sv-comp16.ControlFlow ukojak.sv-comp16.ControlFlow vvt.sv-comp16.ControlFlow
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 ]] -alias empty -enable-recursion -noprofile -cref -sv-comp -lattice -include-lattice symb -nosserr -svcomp-witness error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/blast.2016-01-03_1736.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/blast.2016-01-03_1736.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 ]] -svcomp [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/forest.2016-01-09_2349.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/forest.2016-01-09_2349.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 ]] -lpi-svcomp16 -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/lpi.2016-01-10_2201.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/lpi.2016-01-10_2201.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 ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/skink.2016-01-15_2252.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/skink.2016-01-15_2252.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 ]] [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/vvt.2016-01-17_2314.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/vvt.2016-01-17_2314.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/ 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) 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)
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-termination.cil.c false(reach) 2.3  460 false(reach) 120     86 false(reach) 1.2  130 false(reach) 15   660 false(reach) 52   1100 false(reach) 79   900 false(reach) 11   450 false(reach) 800    5100 false(reach) 10    200 true .54  8.9 witness unconfirmed .74 33 false(reach) 38   720 false(reach) 1.2  88 unknown 15   840 witness timeout 13   140 witness unconfirmed 550    69   false(reach) 77 1300 timeout 140 1800 witness unconfirmed 2.7  69
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c false(reach) .69 110 false(reach) 20     50 false(reach) .33 36 exception 6.7 290 false(reach) 31   800 false(reach) 97   820 false(reach) 13   480 false(reach) 800    4900 false(reach) 5.8  180 unknown .96  36   witness unconfirmed .46 28 false(reach) 20   540 false(reach) .54 45 unknown 14   620 witness unconfirmed 4.5 100 false(reach) 420    20   false(reach) 54 970 timeout 120 1800 witness unconfirmed 1.4  39
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c false(reach) .86 190 false(reach) 19     55 false(reach) .52 49 exception 7.3 290 false(reach) 39   1000 false(reach) 120   830 false(reach) 14   540 false(reach) 810    7700 false(reach) 8.1  190 true .97  18   witness unconfirmed .52 32 false(reach) 32   680 false(reach) .73 53 unknown 17   790 witness unconfirmed 6.2 140 timeout 900    37   false(reach) 62 1100 timeout 120 1500 witness unconfirmed 2.0  39
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c false(reach) .46 63 false(reach) 5.8   54 false(reach) .24 32 false(reach) 18   750 false(reach) 7.8 390 false(reach) 10   440 false(reach) 9.2 320 witness timeout 860    7600 witness timeout 6.2  180 unknown .80  39   false(reach) .36 27 false(reach) 9.6 410 false(reach) .49 44 unknown 37   620 witness unconfirmed 4.1 88 false(reach) 350    15   false(reach) 29 610 false(reach) 39 780 witness unconfirmed .97 34
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c true 2.3  460 true 430     210 true 8.3  130 timeout 900   6600 true 41   960 true 370   820 true 10   430 true .58 62 true 2.1  75 true 3.1   43   true 2.9  40 true 19   520 true 1.3  91 unknown 16   840 true 11   150 timeout 900    69   true 83 1300 timeout 120 2300 unknown 3.0  64
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c true .75 150 true 120     100 true 3.6  51 true 41   1000 true 26   800 true 170   820 true 110   2300 true .28 30 true 1.6  39 true 3.8   41   true 3.3  32 true 46   1000 true .71 56 unknown 18   810 true 5.6 100 timeout 900    20   true 66 1200 timeout 150 1900 true 6.8  120
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c true .67 110 true 140     120 true 2.3  37 exception 5.7 280 true 19   600 true 90   800 true 10   440 true .21 24 true .92 34 true .71  13   true 1.5  30 true 13   460 true .51 41 unknown 12   600 true 5.1 95 timeout 900    20   true 64 1500 timeout 110 2200 unknown 1.3  44
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c true 1.1  190 true 240     210 true 4.0  50 exception 6.0 280 true 25   760 true 120   830 true 11   470 true .25 35 true 1.1  46 unknown 1.1   41   true 2.4  30 true 19   530 true .68 52 unknown 16   810 true 6.4 110 timeout 900    37   true 73 1800 timeout 99 1400 unknown 2.0  37
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c true .21 32 true 1.6   31 true 1.3  28 true 7.9 410 true 5.3 230 true 5.6 240 true 4.3 210 true .11 17 true .76 28 unknown .73  39   true .48 25 true 4.8 240 true .32 34 unknown 13   520 true 3.4 73 true 230    9.3 true 16 410 true 36 750 unknown .52 23
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c true .44 63 true 1.7   34 true 1.6  31 true 14   600 true 6.4 250 true 7.9 300 true 6.3 280 true .17 21 true 1.1  33 true .93  40   true .91 27 true 7.4 260 true .44 37 unknown 13   640 true 3.8 84 true 620    15   true 19 490 true 56 1000 unknown .78 28
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c false(reach) 35    240 false(reach) 12     45 false(reach) 1.9  67 timeout 900   1600 false(reach) 33   920 false(reach) 10   440 false(reach) 8.5 350 false(reach) 810    6200 false(reach) 62    290 unknown .22  7.6 witness timeout .67 26 false(reach) 24   520 false(reach) 2.3  77 unknown 7.4 340 witness timeout 6.6 130 witness unconfirmed 660    22   false(reach) 17 370 timeout 35 580 witness unconfirmed 4.2  69
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(reach) 41    260 false(reach) 15     43 false(reach) 2.0  67 timeout 900   1500 false(reach) 34   910 false(reach) 11   450 false(reach) 10   350 false(reach) 810    6400 false(reach) 62    300 true 1.0   39   witness timeout .82 26 false(reach) 26   570 false(reach) 2.6  76 unknown 7.4 330 witness timeout 6.5 140 witness unconfirmed 700    23   false(reach) 19 500 timeout 38 580 witness unconfirmed 4.6  78
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c witness timeout 78    340 witness unconfirmed 14     45 witness timeout 2.2  80 timeout 900   860 false(reach) 36   950 false(reach) 11   460 false(reach) 8.6 360 unknown 900    4300 false(reach) 77    330 true .87  39   witness timeout .81 26 false(reach) 25   560 false(reach) 2.4  76 unknown 7.3 320 witness timeout 7.2 130 witness unconfirmed 650    26   unknown 17 490 timeout 40 810 witness unconfirmed 5.1  68
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c false(reach) 45    260 false(reach) 14     45 false(reach) 2.0  70 timeout 900   2400 false(reach) 34   910 false(reach) 11   450 false(reach) 10   350 false(reach) 810    6000 false(reach) 62    290 true 3.3   40   witness timeout .63 26 false(reach) 28   530 false(reach) 2.4  75 unknown 8.4 330 witness timeout 5.5 130 witness unconfirmed 770    22   false(reach) 17 510 timeout 36 700 witness unconfirmed 3.7  67
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c false(reach) .40 43 false(reach) .19  26 false(reach) .16 27 timeout 900   3600 false(reach) 8.6 370 false(reach) 38   930 false(reach) 18   690 false(reach) 810    5000 false(reach) 4.1  180 true 1.4   40   false(reach) .28 26 false(reach) 8.6 360 false(reach) .69 78 unknown 7.7 350 witness timeout 4.7 110 witness unconfirmed 18    22   false(reach) 13 340 false(reach) 14 350 witness unconfirmed .39 20
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c false(reach) 86    340 exception (gremlins) 1.6   29 false(reach) 12    290 timeout 900   2300 false(reach) 51   1000 false(reach) 71   1500 false(reach) 160   2700 witness timeout 810    5400 witness timeout 85    340 true .92  39   witness timeout 2.9  27 false(reach) 43   990 witness timeout 5.0  79 unknown 8.1 370 witness timeout 14   160 timeout 900    23   false(reach) 27 610 timeout 65 1600 witness unconfirmed 5.6  72
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c witness timeout 71    320 exception (gremlins) 1.8   29 false(reach) 3.6  120 timeout 900   2900 false(reach) 53   1200 false(reach) 540   1200 false(reach) 160   3900 witness timeout 800    5600 witness timeout 120    360 unknown .90  40   witness timeout 4.6  27 false(reach) 40   940 witness timeout 7.5  140 unknown 8.5 370 witness timeout 13   190 timeout 900    26   false(reach) 25 630 timeout 38 740 witness unconfirmed 3.7  77
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c false(reach) 29    200 exception (gremlins) 1.7   28 false(reach) 3.2  120 timeout 900   3700 false(reach) 31   880 false(reach) 660   1500 false(reach) 130   3800 witness timeout 800    5400 witness timeout 97    340 error (139) 7.6   40   witness timeout .66 28 false(reach) 24   510 false(reach) 6.2  150 unknown 7.8 360 witness timeout 6.2 140 timeout 900    23   false(reach) 21 450 timeout 61 1300 witness unconfirmed 1.3  33
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c false(reach) 5.5  90 exception (gremlins) 2.8   29 false(reach) .17 27 timeout 900   1500 false(reach) 17   550 false(reach) 50   1500 false(reach) 76   3700 unknown 890    1900 false(reach) 5.8  180 true 1.6   40   witness timeout 1.1  26 exception 13   370 witness timeout .72 65 unknown 8.3 360 witness timeout 4.8 120 false(reach) 120    23   false(reach) 24 530 false(reach) 17 370 witness unconfirmed .64 25
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c false(reach) 30    200 false(reach) 2.9   40 false(reach) 2.9  120 witness unconfirmed 8.8 440 false(reach) 30   780 false(reach) 8.8 430 false(reach) 7.8 310 unknown 890    2000 false(reach) 84    350 true .87  39   false(reach) 1.2  26 false(reach) 21   450 false(reach) .90 63 unknown 7.8 360 witness timeout 5.0 130 false(reach) 670    22   false(reach) 14 350 false(reach) 15 370 witness unconfirmed 1.2  37
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c false(reach) 19    170 false(reach) 2.2   42 false(reach) 2.8  110 false(reach) 10   460 false(reach) 27   680 false(reach) 8.2 430 false(reach) 9.3 310 unknown 890    1800 witness timeout 65    300 false(reach) 240     66   witness timeout 1.1  26 false(reach) 20   480 false(reach) .80 62 unknown 8.1 370 witness timeout 5.5 130 false(reach) 570    22   false(reach) 14 410 false(reach) 15 470 witness unconfirmed 1.4  25
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c false(reach) .36 42 false(reach) .11  26 false(reach) .18 27 false(reach) 6.9 350 false(reach) 6.9 370 false(reach) 5.8 260 false(reach) 5.2 230 unknown 890    1900 false(reach) 4.7  180 error (139) 4.4   40   false(reach) .20 28 false(reach) 8.6 360 witness timeout .43 34 unknown 8.7 360 false(reach) 4.8 130 false(reach) .79 25   false(reach) 11 340 false(reach) 13 420 witness unconfirmed .59 25
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c true 65    350 true 79     64 true 850    1200 timeout 900   1500 true 35   900 true 33   800 true 26   1300 true 61    1800 true 5.2  270 error (134) 5.3   39   true 42    30 true 30   730 true 23    82 unknown 8.3 340 true 99   180 timeout 900    22   true 33 1100 timeout 34 570 unknown 150    110
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 82    370 timeout 650     190 true 850    1200 timeout 900   3600 true 34   890 true 32   880 true 29   1300 true 62    1800 true 7.1  280 true .85  39   true 34    29 true 35   840 true 92    110 unknown 7.4 330 true 83   180 timeout 900    23   true 33 810 timeout 37 710 unknown 150    100
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c true 150    490 true 180     68 true 850    1400 timeout 900   3700 true 43   1000 true 32   870 true 32   1300 unknown 890    4300 true 6.2  320 true 3.4   39   true 35    30 true 34   790 true 82    110 unknown 7.4 320 true 89   180 timeout 900    26   true 35 1000 timeout 37 640 unknown 130    100
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c true 78    370 timeout 660     190 true 850    1200 timeout 900   2500 true 36   900 true 35   850 true 27   1800 true 62    1800 true 5.6  270 true .93  39   true 34    29 true 33   780 true 18    76 unknown 7.5 330 true 88   180 timeout 900    23   true 34 830 timeout 35 690 unknown 95    110
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c timeout 900    7500 timeout 650     250 true 850    1100 timeout 900   2500 true 33   900 true 260   890 true 33   2300 unknown 890    1800 true 5.6  260 true 2.9   40   timeout 900    130 timeout 900   4500 true 7.5  70 unknown 8.3 340 true 880   360 timeout 900    22   true 32 670 timeout 54 1100 true 510    130
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c true 2.0  53 true .63  27 true 630    970 true 5.6 260 true 7.5 390 true 4.0 230 true 3.7 210 true 1.9  140 true .82 32 error (139) 18     39   true .33 24 true 17   410 true 1.4  57 unknown 36   1000 true 880   360 timeout 900    7.8 true 11 340 true 55 1400 true 5.6  52
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true .80 33 true .89  26 true 160    440 true 4.1 230 true 4.9 270 true 3.8 210 true 2.9 190 true .97 70 true .58 26 true .53  39   true .13 23 true 5.6 310 true .69 52 unknown 24   860 true 880   280 timeout 900    7.0 true 11 320 true 22 430 true 1.3  44
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c timeout 900    7700 true 210     81 true 850    1100 timeout 900   1400 true 33   860 true 210   880 true 36   2300 unknown 890    1800 true 5.7  280 true .95  39   timeout 900    120 timeout 900   4700 true 73    84 unknown 8.3 370 true 880   360 timeout 900    22   true 33 840 timeout 55 1200 true 310    120
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c timeout 900    7600 true 220     84 true 850    1000 timeout 900   2500 true 38   940 true 350   980 true 34   2300 unknown 890    1800 true 6.0  280 true 2.7   40   timeout 900    120 timeout 900   4800 true 160    91 unknown 8.3 370 true 880   360 timeout 900    22   true 27 550 timeout 44 890 true 550    130
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c timeout 900    7400 true 220     90 true 850    1000 timeout 900   950 true 36   890 true 320   1300 true 35   2300 unknown 900    1800 true 6.5  280 true .78  39   timeout 900    130 timeout 900   4800 true 10    61 unknown 8.6 370 true 880   370 timeout 900    22   true 31 680 timeout 54 840 true 570    140
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c timeout 900    7400 timeout 650     220 true 850    1000 timeout 900   2600 true 54   1300 true 390   1000 true 120   3600 unknown 890    1900 true 7.5  290 true 2.9   40   timeout 900    140 timeout 900   4900 timeout 900    170 unknown 8.5 380 true 880   330 timeout 900    25   true 36 940 timeout 29 690 true 880    180
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c timeout 900    7500 timeout 650     180 true 850    1000 true 30   850 true 50   1200 true 440   1400 true 100   3600 unknown 890    1900 true 5.8  290 true 56     40   timeout 900    130 timeout 900   4700 true 130    87 unknown 9.0 360 true 880   340 timeout 900    22   true 37 1300 timeout 56 1200 timeout 900    140
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c timeout 900    7700 true 110     58 true 850    1000 timeout 900   2500 true 34   890 true 390   1100 true 34   2300 unknown 890    1900 true 6.1  280 true 2.8   39   timeout 900    120 timeout 900   4700 true 4.8  65 unknown 8.6 370 true 880   340 timeout 900    23   true 33 590 timeout 45 1000 true 160    160
locks/test_locks_14_false-unreach-call.c false(reach) .18 27 false(reach) .096 24 false(reach) .20 25 timeout 900   2600 timeout 900   970 false(reach) 17   700 false(reach) 95   3600 false(reach) 100    2700 false(reach) 3.6  170 unknown .60  39   false(reach) .12 24 timeout 900   950 false(reach) .30 37 witness unconfirmed 19   750 witness timeout 3.7 84 false(reach) 3.3  120   false(reach) 11 340 false(reach) 11 330 witness unconfirmed .24 18
locks/test_locks_15_false-unreach-call.c false(reach) .15 29 false(reach) .12  26 false(reach) .15 25 timeout 900   3600 timeout 900   1200 false(reach) 20   760 false(reach) 96   2400 false(reach) 110    3700 false(reach) 3.7  170 false(reach) 3.0   39   false(reach) .18 24 exception 6.6 320 false(reach) .40 37 witness unconfirmed 35   1200 witness timeout 3.6 85 false(reach) 6.8  250   false(reach) 11 330 false(reach) 12 340 witness unconfirmed .23 14
locks/test_locks_10_true-unreach-call.c true .13 26 timeout 730     430 true 850    2900 true 4.2 220 true 7.2 290 true 340   2700 true 33   2300 true 9.2  830 true 1.1  59 unknown .52  39   true 31    31 true 6.6 330 true .23 24 unknown 52   1200 true 2.9 77 timeout 900    170   true 24 650 true 16 380 true .51 30
locks/test_locks_11_true-unreach-call_false-termination.c true .11 26 timeout 760     440 true 850    3500 true 4.0 220 true 6.4 300 timeout 900   2800 true 160   3600 true 11    1000 true 1.1  67 true .20  7.5 true 84    51 true 6.9 320 true .21 24 unknown 63   1300 true 3.1 77 timeout 900    170   true 25 1000 true 20 420 true .61 25
locks/test_locks_12_true-unreach-call_false-termination.c true .14 26 timeout 790     410 true 850    4000 true 4.1 220 true 6.9 350 timeout 900   1300 true 160   3600 true 14    1200 true 1.2  77 error (139) 4.4   39   true 240    110 true 6.3 320 true .23 25 unknown 95   1300 true 3.0 79 timeout 900    190   true 42 2100 true 22 510 true .62 29
locks/test_locks_13_true-unreach-call.c true .11 27 timeout 780     400 true 850    5000 true 4.2 220 true 7.4 330 timeout 900   1500 true 160   3500 true 16    1400 true 1.4  86 true 3.7   39   true 760    230 true 6.8 320 true .18 24 unknown 75   1200 true 3.1 81 timeout 900    220   true 64 3800 true 24 620 true .74 32
locks/test_locks_14_true-unreach-call.c true .15 29 timeout 780     410 true 850    5300 true 4.2 220 true 10   480 timeout 900   1500 true 160   2500 true 19    1600 true 1.4  96 error (139) 370     40   timeout 900    270 true 7.3 330 true .21 25 unknown 81   1300 true 3.2 82 timeout 900    290   true 110 5400 true 26 620 true .94 31
locks/test_locks_15_true-unreach-call_false-termination.c true .16 27 timeout 810     410 true 850    2000 true 3.6 220 true 11   450 timeout 900   1100 true 160   3600 true 23    1800 true 1.7  110 true .68  39   timeout 900    240 true 7.5 330 true .22 25 unknown 75   1200 true 3.1 78 timeout 900    510   true 250 7200 true 27 630 true .93 37
locks/test_locks_5_true-unreach-call_false-termination.c true .11 24 true 15     41 true 180    1000 true 3.4 210 true 5.0 260 true 4.9 230 true 4.2 220 true 2.3  230 true .65 29 true 2.9   38   true .39 23 true 5.6 300 true .22 25 unknown 28   910 true 3.1 81 timeout 900    25   true 11 320 true 13 370 true .26 23
locks/test_locks_6_true-unreach-call_false-termination.c true .15 24 true 30     47 true 270    1400 true 4.0 210 true 5.2 270 true 6.4 270 true 5.5 230 true 3.1  320 true .68 34 error (134) 7.8   38   true .89 23 true 5.9 300 true .26 24 unknown 34   970 true 3.0 80 timeout 900    160   true 13 430 true 13 340 true .33 27
locks/test_locks_7_true-unreach-call_false-termination.c true .12 25 true 86     73 true 400    1800 true 4.1 220 true 6.2 270 true 6.7 300 true 7.2 330 true 4.3  430 true .85 39 timeout .086 3.5 true 1.7  24 true 6.6 310 true .21 25 unknown 41   1200 true 3.0 68 timeout 900    530   true 17 490 true 15 450 true .34 25
locks/test_locks_8_true-unreach-call_false-termination.c true .12 25 true 170     190 true 550    2300 true 4.0 220 true 6.8 290 true 13   580 true 9.6 650 true 5.3  550 true .83 45 error (134) 53     39   true 4.8  27 true 5.7 320 true .21 24 unknown 47   1100 true 3.0 75 timeout 900    320   true 17 480 true 15 490 true .39 32
locks/test_locks_9_true-unreach-call.c true .13 25 true 410     230 true 780    2800 true 3.4 220 true 5.8 280 true 140   1400 true 18   690 true 7.2  680 true .86 52 unknown .54  38   true 11    27 true 5.9 310 true .23 25 unknown 52   1200 true 3.1 82 timeout 900    220   true 23 540 true 16 350 true .54 25
../../sv-benchmarks/c/ 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) 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 48 7100 59000 48 11000 6000 48 17000 47000 48 20000 66000 48 2900 34000 48 10000 43000 48 2400 75000 48 21000 120000 48 860 8600 48 820 1700 48 9400   2800 48 7900 54000 48 1500 3000 48 1100 32000 48 8500   7600 48 35000 4000 48 1800 49000 48 2200 41000 48 4500 3000
    correct results 39 680 5700 32 2900 2300 47 17000 47000 21 200 8000 46 1100 31000 43 5500 35000 48 2400 75000 31 6200 64000 43 480 7100 21 330 800 27 1300   1000 38 700 19000 43 630 2500 0 31 8400   5400 10 3000 510 47 1800 49000 23 510 12000 20 3000 1400
        correct true 23 380 2900 19 2700 1800 30 17000 46000 17 150 5800 30 640 19000 25 3800 21000 30 1500 50000 22 300 16000 30 88 4100 19 90 690 21 1300   890 23 340 10000 29 610 1500 0 30 8400   5300 2 850 24 30 1300 39000 15 380 8800 20 3000 1400
        correct false 16 300 2700 13 210 560 17 34 1300 4 50 2200 16 490 13000 18 1800 14000 18 850 25000 9 5900 48000 13 390 3000 2 240 100 6 2.4 160 15 370 8600 14 22 960 0 1 4.8 130 8 2100 490 17 450 9700 8 140 3400 0
    incorrect results 0 0 0 0 0 0 0 0 0 9 12 300 0 0 0 0 0 0 0 0 0
        incorrect true 0 0 0 0 0 0 0 0 0 9 12 300 0 0 0 0 0 0 0 0 0
        incorrect false 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
score (48 tasks, max score: 78) 62 51 77 38 76 68 78 53 73 -248 48 61 72 0 61 12 77 38 40
Run set 2ls.sv-comp16.ControlFlow blast.sv-comp16.ControlFlow cbmc.sv-comp16.ControlFlow cpa-bam.sv-comp16.ControlFlow cpa-kind.sv-comp16.ControlFlow cpa-refsel.sv-comp16.ControlFlow cpa-seq.sv-comp16.ControlFlow esbmc.sv-comp16.ControlFlow esbmcdepthk.sv-comp16.ControlFlow forest.sv-comp16.ControlFlow impara.sv-comp16.ControlFlow lpi.sv-comp16.ControlFlow seahorn.sv-comp16.ControlFlow skink.sv-comp16.ControlFlow smack.sv-comp16.ControlFlow symbiotic3.sv-comp16.ControlFlow uautomizer.sv-comp16.ControlFlow ukojak.sv-comp16.ControlFlow vvt.sv-comp16.ControlFlow