Tool JayHorn 0.6-alpha JBMC 5.10 (cbmc-5.10-1744-gdf5e3b8-dirty) JPF 3a45016c72f2e7bd617f7984d07839c798528183 SPF Mon Nov 19 09:51:16 CET 2018
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-06 11:12:12 CET 2018-12-06 11:33:09 CET 2018-12-06 11:55:55 CET 2018-12-07 20:12:45 CET
Run set jayhorn.sv-comp19_prop-reachsafety_java.ReachSafety-Java jbmc.sv-comp19_prop-reachsafety_java.ReachSafety-Java jpf.sv-comp19_prop-reachsafety_java.ReachSafety-Java spf.sv-comp19_prop-reachsafety_java.ReachSafety-Java
../sv-benchmarks/java/ status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J)
jayhorn-recursive/Ackermann01.yml false 12   330 110 false 1.1  51 9.8 false 1.5 63 11 false 2.1 95 18
jayhorn-recursive/Addition.yml true 5.9 330 52 error (42) 880    7100 7400   true 1.5 60 14 true 2.0 90 19
jayhorn-recursive/InfiniteLoop.yml unknown 3.2 140 27 false 1.1  51 9.6 false 1.5 62 14 false 1.8 79 16
jayhorn-recursive/SatAckermann01.yml true 5.7 300 48 error (42) 880    270 6400   true 1.6 60 13 true 7.1 250 69
jayhorn-recursive/SatAckermann02.yml true 13   520 96 error (42) 880    270 5500   true 1.6 61 15 true 6.9 240 70
jayhorn-recursive/SatAckermann03.yml true 12   460 110 error (42) 880    270 5300   true 1.6 63 17 true 7.3 260 77
jayhorn-recursive/SatAddition01.yml true 5.9 320 51 error (42) 880    2000 4700   timeout 910   1100 4000 true 2.1 100 20
jayhorn-recursive/SatEvenOdd01.yml timeout 900   3000 9300 error (42) 880    390 8300   timeout 910   1100 4100 true 2.1 95 18
jayhorn-recursive/SatFibonacci01.yml true 6.7 350 59 error (42) 880    160 5200   true 1.6 60 15 true 2.8 150 26
jayhorn-recursive/SatFibonacci02.yml true 19   790 130 true 2.0  51 19   true 1.6 59 14 true 1.9 78 15
jayhorn-recursive/SatFibonacci03.yml true 25   870 160 error (42) 880    160 7500   true 1.5 61 13 true 2.8 150 26
jayhorn-recursive/SatGcd.yml true 5.6 320 53 error (42) 880    2500 6700   true 1.5 62 14 true 65   110 930
jayhorn-recursive/SatHanoi01.yml timeout 900   2700 12000 error (42) 880    210 6400   true 1.5 62 12 true 4.9 260 40
jayhorn-recursive/SatMccarthy91.yml true 6.2 340 51 error (42) 880    210 4500   timeout 910   1100 4100 true 43   390 520
jayhorn-recursive/SatMultCommutative01.yml timeout 900   2500 9300 error (42) 880    570 4600   true 1.6 60 13 true 2.3 100 21
jayhorn-recursive/SatPrimes01.yml true 9.6 370 68 error (42) 880    220 5800   true 1.6 59 14 unknown 230   570 2400
jayhorn-recursive/UnsatAckermann01.yml false 13   340 110 false 7.4  91 76   timeout 910   1100 4000 false 1.8 89 17
jayhorn-recursive/UnsatAddition01.yml false 11   320 89 false 1.0  51 9.3 timeout 910   1100 3900 false 1.8 88 16
jayhorn-recursive/UnsatAddition02.yml true 120   2500 990 error (42) 880    11000 8900   timeout 910   1100 4100 true 2.4 100 21
jayhorn-recursive/UnsatEvenOdd01.yml false 13   340 110 false 1.0  51 9.9 false 1.6 61 14 false 1.9 94 18
jayhorn-recursive/UnsatFibonacci01.yml false 13   360 110 false 2.6  54 28   timeout 910   1100 3700 false 1.9 91 19
jayhorn-recursive/UnsatFibonacci02.yml false 24   500 200 error (42) 880    160 5500   timeout 910   1100 3800 false 2.3 110 21
jayhorn-recursive/UnsatMccarthy91.yml false 9.7 320 81 false 1.1  51 9.6 timeout 910   1100 4000 false 1.8 90 17
jbmc-regression/ArithmeticException1.yml false 11   310 100 false 1.1  52 11   false 1.6 62 15 false 1.9 87 17
jbmc-regression/ArithmeticException5.yml true 3.8 250 37 true 1.4  50 13   true 1.5 62 14 true 1.8 77 12
jbmc-regression/ArithmeticException6.yml false 10   310 83 false 1.1  51 11   false 1.6 60 14 false 1.9 88 15
jbmc-regression/ArrayIndexOutOfBoundsException1.yml false 14   430 110 false .99 51 9.7 false 1.6 61 14 false 1.9 89 15
jbmc-regression/ArrayIndexOutOfBoundsException2.yml false 13   400 100 false .99 51 10   false 1.6 60 15 false 1.9 89 18
jbmc-regression/ArrayIndexOutOfBoundsException3.yml false 17   440 150 false 1.0  51 9.7 false 1.5 60 15 false 1.9 91 17
jbmc-regression/BufferedReaderReadLine.yml timeout 900   3400 9300 false 1.2  51 11   false 1.6 63 15 false 1.9 88 18
jbmc-regression/CharSequenceBug.yml unknown 34   1000 300 false 1.1  51 10   false 1.5 63 14 false 1.9 87 16
jbmc-regression/CharSequenceToString.yml unknown 52   1300 490 true 1.8  51 21   unknown 1.6 77 14 false 1.9 95 18
jbmc-regression/ClassCastException1.yml unknown 12   350 98 false 1.1  51 11   false 1.5 63 16 false 1.7 81 16
jbmc-regression/ClassCastException2.yml true 4.7 290 44 true 1.5  51 16   true 1.7 62 13 true 1.7 76 16
jbmc-regression/ClassCastException3.yml false 14   440 110 false 1.1  50 11   false 1.5 63 16 false 1.8 78 17
jbmc-regression/Class_method1.yml true 3.7 240 39 true 1.5  51 16   true 1.6 60 14 true 1.8 76 16
jbmc-regression/Inheritance1.yml true 4.9 300 41 true 1.6  51 16   true 1.5 59 13 true 1.7 75 15
jbmc-regression/NegativeArraySizeException1.yml false 7.7 300 70 false 1.0  51 8.5 false 1.6 59 13 false 1.8 81 16
jbmc-regression/NegativeArraySizeException2.yml false 7.5 290 73 false 1.1  58 11   false 1.5 61 14 false 1.9 78 15
jbmc-regression/NullPointerException1.yml unknown 3.2 140 31 true 1.5  51 15   true 1.5 60 13 true 1.8 79 15
jbmc-regression/NullPointerException2.yml unknown 3.3 140 32 false 1.0  50 9.4 false 1.6 60 13 false 1.9 79 15
jbmc-regression/NullPointerException3.yml unknown 3.3 150 32 false 1.0  51 9.0 false 1.4 59 15 false 1.7 78 16
jbmc-regression/NullPointerException4.yml unknown 3.3 140 30 false 1.1  50 10   false 1.6 62 15 false 1.8 80 15
jbmc-regression/RegexMatches01.yml timeout 900   3200 10000 error (10) 1.2  52 10   true 1.5 62 14 true 1.8 77 17
jbmc-regression/RegexMatches02.yml timeout 900   2900 9900 error (10) 1.2  52 9.7 unknown 1.8 77 17 true 1.8 80 16
jbmc-regression/RegexSubstitution01.yml timeout 900   3400 11000 error (10) 99    8200 1200   true 1.7 64 16 true 2.0 80 19
jbmc-regression/RegexSubstitution02.yml timeout 900   3000 11000 out of memory 120    13000 1300   false 1.6 62 14 unknown 1.9 79 18
jbmc-regression/RegexSubstitution03.yml timeout 900   3200 12000 error (10) 2.7  110 30   true 1.7 63 15 true 1.8 79 16
jbmc-regression/StaticCharMethods01.yml unknown 12   330 93 true 2.3  53 32   true 1.6 61 14 true 1.7 78 15
jbmc-regression/StaticCharMethods02.yml unknown 32   970 300 false 1.7  64 17   unknown 1.7 75 15 false 1.9 91 16
jbmc-regression/StaticCharMethods03.yml unknown 32   940 280 false 1.6  56 22   unknown 1.6 77 14 false 1.8 87 17
jbmc-regression/StaticCharMethods04.yml unknown 8.1 320 75 false 1.2  52 12   false 1.6 63 13 false 1.7 81 15
jbmc-regression/StaticCharMethods05.yml timeout 900   3200 9800 false 2.7  73 27   unknown 1.8 64 14 unknown 1.8 80 14
jbmc-regression/StaticCharMethods06.yml unknown 33   950 280 true 4.3  62 48   unknown 1.6 76 13 true 1.9 87 16
jbmc-regression/StringBuilderAppend01.yml timeout 900   3100 10000 error (134) 1.4  55 14   true 1.7 63 15 true 1.8 81 15
jbmc-regression/StringBuilderAppend02.yml timeout 900   3300 12000 error (42) 880    170 12000   false 1.8 64 13 unknown 2.0 80 18
jbmc-regression/StringBuilderCapLen01.yml unknown 33   810 310 error (10) 1.1  51 11   true 1.6 62 13 true 1.8 79 17
jbmc-regression/StringBuilderCapLen02.yml unknown 68   1300 640 false 1.1  51 10   false 1.6 62 15 false 1.9 87 15
jbmc-regression/StringBuilderCapLen03.yml unknown 42   1200 400 false 1.0  51 9.9 false 1.5 62 15 unknown 1.8 79 14
jbmc-regression/StringBuilderCapLen04.yml unknown 42   1200 350 error (10) 1.0  50 11   false 1.6 62 15 unknown 1.7 81 15
jbmc-regression/StringBuilderChars01.yml timeout 900   3400 5800 true 7.7  450 110   true 1.5 59 15 true 1.9 77 15
jbmc-regression/StringBuilderChars02.yml unknown 69   1300 740 false 1.1  51 12   false 1.5 61 13 false 1.8 83 16
jbmc-regression/StringBuilderChars03.yml unknown 43   1300 410 false 1.0  51 8.9 false 1.7 62 14 unknown 1.7 77 15
jbmc-regression/StringBuilderChars04.yml timeout 910   3400 5600 false 1.4  53 12   unknown 1.8 77 14 unknown 1.9 80 18
jbmc-regression/StringBuilderChars05.yml unknown 84   1400 960 false 1.2  52 12   false 1.7 62 15 unknown 1.7 79 14
jbmc-regression/StringBuilderChars06.yml unknown 120   1600 1500 false 1.1  51 12   false 1.6 61 15 unknown 1.8 81 16
jbmc-regression/StringBuilderConstructors01.yml unknown 34   1000 310 true 1.7  51 21   unknown 1.6 76 13 unknown 1.9 95 17
jbmc-regression/StringBuilderConstructors02.yml unknown 49   1400 430 false 1.1  51 10   false 1.6 61 14 unknown 1.8 80 15
jbmc-regression/StringBuilderInsertDelete01.yml timeout 900   3100 9700 error (42) 880    130 12000   true 1.6 62 13 true 1.8 82 16
jbmc-regression/StringBuilderInsertDelete02.yml timeout 900   3400 11000 error (42) 880    120 13000   false 1.6 63 15 unknown 1.9 80 18
jbmc-regression/StringBuilderInsertDelete03.yml timeout 900   3400 11000 error (42) 880    130 12000   false 1.9 65 16 unknown 1.8 82 17
jbmc-regression/StringCompare01.yml unknown 15   440 120 error (10) 1.3  52 15   true 1.6 59 15 true 1.8 76 17
jbmc-regression/StringCompare02.yml unknown 280   1700 3200 error (10) 1.0  51 11   false 1.6 62 14 unknown 1.7 80 15
jbmc-regression/StringCompare03.yml unknown 240   1700 3300 error (10) 1.1  51 11   unknown 1.6 75 13 unknown 1.7 79 17
jbmc-regression/StringCompare04.yml unknown 400   2100 4700 false 1.2  60 12   false 1.6 63 14 unknown 1.8 80 16
jbmc-regression/StringCompare05.yml unknown 49   1300 500 false 1.0  51 10   false 1.6 60 15 false 1.8 80 17
jbmc-regression/StringConcatenation01.yml timeout 900   3200 10000 true 10    100 130   unknown 1.6 77 15 false 1.8 82 15
jbmc-regression/StringConcatenation02.yml timeout 900   3400 10000 false 1.5  57 15   false 1.5 62 13 false 1.8 83 19
jbmc-regression/StringConcatenation03.yml timeout 900   2900 10000 false 1.2  53 13   false 1.6 61 14 false 1.9 81 16
jbmc-regression/StringConcatenation04.yml unknown 140   1600 1600 false 1.2  52 11   false 1.5 61 13 false 1.8 83 15
jbmc-regression/StringConstructors01.yml unknown 110   1600 1200 true 3.6  71 46   true 1.6 60 14 true 1.8 79 15
jbmc-regression/StringConstructors02.yml unknown 40   1200 380 false 1.1  51 9.6 unknown 1.6 78 16 false 1.8 83 16
jbmc-regression/StringConstructors03.yml timeout 900   3100 12000 false 1.2  52 13   unknown 1.7 74 14 false 1.8 85 17
jbmc-regression/StringConstructors04.yml unknown 380   2100 4000 false 1.7  52 19   false 1.5 61 13 false 1.8 84 18
jbmc-regression/StringConstructors05.yml unknown 160   1900 1600 false 2.5  57 28   false 1.6 65 13 false 1.9 89 16
jbmc-regression/StringContains01.yml unknown 250   1700 2600 false .99 51 11   unknown 1.6 77 14 false 1.8 86 15
jbmc-regression/StringContains02.yml unknown 33   1100 300 false 1.0  51 11   false 1.6 62 16 false 1.8 82 16
jbmc-regression/StringIndexMethods01.yml unknown 14   320 120 true 6.5  81 68   true 1.6 62 15 true 1.7 79 14
jbmc-regression/StringIndexMethods02.yml unknown 32   990 300 false 1.2  51 11   false 1.6 60 14 false 1.9 92 18
jbmc-regression/StringIndexMethods03.yml unknown 34   990 310 false 1.1  59 10   false 1.5 62 14 false 2.0 91 20
jbmc-regression/StringIndexMethods04.yml unknown 34   1100 320 false 1.1  52 11   false 1.5 60 13 false 1.8 90 18
jbmc-regression/StringIndexMethods05.yml unknown 34   1100 290 false 1.1  51 11   false 1.6 62 15 false 1.8 88 16
jbmc-regression/StringMiscellaneous01.yml unknown 110   1600 950 true 13    66 150   true 1.7 62 17 unknown 1.9 78 18
jbmc-regression/StringMiscellaneous02.yml unknown 31   1000 270 false 1.0  59 8.9 false 1.5 63 13 false 2.0 94 17
jbmc-regression/StringMiscellaneous03.yml unknown 450   2000 5400 false 1.7  67 19   unknown 1.6 75 14 false 2.0 92 16
jbmc-regression/StringMiscellaneous04.yml timeout 900   2800 11000 true 4.7  64 66   true 1.6 62 14 true 1.9 77 16
jbmc-regression/StringStartEnd01.yml unknown 42   870 350 true 3.6  65 39   true 1.6 60 14 true 1.7 78 14
jbmc-regression/StringStartEnd02.yml timeout 900   3400 10000 false 1.7  51 19   false 1.5 61 14 false 1.9 84 18
jbmc-regression/StringStartEnd03.yml timeout 900   3200 13000 false 1.9  55 20   false 1.5 61 13 false 1.9 87 18
jbmc-regression/StringValueOf01.yml timeout 900   3400 7900 error (10) 2.2  110 28   true 1.5 62 15 true 1.9 81 17
jbmc-regression/StringValueOf02.yml unknown 460   2300 5100 false 2.1  92 20   false 1.6 61 12 false 1.9 80 15
jbmc-regression/StringValueOf03.yml timeout 900   3400 8900 false 2.9  110 33   false 1.7 62 17 false 1.8 79 14
jbmc-regression/StringValueOf04.yml unknown 11   340 91 false 1.1  51 10   false 1.5 62 12 false 1.8 78 16
jbmc-regression/StringValueOf05.yml unknown 46   1300 470 false 1.3  52 13   unknown 1.6 78 15 unknown 1.9 94 16
jbmc-regression/StringValueOf06.yml unknown 12   330 110 false 1.1  51 10   false 1.5 60 16 false 1.9 82 17
jbmc-regression/StringValueOf07.yml unknown 46   1200 430 false 1.7  54 20   false 1.6 61 14 unknown 1.9 81 17
jbmc-regression/StringValueOf08.yml unknown 54   1300 500 false 2.1  160 22   false 1.5 63 14 unknown 1.8 80 16
jbmc-regression/StringValueOf09.yml unknown 52   1300 490 false 1.9  160 21   false 1.6 62 15 unknown 1.7 86 14
jbmc-regression/StringValueOf10.yml unknown 450   2100 5400 false 1.1  51 10   false 1.6 64 13 false 1.9 86 16
jbmc-regression/SubString01.yml unknown 17   450 140 true 2.0  52 22   true 1.5 61 14 true 1.7 79 17
jbmc-regression/SubString02.yml unknown 51   1300 520 false 1.2  52 11   false 1.6 63 14 false 1.9 88 16
jbmc-regression/SubString03.yml unknown 52   1300 460 false 1.1  52 11   false 1.5 62 16 false 1.9 84 16
jbmc-regression/TokenTest01.yml timeout 900   3400 9000 true 86    790 1000   true 1.5 61 14 true 1.9 79 18
jbmc-regression/TokenTest02.yml timeout 900   3300 9800 out of memory 260    13000 3500   unknown 1.7 78 14 unknown 1.8 80 15
jbmc-regression/Validate01.yml unknown 18   470 150 error (10) 1.2  52 12   true 1.6 62 14 true 1.7 78 16
jbmc-regression/Validate02.yml timeout 900   2500 11000 error (10) 1.2  51 11   false 1.7 61 13 unknown 2.0 82 17
jbmc-regression/aastore_aaload1.yml timeout 910   3400 6500 out of memory 540    14000 6800   unknown 1.8 75 15 true 120   140 1600
jbmc-regression/array1.yml timeout 900   2600 12000 out of memory 230    14000 2900   unknown 1.6 75 13 true 2.0 91 17
jbmc-regression/array2.yml true 18   450 150 true 1.9  51 24   true 1.5 60 14 true 2.0 94 18
jbmc-regression/arraylength1.yml true 4.5 290 40 true 1.6  51 17   unknown 1.7 76 13 true 1.9 90 17
jbmc-regression/arrayread1.yml true 4.8 300 45 true 1.6  51 16   true 1.5 62 15 true 1.7 87 15
jbmc-regression/assert1.yml true 4.5 300 44 true 1.9  51 20   true 1.6 60 14 true 1.9 89 18
jbmc-regression/assert2.yml false 7.9 300 70 false 1.1  51 9.4 true 1.6 61 14 false 2.0 94 17
jbmc-regression/assert3.yml false 8.0 300 76 false 1.0  51 11   true 1.5 61 14 false 1.8 86 15
jbmc-regression/assert4.yml false 8.0 310 77 false 1.1  51 9.9 true 1.6 62 14 false 2.0 94 20
jbmc-regression/assert5.yml true 4.4 300 40 true 1.7  51 18   true 1.5 61 12 true 1.9 89 16
jbmc-regression/assert6.yml true 4.2 300 37 true 1.5  51 17   true 1.5 63 14 true 1.8 89 16
jbmc-regression/astore_aload1.yml timeout 900   4900 7000 true 9.4  120 110   true 1.7 62 15 true 1.8 79 15
jbmc-regression/athrow1.yml false 11   320 96 false 1.0  51 8.8 false 1.6 60 13 false 1.9 78 18
jbmc-regression/basic1.yml true 5.7 310 54 true 1.5  51 17   true 1.6 59 15 true 1.8 78 16
jbmc-regression/bitwise1.yml unknown 8.6 320 76 true 1.5  51 16   true 1.5 60 12 true 2.0 93 19
jbmc-regression/boolean1.yml true 3.7 240 34 true 1.5  51 16   true 1.5 59 14 true 1.8 79 16
jbmc-regression/boolean2.yml true 5.3 320 46 true 1.6  51 17   true 1.5 59 13 true 1.8 78 17
jbmc-regression/bug-test-gen-095.yml unknown 120   1600 1300 false 1.2  51 11   false 1.6 62 14 false 1.9 83 17
jbmc-regression/bug-test-gen-119-2.yml unknown 12   340 98 true 3.0  53 34   true 1.6 61 14 true 1.8 77 17
jbmc-regression/bug-test-gen-119.yml unknown 14   340 110 true 1.8  51 18   true 1.4 61 13 true 1.9 82 15
jbmc-regression/calc.yml timeout 900   2400 11000 error (42) 880    340 8900   unknown 1.7 77 14 true 32   130 400
jbmc-regression/cast1.yml unknown 57   1300 610 true 1.9  52 22   true 1.5 60 13 false 1.9 87 16
jbmc-regression/catch1.yml true 4.9 290 41 true 1.5  51 17   true 1.5 60 14 true 1.7 78 16
jbmc-regression/char1.yml unknown 33   950 260 true 1.9  59 24   unknown 1.7 76 14 true 2.1 92 18
jbmc-regression/charArray.yml unknown 35   1100 300 true 6.9  170 90   unknown 1.6 74 14 unknown 1.9 89 19
jbmc-regression/classtest1.yml unknown 4.2 170 38 true 1.4  50 15   true 1.5 61 14 true 1.7 77 15
jbmc-regression/const1.yml true 3.9 250 39 true 1.6  51 18   true 1.5 61 12 true 1.7 78 13
jbmc-regression/constructor1.yml true 19   480 160 true 1.6  52 16   true 1.6 67 14 true 1.8 79 15
jbmc-regression/enum1.yml true 4.6 250 41 true 1.9  51 21   true 1.5 62 13 true 1.7 76 15
jbmc-regression/exceptions1.yml false 44   1200 410 false 1.1  51 10   false 1.6 60 14 false 1.8 80 15
jbmc-regression/exceptions10.yml false 16   460 130 false 1.1  51 10   false 1.5 62 13 false 1.8 79 16
jbmc-regression/exceptions11.yml false 18   460 170 false 1.0  51 9.8 false 1.5 63 15 false 1.7 80 14
jbmc-regression/exceptions12.yml false 15   450 120 false 1.1  51 10   false 1.5 62 14 false 1.7 78 15
jbmc-regression/exceptions13.yml false 15   450 120 false 1.1  51 11   false 1.6 62 14 false 1.7 78 18
jbmc-regression/exceptions14.yml true 5.1 310 45 true 1.5  51 19   true 1.5 60 14 true 1.7 81 16
jbmc-regression/exceptions15.yml true 5.9 310 54 true 1.6  51 16   true 1.5 61 14 true 1.8 80 15
jbmc-regression/exceptions16.yml false 12   330 100 false 1.2  51 11   false 1.5 60 14 false 1.8 83 15
jbmc-regression/exceptions18.yml true 4.6 290 43 true 1.6  51 17   true 1.5 62 14 true 1.7 79 17
jbmc-regression/exceptions2.yml false 12   320 90 false 1.1  51 8.9 false 1.6 59 15 false 1.8 79 15
jbmc-regression/exceptions3.yml false 12   330 98 false 1.0  51 9.9 false 1.7 61 15 false 1.7 78 15
jbmc-regression/exceptions4.yml true 5.1 310 50 true 1.5  51 17   true 1.5 60 15 true 1.8 78 17
jbmc-regression/exceptions5.yml true 7.6 340 62 true 1.7  51 17   true 1.6 62 14 true 1.8 76 16
jbmc-regression/exceptions6.yml unknown 4.5 170 36 false 1.1  51 9.2 false 1.5 62 16 false 1.8 77 16
jbmc-regression/exceptions7.yml false 19   510 160 false 1.1  51 9.7 false 1.6 61 13 false 1.7 76 16
jbmc-regression/exceptions8.yml false 18   470 160 false 1.1  51 9.3 false 1.6 61 13 false 1.8 79 18
jbmc-regression/exceptions9.yml true 5.1 300 38 true 1.6  51 17   true 1.6 62 15 true 1.8 78 15
jbmc-regression/fcmpx_dcmpx1.yml true 4.0 290 39 true 1.5  51 15   true 1.5 60 13 true 1.7 78 16
jbmc-regression/iarith1.yml unknown 4.6 180 42 true 1.5  51 17   true 1.6 62 14 true 1.9 79 14
jbmc-regression/iarith2.yml true 4.2 300 42 true 1.6  51 18   true 1.6 62 14 true 1.8 78 18
jbmc-regression/if_acmp1.yml true 6.0 310 56 true 1.6  52 22   true 1.6 58 15 true 1.9 78 16
jbmc-regression/if_expr1.yml true 5.1 330 46 true 1.6  51 18   true 1.5 61 13 true 1.8 89 15
jbmc-regression/if_icmp1.yml true 5.3 320 49 true 1.7  51 18   true 1.6 60 13 true 2.1 92 16
jbmc-regression/ifxx1.yml true 3.7 250 33 true 1.5  51 17   true 1.5 62 13 true 2.0 79 14
jbmc-regression/instanceof1.yml true 4.0 250 43 true 1.5  51 14   true 1.6 60 12 false 1.7 79 15
jbmc-regression/instanceof2.yml unknown 4.2 170 42 true 1.7  51 15   true 1.5 59 13 true 1.8 77 15
jbmc-regression/instanceof3.yml true 3.8 250 39 true 1.6  51 16   true 1.6 60 14 true 1.9 78 16
jbmc-regression/instanceof4.yml true 3.8 250 33 true 1.5  51 14   true 1.6 59 13 true 1.7 76 16
jbmc-regression/instanceof5.yml unknown 4.3 170 41 true 1.4  51 16   true 1.5 59 13 true 1.6 78 17
jbmc-regression/instanceof6.yml true 25   560 220 true 1.6  51 20   true 1.5 59 11 true 1.7 79 14
jbmc-regression/instanceof7.yml true 28   660 230 true 1.6  51 19   true 1.6 61 16 true 1.7 77 13
jbmc-regression/instanceof8.yml true 4.5 300 40 true 1.8  51 21   true 1.6 60 12 true 1.8 79 16
jbmc-regression/interface1.yml false 12   340 110 false 1.1  51 9.8 false 1.5 61 14 false 1.7 80 14
jbmc-regression/java_append_char.yml unknown 120   1600 1200 false 1.9  56 21   false 1.6 61 14 false 1.8 81 16
jbmc-regression/lazyloading4.yml true 4.8 290 46 true 1.5  58 15   true 1.5 60 11 true 1.8 79 15
jbmc-regression/list1.yml timeout 900   2700 11000 true 50    190 600   true 11   220 95 true 42   260 490
jbmc-regression/long1.yml unknown 28   570 230 true 1.5  59 15   true 1.5 61 14 true 1.8 78 18
jbmc-regression/lookupswitch1.yml true 6.9 350 62 true 1.6  51 18   true 1.5 62 12 true 1.8 87 15
jbmc-regression/multinewarray.yml true 5.0 260 42 true 2.9  55 33   true 1.6 59 13 true 1.8 77 16
jbmc-regression/overloading1.yml true 4.3 300 39 true 1.5  51 14   true 1.4 60 13 true 1.7 74 17
jbmc-regression/package1.yml true 3.9 250 34 true 1.5  51 14   true 1.6 61 16 true 1.7 76 17
jbmc-regression/putfield_getfield1.yml true 4.4 300 42 true 1.5  51 15   true 1.6 61 14 true 1.7 77 15
jbmc-regression/putstatic_getstatic1.yml true 4.0 260 37 true 1.5  51 16   true 1.5 62 13 true 1.7 76 16
jbmc-regression/recursion2.yml true 7.8 380 65 true 1.8  51 20   true 1.5 61 13 true 1.7 74 14
jbmc-regression/return1.yml false 8.0 300 78 false 1.0  51 11   false 1.5 60 14 false 1.9 79 18
jbmc-regression/return2.yml false 7.7 310 69 false 1.1  51 11   false 1.5 62 14 false 1.8 87 17
jbmc-regression/store_load1.yml true 4.7 300 42 true 1.6  52 16   true 1.6 59 14 true 1.7 78 14
jbmc-regression/swap1.yml unknown 9.7 330 84 true 1.4  51 14   true 1.5 62 15 true 1.7 76 13
jbmc-regression/synchronized.yml false 7.6 300 75 true 1.5  51 15   true 1.6 59 16 true 1.7 78 15
jbmc-regression/tableswitch1.yml true 6.6 340 53 true 1.6  52 16   true 1.5 62 15 true 1.9 90 15
jbmc-regression/uninitialised1.yml true 4.0 240 40 true 1.5  51 16   true 1.5 62 14 true 1.8 77 15
jbmc-regression/virtual1.yml true 4.3 300 44 true 1.5  51 18   true 1.5 61 14 true 1.7 80 15
jbmc-regression/virtual2.yml false 9.9 320 95 false 1.0  51 12   false 1.5 61 14 false 1.8 79 15
jbmc-regression/virtual4.yml true 4.6 310 39 true 1.5  51 14   true 1.5 59 14 true 1.7 78 15
jbmc-regression/virtual_function_unwinding.yml true 5.8 310 49 true 1.6  51 16   true 1.6 61 14 true 1.8 77 15
jpf-regression/ExDarko_false.yml unknown 87   1500 900 false 1.2  51 12   false 1.5 61 15 false 2.0 95 18
jpf-regression/ExDarko_true.yml true 9.7 370 81 true 1.9  52 23   true 1.6 60 12 true 2.0 92 19
jpf-regression/ExException_false.yml false 14   370 130 false 1.1  58 10   false 1.6 60 16 false 1.9 92 18
jpf-regression/ExException_true.yml true 6.1 320 51 true 1.7  51 21   true 1.6 62 14 true 1.9 79 17
jpf-regression/ExGenSymExe_false.yml false 69   1500 660 false 1.1  51 10   false 1.6 60 13 false 2.0 77 25
jpf-regression/ExGenSymExe_true.yml true 78   1300 750 true 1.7  51 18   true 1.5 60 14 true 1.8 79 16
jpf-regression/ExLazy_false.yml false 9.8 310 80 false 1.2  59 15   false 1.6 61 15 false 1.8 87 14
jpf-regression/ExLazy_true.yml true 5.9 330 50 true 1.6  51 17   true 1.5 62 13 true 1.9 94 18
jpf-regression/ExMIT_false.yml false 8.4 310 70 false 1.0  51 9.2 true 1.6 61 13 false 1.9 88 15
jpf-regression/ExMIT_true.yml true 4.1 290 39 true 1.5  51 17   true 1.5 61 14 true 1.9 91 18
jpf-regression/ExSymExe10_false.yml false 14   370 130 false 1.1  51 11   false 1.5 63 16 false 1.8 88 18
jpf-regression/ExSymExe10_true.yml true 6.4 330 60 true 1.6  51 17   true 1.5 62 14 true 1.9 90 15
jpf-regression/ExSymExe11_false.yml false 13   350 120 false 1.1  51 9.8 false 1.5 63 14 false 1.8 80 15
jpf-regression/ExSymExe11_true.yml true 5.6 320 52 true 1.6  51 16   true 1.6 61 15 true 1.8 85 15
jpf-regression/ExSymExe12_false.yml false 14   360 110 false 1.1  51 11   false 1.6 61 13 false 2.0 96 17
jpf-regression/ExSymExe12_true.yml true 6.9 340 62 true 1.8  51 18   true 1.5 62 14 true 1.9 85 16
jpf-regression/ExSymExe13_false.yml false 15   400 130 false 1.1  51 10   false 1.6 62 14 false 2.0 89 18
jpf-regression/ExSymExe13_true.yml true 7.5 350 67 true 1.7  52 19   true 1.5 63 13 true 1.9 92 19
jpf-regression/ExSymExe14_false.yml false 15   370 130 false 1.1  51 11   false 1.6 63 14 false 2.0 86 17
jpf-regression/ExSymExe14_true.yml true 6.4 330 49 true 1.7  51 19   true 1.5 60 13 true 1.8 88 17
jpf-regression/ExSymExe15_false.yml false 14   350 120 false 1.2  51 10   false 1.6 63 13 false 1.8 89 15
jpf-regression/ExSymExe15_true.yml true 6.4 330 54 true 1.6  51 21   true 1.6 63 15 true 1.9 87 18
jpf-regression/ExSymExe16_false.yml false 13   330 120 false 1.1  52 12   false 1.5 60 13 false 1.8 77 18
jpf-regression/ExSymExe16_true.yml true 6.1 320 51 true 1.6  51 17   true 1.6 61 13 true 1.7 79 14
jpf-regression/ExSymExe17_false.yml false 13   330 110 false 1.1  51 9.4 false 1.5 62 13 false 1.8 78 18
jpf-regression/ExSymExe17_true.yml true 5.2 300 49 true 1.7  51 17   true 1.6 59 15 true 1.8 78 15
jpf-regression/ExSymExe18_false.yml false 14   360 130 false 1.2  51 9.8 false 1.5 63 16 false 1.8 88 17
jpf-regression/ExSymExe18_true.yml true 6.4 310 57 true 1.6  51 17   true 1.6 59 14 true 1.7 77 15
jpf-regression/ExSymExe19_false.yml false 15   360 120 false 1.2  52 13   false 1.6 62 13 false 1.9 88 19
jpf-regression/ExSymExe19_true.yml true 6.9 330 65 true 1.7  51 16   true 1.6 63 16 true 2.5 130 23
jpf-regression/ExSymExe1_false.yml false 42   1100 260 false 1.2  53 11   false 1.5 63 15 false 2.2 120 21
jpf-regression/ExSymExe1_true.yml true 5.2 310 51 true 1.5  51 16   true 1.6 61 14 true 1.7 77 14
jpf-regression/ExSymExe20_false.yml false 23   480 210 false 1.2  52 10   false 1.7 63 13 false 3.5 180 38
jpf-regression/ExSymExe20_true.yml true 6.0 320 51 true 1.6  51 20   true 1.6 61 14 true 1.8 76 16
jpf-regression/ExSymExe21_false.yml false 17   420 140 false 1.1  51 11   false 1.6 61 14 false 2.4 120 21
jpf-regression/ExSymExe21_true.yml true 5.5 310 48 true 1.6  51 19   true 1.5 62 15 true 1.8 78 17
jpf-regression/ExSymExe25_false.yml false 15   350 130 false 1.0  51 9.1 false 1.5 61 14 false 1.8 95 17
jpf-regression/ExSymExe25_true.yml true 5.6 320 50 true 1.6  59 17   true 1.5 59 14 true 1.9 78 15
jpf-regression/ExSymExe26_false.yml false 21   410 170 false 1.2  53 12   false 1.5 62 14 false 2.4 140 23
jpf-regression/ExSymExe26_true.yml true 5.3 310 48 true 1.6  51 17   true 1.6 59 15 true 1.7 76 16
jpf-regression/ExSymExe27_false.yml false 14   340 110 false 1.1  51 11   false 1.6 60 16 false 1.8 89 14
jpf-regression/ExSymExe27_true.yml true 5.4 310 50 true 1.6  51 19   true 1.5 60 13 true 1.7 79 15
jpf-regression/ExSymExe28_false.yml false 14   340 110 false 1.1  51 8.6 false 1.5 61 14 false 2.0 94 17
jpf-regression/ExSymExe28_true.yml true 5.4 310 45 true 1.6  59 15   true 1.5 62 14 true 1.7 79 14
jpf-regression/ExSymExe29_false.yml false 40   1100 260 false 1.1  51 11   false 1.5 61 13 false 2.7 170 26
jpf-regression/ExSymExe29_true.yml true 5.3 310 49 true 1.6  51 19   true 1.6 62 16 true 1.7 75 15
jpf-regression/ExSymExe2_false.yml false 41   1200 280 false 1.1  51 9.9 false 1.7 61 16 false 2.1 130 20
jpf-regression/ExSymExe2_true.yml true 5.3 310 48 true 1.7  52 16   true 1.6 59 16 true 1.8 78 16
jpf-regression/ExSymExe3_false.yml false 15   340 120 false 1.1  51 10   false 1.5 63 14 false 1.9 90 17
jpf-regression/ExSymExe3_true.yml true 5.1 310 49 true 1.7  51 21   true 1.5 59 14 true 1.7 78 14
jpf-regression/ExSymExe4_false.yml false 38   1100 240 false 1.2  51 11   false 1.7 60 15 false 2.0 120 21
jpf-regression/ExSymExe4_true.yml true 5.2 310 53 true 1.6  51 16   true 1.6 59 14 true 1.8 80 14
jpf-regression/ExSymExe5_false.yml false 14   360 130 false 1.1  51 12   false 1.6 60 14 false 1.8 88 16
jpf-regression/ExSymExe5_true.yml true 5.2 310 47 true 1.6  51 18   true 1.6 62 15 true 1.7 80 15
jpf-regression/ExSymExe6_false.yml false 41   990 290 false 1.1  61 11   false 1.5 63 15 false 1.9 85 17
jpf-regression/ExSymExe6_true.yml true 6.0 340 52 true 1.6  51 19   true 1.6 62 13 true 1.7 78 14
jpf-regression/ExSymExe7_false.yml false 20   450 170 false 1.1  52 11   true 1.5 63 12 false 2.1 120 21
jpf-regression/ExSymExe7_true.yml true 8.7 340 75 true 1.7  51 19   true 1.5 62 14 true 2.1 120 18
jpf-regression/ExSymExe8_false.yml false 40   1100 280 false 1.1  51 12   false 1.6 61 15 false 2.3 130 21
jpf-regression/ExSymExe8_true.yml true 5.5 320 46 true 1.5  51 19   true 1.6 62 13 true 2.6 75 29
jpf-regression/ExSymExe9_false.yml false 14   330 130 false 1.1  51 9.7 false 1.5 61 12 false 1.8 78 16
jpf-regression/ExSymExe9_true.yml true 5.2 300 53 true 1.6  51 17   true 1.6 59 12 true 1.7 78 14
jpf-regression/ExSymExeArrays_false.yml false 20   490 150 false 1.1  51 11   false 1.5 59 13 false 1.8 77 17
jpf-regression/ExSymExeArrays_true.yml true 23   590 210 true 1.6  51 17   true 1.5 59 15 true 1.7 76 16
jpf-regression/ExSymExeBool_false.yml false 13   320 110 false 1.2  51 10   false 1.5 63 14 false 1.7 79 17
jpf-regression/ExSymExeBool_true.yml true 5.1 300 43 true 1.5  51 15   true 1.6 62 15 true 1.8 77 18
jpf-regression/ExSymExeComplexMath_false.yml unknown 14   420 120 false 1.1  52 10   false 1.7 59 15 false 1.9 77 16
jpf-regression/ExSymExeComplexMath_true.yml unknown 15   430 120 true 1.6  52 18   true 1.6 62 17 true 1.8 76 18
jpf-regression/ExSymExeD2I_false.yml unknown 16   440 120 false 1.0  51 9.3 false 1.5 60 15 false 1.7 75 15
jpf-regression/ExSymExeD2I_true.yml true 6.3 310 58 true 1.7  59 18   true 1.5 61 12 true 1.9 88 17
jpf-regression/ExSymExeD2L_false.yml unknown 21   550 170 false 1.0  51 8.9 false 1.5 60 13 false 1.9 89 17
jpf-regression/ExSymExeD2L_true.yml true 6.0 310 47 true 1.6  51 18   true 1.6 59 14 true 1.9 89 16
jpf-regression/ExSymExeF2I_false.yml unknown 15   450 130 false .99 51 9.1 false 1.5 62 13 false 1.8 77 18
jpf-regression/ExSymExeF2I_true.yml true 6.2 310 59 true 1.6  51 20   true 1.5 62 14 true 1.8 88 15
jpf-regression/ExSymExeF2L_false.yml unknown 48   1400 350 false 1.1  51 9.6 false 1.6 60 14 false 2.0 87 19
jpf-regression/ExSymExeF2L_true.yml true 6.5 320 58 true 1.7  51 20   true 1.6 61 15 true 2.0 89 20
jpf-regression/ExSymExeFNEG_false.yml unknown 18   470 150 false 1.1  51 12   false 1.5 61 14 false 1.8 86 16
jpf-regression/ExSymExeFNEG_true.yml unknown 18   480 160 true 1.6  51 20   true 1.6 59 14 true 1.9 93 17
jpf-regression/ExSymExeGetStatic_false.yml false 13   330 120 false 1.2  52 9.3 false 1.6 62 14 false 1.7 82 15
jpf-regression/ExSymExeGetStatic_true.yml true 5.2 300 50 true 1.6  51 15   true 1.5 62 14 true 1.8 80 16
jpf-regression/ExSymExeI2D_false.yml false 13   330 110 false 1.1  51 10   false 1.5 71 15 false 1.9 92 17
jpf-regression/ExSymExeI2D_true.yml true 6.4 330 54 true 1.7  51 15   true 1.5 60 14 true 2.8 130 28
jpf-regression/ExSymExeI2F_false.yml false 13   320 110 false 1.1  51 8.7 false 1.5 62 14 false 1.8 78 17
jpf-regression/ExSymExeI2F_true.yml true 6.3 320 59 true 1.6  52 16   true 1.5 61 13 true 1.7 81 14
jpf-regression/ExSymExeLCMP_false.yml false 13   320 100 false 1.0  51 9.6 false 1.6 63 13 false 1.8 87 15
jpf-regression/ExSymExeLCMP_true.yml true 5.6 310 42 true 1.6  51 17   true 1.6 60 14 true 2.1 92 18
jpf-regression/ExSymExeLongBytecodes_false.yml false 14   350 130 false 1.0  51 10   false 1.7 63 14 false 1.8 89 18
jpf-regression/ExSymExeLongBytecodes_true.yml true 7.1 330 60 true 1.8  52 18   true 1.6 63 14 true 1.9 89 17
jpf-regression/ExSymExeResearch_false.yml false 15   360 130 false 1.0  51 11   false 1.6 63 13 false 1.9 90 19
jpf-regression/ExSymExeResearch_true.yml true 7.3 350 65 true 1.6  51 17   true 1.6 59 14 true 1.9 90 18
jpf-regression/ExSymExeSimple_false.yml false 16   440 150 false 1.1  51 12   false 1.6 61 13 false 1.9 94 16
jpf-regression/ExSymExeSimple_true.yml true 6.5 320 57 true 1.7  51 19   true 1.6 63 14 true 1.8 87 17
jpf-regression/ExSymExeSuzette_false.yml false 15   370 130 false 1.0  51 9.3 false 1.6 62 14 false 2.0 95 15
jpf-regression/ExSymExeSuzette_true.yml true 6.5 320 51 true 1.6  51 18   true 1.5 61 14 true 1.9 93 17
jpf-regression/ExSymExeSwitch_false.yml false 9.8 320 89 false 1.0  51 11   false 1.5 62 15 false 2.0 95 16
jpf-regression/ExSymExeSwitch_true.yml true 5.5 310 46 true 1.6  51 16   true 1.6 62 14 true 1.9 89 16
jpf-regression/ExSymExeTestAssignments_false.yml false 9.8 310 91 false 1.0  51 10   false 1.6 63 15 false 1.9 86 17
jpf-regression/ExSymExeTestAssignments_true.yml true 4.7 290 46 true 1.5  51 16   true 1.5 60 15 true 1.9 91 16
jpf-regression/ExSymExeTestClassFields_false.yml false 13   320 110 false 1.1  59 11   true 1.6 60 15 false 1.8 90 16
jpf-regression/ExSymExeTestClassFields_true.yml true 5.2 310 51 true 1.6  51 15   true 1.5 60 14 true 1.9 88 15
jpf-regression/ExSymExe_false.yml false 13   330 100 false 1.2  52 11   false 1.6 61 15 false 1.8 79 15
jpf-regression/ExSymExe_true.yml true 5.5 320 50 true 1.6  53 16   true 1.6 59 14 true 1.8 76 15
jpf-regression/TestLazy_false.yml unknown 19   480 150 false 1.2  51 12   false 1.6 61 15 false 1.8 88 16
jpf-regression/TestLazy_true.yml unknown 18   460 150 true 1.7  51 20   true 1.5 64 15 true 1.8 95 18
MinePump/spec1-5_product1.yml timeout 900   3400 6600 false 5.3  93 61   false 2.1 72 19 false 2.3 100 20
MinePump/spec1-5_product10.yml timeout 900   3400 5700 false 5.3  94 58   false 1.7 64 16 false 2.1 81 19
MinePump/spec1-5_product11.yml timeout 900   3400 6500 false 130    560 1400   false 1.8 64 15 false 2.0 83 16
MinePump/spec1-5_product12.yml timeout 900   3500 6900 false 130    560 1500   false 1.9 65 20 false 1.9 82 16
MinePump/spec1-5_product13.yml timeout 900   3400 6700 false 5.5  93 72   false 1.8 64 15 false 2.1 86 17
MinePump/spec1-5_product14.yml timeout 900   3400 6200 false 5.4  92 66   false 1.9 64 16 false 2.2 88 19
MinePump/spec1-5_product15.yml timeout 900   3500 5800 false 150    600 1700   false 1.8 64 17 false 2.0 81 17
MinePump/spec1-5_product16.yml timeout 900   3400 6000 false 150    600 1700   false 1.8 63 16 false 2.0 87 19
MinePump/spec1-5_product17.yml timeout 900   3500 6500 false 5.4  93 63   false 1.7 65 17 false 2.1 82 18
MinePump/spec1-5_product18.yml timeout 900   3500 6800 false 5.4  92 64   false 1.9 63 16 false 2.1 78 16
MinePump/spec1-5_product19.yml timeout 910   3400 6500 false 150    590 1700   false 1.9 62 18 false 2.2 94 19
MinePump/spec1-5_product2.yml timeout 900   3400 6700 false 5.5  92 75   false 1.9 64 19 false 2.0 82 16
MinePump/spec1-5_product20.yml timeout 900   3500 6800 false 160    600 1800   false 1.8 62 15 false 2.1 90 16
MinePump/spec1-5_product21.yml timeout 910   3500 6500 false 5.6  95 65   false 1.7 63 14 false 2.0 82 20
MinePump/spec1-5_product22.yml timeout 900   3500 7000 false 5.6  94 68   false 1.7 62 16 false 1.9 82 18
MinePump/spec1-5_product23.yml timeout 900   3500 5900 false 180    650 1700   false 1.7 62 15 false 2.0 83 20
MinePump/spec1-5_product24.yml timeout 910   3500 6100 false 190    650 2100   false 1.8 64 15 false 1.9 84 17
MinePump/spec1-5_product25.yml timeout 900   3400 6300 false 5.3  92 64   false 1.7 64 17 false 2.0 82 20
MinePump/spec1-5_product26.yml timeout 900   3500 6200 false 5.6  92 75   false 1.9 64 18 false 1.9 81 17
MinePump/spec1-5_product27.yml timeout 910   3500 6400 false 150    600 1700   false 1.9 61 18 false 2.2 85 18
MinePump/spec1-5_product28.yml timeout 910   3400 7200 false 150    600 1800   false 1.7 61 18 false 2.1 81 16
MinePump/spec1-5_product29.yml timeout 910   3400 6100 false 5.4  93 65   false 2.0 62 16 false 2.1 88 21
MinePump/spec1-5_product3.yml timeout 900   3400 6700 false 130    550 1600   false 1.7 64 14 false 1.9 82 18
MinePump/spec1-5_product30.yml timeout 900   3500 5700 false 5.5  94 65   false 1.8 66 15 false 2.2 84 21
MinePump/spec1-5_product31.yml timeout 910   3500 6100 false 170    650 2000   false 2.1 66 19 false 2.2 82 21
MinePump/spec1-5_product32.yml timeout 900   3400 6500 false 180    650 1700   false 1.7 62 16 false 2.0 81 19
MinePump/spec1-5_product33.yml timeout 900   3500 6200 false 120    540 1300   false 1.8 61 17 false 1.9 84 20
MinePump/spec1-5_product34.yml timeout 900   3400 6200 false 120    540 1400   false 1.9 64 18 false 2.0 85 20
MinePump/spec1-5_product35.yml timeout 900   3400 6000 false 160    600 1700   false 1.8 61 15 false 2.0 82 18
MinePump/spec1-5_product36.yml timeout 910   3500 5600 false 160    610 1800   false 1.8 62 17 false 2.2 87 17
MinePump/spec1-5_product37.yml timeout 910   3400 6000 false 130    590 1600   false 1.7 62 15 false 2.1 83 21
MinePump/spec1-5_product38.yml timeout 910   3500 6700 false 140    580 1800   false 1.7 64 15 false 2.1 80 19
MinePump/spec1-5_product39.yml timeout 910   3500 7100 false 180    650 1600   false 1.7 62 17 false 1.9 78 18
MinePump/spec1-5_product4.yml timeout 900   3400 6400 false 130    570 1600   false 1.7 64 15 false 2.3 82 20
MinePump/spec1-5_product40.yml timeout 910   3400 6300 false 180    660 1800   false 1.7 61 16 false 2.0 84 17
MinePump/spec1-5_product41.yml timeout 910   3500 5800 false 120    560 1400   false 1.9 63 16 false 2.0 83 17
MinePump/spec1-5_product42.yml timeout 900   3400 6500 false 130    570 1400   false 1.9 64 17 false 2.1 82 18
MinePump/spec1-5_product43.yml timeout 900   3400 6800 false 160    640 2600   false 1.8 61 15 false 2.2 84 18
MinePump/spec1-5_product44.yml timeout 900   3400 6900 false 180    640 2000   false 1.7 65 16 false 2.0 90 18
MinePump/spec1-5_product45.yml timeout 900   3500 7100 false 150    600 2000   false 1.7 62 16 false 1.9 89 17
MinePump/spec1-5_product46.yml timeout 910   3500 7400 false 150    600 1700   false 1.7 65 13 false 2.2 80 17
MinePump/spec1-5_product47.yml timeout 900   3500 6600 false 200    690 2800   false 2.0 61 16 false 2.0 82 16
MinePump/spec1-5_product48.yml timeout 900   3400 6500 false 210    690 2700   false 1.7 65 18 false 2.0 83 19
MinePump/spec1-5_product49.yml timeout 900   3500 6500 false 130    580 1400   false 1.9 64 19 false 2.0 83 17
MinePump/spec1-5_product5.yml timeout 900   3400 6500 false 5.3  92 60   false 1.8 63 16 false 1.9 88 17
MinePump/spec1-5_product50.yml timeout 910   3500 6600 false 140    580 1600   false 1.8 62 15 false 2.2 81 20
MinePump/spec1-5_product51.yml timeout 910   3500 5800 false 180    650 1900   false 1.8 61 15 false 2.0 81 17
MinePump/spec1-5_product52.yml timeout 900   3400 6000 false 190    660 2100   false 1.7 62 16 false 2.2 83 17
MinePump/spec1-5_product53.yml timeout 900   3500 6400 false 160    620 2400   false 1.8 64 17 false 2.0 80 17
MinePump/spec1-5_product54.yml timeout 900   3400 6200 false 160    620 2200   false 1.8 62 17 false 1.9 81 18
MinePump/spec1-5_product55.yml timeout 910   3400 6000 false 230    710 2800   false 1.8 65 16 false 2.1 81 19
MinePump/spec1-5_product56.yml timeout 910   3400 6100 false 230    710 3100   false 1.7 62 16 false 2.0 83 14
MinePump/spec1-5_product57.yml timeout 910   3400 6000 true 250    610 2800   true 2.8 110 26 true 3.8 220 33
MinePump/spec1-5_product58.yml timeout 910   3500 5900 true 250    620 3000   true 2.4 90 21 true 4.1 210 38
MinePump/spec1-5_product59.yml timeout 900   3400 5100 true 340    700 3800   true 2.7 93 23 true 3.3 190 32
MinePump/spec1-5_product6.yml timeout 900   3400 5800 false 5.4  92 76   false 1.9 63 17 false 2.0 82 17
MinePump/spec1-5_product60.yml timeout 900   3300 6800 true 360    710 3900   true 2.4 91 21 true 3.7 210 30
MinePump/spec1-5_product61.yml timeout 900   3500 6400 true 310    650 3900   true 2.2 88 21 true 3.6 210 29
MinePump/spec1-5_product62.yml timeout 910   3400 6400 true 310    650 3900   true 2.4 90 23 true 3.5 200 29
MinePump/spec1-5_product63.yml timeout 910   3400 6900 true 450    750 4700   true 2.5 92 22 true 3.5 190 30
MinePump/spec1-5_product64.yml timeout 910   3400 6500 true 460    760 4800   true 2.7 90 24 true 3.8 210 35
MinePump/spec1-5_product7.yml timeout 910   3500 6400 false 150    590 1700   false 1.8 65 17 false 2.1 82 19
MinePump/spec1-5_product8.yml timeout 910   3500 7000 false 150    590 1700   false 1.8 64 16 false 2.0 82 17
MinePump/spec1-5_product9.yml timeout 900   3400 6800 false 5.2  91 67   false 1.7 64 14 false 1.9 83 16
../sv-benchmarks/java/ status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J) status cpu (s) mem (MB) energy (J)
total 368 96000   480000 830000 368 28000 140000 280000 368 8800   33000 41000 368 1300   34000 13000
    correct results 186 2100   72000 18000 331 9700 47000 110000 331 550   21000 4900 337 970   31000 9900
        correct true 109 800   37000 7100 139 3100 14000 36000 151 250   9600 2300 156 620   15000 6800
        correct false 77 1300   34000 11000 192 6600 33000 77000 180 300   11000 2700 181 350   16000 3100
    incorrect results 2 120   2800 1100 0 6 9.5 370 83 6 11   530 100
        incorrect true 1 120   2500 990 0 6 9.5 370 83 2 4.2 180 37
        incorrect false 1 7.6 300 75 0 0 4 7.2 340 64
Run set jayhorn.sv-comp19_prop-reachsafety_java.ReachSafety-Java jbmc.sv-comp19_prop-reachsafety_java.ReachSafety-Java jpf.sv-comp19_prop-reachsafety_java.ReachSafety-Java spf.sv-comp19_prop-reachsafety_java.ReachSafety-Java