Tool JPF 3a45016c72f2e7bd617f7984d07839c798528183
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:55:55 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 false 1 --- inspect 1.5 .67 63 11 .070 0     
jayhorn-recursive/Addition.yml true 2 --- inspect 1.5 .66 60 14 .070 .057 
jayhorn-recursive/InfiniteLoop.yml false 1 --- inspect 1.5 .64 62 14 .070 .057 
jayhorn-recursive/SatAckermann01.yml true 2 --- inspect 1.6 .69 60 13 .070 .057 
jayhorn-recursive/SatAckermann02.yml true 2 --- inspect 1.6 .72 61 15 .070 0     
jayhorn-recursive/SatAckermann03.yml true 2 --- inspect 1.6 .65 63 17 .070 0     
jayhorn-recursive/SatAddition01.yml timeout 0 --- inspect 910   120    1100 4000 .049 0     
jayhorn-recursive/SatEvenOdd01.yml timeout 0 --- inspect 910   120    1100 4100 .049 0     
jayhorn-recursive/SatFibonacci01.yml true 2 --- inspect 1.6 .68 60 15 .070 0     
jayhorn-recursive/SatFibonacci02.yml true 2 --- inspect 1.6 .67 59 14 .070 0     
jayhorn-recursive/SatFibonacci03.yml true 2 --- inspect 1.5 .64 61 13 .070 0     
jayhorn-recursive/SatGcd.yml true 2 --- inspect 1.5 .63 62 14 .070 .057 
jayhorn-recursive/SatHanoi01.yml true 2 --- inspect 1.5 .65 62 12 .070 0     
jayhorn-recursive/SatMccarthy91.yml timeout 0 --- inspect 910   120    1100 4100 .049 0     
jayhorn-recursive/SatMultCommutative01.yml true 2 --- inspect 1.6 .67 60 13 .070 0     
jayhorn-recursive/SatPrimes01.yml true 2 --- inspect 1.6 .68 59 14 .070 0     
jayhorn-recursive/UnsatAckermann01.yml timeout 0 --- inspect 910   120    1100 4000 .049 0     
jayhorn-recursive/UnsatAddition01.yml timeout 0 --- inspect 910   120    1100 3900 .049 .057 
jayhorn-recursive/UnsatAddition02.yml timeout 0 --- inspect 910   120    1100 4100 .049 .057 
jayhorn-recursive/UnsatEvenOdd01.yml false 1 --- inspect 1.6 .66 61 14 .070 0     
jayhorn-recursive/UnsatFibonacci01.yml timeout 0 --- inspect 910   120    1100 3700 .049 0     
jayhorn-recursive/UnsatFibonacci02.yml timeout 0 --- inspect 910   120    1100 3800 .049 0     
jayhorn-recursive/UnsatMccarthy91.yml timeout 0 --- inspect 910   120    1100 4000 .049 .057 
jbmc-regression/ArithmeticException1.yml false 1 --- inspect 1.6 .69 62 15 .070 .098 
jbmc-regression/ArithmeticException5.yml true 2 --- inspect 1.5 .62 62 14 .070 .22  
jbmc-regression/ArithmeticException6.yml false 1 --- inspect 1.6 .69 60 14 .070 .041 
jbmc-regression/ArrayIndexOutOfBoundsException1.yml false 1 --- inspect 1.6 .65 61 14 .070 .15  
jbmc-regression/ArrayIndexOutOfBoundsException2.yml false 1 --- inspect 1.6 .71 60 15 .070 0     
jbmc-regression/ArrayIndexOutOfBoundsException3.yml false 1 --- inspect 1.5 .63 60 15 .070 .074 
jbmc-regression/BufferedReaderReadLine.yml false 1 --- inspect 1.6 .70 63 15 .070 .016 
jbmc-regression/CharSequenceBug.yml false 1 --- inspect 1.5 .65 63 14 .070 .057 
jbmc-regression/CharSequenceToString.yml unknown 0 --- inspect 1.6 .67 77 14 .070 .16  
jbmc-regression/ClassCastException1.yml false 1 --- inspect 1.5 .63 63 16 .070 .012 
jbmc-regression/ClassCastException2.yml true 2 --- inspect 1.7 .71 62 13 .070 .057 
jbmc-regression/ClassCastException3.yml false 1 --- inspect 1.5 .67 63 16 .070 0     
jbmc-regression/Class_method1.yml true 2 --- inspect 1.6 .66 60 14 .070 0     
jbmc-regression/Inheritance1.yml true 2 --- inspect 1.5 .65 59 13 .070 .057 
jbmc-regression/NegativeArraySizeException1.yml false 1 --- inspect 1.6 .68 59 13 .070 .0041
jbmc-regression/NegativeArraySizeException2.yml false 1 --- inspect 1.5 .67 61 14 .070 0     
jbmc-regression/NullPointerException1.yml true 2 --- inspect 1.5 .64 60 13 .070 .016 
jbmc-regression/NullPointerException2.yml false 1 --- inspect 1.6 .68 60 13 .070 .074 
jbmc-regression/NullPointerException3.yml false 1 --- inspect 1.4 .63 59 15 .070 .016 
jbmc-regression/NullPointerException4.yml false 1 --- inspect 1.6 .66 62 15 .070 0     
jbmc-regression/RegexMatches01.yml true 2 --- inspect 1.5 .63 62 14 .070 .029 
jbmc-regression/RegexMatches02.yml unknown 0 --- inspect 1.8 .71 77 17 .070 .029 
jbmc-regression/RegexSubstitution01.yml true 2 --- inspect 1.7 .70 64 16 .070 .041 
jbmc-regression/RegexSubstitution02.yml false 1 --- inspect 1.6 .75 62 14 .070 .041 
jbmc-regression/RegexSubstitution03.yml true 2 --- inspect 1.7 .69 63 15 .070 .098 
jbmc-regression/StaticCharMethods01.yml true 2 --- inspect 1.6 .66 61 14 .070 0     
jbmc-regression/StaticCharMethods02.yml unknown 0 --- inspect 1.7 .68 75 15 .070 0     
jbmc-regression/StaticCharMethods03.yml unknown 0 --- inspect 1.6 .69 77 14 .070 .057 
jbmc-regression/StaticCharMethods04.yml false 1 --- inspect 1.6 .64 63 13 .070 0     
jbmc-regression/StaticCharMethods05.yml unknown 0 --- inspect 1.8 .72 64 14 .070 .090 
jbmc-regression/StaticCharMethods06.yml unknown 0 --- inspect 1.6 .69 76 13 .070 .057 
jbmc-regression/StringBuilderAppend01.yml true 2 --- inspect 1.7 .68 63 15 .070 .057 
jbmc-regression/StringBuilderAppend02.yml false 1 --- inspect 1.8 .71 64 13 .070 0     
jbmc-regression/StringBuilderCapLen01.yml true 2 --- inspect 1.6 .68 62 13 .070 .057 
jbmc-regression/StringBuilderCapLen02.yml false 1 --- inspect 1.6 .68 62 15 .070 0     
jbmc-regression/StringBuilderCapLen03.yml false 1 --- inspect 1.5 .67 62 15 .070 .057 
jbmc-regression/StringBuilderCapLen04.yml false 1 --- inspect 1.6 .69 62 15 .070 0     
jbmc-regression/StringBuilderChars01.yml true 2 --- inspect 1.5 .64 59 15 .070 0     
jbmc-regression/StringBuilderChars02.yml false 1 --- inspect 1.5 .65 61 13 .070 0     
jbmc-regression/StringBuilderChars03.yml false 1 --- inspect 1.7 .68 62 14 .070 .070 
jbmc-regression/StringBuilderChars04.yml unknown 0 --- inspect 1.8 .72 77 14 .070 0     
jbmc-regression/StringBuilderChars05.yml false 1 --- inspect 1.7 .70 62 15 .070 0     
jbmc-regression/StringBuilderChars06.yml false 1 --- inspect 1.6 .69 61 15 .070 0     
jbmc-regression/StringBuilderConstructors01.yml unknown 0 --- inspect 1.6 .68 76 13 .070 0     
jbmc-regression/StringBuilderConstructors02.yml false 1 --- inspect 1.6 .69 61 14 .070 .057 
jbmc-regression/StringBuilderInsertDelete01.yml true 2 --- inspect 1.6 .69 62 13 .070 0     
jbmc-regression/StringBuilderInsertDelete02.yml false 1 --- inspect 1.6 .69 63 15 .070 0     
jbmc-regression/StringBuilderInsertDelete03.yml false 1 --- inspect 1.9 .74 65 16 .070 0     
jbmc-regression/StringCompare01.yml true 2 --- inspect 1.6 .64 59 15 .070 0     
jbmc-regression/StringCompare02.yml false 1 --- inspect 1.6 .69 62 14 .070 0     
jbmc-regression/StringCompare03.yml unknown 0 --- inspect 1.6 .67 75 13 .070 0     
jbmc-regression/StringCompare04.yml false 1 --- inspect 1.6 .71 63 14 .070 .057 
jbmc-regression/StringCompare05.yml false 1 --- inspect 1.6 .68 60 15 .070 0     
jbmc-regression/StringConcatenation01.yml unknown 0 --- inspect 1.6 .68 77 15 .070 .057 
jbmc-regression/StringConcatenation02.yml false 1 --- inspect 1.5 .64 62 13 .070 .057 
jbmc-regression/StringConcatenation03.yml false 1 --- inspect 1.6 .69 61 14 .070 .078 
jbmc-regression/StringConcatenation04.yml false 1 --- inspect 1.5 .66 61 13 .070 .020 
jbmc-regression/StringConstructors01.yml true 2 --- inspect 1.6 .67 60 14 .070 0     
jbmc-regression/StringConstructors02.yml unknown 0 --- inspect 1.6 .65 78 16 .070 0     
jbmc-regression/StringConstructors03.yml unknown 0 --- inspect 1.7 .71 74 14 .070 0     
jbmc-regression/StringConstructors04.yml false 1 --- inspect 1.5 .66 61 13 .070 .057 
jbmc-regression/StringConstructors05.yml false 1 --- inspect 1.6 .70 65 13 .070 .066 
jbmc-regression/StringContains01.yml unknown 0 --- inspect 1.6 .66 77 14 .070 0     
jbmc-regression/StringContains02.yml false 1 --- inspect 1.6 .69 62 16 .070 .082 
jbmc-regression/StringIndexMethods01.yml true 2 --- inspect 1.6 .68 62 15 .070 .057 
jbmc-regression/StringIndexMethods02.yml false 1 --- inspect 1.6 .67 60 14 .070 0     
jbmc-regression/StringIndexMethods03.yml false 1 --- inspect 1.5 .66 62 14 .070 0     
jbmc-regression/StringIndexMethods04.yml false 1 --- inspect 1.5 .69 60 13 .070 .057 
jbmc-regression/StringIndexMethods05.yml false 1 --- inspect 1.6 .67 62 15 .070 0     
jbmc-regression/StringMiscellaneous01.yml true 2 --- inspect 1.7 .76 62 17 .070 .020 
jbmc-regression/StringMiscellaneous02.yml false 1 --- inspect 1.5 .66 63 13 .070 0     
jbmc-regression/StringMiscellaneous03.yml unknown 0 --- inspect 1.6 .73 75 14 .070 .057 
jbmc-regression/StringMiscellaneous04.yml true 2 --- inspect 1.6 .69 62 14 .070 .25  
jbmc-regression/StringStartEnd01.yml true 2 --- inspect 1.6 .68 60 14 .070 0     
jbmc-regression/StringStartEnd02.yml false 1 --- inspect 1.5 .63 61 14 .070 0     
jbmc-regression/StringStartEnd03.yml false 1 --- inspect 1.5 .68 61 13 .070 .057 
jbmc-regression/StringValueOf01.yml true 2 --- inspect 1.5 .65 62 15 .070 0     
jbmc-regression/StringValueOf02.yml false 1 --- inspect 1.6 .69 61 12 .070 .057 
jbmc-regression/StringValueOf03.yml false 1 --- inspect 1.7 .73 62 17 .070 0     
jbmc-regression/StringValueOf04.yml false 1 --- inspect 1.5 .63 62 12 .070 0     
jbmc-regression/StringValueOf05.yml unknown 0 --- inspect 1.6 .66 78 15 .070 0     
jbmc-regression/StringValueOf06.yml false 1 --- inspect 1.5 .68 60 16 .070 .057 
jbmc-regression/StringValueOf07.yml false 1 --- inspect 1.6 .70 61 14 .070 .020 
jbmc-regression/StringValueOf08.yml false 1 --- inspect 1.5 .67 63 14 .070 .19  
jbmc-regression/StringValueOf09.yml false 1 --- inspect 1.6 .69 62 15 .070 0     
jbmc-regression/StringValueOf10.yml false 1 --- inspect 1.6 .67 64 13 .070 .057 
jbmc-regression/SubString01.yml true 2 --- inspect 1.5 .63 61 14 .070 .057 
jbmc-regression/SubString02.yml false 1 --- inspect 1.6 .69 63 14 .070 0     
jbmc-regression/SubString03.yml false 1 --- inspect 1.5 .66 62 16 .070 .057 
jbmc-regression/TokenTest01.yml true 2 --- inspect 1.5 .69 61 14 .070 .086 
jbmc-regression/TokenTest02.yml unknown 0 --- inspect 1.7 .69 78 14 .070 .0041
jbmc-regression/Validate01.yml true 2 --- inspect 1.6 .69 62 14 .070 0     
jbmc-regression/Validate02.yml false 1 --- inspect 1.7 .67 61 13 .070 0     
jbmc-regression/aastore_aaload1.yml unknown 0 --- inspect 1.8 .74 75 15 .070 0     
jbmc-regression/array1.yml unknown 0 --- inspect 1.6 .67 75 13 .070 0     
jbmc-regression/array2.yml true 2 --- inspect 1.5 .66 60 14 .070 0     
jbmc-regression/arraylength1.yml unknown 0 --- inspect 1.7 .72 76 13 .070 0     
jbmc-regression/arrayread1.yml true 2 --- inspect 1.5 .65 62 15 .070 .057 
jbmc-regression/assert1.yml true 2 --- inspect 1.6 .70 60 14 .070 0     
jbmc-regression/assert2.yml true -32 --- inspect 1.6 .68 61 14 .070 0     
jbmc-regression/assert3.yml true -32 --- inspect 1.5 .62 61 14 .070 0     
jbmc-regression/assert4.yml true -32 --- inspect 1.6 .70 62 14 .070 .057 
jbmc-regression/assert5.yml true 2 --- inspect 1.5 .69 61 12 .070 0     
jbmc-regression/assert6.yml true 2 --- inspect 1.5 .66 63 14 .070 0     
jbmc-regression/astore_aload1.yml true 2 --- inspect 1.7 .68 62 15 .070 .057 
jbmc-regression/athrow1.yml false 1 --- inspect 1.6 .68 60 13 .070 .070 
jbmc-regression/basic1.yml true 2 --- inspect 1.6 .67 59 15 .070 .0041
jbmc-regression/bitwise1.yml true 2 --- inspect 1.5 .64 60 12 .070 0     
jbmc-regression/boolean1.yml true 2 --- inspect 1.5 .67 59 14 .070 0     
jbmc-regression/boolean2.yml true 2 --- inspect 1.5 .66 59 13 .070 .057 
jbmc-regression/bug-test-gen-095.yml false 1 --- inspect 1.6 .69 62 14 .070 0     
jbmc-regression/bug-test-gen-119-2.yml true 2 --- inspect 1.6 .73 61 14 .070 0     
jbmc-regression/bug-test-gen-119.yml true 2 --- inspect 1.4 .63 61 13 .070 .057 
jbmc-regression/calc.yml unknown 0 --- inspect 1.7 .68 77 14 .070 .066 
jbmc-regression/cast1.yml true 2 --- inspect 1.5 .66 60 13 .070 0     
jbmc-regression/catch1.yml true 2 --- inspect 1.5 .65 60 14 .070 .012 
jbmc-regression/char1.yml unknown 0 --- inspect 1.7 .69 76 14 .070 .057 
jbmc-regression/charArray.yml unknown 0 --- inspect 1.6 .68 74 14 .070 0     
jbmc-regression/classtest1.yml true 2 --- inspect 1.5 .63 61 14 .070 0     
jbmc-regression/const1.yml true 2 --- inspect 1.5 .64 61 12 .070 .057 
jbmc-regression/constructor1.yml true 2 --- inspect 1.6 .71 67 14 .070 7.9   
jbmc-regression/enum1.yml true 2 --- inspect 1.5 .67 62 13 .070 .057 
jbmc-regression/exceptions1.yml false 1 --- inspect 1.6 .68 60 14 .070 0     
jbmc-regression/exceptions10.yml false 1 --- inspect 1.5 .64 62 13 .070 .070 
jbmc-regression/exceptions11.yml false 1 --- inspect 1.5 .66 63 15 .070 .070 
jbmc-regression/exceptions12.yml false 1 --- inspect 1.5 .64 62 14 .070 .070 
jbmc-regression/exceptions13.yml false 1 --- inspect 1.6 .68 62 14 .070 .061 
jbmc-regression/exceptions14.yml true 2 --- inspect 1.5 .64 60 14 .070 0     
jbmc-regression/exceptions15.yml true 2 --- inspect 1.5 .67 61 14 .070 0     
jbmc-regression/exceptions16.yml false 1 --- inspect 1.5 .64 60 14 .070 0     
jbmc-regression/exceptions18.yml true 2 --- inspect 1.5 .64 62 14 .070 0     
jbmc-regression/exceptions2.yml false 1 --- inspect 1.6 .67 59 15 .070 0     
jbmc-regression/exceptions3.yml false 1 --- inspect 1.7 .70 61 15 .070 .057 
jbmc-regression/exceptions4.yml true 2 --- inspect 1.5 .66 60 15 .070 .070 
jbmc-regression/exceptions5.yml true 2 --- inspect 1.6 .67 62 14 .070 .016 
jbmc-regression/exceptions6.yml false 1 --- inspect 1.5 .66 62 16 .070 0     
jbmc-regression/exceptions7.yml false 1 --- inspect 1.6 .71 61 13 .070 .012 
jbmc-regression/exceptions8.yml false 1 --- inspect 1.6 .68 61 13 .070 0     
jbmc-regression/exceptions9.yml true 2 --- inspect 1.6 .66 62 15 .070 .012 
jbmc-regression/fcmpx_dcmpx1.yml true 2 --- inspect 1.5 .67 60 13 .070 .057 
jbmc-regression/iarith1.yml true 2 --- inspect 1.6 .68 62 14 .070 .057 
jbmc-regression/iarith2.yml true 2 --- inspect 1.6 .67 62 14 .070 0     
jbmc-regression/if_acmp1.yml true 2 --- inspect 1.6 .67 58 15 .070 0     
jbmc-regression/if_expr1.yml true 2 --- inspect 1.5 .65 61 13 .070 0     
jbmc-regression/if_icmp1.yml true 2 --- inspect 1.6 .68 60 13 .070 0     
jbmc-regression/ifxx1.yml true 2 --- inspect 1.5 .63 62 13 .070 0     
jbmc-regression/instanceof1.yml true 2 --- inspect 1.6 .65 60 12 .070 0     
jbmc-regression/instanceof2.yml true 2 --- inspect 1.5 .65 59 13 .070 0     
jbmc-regression/instanceof3.yml true 2 --- inspect 1.6 .66 60 14 .070 .057 
jbmc-regression/instanceof4.yml true 2 --- inspect 1.6 .68 59 13 .070 0     
jbmc-regression/instanceof5.yml true 2 --- inspect 1.5 .65 59 13 .070 0     
jbmc-regression/instanceof6.yml true 2 --- inspect 1.5 .62 59 11 .070 0     
jbmc-regression/instanceof7.yml true 2 --- inspect 1.6 .67 61 16 .070 0     
jbmc-regression/instanceof8.yml true 2 --- inspect 1.6 .66 60 12 .070 0     
jbmc-regression/interface1.yml false 1 --- inspect 1.5 .63 61 14 .070 0     
jbmc-regression/java_append_char.yml false 1 --- inspect 1.6 .68 61 14 .070 .057 
jbmc-regression/lazyloading4.yml true 2 --- inspect 1.5 .64 60 11 .070 .057 
jbmc-regression/list1.yml true 2 --- inspect 11   6.5  220 95 .070 0     
jbmc-regression/long1.yml true 2 --- inspect 1.5 .65 61 14 .070 0     
jbmc-regression/lookupswitch1.yml true 2 --- inspect 1.5 .66 62 12 .070 .057 
jbmc-regression/multinewarray.yml true 2 --- inspect 1.6 .64 59 13 .070 0     
jbmc-regression/overloading1.yml true 2 --- inspect 1.4 .62 60 13 .070 0     
jbmc-regression/package1.yml true 2 --- inspect 1.6 .64 61 16 .070 0     
jbmc-regression/putfield_getfield1.yml true 2 --- inspect 1.6 .69 61 14 .070 0     
jbmc-regression/putstatic_getstatic1.yml true 2 --- inspect 1.5 .64 62 13 .070 .057 
jbmc-regression/recursion2.yml true 2 --- inspect 1.5 .64 61 13 .070 .057 
jbmc-regression/return1.yml false 1 --- inspect 1.5 .67 60 14 .070 0     
jbmc-regression/return2.yml false 1 --- inspect 1.5 .65 62 14 .070 0     
jbmc-regression/store_load1.yml true 2 --- inspect 1.6 .67 59 14 .070 .057 
jbmc-regression/swap1.yml true 2 --- inspect 1.5 .65 62 15 .070 .057 
jbmc-regression/synchronized.yml true 2 --- inspect 1.6 .64 59 16 .070 0     
jbmc-regression/tableswitch1.yml true 2 --- inspect 1.5 .63 62 15 .070 .057 
jbmc-regression/uninitialised1.yml true 2 --- inspect 1.5 .65 62 14 .070 .057 
jbmc-regression/virtual1.yml true 2 --- inspect 1.5 .66 61 14 .070 0     
jbmc-regression/virtual2.yml false 1 --- inspect 1.5 .68 61 14 .070 .057 
jbmc-regression/virtual4.yml true 2 --- inspect 1.5 .61 59 14 .070 0     
jbmc-regression/virtual_function_unwinding.yml true 2 --- inspect 1.6 .69 61 14 .070 0     
jpf-regression/ExDarko_false.yml false 1 --- inspect 1.5 .66 61 15 .070 .057 
jpf-regression/ExDarko_true.yml true 2 --- inspect 1.6 .67 60 12 .070 0     
jpf-regression/ExException_false.yml false 1 --- inspect 1.6 .66 60 16 .070 0     
jpf-regression/ExException_true.yml true 2 --- inspect 1.6 .64 62 14 .070 .049 
jpf-regression/ExGenSymExe_false.yml false 1 --- inspect 1.6 .69 60 13 .070 0     
jpf-regression/ExGenSymExe_true.yml true 2 --- inspect 1.5 .65 60 14 .070 .057 
jpf-regression/ExLazy_false.yml false 1 --- inspect 1.6 .68 61 15 .070 0     
jpf-regression/ExLazy_true.yml true 2 --- inspect 1.5 .63 62 13 .070 .057 
jpf-regression/ExMIT_false.yml true -32 --- inspect 1.6 .68 61 13 .070 0     
jpf-regression/ExMIT_true.yml true 2 --- inspect 1.5 .67 61 14 .070 0     
jpf-regression/ExSymExe10_false.yml false 1 --- inspect 1.5 .65 63 16 .070 .057 
jpf-regression/ExSymExe10_true.yml true 2 --- inspect 1.5 .66 62 14 .070 0     
jpf-regression/ExSymExe11_false.yml false 1 --- inspect 1.5 .63 63 14 .070 0     
jpf-regression/ExSymExe11_true.yml true 2 --- inspect 1.6 .66 61 15 .070 .057 
jpf-regression/ExSymExe12_false.yml false 1 --- inspect 1.6 .70 61 13 .070 .057 
jpf-regression/ExSymExe12_true.yml true 2 --- inspect 1.5 .65 62 14 .070 0     
jpf-regression/ExSymExe13_false.yml false 1 --- inspect 1.6 .68 62 14 .070 0     
jpf-regression/ExSymExe13_true.yml true 2 --- inspect 1.5 .62 63 13 .070 .057 
jpf-regression/ExSymExe14_false.yml false 1 --- inspect 1.6 .68 63 14 .070 .057 
jpf-regression/ExSymExe14_true.yml true 2 --- inspect 1.5 .63 60 13 .070 0     
jpf-regression/ExSymExe15_false.yml false 1 --- inspect 1.6 .67 63 13 .070 0     
jpf-regression/ExSymExe15_true.yml true 2 --- inspect 1.6 .68 63 15 .070 0     
jpf-regression/ExSymExe16_false.yml false 1 --- inspect 1.5 .66 60 13 .070 .057 
jpf-regression/ExSymExe16_true.yml true 2 --- inspect 1.6 .67 61 13 .070 .057 
jpf-regression/ExSymExe17_false.yml false 1 --- inspect 1.5 .65 62 13 .070 .057 
jpf-regression/ExSymExe17_true.yml true 2 --- inspect 1.6 .65 59 15 .070 0     
jpf-regression/ExSymExe18_false.yml false 1 --- inspect 1.5 .66 63 16 .070 .057 
jpf-regression/ExSymExe18_true.yml true 2 --- inspect 1.6 .69 59 14 .070 0     
jpf-regression/ExSymExe19_false.yml false 1 --- inspect 1.6 .67 62 13 .070 .041 
jpf-regression/ExSymExe19_true.yml true 2 --- inspect 1.6 .71 63 16 .070 0     
jpf-regression/ExSymExe1_false.yml false 1 --- inspect 1.5 .64 63 15 .070 .045 
jpf-regression/ExSymExe1_true.yml true 2 --- inspect 1.6 .66 61 14 .070 0     
jpf-regression/ExSymExe20_false.yml false 1 --- inspect 1.7 .68 63 13 .070 0     
jpf-regression/ExSymExe20_true.yml true 2 --- inspect 1.6 .67 61 14 .070 0     
jpf-regression/ExSymExe21_false.yml false 1 --- inspect 1.6 .68 61 14 .070 .057 
jpf-regression/ExSymExe21_true.yml true 2 --- inspect 1.5 .64 62 15 .070 0     
jpf-regression/ExSymExe25_false.yml false 1 --- inspect 1.5 .66 61 14 .070 0     
jpf-regression/ExSymExe25_true.yml true 2 --- inspect 1.5 .64 59 14 .070 0     
jpf-regression/ExSymExe26_false.yml false 1 --- inspect 1.5 .68 62 14 .070 0     
jpf-regression/ExSymExe26_true.yml true 2 --- inspect 1.6 .64 59 15 .070 0     
jpf-regression/ExSymExe27_false.yml false 1 --- inspect 1.6 .69 60 16 .070 0     
jpf-regression/ExSymExe27_true.yml true 2 --- inspect 1.5 .64 60 13 .070 .22  
jpf-regression/ExSymExe28_false.yml false 1 --- inspect 1.5 .66 61 14 .070 .057 
jpf-regression/ExSymExe28_true.yml true 2 --- inspect 1.5 .63 62 14 .070 0     
jpf-regression/ExSymExe29_false.yml false 1 --- inspect 1.5 .66 61 13 .070 0     
jpf-regression/ExSymExe29_true.yml true 2 --- inspect 1.6 .67 62 16 .070 0     
jpf-regression/ExSymExe2_false.yml false 1 --- inspect 1.7 .70 61 16 .070 .16  
jpf-regression/ExSymExe2_true.yml true 2 --- inspect 1.6 .68 59 16 .070 0     
jpf-regression/ExSymExe3_false.yml false 1 --- inspect 1.5 .69 63 14 .070 0     
jpf-regression/ExSymExe3_true.yml true 2 --- inspect 1.5 .63 59 14 .070 .17  
jpf-regression/ExSymExe4_false.yml false 1 --- inspect 1.7 .72 60 15 .070 .057 
jpf-regression/ExSymExe4_true.yml true 2 --- inspect 1.6 .69 59 14 .070 0     
jpf-regression/ExSymExe5_false.yml false 1 --- inspect 1.6 .71 60 14 .070 0     
jpf-regression/ExSymExe5_true.yml true 2 --- inspect 1.6 .67 62 15 .070 0     
jpf-regression/ExSymExe6_false.yml false 1 --- inspect 1.5 .65 63 15 .070 0     
jpf-regression/ExSymExe6_true.yml true 2 --- inspect 1.6 .65 62 13 .070 0     
jpf-regression/ExSymExe7_false.yml true -32 --- inspect 1.5 .66 63 12 .070 0     
jpf-regression/ExSymExe7_true.yml true 2 --- inspect 1.5 .66 62 14 .070 .13  
jpf-regression/ExSymExe8_false.yml false 1 --- inspect 1.6 .67 61 15 .070 .057 
jpf-regression/ExSymExe8_true.yml true 2 --- inspect 1.6 .66 62 13 .070 .057 
jpf-regression/ExSymExe9_false.yml false 1 --- inspect 1.5 .64 61 12 .070 .057 
jpf-regression/ExSymExe9_true.yml true 2 --- inspect 1.6 .66 59 12 .070 0     
jpf-regression/ExSymExeArrays_false.yml false 1 --- inspect 1.5 .64 59 13 .070 0     
jpf-regression/ExSymExeArrays_true.yml true 2 --- inspect 1.5 .64 59 15 .070 0     
jpf-regression/ExSymExeBool_false.yml false 1 --- inspect 1.5 .68 63 14 .070 .10  
jpf-regression/ExSymExeBool_true.yml true 2 --- inspect 1.6 .66 62 15 .070 0     
jpf-regression/ExSymExeComplexMath_false.yml false 1 --- inspect 1.7 .70 59 15 .070 0     
jpf-regression/ExSymExeComplexMath_true.yml true 2 --- inspect 1.6 .68 62 17 .070 .057 
jpf-regression/ExSymExeD2I_false.yml false 1 --- inspect 1.5 .64 60 15 .070 0     
jpf-regression/ExSymExeD2I_true.yml true 2 --- inspect 1.5 .67 61 12 .070 .20  
jpf-regression/ExSymExeD2L_false.yml false 1 --- inspect 1.5 .66 60 13 .070 0     
jpf-regression/ExSymExeD2L_true.yml true 2 --- inspect 1.6 .68 59 14 .070 .057 
jpf-regression/ExSymExeF2I_false.yml false 1 --- inspect 1.5 .64 62 13 .070 0     
jpf-regression/ExSymExeF2I_true.yml true 2 --- inspect 1.5 .67 62 14 .070 0     
jpf-regression/ExSymExeF2L_false.yml false 1 --- inspect 1.6 .68 60 14 .070 0     
jpf-regression/ExSymExeF2L_true.yml true 2 --- inspect 1.6 .69 61 15 .070 .057 
jpf-regression/ExSymExeFNEG_false.yml false 1 --- inspect 1.5 .64 61 14 .070 0     
jpf-regression/ExSymExeFNEG_true.yml true 2 --- inspect 1.6 .70 59 14 .070 .045 
jpf-regression/ExSymExeGetStatic_false.yml false 1 --- inspect 1.6 .67 62 14 .070 .057 
jpf-regression/ExSymExeGetStatic_true.yml true 2 --- inspect 1.5 .66 62 14 .070 .057 
jpf-regression/ExSymExeI2D_false.yml false 1 --- inspect 1.5 .69 71 15 .070 8.9   
jpf-regression/ExSymExeI2D_true.yml true 2 --- inspect 1.5 .64 60 14 .070 .049 
jpf-regression/ExSymExeI2F_false.yml false 1 --- inspect 1.5 .65 62 14 .070 0     
jpf-regression/ExSymExeI2F_true.yml true 2 --- inspect 1.5 .65 61 13 .070 0     
jpf-regression/ExSymExeLCMP_false.yml false 1 --- inspect 1.6 .69 63 13 .070 0     
jpf-regression/ExSymExeLCMP_true.yml true 2 --- inspect 1.6 .70 60 14 .070 0     
jpf-regression/ExSymExeLongBytecodes_false.yml false 1 --- inspect 1.7 .68 63 14 .070 0     
jpf-regression/ExSymExeLongBytecodes_true.yml true 2 --- inspect 1.6 .69 63 14 .070 0     
jpf-regression/ExSymExeResearch_false.yml false 1 --- inspect 1.6 .67 63 13 .070 .23  
jpf-regression/ExSymExeResearch_true.yml true 2 --- inspect 1.6 .68 59 14 .070 .045 
jpf-regression/ExSymExeSimple_false.yml false 1 --- inspect 1.6 .67 61 13 .070 .057 
jpf-regression/ExSymExeSimple_true.yml true 2 --- inspect 1.6 .69 63 14 .070 .049 
jpf-regression/ExSymExeSuzette_false.yml false 1 --- inspect 1.6 .66 62 14 .070 0     
jpf-regression/ExSymExeSuzette_true.yml true 2 --- inspect 1.5 .67 61 14 .070 0     
jpf-regression/ExSymExeSwitch_false.yml false 1 --- inspect 1.5 .67 62 15 .070 0     
jpf-regression/ExSymExeSwitch_true.yml true 2 --- inspect 1.6 .67 62 14 .070 0     
jpf-regression/ExSymExeTestAssignments_false.yml false 1 --- inspect 1.6 .70 63 15 .070 0     
jpf-regression/ExSymExeTestAssignments_true.yml true 2 --- inspect 1.5 .66 60 15 .070 0     
jpf-regression/ExSymExeTestClassFields_false.yml true -32 --- inspect 1.6 .68 60 15 .070 .057 
jpf-regression/ExSymExeTestClassFields_true.yml true 2 --- inspect 1.5 .66 60 14 .070 .14  
jpf-regression/ExSymExe_false.yml false 1 --- inspect 1.6 .72 61 15 .070 0     
jpf-regression/ExSymExe_true.yml true 2 --- inspect 1.6 .69 59 14 .070 .11  
jpf-regression/TestLazy_false.yml false 1 --- inspect 1.6 .68 61 15 .070 0     
jpf-regression/TestLazy_true.yml true 2 --- inspect 1.5 .66 64 15 .070 0     
MinePump/spec1-5_product1.yml false 1 --- inspect 2.1 .84 72 19 .070 .057 
MinePump/spec1-5_product10.yml false 1 --- inspect 1.7 .74 64 16 .070 0     
MinePump/spec1-5_product11.yml false 1 --- inspect 1.8 .73 64 15 .070 0     
MinePump/spec1-5_product12.yml false 1 --- inspect 1.9 .76 65 20 .070 .057 
MinePump/spec1-5_product13.yml false 1 --- inspect 1.8 .75 64 15 .070 0     
MinePump/spec1-5_product14.yml false 1 --- inspect 1.9 .76 64 16 .070 .053 
MinePump/spec1-5_product15.yml false 1 --- inspect 1.8 .75 64 17 .070 .057 
MinePump/spec1-5_product16.yml false 1 --- inspect 1.8 .74 63 16 .070 0     
MinePump/spec1-5_product17.yml false 1 --- inspect 1.7 .72 65 17 .070 .057 
MinePump/spec1-5_product18.yml false 1 --- inspect 1.9 .79 63 16 .070 0     
MinePump/spec1-5_product19.yml false 1 --- inspect 1.9 .76 62 18 .070 .0082
MinePump/spec1-5_product2.yml false 1 --- inspect 1.9 .76 64 19 .070 .0041
MinePump/spec1-5_product20.yml false 1 --- inspect 1.8 .74 62 15 .070 0     
MinePump/spec1-5_product21.yml false 1 --- inspect 1.7 .74 63 14 .070 .0041
MinePump/spec1-5_product22.yml false 1 --- inspect 1.7 .74 62 16 .070 .057 
MinePump/spec1-5_product23.yml false 1 --- inspect 1.7 .71 62 15 .070 0     
MinePump/spec1-5_product24.yml false 1 --- inspect 1.8 .72 64 15 .070 0     
MinePump/spec1-5_product25.yml false 1 --- inspect 1.7 .72 64 17 .070 .057 
MinePump/spec1-5_product26.yml false 1 --- inspect 1.9 .76 64 18 .070 .057 
MinePump/spec1-5_product27.yml false 1 --- inspect 1.9 .75 61 18 .070 .057 
MinePump/spec1-5_product28.yml false 1 --- inspect 1.7 .74 61 18 .070 0     
MinePump/spec1-5_product29.yml false 1 --- inspect 2.0 .79 62 16 .070 .061 
MinePump/spec1-5_product3.yml false 1 --- inspect 1.7 .71 64 14 .070 0     
MinePump/spec1-5_product30.yml false 1 --- inspect 1.8 .75 66 15 .070 .0082
MinePump/spec1-5_product31.yml false 1 --- inspect 2.1 .79 66 19 .070 .0082
MinePump/spec1-5_product32.yml false 1 --- inspect 1.7 .73 62 16 .070 0     
MinePump/spec1-5_product33.yml false 1 --- inspect 1.8 .78 61 17 .070 .057 
MinePump/spec1-5_product34.yml false 1 --- inspect 1.9 .76 64 18 .070 0     
MinePump/spec1-5_product35.yml false 1 --- inspect 1.8 .77 61 15 .070 0     
MinePump/spec1-5_product36.yml false 1 --- inspect 1.8 .76 62 17 .070 .10  
MinePump/spec1-5_product37.yml false 1 --- inspect 1.7 .71 62 15 .070 0     
MinePump/spec1-5_product38.yml false 1 --- inspect 1.7 .71 64 15 .070 .061 
MinePump/spec1-5_product39.yml false 1 --- inspect 1.7 .74 62 17 .070 0     
MinePump/spec1-5_product4.yml false 1 --- inspect 1.7 .71 64 15 .070 0     
MinePump/spec1-5_product40.yml false 1 --- inspect 1.7 .72 61 16 .070 .11  
MinePump/spec1-5_product41.yml false 1 --- inspect 1.9 .79 63 16 .070 0     
MinePump/spec1-5_product42.yml false 1 --- inspect 1.9 .79 64 17 .070 .057 
MinePump/spec1-5_product43.yml false 1 --- inspect 1.8 .78 61 15 .070 0     
MinePump/spec1-5_product44.yml false 1 --- inspect 1.7 .72 65 16 .070 0     
MinePump/spec1-5_product45.yml false 1 --- inspect 1.7 .74 62 16 .070 .057 
MinePump/spec1-5_product46.yml false 1 --- inspect 1.7 .71 65 13 .070 0     
MinePump/spec1-5_product47.yml false 1 --- inspect 2.0 .78 61 16 .070 0     
MinePump/spec1-5_product48.yml false 1 --- inspect 1.7 .73 65 18 .070 0     
MinePump/spec1-5_product49.yml false 1 --- inspect 1.9 .74 64 19 .070 .057 
MinePump/spec1-5_product5.yml false 1 --- inspect 1.8 .78 63 16 .070 .057 
MinePump/spec1-5_product50.yml false 1 --- inspect 1.8 .74 62 15 .070 .057 
MinePump/spec1-5_product51.yml false 1 --- inspect 1.8 .74 61 15 .070 .057 
MinePump/spec1-5_product52.yml false 1 --- inspect 1.7 .72 62 16 .070 0     
MinePump/spec1-5_product53.yml false 1 --- inspect 1.8 .77 64 17 .070 .057 
MinePump/spec1-5_product54.yml false 1 --- inspect 1.8 .75 62 17 .070 .0041
MinePump/spec1-5_product55.yml false 1 --- inspect 1.8 .74 65 16 .070 0     
MinePump/spec1-5_product56.yml false 1 --- inspect 1.7 .73 62 16 .070 .0041
MinePump/spec1-5_product57.yml true 2 --- inspect 2.8 1.0  110 26 .070 0     
MinePump/spec1-5_product58.yml true 2 --- inspect 2.4 .91 90 21 .070 .057 
MinePump/spec1-5_product59.yml true 2 --- inspect 2.7 .91 93 23 .070 0     
MinePump/spec1-5_product6.yml false 1 --- inspect 1.9 .76 63 17 .070 .0041
MinePump/spec1-5_product60.yml true 2 --- inspect 2.4 .90 91 21 .070 0     
MinePump/spec1-5_product61.yml true 2 --- inspect 2.2 .86 88 21 .070 0     
MinePump/spec1-5_product62.yml true 2 --- inspect 2.4 .89 90 23 .070 0     
MinePump/spec1-5_product63.yml true 2 --- inspect 2.5 .90 92 22 .070 0     
MinePump/spec1-5_product64.yml true 2 --- inspect 2.7 .94 90 24 .070 .070 
MinePump/spec1-5_product7.yml false 1 --- inspect 1.8 .73 65 17 .070 0     
MinePump/spec1-5_product8.yml false 1 --- inspect 1.8 .75 64 16 .070 0     
MinePump/spec1-5_product9.yml false 1 --- inspect 1.7 .73 64 14 .070 .0082
sv-benchmarks/java/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB)
total 368 290 8800   1300   33000 41000 25    27   
local summary 910  
    correct results 331 482 550   230   21000 4900 23    26   
        correct true 151 302 250   110   9600 2300 11    12   
        correct false 180 180 300   130   11000 2700 13    14   
    incorrect results 6 -192 9.5 4.0 370 83 .42 .11
        incorrect true 6 -192 9.5 4.0 370 83 .42 .11
        incorrect false 0
score (368 tasks, max score: 532) 290
Run set sv-comp19_prop-reachsafety_java.ReachSafety-Java