Tool 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-07 20:12:45 CET
Run set sv-comp19_prop-reachsafety_java.ReachSafety-Java
sv-benchmarks/java/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB)
jayhorn-recursive/Ackermann01.yml 1 2.1 .81 95 18 .070 .020 
jayhorn-recursive/Addition.yml 2 2.0 .84 90 19 .070 0     
jayhorn-recursive/InfiniteLoop.yml 1 1.8 .71 79 16 .070 0     
jayhorn-recursive/SatAckermann01.yml 2 7.1 4.0  250 69 .070 0     
jayhorn-recursive/SatAckermann02.yml 2 6.9 4.0  240 70 .070 0     
jayhorn-recursive/SatAckermann03.yml 2 7.3 4.0  260 77 .070 0     
jayhorn-recursive/SatAddition01.yml 2 2.1 .89 100 20 .070 0     
jayhorn-recursive/SatEvenOdd01.yml 2 2.1 .83 95 18 .070 0     
jayhorn-recursive/SatFibonacci01.yml 2 2.8 1.1  150 26 .070 0     
jayhorn-recursive/SatFibonacci02.yml 2 1.9 .80 78 15 .070 .020 
jayhorn-recursive/SatFibonacci03.yml 2 2.8 1.1  150 26 .070 0     
jayhorn-recursive/SatGcd.yml 2 65   64    110 930 .041 0     
jayhorn-recursive/SatHanoi01.yml 2 4.9 2.0  260 40 .070 0     
jayhorn-recursive/SatMccarthy91.yml 2 43   39    390 520 .041 0     
jayhorn-recursive/SatMultCommutative01.yml 2 2.3 1.0  100 21 .074 0     
jayhorn-recursive/SatPrimes01.yml 0 230   170    570 2400 .033 0     
jayhorn-recursive/UnsatAckermann01.yml 1 1.8 .73 89 17 .070 0     
jayhorn-recursive/UnsatAddition01.yml 1 1.8 .73 88 16 .070 0     
jayhorn-recursive/UnsatAddition02.yml -32 2.4 .98 100 21 .070 0     
jayhorn-recursive/UnsatEvenOdd01.yml 1 1.9 .78 94 18 .070 0     
jayhorn-recursive/UnsatFibonacci01.yml 1 1.9 .78 91 19 .070 .020 
jayhorn-recursive/UnsatFibonacci02.yml 1 2.3 .96 110 21 .070 0     
jayhorn-recursive/UnsatMccarthy91.yml 1 1.8 .77 90 17 .070 .020 
jbmc-regression/ArithmeticException1.yml 1 1.9 .78 87 17 .070 .045 
jbmc-regression/ArithmeticException5.yml 2 1.8 .74 77 12 .070 .045 
jbmc-regression/ArithmeticException6.yml 1 1.9 .79 88 15 .070 .045 
jbmc-regression/ArrayIndexOutOfBoundsException1.yml 1 1.9 .77 89 15 .070 .13  
jbmc-regression/ArrayIndexOutOfBoundsException2.yml 1 1.9 .76 89 18 .070 0     
jbmc-regression/ArrayIndexOutOfBoundsException3.yml 1 1.9 .77 91 17 .070 0     
jbmc-regression/BufferedReaderReadLine.yml 1 1.9 .74 88 18 .070 .016 
jbmc-regression/CharSequenceBug.yml 1 1.9 .77 87 16 .070 0     
jbmc-regression/CharSequenceToString.yml -16 1.9 .76 95 18 .070 0     
jbmc-regression/ClassCastException1.yml 1 1.7 .69 81 16 .070 .029 
jbmc-regression/ClassCastException2.yml 2 1.7 .71 76 16 .070 .012 
jbmc-regression/ClassCastException3.yml 1 1.8 .73 78 17 .070 0     
jbmc-regression/Class_method1.yml 2 1.8 .74 76 16 .070 0     
jbmc-regression/Inheritance1.yml 2 1.7 .69 75 15 .070 0     
jbmc-regression/NegativeArraySizeException1.yml 1 1.8 .73 81 16 .070 0     
jbmc-regression/NegativeArraySizeException2.yml 1 1.9 .82 78 15 .070 0     
jbmc-regression/NullPointerException1.yml 2 1.8 .72 79 15 .070 0     
jbmc-regression/NullPointerException2.yml 1 1.9 .74 79 15 .070 0     
jbmc-regression/NullPointerException3.yml 1 1.7 .72 78 16 .070 0     
jbmc-regression/NullPointerException4.yml 1 1.8 .74 80 15 .070 0     
jbmc-regression/RegexMatches01.yml 2 1.8 .72 77 17 .070 .029 
jbmc-regression/RegexMatches02.yml -32 1.8 .75 80 16 .070 .029 
jbmc-regression/RegexSubstitution01.yml 2 2.0 .78 80 19 .070 .041 
jbmc-regression/RegexSubstitution02.yml 0 1.9 .76 79 18 .070 .041 
jbmc-regression/RegexSubstitution03.yml 2 1.8 .73 79 16 .070 .041 
jbmc-regression/StaticCharMethods01.yml 2 1.7 .72 78 15 .070 0     
jbmc-regression/StaticCharMethods02.yml 1 1.9 .75 91 16 .070 0     
jbmc-regression/StaticCharMethods03.yml 1 1.8 .77 87 17 .070 0     
jbmc-regression/StaticCharMethods04.yml 1 1.7 .68 81 15 .070 .020 
jbmc-regression/StaticCharMethods05.yml 0 1.8 .73 80 14 .070 0     
jbmc-regression/StaticCharMethods06.yml 2 1.9 .75 87 16 .070 0     
jbmc-regression/StringBuilderAppend01.yml 2 1.8 .71 81 15 .070 0     
jbmc-regression/StringBuilderAppend02.yml 0 2.0 .83 80 18 .070 .057 
jbmc-regression/StringBuilderCapLen01.yml 2 1.8 .72 79 17 .070 0     
jbmc-regression/StringBuilderCapLen02.yml 1 1.9 .76 87 15 .070 0     
jbmc-regression/StringBuilderCapLen03.yml 0 1.8 .73 79 14 .070 0     
jbmc-regression/StringBuilderCapLen04.yml 0 1.7 .71 81 15 .070 0     
jbmc-regression/StringBuilderChars01.yml 2 1.9 .73 77 15 .070 0     
jbmc-regression/StringBuilderChars02.yml 1 1.8 .72 83 16 .070 0     
jbmc-regression/StringBuilderChars03.yml 0 1.7 .69 77 15 .070 0     
jbmc-regression/StringBuilderChars04.yml 0 1.9 .72 80 18 .070 0     
jbmc-regression/StringBuilderChars05.yml 0 1.7 .70 79 14 .070 0     
jbmc-regression/StringBuilderChars06.yml 0 1.8 .71 81 16 .070 0     
jbmc-regression/StringBuilderConstructors01.yml 0 1.9 .75 95 17 .070 0     
jbmc-regression/StringBuilderConstructors02.yml 0 1.8 .70 80 15 .070 0     
jbmc-regression/StringBuilderInsertDelete01.yml 2 1.8 .73 82 16 .070 0     
jbmc-regression/StringBuilderInsertDelete02.yml 0 1.9 .76 80 18 .070 0     
jbmc-regression/StringBuilderInsertDelete03.yml 0 1.8 .73 82 17 .070 0     
jbmc-regression/StringCompare01.yml 2 1.8 .73 76 17 .070 0     
jbmc-regression/StringCompare02.yml 0 1.7 .71 80 15 .070 0     
jbmc-regression/StringCompare03.yml 0 1.7 .71 79 17 .070 .020 
jbmc-regression/StringCompare04.yml 0 1.8 .75 80 16 .070 0     
jbmc-regression/StringCompare05.yml 1 1.8 .73 80 17 .070 0     
jbmc-regression/StringConcatenation01.yml -16 1.8 .71 82 15 .070 0     
jbmc-regression/StringConcatenation02.yml 1 1.8 .77 83 19 .070 0     
jbmc-regression/StringConcatenation03.yml 1 1.9 .80 81 16 .070 .14  
jbmc-regression/StringConcatenation04.yml 1 1.8 .75 83 15 .070 .070 
jbmc-regression/StringConstructors01.yml 2 1.8 .75 79 15 .070 0     
jbmc-regression/StringConstructors02.yml 1 1.8 .74 83 16 .070 0     
jbmc-regression/StringConstructors03.yml 1 1.8 .75 85 17 .070 0     
jbmc-regression/StringConstructors04.yml 1 1.8 .75 84 18 .070 .020 
jbmc-regression/StringConstructors05.yml 1 1.9 .72 89 16 .070 0     
jbmc-regression/StringContains01.yml 1 1.8 .73 86 15 .070 0     
jbmc-regression/StringContains02.yml 1 1.8 .74 82 16 .070 0     
jbmc-regression/StringIndexMethods01.yml 2 1.7 .71 79 14 .070 0     
jbmc-regression/StringIndexMethods02.yml 1 1.9 .78 92 18 .070 .020 
jbmc-regression/StringIndexMethods03.yml 1 2.0 .81 91 20 .070 0     
jbmc-regression/StringIndexMethods04.yml 1 1.8 .77 90 18 .070 0     
jbmc-regression/StringIndexMethods05.yml 1 1.8 .73 88 16 .070 0     
jbmc-regression/StringMiscellaneous01.yml 0 1.9 .75 78 18 .070 .020 
jbmc-regression/StringMiscellaneous02.yml 1 2.0 .81 94 17 .070 0     
jbmc-regression/StringMiscellaneous03.yml 1 2.0 .82 92 16 .070 0     
jbmc-regression/StringMiscellaneous04.yml 2 1.9 .74 77 16 .070 .020 
jbmc-regression/StringStartEnd01.yml 2 1.7 .69 78 14 .070 0     
jbmc-regression/StringStartEnd02.yml 1 1.9 .72 84 18 .070 0     
jbmc-regression/StringStartEnd03.yml 1 1.9 .77 87 18 .070 0     
jbmc-regression/StringValueOf01.yml 2 1.9 .81 81 17 .070 0     
jbmc-regression/StringValueOf02.yml 1 1.9 .75 80 15 .070 0     
jbmc-regression/StringValueOf03.yml 1 1.8 .74 79 14 .070 0     
jbmc-regression/StringValueOf04.yml 1 1.8 .74 78 16 .070 .020 
jbmc-regression/StringValueOf05.yml 0 1.9 .75 94 16 .070 0     
jbmc-regression/StringValueOf06.yml 1 1.9 .76 82 17 .070 0     
jbmc-regression/StringValueOf07.yml 0 1.9 .78 81 17 .070 .041 
jbmc-regression/StringValueOf08.yml 0 1.8 .78 80 16 .070 .016 
jbmc-regression/StringValueOf09.yml 0 1.7 .69 86 14 .070 .012 
jbmc-regression/StringValueOf10.yml 1 1.9 .75 86 16 .070 0     
jbmc-regression/SubString01.yml 2 1.7 .73 79 17 .070 0     
jbmc-regression/SubString02.yml 1 1.9 .74 88 16 .070 0     
jbmc-regression/SubString03.yml 1 1.9 .79 84 16 .070 0     
jbmc-regression/TokenTest01.yml 2 1.9 .76 79 18 .070 .029 
jbmc-regression/TokenTest02.yml 0 1.8 .73 80 15 .070 .0041
jbmc-regression/Validate01.yml 2 1.7 .70 78 16 .070 0     
jbmc-regression/Validate02.yml 0 2.0 .77 82 17 .070 .020 
jbmc-regression/aastore_aaload1.yml 2 120   120    140 1600 .033 0     
jbmc-regression/array1.yml 2 2.0 .85 91 17 .070 0     
jbmc-regression/array2.yml 2 2.0 .78 94 18 .070 0     
jbmc-regression/arraylength1.yml 2 1.9 .76 90 17 .070 0     
jbmc-regression/arrayread1.yml 2 1.7 .74 87 15 .070 0     
jbmc-regression/assert1.yml 2 1.9 .75 89 18 .070 0     
jbmc-regression/assert2.yml 1 2.0 .82 94 17 .070 0     
jbmc-regression/assert3.yml 1 1.8 .74 86 15 .070 0     
jbmc-regression/assert4.yml 1 2.0 .79 94 20 .070 0     
jbmc-regression/assert5.yml 2 1.9 .75 89 16 .070 0     
jbmc-regression/assert6.yml 2 1.8 .76 89 16 .070 0     
jbmc-regression/astore_aload1.yml 2 1.8 .75 79 15 .070 0     
jbmc-regression/athrow1.yml 1 1.9 .80 78 18 .070 .033 
jbmc-regression/basic1.yml 2 1.8 .74 78 16 .070 .016 
jbmc-regression/bitwise1.yml 2 2.0 .81 93 19 .070 0     
jbmc-regression/boolean1.yml 2 1.8 .74 79 16 .070 0     
jbmc-regression/boolean2.yml 2 1.8 .72 78 17 .070 0     
jbmc-regression/bug-test-gen-095.yml 1 1.9 .79 83 17 .070 0     
jbmc-regression/bug-test-gen-119-2.yml 2 1.8 .74 77 17 .070 0     
jbmc-regression/bug-test-gen-119.yml 2 1.9 .75 82 15 .070 0     
jbmc-regression/calc.yml 2 32   31    130 400 .070 0     
jbmc-regression/cast1.yml -16 1.9 .77 87 16 .070 0     
jbmc-regression/catch1.yml 2 1.7 .72 78 16 .070 0     
jbmc-regression/char1.yml 2 2.1 .86 92 18 .070 .020 
jbmc-regression/charArray.yml 0 1.9 .79 89 19 .070 0     
jbmc-regression/classtest1.yml 2 1.7 .71 77 15 .070 0     
jbmc-regression/const1.yml 2 1.7 .70 78 13 .070 0     
jbmc-regression/constructor1.yml 2 1.8 .71 79 15 .070 0     
jbmc-regression/enum1.yml 2 1.7 .70 76 15 .070 0     
jbmc-regression/exceptions1.yml 1 1.8 .71 80 15 .070 0     
jbmc-regression/exceptions10.yml 1 1.8 .71 79 16 .070 0     
jbmc-regression/exceptions11.yml 1 1.7 .70 80 14 .070 .016 
jbmc-regression/exceptions12.yml 1 1.7 .70 78 15 .070 .016 
jbmc-regression/exceptions13.yml 1 1.7 .73 78 18 .070 .012 
jbmc-regression/exceptions14.yml 2 1.7 .70 81 16 .070 .012 
jbmc-regression/exceptions15.yml 2 1.8 .71 80 15 .070 .098 
jbmc-regression/exceptions16.yml 1 1.8 .74 83 15 .070 0     
jbmc-regression/exceptions18.yml 2 1.7 .70 79 17 .070 0     
jbmc-regression/exceptions2.yml 1 1.8 .76 79 15 .070 .016 
jbmc-regression/exceptions3.yml 1 1.7 .72 78 15 .070 0     
jbmc-regression/exceptions4.yml 2 1.8 .76 78 17 .070 0     
jbmc-regression/exceptions5.yml 2 1.8 .74 76 16 .070 .012 
jbmc-regression/exceptions6.yml 1 1.8 .74 77 16 .070 0     
jbmc-regression/exceptions7.yml 1 1.7 .71 76 16 .070 .016 
jbmc-regression/exceptions8.yml 1 1.8 .72 79 18 .070 .016 
jbmc-regression/exceptions9.yml 2 1.8 .70 78 15 .070 0     
jbmc-regression/fcmpx_dcmpx1.yml 2 1.7 .70 78 16 .070 0     
jbmc-regression/iarith1.yml 2 1.9 .75 79 14 .070 0     
jbmc-regression/iarith2.yml 2 1.8 .72 78 18 .070 0     
jbmc-regression/if_acmp1.yml 2 1.9 .74 78 16 .070 0     
jbmc-regression/if_expr1.yml 2 1.8 .74 89 15 .070 0     
jbmc-regression/if_icmp1.yml 2 2.1 .83 92 16 .070 0     
jbmc-regression/ifxx1.yml 2 2.0 .78 79 14 .070 0     
jbmc-regression/instanceof1.yml -16 1.7 .71 79 15 .070 0     
jbmc-regression/instanceof2.yml 2 1.8 .74 77 15 .070 0     
jbmc-regression/instanceof3.yml 2 1.9 .78 78 16 .070 0     
jbmc-regression/instanceof4.yml 2 1.7 .69 76 16 .070 0     
jbmc-regression/instanceof5.yml 2 1.6 .68 78 17 .070 0     
jbmc-regression/instanceof6.yml 2 1.7 .69 79 14 .070 0     
jbmc-regression/instanceof7.yml 2 1.7 .69 77 13 .070 .020 
jbmc-regression/instanceof8.yml 2 1.8 .71 79 16 .070 0     
jbmc-regression/interface1.yml 1 1.7 .71 80 14 .070 0     
jbmc-regression/java_append_char.yml 1 1.8 .73 81 16 .070 0     
jbmc-regression/lazyloading4.yml 2 1.8 .74 79 15 .070 0     
jbmc-regression/list1.yml 2 42   34    260 490 .71  0     
jbmc-regression/long1.yml 2 1.8 .74 78 18 .070 0     
jbmc-regression/lookupswitch1.yml 2 1.8 .74 87 15 .070 0     
jbmc-regression/multinewarray.yml 2 1.8 .73 77 16 .070 0     
jbmc-regression/overloading1.yml 2 1.7 .75 74 17 .070 0     
jbmc-regression/package1.yml 2 1.7 .73 76 17 .070 0     
jbmc-regression/putfield_getfield1.yml 2 1.7 .69 77 15 .070 0     
jbmc-regression/putstatic_getstatic1.yml 2 1.7 .73 76 16 .070 0     
jbmc-regression/recursion2.yml 2 1.7 .70 74 14 .070 0     
jbmc-regression/return1.yml 1 1.9 .79 79 18 .070 .020 
jbmc-regression/return2.yml 1 1.8 .75 87 17 .070 0     
jbmc-regression/store_load1.yml 2 1.7 .72 78 14 .070 .020 
jbmc-regression/swap1.yml 2 1.7 .72 76 13 .070 0     
jbmc-regression/synchronized.yml 2 1.7 .69 78 15 .070 0     
jbmc-regression/tableswitch1.yml 2 1.9 .79 90 15 .070 .020 
jbmc-regression/uninitialised1.yml 2 1.8 .74 77 15 .070 0     
jbmc-regression/virtual1.yml 2 1.7 .70 80 15 .070 0     
jbmc-regression/virtual2.yml 1 1.8 .71 79 15 .070 0     
jbmc-regression/virtual4.yml 2 1.7 .71 78 15 .070 0     
jbmc-regression/virtual_function_unwinding.yml 2 1.8 .71 77 15 .070 0     
jpf-regression/ExDarko_false.yml 1 2.0 .80 95 18 .070 0     
jpf-regression/ExDarko_true.yml 2 2.0 .80 92 19 .070 0     
jpf-regression/ExException_false.yml 1 1.9 .77 92 18 .070 .020 
jpf-regression/ExException_true.yml 2 1.9 .73 79 17 .070 0     
jpf-regression/ExGenSymExe_false.yml 1 2.0 .76 77 25 .070 0     
jpf-regression/ExGenSymExe_true.yml 2 1.8 .72 79 16 .070 0     
jpf-regression/ExLazy_false.yml 1 1.8 .73 87 14 .070 .11  
jpf-regression/ExLazy_true.yml 2 1.9 .78 94 18 .070 0     
jpf-regression/ExMIT_false.yml 1 1.9 .77 88 15 .070 0     
jpf-regression/ExMIT_true.yml 2 1.9 .80 91 18 .070 0     
jpf-regression/ExSymExe10_false.yml 1 1.8 .74 88 18 .070 0     
jpf-regression/ExSymExe10_true.yml 2 1.9 .79 90 15 .070 0     
jpf-regression/ExSymExe11_false.yml 1 1.8 .73 80 15 .070 .16  
jpf-regression/ExSymExe11_true.yml 2 1.8 .75 85 15 .070 0     
jpf-regression/ExSymExe12_false.yml 1 2.0 .80 96 17 .070 0     
jpf-regression/ExSymExe12_true.yml 2 1.9 .80 85 16 .070 0     
jpf-regression/ExSymExe13_false.yml 1 2.0 .80 89 18 .070 0     
jpf-regression/ExSymExe13_true.yml 2 1.9 .79 92 19 .070 0     
jpf-regression/ExSymExe14_false.yml 1 2.0 .78 86 17 .070 .020 
jpf-regression/ExSymExe14_true.yml 2 1.8 .74 88 17 .070 0     
jpf-regression/ExSymExe15_false.yml 1 1.8 .76 89 15 .070 .16  
jpf-regression/ExSymExe15_true.yml 2 1.9 .78 87 18 .070 0     
jpf-regression/ExSymExe16_false.yml 1 1.8 .74 77 18 .070 0     
jpf-regression/ExSymExe16_true.yml 2 1.7 .72 79 14 .070 0     
jpf-regression/ExSymExe17_false.yml 1 1.8 .73 78 18 .070 0     
jpf-regression/ExSymExe17_true.yml 2 1.8 .72 78 15 .070 0     
jpf-regression/ExSymExe18_false.yml 1 1.8 .76 88 17 .070 0     
jpf-regression/ExSymExe18_true.yml 2 1.7 .71 77 15 .070 0     
jpf-regression/ExSymExe19_false.yml 1 1.9 .80 88 19 .070 0     
jpf-regression/ExSymExe19_true.yml 2 2.5 1.4  130 23 .070 0     
jpf-regression/ExSymExe1_false.yml 1 2.2 1.1  120 21 .070 0     
jpf-regression/ExSymExe1_true.yml 2 1.7 .73 77 14 .070 0     
jpf-regression/ExSymExe20_false.yml 1 3.5 2.1  180 38 .070 0     
jpf-regression/ExSymExe20_true.yml 2 1.8 .69 76 16 .070 0     
jpf-regression/ExSymExe21_false.yml 1 2.4 1.2  120 21 .070 0     
jpf-regression/ExSymExe21_true.yml 2 1.8 .72 78 17 .070 0     
jpf-regression/ExSymExe25_false.yml 1 1.8 .75 95 17 .070 0     
jpf-regression/ExSymExe25_true.yml 2 1.9 .77 78 15 .070 0     
jpf-regression/ExSymExe26_false.yml 1 2.4 1.0  140 23 .070 0     
jpf-regression/ExSymExe26_true.yml 2 1.7 .71 76 16 .070 .066 
jpf-regression/ExSymExe27_false.yml 1 1.8 .77 89 14 .070 0     
jpf-regression/ExSymExe27_true.yml 2 1.7 .70 79 15 .070 0     
jpf-regression/ExSymExe28_false.yml 1 2.0 .78 94 17 .070 0     
jpf-regression/ExSymExe28_true.yml 2 1.7 .69 79 14 .070 0     
jpf-regression/ExSymExe29_false.yml 1 2.7 1.6  170 26 .070 0     
jpf-regression/ExSymExe29_true.yml 2 1.7 .71 75 15 .070 0     
jpf-regression/ExSymExe2_false.yml 1 2.1 .98 130 20 .070 0     
jpf-regression/ExSymExe2_true.yml 2 1.8 .73 78 16 .070 0     
jpf-regression/ExSymExe3_false.yml 1 1.9 .79 90 17 .070 0     
jpf-regression/ExSymExe3_true.yml 2 1.7 .70 78 14 .070 .020 
jpf-regression/ExSymExe4_false.yml 1 2.0 .95 120 21 .070 0     
jpf-regression/ExSymExe4_true.yml 2 1.8 .73 80 14 .070 0     
jpf-regression/ExSymExe5_false.yml 1 1.8 .75 88 16 .070 0     
jpf-regression/ExSymExe5_true.yml 2 1.7 .73 80 15 .070 0     
jpf-regression/ExSymExe6_false.yml 1 1.9 .75 85 17 .070 0     
jpf-regression/ExSymExe6_true.yml 2 1.7 .71 78 14 .070 0     
jpf-regression/ExSymExe7_false.yml 1 2.1 .94 120 21 .070 0     
jpf-regression/ExSymExe7_true.yml 2 2.1 .95 120 18 .070 0     
jpf-regression/ExSymExe8_false.yml 1 2.3 1.1  130 21 .070 .16  
jpf-regression/ExSymExe8_true.yml 2 2.6 1.2  75 29 .070 0     
jpf-regression/ExSymExe9_false.yml 1 1.8 .74 78 16 .070 0     
jpf-regression/ExSymExe9_true.yml 2 1.7 .70 78 14 .070 0     
jpf-regression/ExSymExeArrays_false.yml 1 1.8 .72 77 17 .070 0     
jpf-regression/ExSymExeArrays_true.yml 2 1.7 .72 76 16 .070 .020 
jpf-regression/ExSymExeBool_false.yml 1 1.7 .70 79 17 .070 0     
jpf-regression/ExSymExeBool_true.yml 2 1.8 .71 77 18 .070 .16  
jpf-regression/ExSymExeComplexMath_false.yml 1 1.9 .74 77 16 .070 0     
jpf-regression/ExSymExeComplexMath_true.yml 2 1.8 .71 76 18 .070 0     
jpf-regression/ExSymExeD2I_false.yml 1 1.7 .69 75 15 .070 0     
jpf-regression/ExSymExeD2I_true.yml 2 1.9 .80 88 17 .070 0     
jpf-regression/ExSymExeD2L_false.yml 1 1.9 .79 89 17 .070 0     
jpf-regression/ExSymExeD2L_true.yml 2 1.9 .80 89 16 .070 0     
jpf-regression/ExSymExeF2I_false.yml 1 1.8 .73 77 18 .070 .11  
jpf-regression/ExSymExeF2I_true.yml 2 1.8 .77 88 15 .070 0     
jpf-regression/ExSymExeF2L_false.yml 1 2.0 .81 87 19 .070 0     
jpf-regression/ExSymExeF2L_true.yml 2 2.0 .81 89 20 .070 0     
jpf-regression/ExSymExeFNEG_false.yml 1 1.8 .73 86 16 .070 0     
jpf-regression/ExSymExeFNEG_true.yml 2 1.9 .77 93 17 .070 0     
jpf-regression/ExSymExeGetStatic_false.yml 1 1.7 .70 82 15 .070 0     
jpf-regression/ExSymExeGetStatic_true.yml 2 1.8 .72 80 16 .070 0     
jpf-regression/ExSymExeI2D_false.yml 1 1.9 .78 92 17 .070 0     
jpf-regression/ExSymExeI2D_true.yml 2 2.8 1.7  130 28 .070 0     
jpf-regression/ExSymExeI2F_false.yml 1 1.8 .77 78 17 .070 0     
jpf-regression/ExSymExeI2F_true.yml 2 1.7 .71 81 14 .070 0     
jpf-regression/ExSymExeLCMP_false.yml 1 1.8 .76 87 15 .070 0     
jpf-regression/ExSymExeLCMP_true.yml 2 2.1 .84 92 18 .070 0     
jpf-regression/ExSymExeLongBytecodes_false.yml 1 1.8 .73 89 18 .070 0     
jpf-regression/ExSymExeLongBytecodes_true.yml 2 1.9 .78 89 17 .070 0     
jpf-regression/ExSymExeResearch_false.yml 1 1.9 .78 90 19 .070 0     
jpf-regression/ExSymExeResearch_true.yml 2 1.9 .81 90 18 .070 0     
jpf-regression/ExSymExeSimple_false.yml 1 1.9 .76 94 16 .070 0     
jpf-regression/ExSymExeSimple_true.yml 2 1.8 .76 87 17 .070 0     
jpf-regression/ExSymExeSuzette_false.yml 1 2.0 .82 95 15 .070 0     
jpf-regression/ExSymExeSuzette_true.yml 2 1.9 .77 93 17 .070 .041 
jpf-regression/ExSymExeSwitch_false.yml 1 2.0 .78 95 16 .070 0     
jpf-regression/ExSymExeSwitch_true.yml 2 1.9 .75 89 16 .070 0     
jpf-regression/ExSymExeTestAssignments_false.yml 1 1.9 .76 86 17 .070 0     
jpf-regression/ExSymExeTestAssignments_true.yml 2 1.9 .79 91 16 .070 0     
jpf-regression/ExSymExeTestClassFields_false.yml 1 1.8 .77 90 16 .070 0     
jpf-regression/ExSymExeTestClassFields_true.yml 2 1.9 .76 88 15 .070 0     
jpf-regression/ExSymExe_false.yml 1 1.8 .72 79 15 .070 0     
jpf-regression/ExSymExe_true.yml 2 1.8 .73 76 15 .070 0     
jpf-regression/TestLazy_false.yml 1 1.8 .76 88 16 .070 0     
jpf-regression/TestLazy_true.yml 2 1.8 .76 95 18 .070 0     
MinePump/spec1-5_product1.yml 1 2.3 .86 100 20 .086 .0082
MinePump/spec1-5_product10.yml 1 2.1 .79 81 19 .070 0     
MinePump/spec1-5_product11.yml 1 2.0 .80 83 16 .070 0     
MinePump/spec1-5_product12.yml 1 1.9 .77 82 16 .070 .0041
MinePump/spec1-5_product13.yml 1 2.1 .82 86 17 .070 0     
MinePump/spec1-5_product14.yml 1 2.2 .84 88 19 .070 .0041
MinePump/spec1-5_product15.yml 1 2.0 .76 81 17 .070 0     
MinePump/spec1-5_product16.yml 1 2.0 .81 87 19 .070 0     
MinePump/spec1-5_product17.yml 1 2.1 .83 82 18 .070 0     
MinePump/spec1-5_product18.yml 1 2.1 .82 78 16 .070 0     
MinePump/spec1-5_product19.yml 1 2.2 .92 94 19 .070 7.6   
MinePump/spec1-5_product2.yml 1 2.0 .80 82 16 .070 .020 
MinePump/spec1-5_product20.yml 1 2.1 .80 90 16 .070 0     
MinePump/spec1-5_product21.yml 1 2.0 .81 82 20 .070 .0082
MinePump/spec1-5_product22.yml 1 1.9 .79 82 18 .070 .0041
MinePump/spec1-5_product23.yml 1 2.0 .81 83 20 .070 0     
MinePump/spec1-5_product24.yml 1 1.9 .76 84 17 .070 0     
MinePump/spec1-5_product25.yml 1 2.0 .82 82 20 .070 0     
MinePump/spec1-5_product26.yml 1 1.9 .76 81 17 .070 0     
MinePump/spec1-5_product27.yml 1 2.2 .84 85 18 .070 0     
MinePump/spec1-5_product28.yml 1 2.1 .83 81 16 .070 .0082
MinePump/spec1-5_product29.yml 1 2.1 .83 88 21 .070 0     
MinePump/spec1-5_product3.yml 1 1.9 .77 82 18 .070 0     
MinePump/spec1-5_product30.yml 1 2.2 .84 84 21 .070 0     
MinePump/spec1-5_product31.yml 1 2.2 .87 82 21 .070 0     
MinePump/spec1-5_product32.yml 1 2.0 .78 81 19 .070 0     
MinePump/spec1-5_product33.yml 1 1.9 .76 84 20 .070 0     
MinePump/spec1-5_product34.yml 1 2.0 .82 85 20 .070 .025 
MinePump/spec1-5_product35.yml 1 2.0 .79 82 18 .070 0     
MinePump/spec1-5_product36.yml 1 2.2 .84 87 17 .070 0     
MinePump/spec1-5_product37.yml 1 2.1 .83 83 21 .070 0     
MinePump/spec1-5_product38.yml 1 2.1 .82 80 19 .070 .066 
MinePump/spec1-5_product39.yml 1 1.9 .77 78 18 .070 .0041
MinePump/spec1-5_product4.yml 1 2.3 .85 82 20 .070 0     
MinePump/spec1-5_product40.yml 1 2.0 .81 84 17 .070 .025 
MinePump/spec1-5_product41.yml 1 2.0 .79 83 17 .070 0     
MinePump/spec1-5_product42.yml 1 2.1 .81 82 18 .070 0     
MinePump/spec1-5_product43.yml 1 2.2 .82 84 18 .070 0     
MinePump/spec1-5_product44.yml 1 2.0 .78 90 18 .070 .020 
MinePump/spec1-5_product45.yml 1 1.9 .78 89 17 .070 0     
MinePump/spec1-5_product46.yml 1 2.2 .84 80 17 .070 0     
MinePump/spec1-5_product47.yml 1 2.0 .81 82 16 .070 0     
MinePump/spec1-5_product48.yml 1 2.0 .77 83 19 .070 0     
MinePump/spec1-5_product49.yml 1 2.0 .77 83 17 .074 0     
MinePump/spec1-5_product5.yml 1 1.9 .78 88 17 .070 0     
MinePump/spec1-5_product50.yml 1 2.2 .85 81 20 .074 .025 
MinePump/spec1-5_product51.yml 1 2.0 .77 81 17 .074 .020 
MinePump/spec1-5_product52.yml 1 2.2 .80 83 17 .074 0     
MinePump/spec1-5_product53.yml 1 2.0 .82 80 17 .074 .0082
MinePump/spec1-5_product54.yml 1 1.9 .80 81 18 .074 .066 
MinePump/spec1-5_product55.yml 1 2.1 .79 81 19 .074 .0082
MinePump/spec1-5_product56.yml 1 2.0 .79 83 14 .074 0     
MinePump/spec1-5_product57.yml 2 3.8 1.3  220 33 .34  0     
MinePump/spec1-5_product58.yml 2 4.1 1.3  210 38 .34  0     
MinePump/spec1-5_product59.yml 2 3.3 1.1  190 32 .34  .0082
MinePump/spec1-5_product6.yml 1 2.0 .79 82 17 .070 0     
MinePump/spec1-5_product60.yml 2 3.7 1.2  210 30 .34  0     
MinePump/spec1-5_product61.yml 2 3.6 1.2  210 29 .34  .033 
MinePump/spec1-5_product62.yml 2 3.5 1.2  200 29 .34  .0041
MinePump/spec1-5_product63.yml 2 3.5 1.2  190 30 .34  0     
MinePump/spec1-5_product64.yml 2 3.8 1.2  210 35 .34  0     
MinePump/spec1-5_product7.yml 1 2.1 .83 82 19 .070 .0041
MinePump/spec1-5_product8.yml 1 2.0 .76 82 17 .070 0     
MinePump/spec1-5_product9.yml 1 1.9 .77 83 16 .070 0     
sv-benchmarks/java/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB)
total 368 365 1300   760   34000 13000 28    11    
local summary 5000  
    correct results 337 493 970   560   31000 9900 26    10    
        correct true 156 312 620   420   15000 6800 14    .82 
        correct false 181 181 350   140   16000 3100 13    9.4  
    incorrect results 6 -128 11   4.7 530 100 .42 .029
        incorrect true 2 -64 4.2 1.7 180 37 .14 .029
        incorrect false 4 -64 7.2 2.9 340 64 .28 0    
score (368 tasks, max score: 532) 365
Run set sv-comp19_prop-reachsafety_java.ReachSafety-Java