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